論文の概要: Agentic Proving for Program Verification

• arxiv url: http://arxiv.org/abs/2605.23772v1
• Date: Fri, 22 May 2026 15:41:27 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-25 17:29:20.415232
• Title: Agentic Proving for Program Verification
• Title（参考訳）: プログラム検証のためのエージェント証明
• Authors: Alessandro Sosso, Akhil Arora, Bas Spitters,
• Abstract要約: エージェントシステムは、形式数学における自動定理証明のための最先端のアプローチとして登場した。 検証可能なコード生成のためのLean 4ベンチマークであるCLEVERのエージェント証明フレームワークでClaude Codeを評価した。
• 参考スコア（独自算出の注目度）: 44.663012714194025
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Agentic systems have recently emerged as state-of-the-art approaches for automated theorem proving in formal mathematics. To assess how far these capabilities extend to program verification, we evaluate Claude Code in an agentic proving framework on CLEVER, a Lean 4 benchmark for verifiable code generation. Our results show that Claude generates arguably valid specifications for 98.8% of problems (with 81.3% also accepted by CLEVER's isomorphism-based scoring on the correct portion of the benchmark), certifies implementations against correct ground-truth specifications for 87.5% of problems, and reaches a 98.1% success rate on the end-to-end program generation and verification pipeline over entries with self-consistent premises. Across all stages, Claude further provides high-quality feedback on its own attempts (as confirmed under manual review), identifying underlying causes of failure and lingering bugs in the dataset. These findings highlight a growing mismatch between the difficulty of existing program verification benchmarks and the capabilities of modern agentic provers, and point to the need for more rigorous, bug-resilient evaluation methodologies, and in particular for alternatives to isomorphism-based scoring of generated specifications. More broadly, our results provide empirical evidence that tight compiler-in-the-loop agentic paradigms are currently the most effective approach for foundational program verification.
• Abstract（参考訳）: エージェントシステムは、最近、形式数学における自動定理証明のための最先端のアプローチとして登場した。 これらの機能がプログラム検証にどの程度まで拡張されているかを評価するため、コード生成を検証するリーン4ベンチマークであるCLEVERのエージェント証明フレームワークで、Claude Codeを評価した。 この結果から,CLEVERは,98.8%の課題に対して妥当な仕様(81.3%)を生成し,87.5%の課題に対して正しい基盤トラスト仕様に対する実装を認定し,自己整合性のある前提を持つ項目に対して,エンドツーエンドのプログラム生成と検証パイプラインで98.1%の成功率を達成した。 すべてのステージにわたって、Claudeはさらに、(手作業によるレビューで確認された)自身の試みに関する高品質なフィードバックを提供し、データセットの障害の原因を特定し、バグを警告する。 これらの結果は、既存のプログラム検証ベンチマークの難しさと現代のエージェント・プロバーの能力とのミスマッチが増大し、より厳密でバグ耐性のある評価手法の必要性、特に、生成した仕様の同型性に基づく評価に代わる方法の必要性が指摘されている。 より広範に、我々の結果は、タイトなコンパイラ・イン・ザ・ループのエージェントパラダイムが、現在、基礎的プログラム検証の最も効果的なアプローチであることを示す実証的な証拠を提供する。

関連論文リスト

• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
  大規模な言語モデルは、自動化されたソフトウェア工学における約束を示すが、その正しさの保証は、誤ったコードや幻覚的なコードによってしばしば損なわれる。 NaturalLanguage2VerifiedCodeデータセット:60の複雑なアルゴリズム問題の集合を提供する。 7個のオープンウェイト LLM でランダムに選択された11個の問題集合をタイレッドプロンプト戦略を用いて評価した。 以上の結果から,コンテキストレスなプロンプトがほぼユニバーサルの失敗につながる一方で,構造的アンカーと反復的自己修復が劇的なパフォーマンスの転換を促進することが示唆された。
  論文  参考訳（メタデータ） (2026-04-24T14:28:10Z)
• ProdCodeBench: A Production-Derived Benchmark for Evaluating AI Coding Agents [10.578603956693696]
  本稿では,ProdCodeBenchを用いて実運用用ベンチマークの計算手法を提案する。 それぞれのキュレートされたサンプルは、7つのプログラミング言語にまたがる冗長なプロンプト、コミットされたコード変更、フェイル・ツー・パステストで構成されている。 4つの基礎モデルの体系的な分析は、53.2%から72.2%の範囲で解決する。
  論文  参考訳（メタデータ） (2026-04-02T01:52:55Z)
• WybeCoder: Verified Imperative Code Generation [22.401681809856896]
  WybeCoderはエージェントコード検証フレームワークである。 コード、不変性、そして証明が共進化する所で、証明・アズ・ユー・ジェネレーション開発を可能にする。
  論文  参考訳（メタデータ） (2026-03-31T00:06:44Z)
• HLE-Verified: A Systematic Verification and Structured Revision of Humanity's Last Exam [63.84155758655084]
  HumanityのLast Exam (HLE)は、フロンティアの大規模言語モデルを評価するために広く使われているベンチマークである。 HLE-Verifiedは,透過的検証プロトコルときめ細かい誤り分類法を備えたHLEの検証および改訂版である。 我々は,HLEとHLE-Verifiedの7つの最先端言語モデルを評価し,平均7～10ポイントの絶対精度を観測した。
  論文  参考訳（メタデータ） (2026-02-15T02:50:15Z)
• PRIME: A Process-Outcome Alignment Benchmark for Verifiable Reasoning in Mathematics and Engineering [71.15346406323827]
  本稿では,プロセス・アウトカム・アライメント・アライメント・検証における検証結果を評価するベンチマークであるPRIMEを紹介する。 現在の検証器は、しばしば導出欠陥を検出するのに失敗する。 本稿では,PRIMEで選択した検証手法を利用したプロセス認識型RLVRトレーニングパラダイムを提案する。
  論文  参考訳（メタデータ） (2026-02-12T04:45:01Z)
• Failure-Aware Enhancements for Large Language Model (LLM) Code Generation: An Empirical Study on Decision Framework [0.26508608365976566]
  GitHubの25のプロジェクトに関する実証調査では、プログレッシブプロンプトが平均96.9%のタスク完了を達成した。 自己批判はコードレビュー可能なロジックエラーで成功するが、外部サービス統合では完全に失敗する。 RAGは、より優れた効率で、すべての障害タイプで最高の完成を達成する。
  論文  参考訳（メタデータ） (2026-02-02T23:08:03Z)
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
  本稿では,障害の局所化と修復のためのオラクルとして形式仕様を用いたDafny用のAPRツールを提案する。 プログラム内の各ステートメントの状態を決定するために、Hoareロジックの使用を含む一連のステップを通じて、障害をローカライズします。 また, GPT-4o miniが74.18%と高い修理成功率を示した。
  論文  参考訳（メタデータ） (2025-07-04T15:36:12Z)
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
  本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。 評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
  論文  参考訳（メタデータ） (2025-05-25T19:00:52Z)

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

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