論文の概要: 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の拡張を示し、ユーザビリティのフィードバックを奨励します。

関連論文リスト

• 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)
• 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)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。 本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。 我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
  論文  参考訳（メタデータ） (2023-05-26T14:55:35Z)

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

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