論文の概要: 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%を検証している。 特に、多くのプログラムは、元のアサーションよりも少ないアサーションで検証でき、証明は複数の有効な修復戦略をしばしば認め、元のアサーションを回復することは不要であることを強調している。 これらの結果は、自動アサーション推論が証明工学の労力を大幅に削減し、よりスケーラブルでアクセスしやすい形式的検証へのステップを示すことを示している。

関連論文リスト

• 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)
• 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)
• 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)

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

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