論文の概要: DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
- arxiv url: http://arxiv.org/abs/2601.05385v1
- Date: Thu, 08 Jan 2026 21:16:55 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-01-12 17:41:49.776495
- Title: DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
- Title（参考訳）: DafnyPro: ダニープログラムのためのLLM支援自動検証
- Authors: Debangshu Banerjee, Olivier Bouissou, Stefan Zetzsche,
- Abstract要約: 本稿では,Dafny で検証アノテーションを生成するための LLM を強化する推論時フレームワークである DafnyPro を紹介する。
DafnyProは、基本的なプログラムロジックの変更を防止するdiff-checker、不要な不変性を除去するpruner、事前定義された問題に依存しない証明戦略を検索し適用するヒント強化システムという3つの重要なコンポーネントで構成されている。
Clover, MBPP-Dafny, HumanEval-Dafny, DafnyBench の4つのベンチマークで, Claude Sonnet 3.5 と 3.7 を用いて DafnyPro を評価する。
- 参考スコア（独自算出の注目度）: 1.8995408467377901
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present DafnyPro, an inference-time framework that enhances LLMs for generating verification annotations in Dafny. DafnyPro comprises three key components: a diff-checker that prevents modifications to base program logic, a pruner that removes unnecessary invariants, and a hint-augmentation system that retrieves and applies predefined, problem-independent proof strategies. We evaluate DafnyPro using Claude Sonnet 3.5 and 3.7 on four benchmarks: Clover, MBPP-Dafny, HumanEval-Dafny, and DafnyBench, achieving consistent performance gains in all cases. Notably, on DafnyBench, the most challenging benchmark, Claude Sonnet 3.5 enhanced with DafnyPro achieves 86% correct proofs, a 16 pp improvement over the base model. We also fine-tune two Qwen models on training data derived from verification attempts by larger models enhanced with DafnyPro. Our 7B and 14B models achieve 68% and 70% correct proofs on DafnyBench, respectively, demonstrating that smaller models can maintain high verification accuracy.
- Abstract（参考訳）: 本稿では,Dafny で検証アノテーションを生成するための LLM を強化する推論時フレームワークである DafnyPro を紹介する。
DafnyProは、基本的なプログラムロジックの変更を防止するdiff-checker、不要な不変性を除去するpruner、事前定義された問題に依存しない証明戦略を検索し適用するヒント強化システムという3つの重要なコンポーネントで構成されている。
Clover, MBPP-Dafny, HumanEval-Dafny, DafnyBench の4つのベンチマークで, Claude Sonnet 3.5 と 3.7 を用いて DafnyPro を評価する。
特に、最も難しいベンチマークであるDafnyBenchでは、DafnyProで強化されたClaude Sonnet 3.5が86%の正しい証明を達成し、ベースモデルよりも16pp向上した。
DafnyProで強化されたより大きなモデルによる検証の試みから得られたトレーニングデータについて、2つのQwenモデルを微調整する。
我々の 7B モデルと 14B モデルはそれぞれ DafnyBench 上で 68% と 70% の正解を達成し,より小さなモデルで高い精度を維持可能であることを示した。
関連論文リスト
- ReFIne: A Framework for Trustworthy Large Reasoning Models with Reliability, Faithfulness, and Interpretability [23.70973331911138]
使用可能な推論システムは、解釈可能性、忠実性、信頼性の3つの特性を特徴とする、信頼できるものでなければならない、と我々は主張する。
本稿では,GRPOと教師付き微調整を統合した新しいトレーニングフレームワークReFIneを提案する。
実験の結果,ReFIneモデルはより明確でより構造化された推論トレースを生成することがわかった。
論文 参考訳（メタデータ） (2025-10-10T07:08:44Z) - Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction [95.91743732150233]
一連のオープンソースの言語モデルであるGoedel-Prover-V2は、自動定理の新たな最先端を証明した。
我々は、より複雑な定理をマスターするためにモデルを訓練することの困難さを増す合成タスクを生成する。
Goedel-Prover-V2-32Bは、標準モードのpass@32でMiniF2Fの88.1%、自己補正モードの90.4%を達成する。
論文 参考訳（メタデータ） (2025-08-05T16:28:22Z) - Reasoning Models Are More Easily Gaslighted Than You Think [85.84943447589511]
我々はOpenAIのo4-mini、Claude-3.7-Sonnet、Gemini-2.5-Flashの3つの最先端推論モデルを評価する。
ガス灯消火プロンプトによる精度低下が認められた。
GaslightingBench-Rは、推論モデルの認識可能性を評価するために設計された新しい診断ベンチマークである。
論文 参考訳（メタデータ） (2025-06-11T12:52:25Z) - VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。
評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
論文 参考訳（メタデータ） (2025-05-25T19:00:52Z) - Benchmarking Reasoning Robustness in Large Language Models [76.79744000300363]
新規データや不完全データでは,性能が著しく低下することがわかった。
これらの結果は、厳密な論理的推論に対するリコールへの依存を浮き彫りにした。
本稿では,情報不足によって引き起こされる幻覚を利用して推論ギャップを明らかにする,Math-RoBと呼ばれる新しいベンチマークを提案する。
論文 参考訳（メタデータ） (2025-03-06T15:36:06Z) - The Best Instruction-Tuning Data are Those That Fit [17.401088816596054]
事前訓練された大言語モデル(LLM)から強機能を引き出すためには,SFT(Supervised Fine-tuning)データが必要である。
GRAPE*は,対象モデルの特異な特徴を考慮に入れた,新しいSFTフレームワークである。
各命令に対して、様々なLSMからの応答を収集し、ターゲットモデルによって測定された最も高い確率の命令を選択する。
論文 参考訳（メタデータ） (2025-02-06T16:31:21Z) - dafny-annotator: AI-Assisted Verification of Dafny Programs [4.651620941143133]
本稿では,大言語モデルと検索を組み合わせたダファニーアノテーションの構築について検討する。
DafnyBench プログラムのコレクションから得られたテストセットでは、LLaMa 3.1 8B でガイドされたgreedy search が15.7%のメソッドに注釈を付けることに成功した。
我々の結果は、大規模な人為的な例がまだない言語のための有能なAIアシスタントへの道のりを示唆している。
論文 参考訳（メタデータ） (2024-11-05T19:27:56Z) - 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) - Step-DPO: Step-wise Preference Optimization for Long-chain Reasoning of LLMs [54.05511925104712]
本稿では,Step-DPOと呼ばれるシンプルで効果的でデータ効率のよい手法を提案する。
Step-DPOは、個々の推論ステップを、論理的に回答を評価するのではなく、優先最適化の単位として扱う。
以上の結果から,70B パラメータ以上のモデルでは,10K の選好データペアと500 Step-DPO トレーニングステップ以下では,MATH の精度が約3%向上する可能性が示唆された。
論文 参考訳（メタデータ） (2024-06-26T17:43:06Z) - DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。
この合成データセットでDeepSeekMath 7Bモデルを微調整します。
我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
論文 参考訳（メタデータ） (2024-05-23T09:03:42Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。