論文の概要: Preguss: It Analyzes, It Specifies, It Verifies

• arxiv url: http://arxiv.org/abs/2508.14532v1
• Date: Wed, 20 Aug 2025 08:40:22 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-21 16:52:41.39556
• Title: Preguss: It Analyzes, It Specifies, It Verifies
• Title（参考訳）: Preguss: 分析し、特定し、検証する
• Authors: Zhongyi Wang, Tengjie Lin, Mingshuai Chen, Mingqi Yang, Haokun Li, Xiao Yi, Shengchao Qin, Jianwei Yin,
• Abstract要約: 大規模言語モデル(LLM)は、最近、形式検証における自動化の度合いを高める可能性を実証している。 この記事では、フォーマルな仕様の生成と改善を自動化するモジュール式できめ細かいフレームワークであるPregussの概要を述べる。
• 参考スコア（独自算出の注目度）: 14.717270519465218
• License: http://creativecommons.org/licenses/by-nc-nd/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 context-length limitations and, more importantly, the difficulty of inferring complex, interprocedural specifications. This paper outlines Preguss - a modular, fine-grained framework for automating the generation and refinement of formal specifications. Preguss synergizes between static analysis and deductive verification by orchestrating two components: (i) potential runtime error (RTE)-guided construction and prioritization of verification units, and (ii) LLM-aided synthesis of interprocedural specifications at the unit level. We envisage that Preguss paves a compelling path towards the automated verification of large-scale programs.
• Abstract（参考訳）: 大規模なソフトウェアとハードウェアシステムの完全な自動検証は、間違いなく正式な方法の聖杯である。 大規模言語モデル(LLM)は、例えば、帰納的検証に不可欠な形式仕様を生成することで、形式的検証における自動化の度合いを向上する可能性を最近証明した。 この記事では、フォーマルな仕様の生成と改善を自動化するモジュール式できめ細かいフレームワークであるPregussの概要を述べる。 Pregussは2つのコンポーネントをオーケストレーションすることで静的解析と導出検証を相乗化する。 (i)潜在的実行エラー(RTE)による検証ユニットの構築と優先順位付け (II)単位レベルでのLLM支援による相互運用仕様の合成。 我々は,Pregussが大規模プログラムの自動検証に向けて魅力的な道を歩むことを示唆する。

関連論文リスト

• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [68.00108157244952]
  強化学習(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)
• Logic Mining from Process Logs: Towards Automated Specification and Verification [0.0]
  本稿では、ワークフローを介して発見されたプロセスモデルから論理的仕様を生成するアプローチを提案する。 本研究では、品質データ、特にノイズが生成された仕様の構造とテスト容易性に与える影響について検討する。
  論文  参考訳（メタデータ） (2025-06-10T09:44:19Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  本稿では,学習されたタイムドオートマトンとシステムに関する公式知識グラフを組み合わせることで,CPPSのモデルベース異常検出を改善することを目的とする。 モデルと検出された異常の両方を知識グラフに記述し、モデルと検出された異常をより容易に解釈できるようにする。
  論文  参考訳（メタデータ） (2023-08-25T15:25:57Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。 本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。 我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
  論文  参考訳（メタデータ） (2023-05-26T14:55:35Z)

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

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