Fugu-MT 論文翻訳(概要): Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles

論文の概要: Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles

arxiv url: http://arxiv.org/abs/2601.12845v1
Date: Mon, 19 Jan 2026 08:56:43 GMT
ステータス: 翻訳完了
システム内更新日: 2026-01-21 22:47:22.82125
Title: Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles
Title（参考訳）: LLMとテストオラクルを用いた形式仕様の自動生成と検証アノテーション
Authors: João Pascoal Faria, Emanuel Trigo, Vinicius Honorato, Rui Abreu,
Abstract要約: 110 Dafnyプログラムの実験では、Claude Opus 4.5 と GPT-5.2 を組み合わせたマルチモデルアプローチが、少なくとも8回の修正イテレーションで98.2%のプログラムに対して正しいアノテーションを生成した。ロジスティック回帰分析では、証明-ヘルパーアノテーションが現在のLLMの難易度に不相応に寄与していることが示された。
参考スコア（独自算出の注目度）: 3.4742046772246837
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Recent verification tools aim to make formal verification more accessible to software engineers by automating most of the verification process. However, annotating conventional programs with the formal specification and verification constructs (preconditions, postconditions, loop invariants, auxiliary predicates and functions and proof helpers) required to prove their correctness still demands significant manual effort and expertise. This paper investigates how LLMs can automatically generate such annotations for programs written in Dafny, a verification-aware programming language, starting from conventional code accompanied by natural language specifications (in comments) and test code. In experiments on 110 Dafny programs, a multimodel approach combining Claude Opus 4.5 and GPT-5.2 generated correct annotations for 98.2% of the programs within at most 8 repair iterations, using verifier feedback. A logistic regression analysis shows that proof-helper annotations contribute disproportionately to problem difficulty for current LLMs. Assertions in the test cases served as static oracles to automatically validate the generated pre/postconditions. We also compare generated and manual solutions and present an extension for Visual Studio Code to incorporate automatic generation into the IDE, with encouraging usability feedback.
Abstract（参考訳）: 最近の検証ツールは、ほとんどの検証プロセスを自動化して、フォーマルな検証をよりソフトウェアエンジニアにしやすくすることを目的としている。しかしながら、形式的な仕様と検証構造(前提条件、後条件、ループ不変量、補助述語と関数と証明ヘルパー)で従来のプログラムに注釈を付けるには、依然としてかなりの手作業と専門知識が必要である。本稿では,自然言語仕様(コメント)やテストコードに付随する従来のコードから始めて,検証対応のプログラミング言語であるDafnyで書かれたプログラムに対して,LCMがこのようなアノテーションを自動生成する方法について検討する。 110 Dafnyプログラムの実験において、Claude Opus 4.5 と GPT-5.2 を組み合わせたマルチモデルアプローチは、検証者フィードバックを用いて、少なくとも8回の修正イテレーションで98.2%のプログラムに対して正しいアノテーションを生成した。ロジスティック回帰分析では、証明-ヘルパーアノテーションが現在のLLMの難易度に不相応に寄与していることが示された。テストケースの挿入は、生成されたプレ/ポスト条件を自動的に検証するために静的なオラクルとして機能した。また、生成したソリューションと手動のソリューションを比較し、IDEに自動生成を組み込むVisual Studio Codeの拡張を示し、ユーザビリティのフィードバックを奨励します。

関連論文リスト

Evaluating LLM-Generated ACSL Annotations for Formal Verification [0.0]
本稿では,ACSL 仕様を人的・学習的支援なしに自動生成・検証できる形式分析ツールの規模を実証的に評価する。 5つのACSL生成システムを比較する:ルールベースのPythonスクリプト、Frama-CのRTEプラグイン、3つの大きな言語モデル。生成された仕様はすべて、複数のSMTソルバを動力とするFrama-C WPプラグインを使用して、同一条件下で検証される。
論文参考訳（メタデータ） (2026-02-14T19:18:34Z)
Guidelines to Prompt Large Language Models for Code Generation: An Empirical Characterization [82.29178197694819]
我々は、開発固有のプロンプト最適化ガイドラインを導出し、評価する。コード生成プロンプトを自動的に洗練するために、反復的でテスト駆動のアプローチを使用します。我々は50人の実践者と評価を行い,提案した即興改善パターンの使用状況について報告する。
論文参考訳（メタデータ） (2026-01-19T15:01:42Z)
Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification? [1.9551668880584971]
大規模言語モデル(LLM)は、自然言語のヒントから正式な後条件を推測する際の約束を示す。 NL2Contractは,非公式な自然言語を形式的関数型コントラクトに変換するためにLLMを使用するタスクである。 NL2Contract with different LLMs and compared it to the task of postcondition generation nl2postcond。
論文参考訳（メタデータ） (2025-10-14T16:37:39Z)
Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文参考訳（メタデータ） (2025-10-08T10:25:12Z)
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)
Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Models [54.14602121129874]
トレーニングデータを自動的に生成する最初のスケーラブルで信頼性の高いAutoIFを導入する。 AutoIFは命令追従データ品質の検証をコード検証に変換する。
論文参考訳（メタデータ） (2024-06-19T13:29:53Z)
Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
論文参考訳（メタデータ） (2024-03-31T18:15:49Z)
Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
論文参考訳（メタデータ） (2023-11-15T14:41:57Z)
Knowledge-Augmented Language Model Verification [68.6099592486075]
最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
論文参考訳（メタデータ） (2023-10-19T15:40:00Z)
Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
論文参考訳（メタデータ） (2023-05-26T14:55:35Z)

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

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