論文の概要: Supporting Software Formal Verification with Large Language Models: An Experimental Study

• arxiv url: http://arxiv.org/abs/2507.04857v1
• Date: Mon, 07 Jul 2025 10:30:05 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-08 15:46:35.379922
• Title: Supporting Software Formal Verification with Large Language Models: An Experimental Study
• Title（参考訳）: 大規模言語モデルによるソフトウェア形式検証支援に関する実験的検討
• Authors: Weiqi Wang, Marie Farrell, Lucas C. Cordeiro, Liping Zhao,
• Abstract要約: SpecVerifyは、大規模な言語モデルと正式な検証ツールを統合している。 このフレームワークは、Claude 3.5 SonnetとESBMC検証器を組み合わせて自動化ワークフローを形成する。 ロッキード・マーティンの9つのサイバー物理システムで評価されたSpecVerifyは、NASAのCoCoSimに匹敵する46.5%の精度を達成している。
• 参考スコア（独自算出の注目度）: 9.688989142858954
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal methods have been employed for requirements verification for a long time. However, it is difficult to automatically derive properties from natural language requirements. SpecVerify addresses this challenge by integrating large language models (LLMs) with formal verification tools, providing a more flexible mechanism for expressing requirements. This framework combines Claude 3.5 Sonnet with the ESBMC verifier to form an automated workflow. Evaluated on nine cyber-physical systems from Lockheed Martin, SpecVerify achieves 46.5% verification accuracy, comparable to NASA's CoCoSim, but with lower false positives. Our framework formulates assertions that extend beyond the expressive power of LTL and identifies falsifiable cases that are missed by more traditional methods. Counterexample analysis reveals CoCoSim's limitations stemming from model connection errors and numerical approximation issues. While SpecVerify advances verification automation, our comparative study of Claude, ChatGPT, and Llama shows that high-quality requirements documentation and human monitoring remain critical, as models occasionally misinterpret specifications. Our results demonstrate that LLMs can significantly reduce the barriers to formal verification, while highlighting the continued importance of human-machine collaboration in achieving optimal results.
• Abstract（参考訳）: 形式的手法は、長い間要求検証に用いられてきた。 しかし、自然言語の要求からプロパティを自動的に導出することは困難である。 SpecVerifyはこの課題に対処するため、大きな言語モデル(LLM)を形式的な検証ツールに統合し、要求を表現するためのより柔軟なメカニズムを提供する。 このフレームワークは、Claude 3.5 SonnetとESBMC検証器を組み合わせて自動化ワークフローを形成する。 ロッキード・マーティンの9つのサイバー物理システムで評価されたSpecVerifyは、NASAのCoCoSimに匹敵する46.5%の精度を達成しているが、偽陽性は低い。 我々のフレームワークは、LTLの表現力を超えて拡張するアサーションを定式化し、より伝統的な手法に欠かせない偽のケースを識別する。 反例解析により、モデル接続誤差と数値近似問題に起因するCoCoSimの限界が明らかになった。 SpecVerifyは検証自動化を進歩させていますが、Claude、ChatGPT、Llamaの比較研究は、高品質な要求文書と人間の監視が重要であることを示しています。 以上の結果から,LLMは,人間と機械の協調作業の継続的な重要度を強調しつつ,形式的検証の障壁を著しく低減できることが示された。

関連論文リスト

• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [5.783301542485619]
  エンドツーエンドのプログラム検証タスクにおいて,大規模言語モデル(LLM)を評価するために設計された新しいベンチマークを導入する。 評価の結果,o3-miniのような最先端(SOTA)モデルでさえ4%未満のパス率を達成でき,多くの出力がコンパイルに失敗していることがわかった。
  論文  参考訳（メタデータ） (2025-05-25T19:00:52Z)
• Model Utility Law: Evaluating LLMs beyond Performance through Mechanism Interpretable Metric [99.56567010306807]
  大規模言語モデル(LLM)は、学術、産業、そして日々のアプリケーションに欠かせないものになっている。 大規模言語モデル (LLM) 時代における評価の課題の1つは一般化問題である。 従来の性能スコアを補完するメカニズムの解釈可能性向上指標であるモデル利用指数(MUI)を提案する。
  論文  参考訳（メタデータ） (2025-04-10T04:09:47Z)
• Inference-Time Intervention in Large Language Models for Reliable Requirement Verification [2.3759432635713895]
  推論時間介入技術は微調整に代わる有望な手段である。 我々は、介入が通常時間を要する要求検証プロセスを自動化するためのきめ細かい制御を可能にする方法を実証する。 提案手法は, ベースラインモデルと微調整手法の両方において, 頑健で信頼性の高い出力を実現する。
  論文  参考訳（メタデータ） (2025-03-18T10:49:36Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。 我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• FaithEval: Can Your Language Model Stay Faithful to Context, Even If "The Moon is Made of Marshmallows" [74.7488607599921]
  FaithEvalは、コンテキストシナリオにおける大規模言語モデル(LLM)の忠実度を評価するためのベンチマークである。 FaithEvalは4.9Kの高品質な問題で構成され、厳格な4段階のコンテキスト構築と検証フレームワークを通じて検証されている。 我々の研究は、最先端のモデルでさえ、与えられた文脈に忠実であり続けるのに苦労することが多く、大きなモデルが必ずしも改善された忠実を示すとは限らないことを明らかにしている。
  論文  参考訳（メタデータ） (2024-09-30T06:27:53Z)
• Improving Retrieval Augmented Language Model with Self-Reasoning [20.715106330314605]
  本稿では,ALMの信頼性とトレーサビリティ向上を目的とした,新たな自己推論フレームワークを提案する。 このフレームワークは、関連性を認識したプロセス、エビデンスを認識した選択プロセス、軌跡解析プロセスの3つのプロセスで自己推論軌道を構築することを含む。 提案手法の優位性を示すため,4つの公開データセットにまたがるフレームワークの評価を行った。
  論文  参考訳（メタデータ） (2024-07-29T09:05:10Z)
• Simultaneous Machine Translation with Large Language Models [51.470478122113356]
  我々は,SimulMTタスクに大規模言語モデルを適用する可能性を検討する。 MUST-Cデータセットと異なる9言語でtextttLlama2-7b-chatモデルを用いて実験を行った。 その結果,LLM は BLEU と LAAL の指標で専用MT モデルよりも優れていた。
  論文  参考訳（メタデータ） (2023-09-13T04:06:47Z)

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

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