論文の概要: A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs

• arxiv url: http://arxiv.org/abs/2512.24594v1
• Date: Wed, 31 Dec 2025 03:31:51 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-01 23:27:28.555935
• Title: A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs
• Title（参考訳）: 1001 LoCの物語:大規模プログラム検証のための潜在的実行時エラーガイド型仕様合成
• Authors: Zhongyi Wang, Tengjie Lin, Mingshuai Chen, Haokun Li, Mingqi Yang, Xiao Yi, Shengchao Qin, Yixing Luo, Xiaofeng Li, Bin Gu, Liqiang Lu, Jianwei Yin,
• Abstract要約: 本稿では、フォーマルな仕様の生成と改善を自動化するためのモジュラーできめ細かいフレームワークであるPregussについて述べる。 以上の結果から, Preguss は最先端の LLM ベースのアプローチを大きく上回っていることがわかった。 約1000LOCを超える実世界のプログラムに対して高度に自動化されたRTE-freeness検証を可能にし、80.6%88.9%の人間による検証を削減した。
• 参考スコア（独自算出の注目度）: 34.387390697713556
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Fully automated verification of large-scale software and hardware systems is arguably the holy grail of formal methods. Large language models (LLMs) have recently demonstrated their potential for enhancing the degree of automation in formal verification by, e.g., generating formal specifications as essential to deductive verification, yet exhibit poor scalability due to long-context reasoning limitations and, more importantly, the difficulty of inferring complex, interprocedural specifications. This paper presents Preguss -- a modular, fine-grained framework for automating the generation and refinement of formal specifications. Preguss synergizes between static analysis and deductive verification by steering two components in a divide-and-conquer fashion: (i) potential runtime error-guided construction and prioritization of verification units, and (ii) LLM-aided synthesis of interprocedural specifications at the unit level. We show that Preguss substantially outperforms state-of-the-art LLM-based approaches and, in particular, it enables highly automated RTE-freeness verification for real-world programs with over a thousand LoC, with a reduction of 80.6%~88.9% human verification effort.
• Abstract（参考訳）: 大規模なソフトウェアとハードウェアシステムの完全な自動検証は、間違いなく正式な方法の聖杯である。 大規模言語モデル(LLM)は、例えば、帰納的検証に不可欠な形式仕様を生成することで、形式的検証における自動化の度合いを向上する可能性を最近証明した。 本稿では、フォーマルな仕様の生成と改善を自動化するためのモジュラーできめ細かいフレームワークであるPregussについて述べる。 Pregussは2つのコンポーネントを分割・分散方式で操り、静的解析と導出検証を相乗化する。 一 検証ユニットの潜在的実行時エラー誘導構築及び優先順位付け (II)単位レベルでのLLM支援による相互運用仕様の合成。 Preguss は最先端の LLM ベースのアプローチよりも大幅に優れており、特に、1000 LoC 以上の実世界のプログラムに対して、高度に自動化された RTE-freeness 検証を可能にし、80.6%~88.9% の人的検証努力を削減できることを示す。

関連論文リスト

• Preguss: It Analyzes, It Specifies, It Verifies [14.717270519465218]
  大規模言語モデル(LLM)は、最近、形式検証における自動化の度合いを高める可能性を実証している。 この記事では、フォーマルな仕様の生成と改善を自動化するモジュール式できめ細かいフレームワークであるPregussの概要を述べる。
  論文  参考訳（メタデータ） (2025-08-20T08:40:22Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
  VERIFAI1は、このギャップを埋めるための自動化および半自動化アプローチを調査することを目的としている。 本論文では, 課題の繰り返しと今後の研究方向性を明らかにするために, 関連文献の予備的な合成について述べる。
  論文  参考訳（メタデータ） (2025-07-18T19:15:50Z)
• Supporting Software Formal Verification with Large Language Models: An Experimental Study [9.688989142858954]
  SpecVerifyは、大規模な言語モデルと正式な検証ツールを統合している。 このフレームワークは、Claude 3.5 SonnetとESBMC検証器を組み合わせて自動化ワークフローを形成する。 ロッキード・マーティンの9つのサイバー物理システムで評価されたSpecVerifyは、NASAのCoCoSimに匹敵する46.5%の精度を達成している。
  論文  参考訳（メタデータ） (2025-07-07T10:30:05Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  より大規模なモデルではなく、推論時間の増加を活用する統合されたテスト時間計算スケーリングフレームワークを提案する。 当社のフレームワークには,内部TTCと外部TTCの2つの補完戦略が組み込まれている。 当社の textbf32B モデルは,DeepSeek R1 671B や OpenAI o1 など,はるかに大きなモデルを上回る 46% の課題解決率を実現している。
  論文  参考訳（メタデータ） (2025-03-31T07:31:32Z)

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

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