論文の概要: Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs

• arxiv url: http://arxiv.org/abs/2507.03659v3
• Date: Mon, 08 Sep 2025 19:11:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-10 12:33:22.758396
• Title: Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
• Title（参考訳）: LLMを用いたダニープログラムにおける算数誤差の仕様ガイドによる修復
• Authors: Valentina Wu, Alexandra Mendes, Alexandre Abreu,
• Abstract要約: 本稿では,障害の局所化と修復のためのオラクルとして形式仕様を用いたDafny用のAPRツールを提案する。 プログラム内の各ステートメントの状態を決定するために、Hoareロジックの使用を含む一連のステップを通じて、障害をローカライズします。 また, GPT-4o miniが74.18%と高い修理成功率を示した。
• 参考スコア（独自算出の注目度）: 79.74676890436174
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Debugging and repairing faults when programs fail to formally verify can be complex and time-consuming. Automated Program Repair (APR) can ease this burden by automatically identifying and fixing faults. However, traditional APR techniques often rely on test suites for validation, but these may not capture all possible scenarios. In contrast, formal specifications provide strong correctness criteria, enabling more effective automated repair. In this paper, we present an APR tool for Dafny, a verification-aware programming language that uses formal specifications - including pre-conditions, post-conditions, and invariants - as oracles for fault localization and repair. Assuming the correctness of the specifications and focusing on arithmetic bugs, we localize faults through a series of steps, which include using Hoare logic to determine the state of each statement within the program, and applying Large Language Models (LLMs) to synthesize candidate fixes. The models considered are GPT-4o mini, Llama 3, Mistral 7B, and Llemma 7B. We evaluate our approach using DafnyBench, a benchmark of real-world Dafny programs. Our tool achieves 89.6% fault localization coverage and GPT-4o mini yields the highest repair success rate of 74.18%. These results highlight the potential of combining formal reasoning with LLM-based program synthesis for automated program repair.
• Abstract（参考訳）: プログラムが公式に検証できない場合、障害のデバッグと修復は複雑で時間がかかる可能性がある。 自動プログラム修復(APR)は、障害を自動的に識別し、修正することで、この負担を軽減します。 しかしながら、従来のAPR技術は検証のためにテストスイートに依存することが多いが、これらはすべてのシナリオをキャプチャするわけではない。 対照的に、正式な仕様は強い正当性基準を提供し、より効果的な自動修理を可能にする。 本稿では,プリコンディションやポストコンディション,不変性など,形式仕様を使用する検証対応プログラミング言語であるDafnyのAPRツールを,障害の局所化と修復のためのオーラクルとして提案する。 仕様の正しさを仮定し、算術的なバグに注目すると、プログラム内の各文の状態を決定するためにHoareロジックを使用し、候補修正を合成するためにLarge Language Models (LLM)を適用するなど、一連のステップで障害をローカライズする。 検討されたモデルは、GPT-4o mini、Llama 3、Mistral 7B、Llemma 7Bである。 実世界のDafnyプログラムのベンチマークであるDafnyBenchを用いて,我々のアプローチを評価する。 また, GPT-4o miniが74.18%と高い修理成功率を示した。 これらの結果から, 自動プログラム修復のための形式推論とLCMに基づくプログラム合成を併用する可能性が示唆された。

関連論文リスト

• Do AI models help produce verified bug fixes? [62.985237003585674]
  大規模言語モデルは、ソフトウェアバグの修正に使用される。 本稿では,プログラマが大規模言語モデルを用いて,自身のスキルを補完する方法について検討する。 その結果は、プログラムバグに対する保証された修正を提供するAIとLLMの適切な役割への第一歩となる。
  論文  参考訳（メタデータ） (2025-07-21T17:30:16Z)
• Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization [0.0]
  導入プログラミング課題(IPAs)のための自動プログラム修復(APR)は、多数の学生の参加によって動機付けられている。 本稿では,FMに基づく障害局所化とLarge Language Models(LLMs)の長所を組み合わせた新しいアプローチを提案する。 提案手法では,MaxSATに基づく障害位置定位法を用いて,プログラムのバグ部分を特定し,これらのバグ文を欠いたプログラムスケッチをLLMに提示する。
  論文  参考訳（メタデータ） (2024-12-19T12:08:44Z)
• Subtle Errors in Reasoning: Preference Learning via Error-injected Self-editing [59.405145971637204]
  eRror-Injected Self-Editing (RISE) と呼ばれる新しい好み学習フレームワークを提案する。 RISEは、事前定義された微妙なエラーをピボットトークンに注入する。 RISEの有効性を検証する実験では、Qwen2-7B-Instructでの優先学習により、GSM8Kでは3.0%、MATHでは7.9%が顕著に改善され、トレーニングサンプルは4.5Kに留まった。
  論文  参考訳（メタデータ） (2024-10-09T07:43:38Z)
• 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)
• A Deep Dive into Large Language Models for Automated Bug Localization and Repair [12.756202755547024]
  大規模言語モデル(LLM)は、自動プログラム修復(APR)など、様々なソフトウェアエンジニアリングタスクにおいて顕著な効果を示している。 本研究では,LSMを用いた自動バグ修正について深く検討する。 異なるLLMを用いてバグの局所化と修正を分離することにより、多様なコンテキスト情報の効果的な統合が可能になる。 Toggleは、CodeXGLUEコード改善ベンチマークで、新しい最先端(SOTA)パフォーマンスを実現する。
  論文  参考訳（メタデータ） (2024-04-17T17:48:18Z)
• An Empirical Evaluation of Pre-trained Large Language Models for Repairing Declarative Formal Specifications [7.286515881369693]
  本稿では,大規模言語モデル(LLM)がアロイの宣言的仕様を修復する能力について,体系的に検討する。 単エージェントと二エージェントのパラダイムを含む12の異なる修復設定を設計し,LLMを多用した。 自動プロンプティング機能を備えたデュアルエージェントは,イテレーション数やトークン使用量の増加とともに,他の設定よりも優れていた。
  論文  参考訳（メタデータ） (2024-04-17T03:46:38Z)
• Aligning the Objective of LLM-based Program Repair [14.935596175148586]
  本稿では,大規模言語モデル (LLM) をプログラム修復に適用するための新しいアプローチについて検討する。 我々の中核的な洞察は、LLMのAPR能力は、単にトレーニング目標に出力を合わせるだけで大幅に改善できるということです。 この知見に基づいて、我々はAPRの直接的なプロンプトフレームワークであるD4Cを設計した。
  論文  参考訳（メタデータ） (2024-04-13T02:36:40Z)
• A Novel Approach for Automatic Program Repair using Round-Trip Translation with Large Language Models [50.86686630756207]
  研究によると、ある文の文法的誤りは、それを他の言語に翻訳し、その語を返せば修正できる。 現在の自動プログラム修復(APR)生成モデルは、ソースコードで事前訓練され、修正のために微調整されている。 本稿では,あるプログラミング言語から別のプログラミング言語,あるいは自然言語へのコード変換,そして,その逆といった,微調整ステップをバイパスし,ラウンド・トリップ変換(RTT)を用いる手法を提案する。
  論文  参考訳（メタデータ） (2024-01-15T22:36:31Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)
• Is Self-Repair a Silver Bullet for Code Generation? [68.02601393906083]
  大規模な言語モデルは、コード生成において顕著な適性を示しているが、それでも複雑なタスクを実行するのに苦労している。 自己修復(Self-repair) — モデルが自身のコードをデバッグし、修復する — は、最近、パフォーマンスを向上する一般的な方法になっている。 我々は,Code Llama, GPT-3.5, GPT-4によるHumanEvalとAPPSの自己修復能力について分析した。
  論文  参考訳（メタデータ） (2023-06-16T15:13:17Z)
• Fully Autonomous Programming with Large Language Models [0.9558392439655015]
  LLM(Large Language Models)を用いたプログラム合成への最近のアプローチは、"ニアミスシンドローム"を示す。 我々は、LLMとプログラム合成ベンチマーク2としてOpenAI Codexを使用し、問題記述と評価のためのテストのデータベースとして使用します。 結果として生じるフレームワークは、修復フェーズなしでのCodexの従来の使用法と、従来の遺伝的プログラミングアプローチの両方を上回ります。
  論文  参考訳（メタデータ） (2023-04-20T16:12:05Z)

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

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