論文の概要: AxDafny: Agentic Verified Code Generation in Dafny
- arxiv url: http://arxiv.org/abs/2606.32007v1
- Date: Tue, 30 Jun 2026 17:39:43 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-01 18:27:19.331053
- Title: AxDafny: Agentic Verified Code Generation in Dafny
- Title（参考訳）: AxDafny: Dafnyのエージェント検証コード生成
- Abstract要約: 本研究では,ダフニーにおけるエージェントコード生成について検討する。そこでは,モデルが検証のために実行可能なコードと証明可能なアーティファクトの両方を生成する必要がある。
AxDafnyは,実装,不変性,アサーション,終了引数を反復的に生成するバリデーション誘導修復フレームワークである。
またLiveCodeBench-Pro-Dafnyという,250の競合型プログラミング問題のベンチマークも導入した。
- 参考スコア（独自算出の注目度）: 0.3499870393443268
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We study agentic code generation in Dafny, where a model must generate both executable code and the proof artifacts for verification. We present AxDafny, a verifier-guided repair framework that iteratively generates implementations, invariants, assertions, and termination arguments. We also introduce LiveCodeBench-Pro-Dafny (LCB-Pro-Dafny), a benchmark of 250 competition-style programming problems translated into Dafny with formal specifications and a verifier-based evaluation harness. On LCB-Pro-Dafny, AxDafny substantially improves verification success over baseline GPT-5.5 performance. On DafnyBench, AxDafny achieves 92.7\% verification success, outperforming the strongest previously reported proof-hint baseline by 6.5 percentage points. Lastly, we show that verification success and runtime test performance measure different aspects of generated code.
- Abstract（参考訳）: 本研究では,ダフニーにおけるエージェントコード生成について検討する。そこでは,モデルが検証のために実行可能なコードと証明成果物の両方を生成する必要がある。
AxDafnyは,実装,不変性,アサーション,終了引数を反復的に生成するバリデーション誘導修復フレームワークである。
また,LiveCodeBench-Pro-Dafny (LCB-Pro-Dafny) も導入した。
LCB-Pro-Dafnyでは、AxDafnyはベースラインのGPT-5.5の性能よりも検証成功を大幅に改善する。
DafnyBenchでは、AxDafnyは92.7%の検証成功を達成し、これまで報告された証明ヒントベースラインを6.5ポイント上回っている。
最後に、検証成功と実行時テスト性能が生成されたコードの異なる側面を測定することを示す。
関連論文リスト
- Automating Formal Verification with Reinforcement Learning and Recursive Inference [0.0]
我々はダフニーで検証可能な報酬(RLVR)と検証者誘導推論時間探索を用いてオープンソースモデルを訓練する。
固定ベースモデルでは、証明修正器を備えた完全な足場は、直接修理中の初期VeriCodingパイロットセットのパスレートを46.2%から69.2%に改善する。
Rust $texttcurve25519-dalek$検証プロジェクトから派生した,レポジトリスケールのLeanベンチマークであるDalek-Benchについても紹介します。
論文 参考訳（メタデータ） (2026-05-29T06:59:28Z) - Agentic Proving for Program Verification [44.663012714194025]
エージェントシステムは、形式数学における自動定理証明のための最先端のアプローチとして登場した。
検証可能なコード生成のためのLean 4ベンチマークであるCLEVERのエージェント証明フレームワークでClaude Codeを評価した。
論文 参考訳（メタデータ） (2026-05-22T15:41:27Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - WybeCoder: Verified Imperative Code Generation [22.401681809856896]
WybeCoderはエージェントコード検証フレームワークである。
コード、不変性、そして証明が共進化する所で、証明・アズ・ユー・ジェネレーション開発を可能にする。
論文 参考訳（メタデータ） (2026-03-31T00:06:44Z) - AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。
このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
論文 参考訳（メタデータ） (2026-02-10T06:58:26Z) - VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code [25.916111156888235]
我々は,Large Language Models (LLM) の形式的検証のための新しいベンチマークを導入する。
筆者らのフレームワークは, 基調整合を定式化された基準, 等価スコアに置き換え, 生成された仕様やコードの品質を厳格に検証する。
以上の結果から,形式的検証可能なコードを生成することは,最先端のLLMにとって依然として大きな課題であることがわかった。
論文 参考訳（メタデータ） (2025-10-07T13:19:05Z) - VERINA: Benchmarking Verifiable Code Generation [46.582574591358735]
大規模言語モデル(LLM)は、ソフトウェア開発にますます統合されている。
LLM生成コードの正確性を保証することは依然として困難である。
検証可能なコード生成は、この制限に対処するための有望なパスを提供する。
論文 参考訳（メタデータ） (2025-05-29T06:12:52Z) - VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。
評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
論文 参考訳（メタデータ） (2025-05-25T19:00:52Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。
SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。
我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳（メタデータ） (2020-10-06T15:47:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。