論文の概要: Lemma Discovery in Agentic Program Verification
- arxiv url: http://arxiv.org/abs/2603.22114v1
- Date: Mon, 23 Mar 2026 15:42:07 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-24 19:11:39.756122
- Title: Lemma Discovery in Agentic Program Verification
- Title（参考訳）: エージェントプログラム検証におけるレムマ発見
- Authors: Huan Zhao, Haoxin Tu, Zhengyao Liu, Martin Rinard, Abhik Roychoudhury,
- Abstract要約: 帰納的検証は、検証条件(VC)を抽出し、それらの公式な証明を書くことによって、コードに対して強い正当性を保証する。
VC証明の専門知識集約的なタスクは、このプロセスの主要なボトルネックであり、最近のLarge Language Model (LLM)エージェントの進歩により部分的に自動化されている。
私たちは、プログラム検証のためのVCの証明は純粋に数学的タスク以上のものであり、プログラムの理解からかなりの恩恵を受けると主張している。
- 参考スコア（独自算出の注目度）: 12.551445518827768
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Deductive verification provides strong correctness guarantees for code by extracting verification conditions (VCs) and writing formal proofs for them. The expertise-intensive task of VC proving is the main bottleneck in this process, and has been partly automated owing to recent advances in Large Language Model (LLM) agents. However, existing proof agents are not able to discover helper lemmas - auxiliary lemmas that aid in proving - and thus fall short as programs grow in size and complexity. In this paper, we argue that VC proving for program verification is more than a purely mathematical task, and benefits considerably from program comprehension. Our key insight is that human-proof engineers often discover and apply helper lemmas based on their understanding of the program semantics, which are not directly reflected in the VCs produced by VC generators. Inspired by this insight, we propose an LLM agent, LemmaNet, that discovers helper lemmas in two ways. Specifically, the agent first synthesizes lemmas offline by directly analyzing the source code and specifications, and then relating this semantic understanding to the mechanical, verbose encoding produced by VC generators. As the proof unfolds, LemmaNet then adapts existing helper lemmas online to accommodate evolving proof states, enabling the agent to effectively discharge complex VCs on-the-fly. We evaluate LemmaNet on SV-COMP and established real-world subjects, including modules of the Linux kernel, Contiki OS, standard C++ library, and X.509 parser. Our experimental results demonstrate that LemmaNet significantly outperforms state-of-the-art approaches, highlighting the importance of program comprehension-aided lemma discovery in agentic program verification.
- Abstract（参考訳）: 帰納的検証は、検証条件(VC)を抽出し、それらの公式な証明を書くことによって、コードに対して強い正当性を保証する。
VC証明の専門知識集約的なタスクは、このプロセスの主要なボトルネックであり、最近のLarge Language Model (LLM)エージェントの進歩により部分的に自動化されている。
しかし、既存の証明エージェントは、証明を助ける補助的な補題であるヘルパー補題を見つけることができず、プログラムのサイズや複雑さが大きくなるにつれて不足する。
本稿では,プログラム検証のためのVC証明は純粋に数学的タスク以上のものであり,プログラム理解の恩恵が大きいことを論じる。
私たちのキーとなる洞察は、VCジェネレータが生成するVCに直接反映されないプログラムセマンティクスの理解に基づいて、人為的なエンジニアがヘルパー・レムマを発見して適用することが多いということです。
この知見にインスパイアされたLLMエージェントであるLemmaNetを提案し、ヘルパー補題を2つの方法で発見する。
具体的には、エージェントはまずソースコードと仕様を直接解析し、その意味理解をVCジェネレータによって生成される機械的冗長な符号化に関連付けることにより、レムマをオフラインに合成する。
証明が展開するにつれて、LemmaNetは既存のヘルパー補題をオンラインで適用して、進化する証明状態に対応する。
我々は、SV-COMP上でLemmaNetを評価し、Linuxカーネルのモジュール、Contiki OS、標準C++ライブラリ、X.509パーサを含む現実世界の課題を確立した。
実験の結果、LemmaNetは最先端の手法よりも優れており、エージェントプログラム検証におけるプログラム理解支援レムマ発見の重要性を強調している。
関連論文リスト
- Neural Theorem Proving for Verification Conditions: A Real-World Benchmark [9.350519191460018]
この研究は、NTP4VC(Neural Theorem Proving for Verification Conditions)を導入し、このタスクのための最初の実世界のマルチ言語ベンチマークを示す。
NTP4VC を用いて,大言語モデル (LLM) の評価を行った。
論文 参考訳（メタデータ） (2026-01-26T20:37:11Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Agentic Program Verification [14.684859166069012]
本稿では,プログラム検証を行うための最初の大規模言語モデルエージェントであるAutoRocqを提案する。
LLMの広範な訓練を実証例に頼っている過去の研究とは異なり、我々のエージェントはオンザフライで学習し、反復的な改善ループを通じて証明を改善する。
このようにして、我々の証明構成は証明エージェントと定理証明器との間の自律的な協調を含む。
論文 参考訳（メタデータ） (2025-11-21T15:51:48Z) - Dissect-and-Restore: AI-based Code Verification with Transient Refactoring [1.2883590530210827]
提案するPrometheusは,現在のAI機能を備えた自動コード検証を容易にする,AI支援システムである。
プロメテウスは、複素補題の構造的分解を通じてより小さく検証可能な部分補題への証明探索を導く。
このアプローチは、ベースラインの68%に比べて、キュレートされたデータセットの86%のタスクをうまく検証します。
論文 参考訳（メタデータ） (2025-10-29T11:23:50Z) - What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus [2.8003002159083237]
我々は,2つの言語で作業する8人の専門家から,詳細なソースコードテレメトリの収集と解析を行うユーザスタディを実施している。
その結果、専門家が証明開発プロセスで遭遇した重要な課題や証明についてどのように考えるかについて興味深い傾向とパターンが明らかになった。
我々はこれらの知見を,AI証明アシスタントのための具体的な設計指針に翻訳する。
論文 参考訳（メタデータ） (2025-08-01T22:16:30Z) - Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。
有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。
生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
論文 参考訳（メタデータ） (2025-07-22T08:13:01Z) - Do AI models help produce verified bug fixes? [62.985237003585674]
大規模言語モデルは、ソフトウェアバグの修正に使用される。
本稿では,プログラマが大規模言語モデルを用いて,自身のスキルを補完する方法について検討する。
その結果は、プログラムバグに対する保証された修正を提供するAIとLLMの適切な役割への第一歩となる。
論文 参考訳（メタデータ） (2025-07-21T17:30:16Z) - Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。
実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
論文 参考訳（メタデータ） (2025-05-28T17:57:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。