論文の概要: Harnessing Code Agents for Automatic Software Verification
- arxiv url: http://arxiv.org/abs/2607.06341v1
- Date: Tue, 07 Jul 2026 14:39:59 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-08 21:24:51.555795
- Title: Harnessing Code Agents for Automatic Software Verification
- Title（参考訳）: 自動ソフトウェア検証のためのハラスティングコードエージェント
- Abstract要約: 大規模言語モデル(LLM)は、自動的に証明を生成することを約束するが、既存のアプローチは、固定された人間設計の証明戦略をシステムに結び付ける。
このような戦略を課すことは不要で制限的であることを示す。
レムマ全体を一般的なコードエージェントに手渡して、独自のアプローチを自由に選択し、検証ハーネスにラップすることは、シンプルでより効果的です。
- 参考スコア（独自算出の注目度）: 0.47154736035631406
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort. Large language models (LLMs) promise to generate these proofs automatically, yet existing approaches wire a fixed, human-designed proof strategy into the system and constrain the model to follow it (retrieving premises and predicting tactics one step at a time, or splitting goals by divide-and-conquer), and still prove only a fraction of their target theorems. We show that imposing such a strategy is unnecessary and limiting. Handing the whole lemma to a general LLM code agent (for example, Claude Code), free to choose its own approach, and wrapping it in a verification harness is both simpler and more effective, achieving full coverage: every targeted lemma proved, with no failures and no Coq expert intervention. The agent writes the proofs under feedback and hard constraints from the harness that keep each one sound (accepted only when the prover's kernel closes it), complete (no obligation left unproved or silently dropped), and terminating (no divergent tactics). We evaluate this harness plus code agent along three dimensions. (1) Core logic: on Iris, the state-of-the-art separation logic for concurrent and memory-manipulating programs, Aria proves all 4,257 lemmas of the four core modules and the 217 lemmas verifying Rust's standard libraries built on it, fully automatically. (2) Comparison with prior LLM provers: on reglang, where prior provers manage barely one in eight, Aria proves all 318. (3) Generality: on iris-lean, the unfinished Lean 4 port of Iris, it proves 72 not-yet-ported lemmas, showing the approach is not specific to Coq. A state-of-the-art model (Claude Opus 4.7) can write proofs for verified software development fully and automatically.
- Abstract（参考訳）: 形式的検証はソフトウェアの正しさを最強に保証するが、スケールしない: Coq のようなインタラクティブな定理証明者によって要求される証明は、膨大な専門家の努力を必要とする。
大規模言語モデル(LLM)は、これらの証明を自動生成することを約束するが、既存のアプローチは、固定された人間設計の証明戦略をシステムに結び付け、それに従うようにモデルを制約する(前提の取得と1ステップずつの予測、あるいは分割して目標を分割する)。
このような戦略を課すことは不要で制限的であることを示す。
一般的なLLMコードエージェント(例えばClaude Code)にすべてのレムマを渡すことで、独自のアプローチを自由に選択し、検証ハーネスにラップすることは、シンプルかつ効果的であると同時に、完全なカバレッジを達成する。
エージェントはフィードバックとハーネスからの厳しい制約の下で証明を書き、それぞれの音を保ち(証明者のカーネルが閉じた時にのみ受け入れる)、完了し(無証明または無音で落とされた義務は残らない)、終了する(分岐戦術は含まない)。
このハーネスとコードエージェントを3次元で評価する。
1) コアロジック: 並列およびメモリ操作プログラムのための最先端の分離ロジックであるIrisでは、Ariaは4つのコアモジュールの4,257のレムマと、217のレムマがRustの標準ライブラリを完全自動で検証していることを証明している。
2) LLM プローバーとの比較:reglang では,先行プローバーが 8 分の1 しか管理できない場合,Aria は 318 を全て証明する。
(3) 一般性: 未完成のIrisのLean 4ポートであるIris-leanでは、72の非yetポートのレムマが証明されており、アプローチがCoqに固有のものではないことを示している。
最先端のモデル(Claude Opus 4.7)は、検証済みのソフトウェア開発の証明を完全かつ自動的に作成することができる。
関連論文リスト
- Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs [21.65389718022749]
提案するQuarryは,証明計画と証明実行を分離した,計画に基づく証明合成フレームワークである。
特に、Quarry は LLM に対して、任意のサブレンマを持つ複数の証明分解を積極的に提案するよう求め、Rocq で一時的に承認されたサブレンマの下でそれらをタイプチェックし、証明状態に基づく困難モデルを用いて候補をランク付けする。
可解性を考慮した評価による計画ベース分解は,予測可能なコストを維持しつつ,自動化を大幅に改善することを示す。
論文 参考訳（メタデータ） (2026-06-16T14:33:15Z) - LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。
4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。
我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
論文 参考訳（メタデータ） (2026-06-03T20:09:39Z) - Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems [100.24694338574402]
本稿では,インダクティブ・デダクティブ・シンセシス(IDS)について述べる。
IDSは約6.8時間で7/7を達成し、1仕様あたり106ドル、専門家の努力の約200倍、SOTAエージェントの約17%を達成している。
IDSはパフォーマンスフィードバックを同じループに組み込んでおり、検証されたシステムよりも最大3倍高速な実装を実現している。
論文 参考訳（メタデータ） (2026-05-22T00:05:36Z) - Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning [20.336209492846752]
形式検証は証明の正当性を保証するが、形式化の忠実性は保証しない。
私たちは、Lean 4の証明を生成する際に、フロンティアモデルがこのギャップを利用するかどうかを調査します。
統一世代における体系的なゲーミングの証拠は見つからない。
論文 参考訳（メタデータ） (2026-04-21T13:37:49Z) - Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。
DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。
クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。
論文 参考訳（メタデータ） (2026-04-20T22:02:57Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。
エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。
この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
論文 参考訳（メタデータ） (2025-05-09T03:38:31Z) - Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。
RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。
これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。
我々は、無害な」知識基盤の著作権保護の名称を提案する。
論文 参考訳（メタデータ） (2025-02-10T09:15:56Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。
1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。
他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。
具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文 参考訳（メタデータ） (2023-11-16T11:26:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。