Fugu-MT 論文翻訳(概要): Inferring multiple helper Dafny assertions with LLMs

論文の概要: Inferring multiple helper Dafny assertions with LLMs

arxiv url: http://arxiv.org/abs/2511.00125v1
Date: Fri, 31 Oct 2025 09:45:39 GMT
ステータス: 翻訳完了
システム内更新日: 2025-11-05 16:37:26.628395
Title: Inferring multiple helper Dafny assertions with LLMs
Title（参考訳）: LLMを用いた複数ヘルパーDafnyアサーションの推論
Authors: Álvaro Silva, Alexandra Mendes, Ruben Martins,
Abstract要約: 本研究では,Dafnyプログラムにおけるヘルパーアサーションの欠落を自動的に推測するために,Large Language Modelsの使用について検討する。推論の難易度を分析するために,アサーション型の分類を導入した。その結果、自動アサーション推論は証明工学の労力を大幅に削減できることが示された。
参考スコア（独自算出の注目度）: 47.33158055894705
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: The Dafny verifier provides strong correctness guarantees but often requires numerous manual helper assertions, creating a significant barrier to adoption. We investigate the use of Large Language Models (LLMs) to automatically infer missing helper assertions in Dafny programs, with a primary focus on cases involving multiple missing assertions. To support this study, we extend the DafnyBench benchmark with curated datasets where one, two, or all assertions are removed, and we introduce a taxonomy of assertion types to analyze inference difficulty. Our approach refines fault localization through a hybrid method that combines LLM predictions with error-message heuristics. We implement this approach in a new tool called DAISY (Dafny Assertion Inference SYstem). While our focus is on multiple missing assertions, we also evaluate DAISY on single-assertion cases. DAISY verifies 63.4% of programs with one missing assertion and 31.7% with multiple missing assertions. Notably, many programs can be verified with fewer assertions than originally present, highlighting that proofs often admit multiple valid repair strategies and that recovering every original assertion is unnecessary. These results demonstrate that automated assertion inference can substantially reduce proof engineering effort and represent a step toward more scalable and accessible formal verification.
Abstract（参考訳）: Dafny検証は強い正確性を保証するが、しばしば手動ヘルパーのアサーションを必要とする。 Dafnyプログラムにおけるヘルパーアサーションの欠落を自動的に推測するために,Large Language Models (LLMs) を用いることについて検討する。本研究では,1,2,あるいはすべてのアサーションを除去するキュレートデータセットを用いたDafnyBenchベンチマークを拡張し,推論の難しさを分析するために,アサーション型の分類を導入した。提案手法は, LLM予測とエラーメッセージヒューリスティックスを組み合わせたハイブリッド手法により, 故障局所化を改良する。このアプローチをDAISY(Dafny Assertion Inference SYstem)と呼ばれる新しいツールで実装する。複数のアサーションの欠如に焦点を当てていますが、単一アサーションのケースではDAISYの評価も行っています。 DAISYは1つのアサーションが欠けているプログラムの63.4%、複数のアサーションが欠けているプログラムの31.7%を検証している。特に、多くのプログラムは、元のアサーションよりも少ないアサーションで検証でき、証明は複数の有効な修復戦略をしばしば認め、元のアサーションを回復することは不要であることを強調している。これらの結果は、自動アサーション推論が証明工学の労力を大幅に削減し、よりスケーラブルでアクセスしやすい形式的検証へのステップを示すことを示している。

関連論文リスト

ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文参考訳（メタデータ） (2025-10-28T16:22:54Z)
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)
Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。 VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
論文参考訳（メタデータ） (2025-05-17T04:16:36Z)
Agentic Verification for Ambiguous Query Disambiguation [42.238086712267396]
本稿では,検索拡張世代(RAG)における問合せの曖昧化という課題に対処する。本稿では,早期にレシーバとジェネレータからのフィードバックを取り入れて,ダイバーシフィケーションと検証を一体化するための共同手法を提案する。広く採用されているASQAベンチマークにおいて,本手法の有効性と有効性を検証し,多種多様かつ検証可能な解釈を実現する。
論文参考訳（メタデータ） (2025-02-14T18:31:39Z)
Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
論文参考訳（メタデータ） (2024-10-05T05:21:48Z)
AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation [6.3585378855805725]
本稿では,アサーション生成におけるLarge-Language Modelsの有効性を評価するための新しいベンチマークを提案する。 AssertioBenchにはOpenCoresから100のキュレートされたVerilogハードウェア設計が含まれており、GoldMineとHARMから生成された各設計について正式に承認されている。
論文参考訳（メタデータ） (2024-06-26T14:47:28Z)
Laurel: Unblocking Automated Verification with Large Language Models [2.6942525604796366]
大規模言語モデルを用いてアサーションを自動的に生成するツールであるLaurellを提案する。実世界の3つのDafnysから抽出した複雑な補題のデータセットであるDafnyGymを、新しいベンチマークで評価した。
論文参考訳（メタデータ） (2024-05-27T03:26:01Z)
Knowledge-Augmented Language Model Verification [68.6099592486075]
最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
論文参考訳（メタデータ） (2023-10-19T15:40:00Z)
SAGA: Summarization-Guided Assert Statement Generation [34.51502565985728]
本稿では,アサート文の自動生成のための新しい要約誘導手法を提案する。我々は、事前訓練された言語モデルを参照アーキテクチャとして利用し、アサート文生成のタスクでそれを微調整する。
論文参考訳（メタデータ） (2023-05-24T07:03:21Z)
GERE: Generative Evidence Retrieval for Fact Verification [57.78768817972026]
本稿では,ジェネレーション方式で証拠を検索する最初のシステムであるGEREを提案する。 FEVERデータセットの実験結果は、GEREが最先端のベースラインよりも大幅に改善されていることを示している。
論文参考訳（メタデータ） (2022-04-12T03:49:35Z)
ReAssert: Deep Learning for Assert Generation [3.8174671362014956]
本稿では、JUnitテストアサーションの自動生成のためのアプローチであるRE-ASSERTを提案する。これは、学習に正確なコード・トゥ・テストのトレーサビリティを使用して、プロジェクトを個別にターゲットすることで達成される。我々はまた、最先端のディープラーニングモデルであるReformerと、ReAssertと既存のアプローチであるATLASを評価するための以前の2つのモデルも利用しています。
論文参考訳（メタデータ） (2020-11-19T11:55:59Z)

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

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