論文の概要: Agentic Program Verification

• arxiv url: http://arxiv.org/abs/2511.17330v1
• Date: Fri, 21 Nov 2025 15:51:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-24 18:08:19.085336
• Title: Agentic Program Verification
• Title（参考訳）: エージェントプログラム検証
• Authors: Haoxin Tu, Huan Zhao, Yahui Song, Mehtab Zafar, Ruijie Meng, Abhik Roychoudhury,
• Abstract要約: 本稿では,プログラム検証を行うための最初の大規模言語モデルエージェントであるAutoRocqを提案する。 LLMの広範な訓練を実証例に頼っている過去の研究とは異なり、我々のエージェントはオンザフライで学習し、反復的な改善ループを通じて証明を改善する。 このようにして、我々の証明構成は証明エージェントと定理証明器との間の自律的な協調を含む。
• 参考スコア（独自算出の注目度）: 14.684859166069012
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automatically generated code is gaining traction recently, owing to the prevalence of Large Language Models (LLMs). Further, the AlphaProof initiative has demonstrated the possibility of using AI for general mathematical reasoning. Reasoning about computer programs (software) can be accomplished via general mathematical reasoning; however, it tends to be more structured and richer in contexts. This forms an attractive proposition, since then AI agents can be used to reason about voluminous code that gets generated by AI. In this work, we present a first LLM agent, AutoRocq, for conducting program verification. Unlike past works, which rely on extensive training of LLMs on proof examples, our agent learns on-the-fly and improves the proof via an iterative refinement loop. The iterative improvement of the proof is achieved by the proof agent communicating with the Rocq (formerly Coq) theorem prover to get additional context and feedback. The final result of the iteration is a proof derivation checked by the Rocq theorem prover. In this way, our proof construction involves autonomous collaboration between the proof agent and the theorem prover. This autonomy facilitates the search for proofs and decision-making in deciding on the structure of the proof tree. Experimental evaluation on SV-COMP benchmarks and on Linux kernel modules shows promising efficacy in achieving automated program verification. As automation in code generation becomes more widespread, we posit that our proof agent can be potentially integrated with AI coding agents to achieve a generate and validate loop, thus moving closer to the vision of trusted automatic programming.
• Abstract（参考訳）: 最近、LLM(Large Language Models)が普及したため、自動生成されたコードが勢いを増している。 さらに、AlphaProofイニシアチブは、一般的な数学的推論にAIを使用する可能性を実証している。 コンピュータプログラム(ソフトウェア)の推論は、一般的な数学的推論によって達成できるが、コンテキストにおいてより構造化され、よりリッチになる傾向がある。 というのも、AIエージェントはAIによって生成される輝かしいコードを理解するのに使えるからだ。 本研究では,プログラム検証を行うための最初のLCMエージェントであるAutoRocqを提案する。 LLMの広範な訓練を実証例に頼っている過去の研究とは異なり、我々のエージェントはオンザフライで学習し、反復的な改善ループを通じて証明を改善する。 証明の反復的改善は、追加の文脈とフィードバックを得るために、Rocq(以前のCoq)定理証明器と通信する証明エージェントによって達成される。 反復の最終結果は、ロックの定理証明器によってチェックされた証明の導出である。 このようにして、我々の証明構成は証明エージェントと定理証明器との間の自律的な協調を含む。 この自律性は、証明木の構造を決定する上で、証明と決定の探索を促進する。 SV-COMPベンチマークとLinuxカーネルモジュールの実験的評価は、自動プログラム検証を実現する上で有望な有効性を示している。 コード生成の自動化がより広まるにつれて、我々は証明エージェントがAIコーディングエージェントと潜在的に統合され、生成と検証のループを達成することができると仮定し、信頼できる自動プログラミングのビジョンに近づきつつある。

関連論文リスト

• Dissect-and-Restore: AI-based Code Verification with Transient Refactoring [1.2883590530210827]
  提案するPrometheusは,現在のAI機能を備えた自動コード検証を容易にする,AI支援システムである。 プロメテウスは、複素補題の構造的分解を通じてより小さく検証可能な部分補題への証明探索を導く。 このアプローチは、ベースラインの68%に比べて、キュレートされたデータセットの86%のタスクをうまく検証します。
  論文  参考訳（メタデータ） (2025-10-29T11:23:50Z)
• Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs [6.65877320351217]
  我々はLeanNavigatorを開発した。これはリーンの定理と証明の大規模なデータセットを生成する新しい方法だ。 我々は10億のトークンを合計470万の定理で生成し、以前のデータセットを桁違いに上回った。 この広範なデータセットを使用して、我々は、定理証明タスクにおいて最先端のReProverモデルより優れたAIモデルを訓練した。
  論文  参考訳（メタデータ） (2025-02-16T06:20:39Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement [25.80131224070207]
  生成したコードが正しいことを数学的に保証するために,形式検証を利用することを目標としている。 LLMによる正式な認証コードの生成は、トレーニングデータの不足と、形式的な証明の複雑さによって妨げられる。 我々は、公式に認証されたコード生成をブートストラップする自己改善フレームワークであるAlphaVerusを紹介した。
  論文  参考訳（メタデータ） (2024-12-09T03:22:35Z)
• Gödel Agent: A Self-Referential Agent Framework for Recursive Self-Improvement [112.04307762405669]
  G"odel AgentはG"odelマシンにインスパイアされた自己進化型フレームワークである。 G"odel Agentは、パフォーマンス、効率、一般化性において手作業によるエージェントを上回る、継続的な自己改善を実現することができる。
  論文  参考訳（メタデータ） (2024-10-06T10:49:40Z)
• miniCodeProps: a Minimal Benchmark for Proving Code Properties [22.548472305010005]
  私たちはLeanの証明アシスタントで201のプログラム仕様のベンチマークであるminiCodePropsを紹介します。 その単純さにもかかわらず、MiniCodePropsは現在のLLMベースのプローバーを壊すのに十分である。
  論文  参考訳（メタデータ） (2024-06-16T21:11:23Z)
• Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  リーンでLLM推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明のステップを提案し、証明の目標を完了し、関連する前提を選択するツールを構築します。 人間を助ける場合、Lean Copilotは平均3.86で手動で入力された証明ステップを2.08ステップしか必要としない。 定理証明プロセスを自動化する場合、Lean Copilotの74.2%の証明ステップは平均85%がエソップ(40.1%)より優れている。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。