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

• arxiv url: http://arxiv.org/abs/2507.03659v1
• Date: Fri, 04 Jul 2025 15:36:12 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-08 15:46:34.822779
• 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 Logicの使用を含む一連のステップを通じて、障害をローカライズします。 実世界のDafnyプログラムのベンチマークであるDafnyBenchを用いて,我々のアプローチを評価する。
• 参考スコア（独自算出の注目度）: 84.30534714651093
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification offers strong assurances of software correctness. However, debugging and repairing the underlying faults can be complex and time-consuming when verification fails. Automated Program Repair (APR) aims to ease this by automatically identifying and fixing faults. Traditional APR techniques often depend on test suites for validation, but these may fail to capture all scenarios. In contrast, formal specifications provide stronger correctness criteria for effective repairs. We present an innovative 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 state-of-the-art Large Language Models (LLMs) to synthesize candidate fixes. The chosen models were 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% accuracy in fault localization, with GPT-4o mini yielding the highest repair success rate (74.18%). These results highlight the potential of combining formal reasoning with LLM-driven program synthesis for automated program repair.
• Abstract（参考訳）: 形式的検証は、ソフトウェアの正しさを強く保証する。 しかし、基礎となる障害のデバッグと修復は複雑で、検証が失敗すると時間がかかる可能性がある。 APR(Automated Program repair)は、障害を自動的に識別し、修正することで、これを容易にすることを目的としている。 従来のAPRテクニックは、検証のためのテストスイートに依存することが多いが、これらはすべてのシナリオをキャプチャできない可能性がある。 対照的に、正式な仕様は、効果的な修復のためのより強い正当性基準を提供する。 本稿では,プリコンディションやポストコンディション,不変(invariant)といった形式仕様を,障害のローカライゼーションと修復のためのオラクルとして使用する,検証対応のプログラミング言語であるDafny用の革新的なAPRツールを提案する。 仕様の正しさを前提として,プログラム内の各ステートメントの状態を決定するHoare Logicや,最新の大規模言語モデル(LLM)など,一連のステップを通じて障害をローカライズして,問題の修正を合成する。 選ばれたモデルは、GPT-4o mini、Llama 3、Mistral 7B、Llemma 7Bである。 実世界のDafnyプログラムのベンチマークであるDafnyBenchを用いて,我々のアプローチを評価する。 また, GPT-4o mini が最も高い修理成功率 (74.18%) を示した。 これらの結果から, 自動プログラム修復のための形式推論とLCM駆動型プログラム合成を併用する可能性が示唆された。

関連論文リスト

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

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

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