論文の概要: Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?

• arxiv url: http://arxiv.org/abs/2510.12702v1
• Date: Tue, 14 Oct 2025 16:37:39 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-15 19:02:32.397184
• Title: Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?
• Title（参考訳）: ポストコンディションを超えて: 大規模言語モデルは自動ソフトウェア検証のための形式的契約を推測できるか?
• Authors: Cedric Richter, Heike Wehrheim,
• Abstract要約: 大規模言語モデル(LLM)は、自然言語のヒントから正式な後条件を推測する際の約束を示す。 NL2Contractは,非公式な自然言語を形式的関数型コントラクトに変換するためにLLMを使用するタスクである。 NL2Contract with different LLMs and compared it to the task of postcondition generation nl2postcond。
• 参考スコア（独自算出の注目度）: 1.9551668880584971
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Automatic software verifiers have become increasingly effective at the task of checking software against (formal) specifications. Yet, their adoption in practice has been hampered by the lack of such specifications in real world code. Large Language Models (LLMs) have shown promise in inferring formal postconditions from natural language hints embedded in code such as function names, comments or documentation. Using the generated postconditions as specifications in a subsequent verification, however, often leads verifiers to suggest invalid inputs, hinting at potential issues that ultimately turn out to be false alarms. To address this, we revisit the problem of specification inference from natural language in the context of automatic software verification. In the process, we introduce NL2Contract, the task of employing LLMs to translate informal natural language into formal functional contracts, consisting of postconditions as well as preconditions. We introduce metrics to validate and compare different NL2Contract approaches, using soundness, bug discriminative power of the generated contracts and their usability in the context of automatic software verification as key metrics. We evaluate NL2Contract with different LLMs and compare it to the task of postcondition generation nl2postcond. Our evaluation shows that (1) LLMs are generally effective at generating functional contracts sound for all possible inputs, (2) the generated contracts are sufficiently expressive for discriminating buggy from correct behavior, and (3) verifiers supplied with LLM inferred functional contracts produce fewer false alarms than when provided with postconditions alone. Further investigations show that LLM inferred preconditions generally align well with developers intentions which allows us to use automatic software verifiers to catch real-world bugs.
• Abstract（参考訳）: 自動検証は、(形式的な)仕様に対してソフトウェアをチェックするタスクにおいて、ますます効果的になっている。 しかし、現実のコードではそのような仕様が欠如しているため、実践的な採用が妨げられている。 大きな言語モデル(LLM)は、関数名やコメント、ドキュメントなど、コードに埋め込まれた自然言語ヒントから正式な後条件を推論する際の約束を示している。 しかし、生成された後条件をその後の検証の仕様として使用すると、検証者は無効な入力を推奨し、最終的には誤報となる可能性のある問題を暗示する。 そこで本研究では,ソフトウェアの自動検証の文脈において,自然言語からの仕様推論の問題を再考する。 そこで本研究では,NL2Contractを導入し,LLMを用いて自然言語を形式的関数型コントラクトに翻訳する手法を提案する。 我々は,NL2Contractアプローチの検証と比較を行うメトリクスを導入し,音質,生成したコントラクトのバグ識別能力,およびソフトウェア自動検証のコンテキストにおけるユーザビリティを重要指標として紹介する。 NL2Contract with different LLMs and compared it to the task of postcondition generation nl2postcond。 評価の結果,(1)LLMはすべての入力に対して機能的契約音を生成するのに一般的に有効であること,(2)生成した契約は正しい動作からバギーを識別するのに十分な表現力があること,(3)LLMを推定した機能的契約を付与した検証器は,ポストコンディショナリのみを備える場合よりも誤警報が少ないことがわかった。 さらなる調査によると、LLM推論の前提条件は開発者意図とよく一致しており、実際のバグをキャッチするために自動ソフトウェア検証器を使用することができます。

関連論文リスト

• Do Large Language Models Respect Contracts? Evaluating and Enforcing Contract-Adherence in Code Generation [11.445615378917578]
  PACTは、プログラムアセスメントおよび契約順応評価フレームワークである。 契約違反に焦点を当てた包括的なテストスーツコーパスを提供する。 様々なプロンプト条件下でのコード生成の体系的解析を可能にする。
  論文  参考訳（メタデータ） (2025-10-14T01:12:37Z)
• Uncovering Systematic Failures of LLMs in Verifying Code Against Natural Language Specifications [0.6813925418351435]
  大規模言語モデル(LLM)はソフトウェア開発において不可欠なツールとなり、要求工学、コード生成、レビュータスクに広く利用されている。 本稿では,LLMが自然言語の要求に適合するかどうかを評価する上で,体系的に失敗していることを明らかにする。 以上の結果から,LCMは要件を満たすことのできないコード実装や潜在的な欠陥を含むコード実装を誤って分類することが多いことが判明した。
  論文  参考訳（メタデータ） (2025-08-17T13:07:26Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  本稿では,Code LLMの命令追従能力を改善するために,前方および後方制約生成を提案する。 IFEvalCodeは、7つのプログラミング言語の1.6Kテストサンプルからなる多言語ベンチマークである。
  論文  参考訳（メタデータ） (2025-07-30T08:08:48Z)
• 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)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。 そこで本研究では,新しい接頭辞オートマトンと,在来型を探索する手法を開発し,LLM生成コードに適切な型付けを強制するための健全なアプローチを構築した。 提案手法は,コード合成,翻訳,修復作業において,コンパイルエラーを半分以上削減し,機能的正しさを著しく向上させる。
  論文  参考訳（メタデータ） (2025-04-12T15:03:00Z)
• Towards Large Language Model Aided Program Refinement [10.089955747110444]
  プログラムの洗練には、正式なハイレベルな仕様文から実行可能なプログラムへの正当性保存の変換が含まれる。 大型言語モデル(LLM)は、非公式な自然言語仕様から自動コード生成を可能にする。 LLM4PRは,形式的プログラム改善手法と非公式なLCMベースの手法を組み合わせたツールである。
  論文  参考訳（メタデータ） (2024-06-26T04:29:27Z)
• Knowledge-Augmented Language Model Verification [68.6099592486075]
  最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。 本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。 その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
  論文  参考訳（メタデータ） (2023-10-19T15:40:00Z)
• Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions? [17.03841665553565]
  大きな言語モデル(LLM)は、プログラマの意図にマッチする仕様への自然言語の意図の翻訳を容易にする可能性がある。 本稿では,プログラムアサーションとして表現された,非公式な自然言語形式的メソッドのポストコンディションにLLMを活用する問題であるnl2postcondについて述べる。
  論文  参考訳（メタデータ） (2023-10-03T06:55:45Z)

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

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