論文の概要: PAT-Agent: Autoformalization for Model Checking

• arxiv url: http://arxiv.org/abs/2509.23675v1
• Date: Sun, 28 Sep 2025 06:32:14 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-30 22:32:19.367363
• Title: PAT-Agent: Autoformalization for Model Checking
• Title（参考訳）: PAT-Agent: モデルチェックの自動化
• Authors: Xinyue Zuo, Yifan Zhang, Hongshu Wang, Yufan Cai, Zhe Hou, Jing Sun, Jin Song Dong,
• Abstract要約: PAT-Agentは自然言語の自動形式化と形式モデル修復のためのエンドツーエンドフレームワークである。 これは、大きな言語モデルの生成能力と形式的検証の厳密さを組み合わせたものである。
• 参考スコア（独自算出の注目度）: 17.082027022913998
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent advances in large language models (LLMs) offer promising potential for automating formal methods. However, applying them to formal verification remains challenging due to the complexity of specification languages, the risk of hallucinated output, and the semantic gap between natural language and formal logic. We introduce PAT-Agent, an end-to-end framework for natural language autoformalization and formal model repair that combines the generative capabilities of LLMs with the rigor of formal verification to automate the construction of verifiable formal models. In PAT-Agent, a Planning LLM first extracts key modeling elements and generates a detailed plan using semantic prompts, which then guides a Code Generation LLM to synthesize syntactically correct and semantically faithful formal models. The resulting code is verified using the Process Analysis Toolkit (PAT) model checker against user-specified properties, and when discrepancies occur, a Repair Loop is triggered to iteratively correct the model using counterexamples. To improve flexibility, we built a web-based interface that enables users, particularly non-FM-experts, to describe, customize, and verify system behaviors through user-LLM interactions. Experimental results on 40 systems show that PAT-Agent consistently outperforms baselines, achieving high verification success with superior efficiency. The ablation studies confirm the importance of both planning and repair components, and the user study demonstrates that our interface is accessible and supports effective formal modeling, even for users with limited formal methods experience.
• Abstract（参考訳）: 大規模言語モデル(LLM)の最近の進歩は、形式的手法の自動化に有望な可能性を秘めている。 しかし、これらを形式的検証に適用することは、仕様言語の複雑さ、幻覚的出力のリスク、そして自然言語と形式論理のセマンティックギャップにより、依然として困難である。 PAT-Agentは,LLMの生成能力と形式検証の厳密さを組み合わせて,検証可能な形式モデルの構築を自動化する,自然言語の自動形式化と形式モデル修復のためのエンドツーエンドフレームワークである。 PAT-Agentでは、プランニング LLM がまずキーモデリング要素を抽出し、セマンティックプロンプトを使って詳細なプランを生成し、次にコード生成 LLM を誘導して、構文的に正確でセマンティックに忠実な形式モデルを合成する。 結果のコードは、ユーザ指定プロパティに対してProcess Analysis Toolkit(PAT)モデルチェッカーを使用して検証される。 柔軟性を向上させるために,ユーザ,特に非FM専門家がユーザ-LLMインタラクションを通じてシステム動作を記述,カスタマイズ,検証できるWebベースのインターフェースを構築した。 40システムの実験結果から, PAT-Agentはベースラインを一貫して上回り, 優れた効率で高い検証成功を実現していることがわかった。 本研究は, 設計と修復の両要素の重要性を検証し, ユーザ・スタディにより, 限られた形式的手法経験を持つユーザであっても, インターフェースがアクセス可能であり, 効果的な形式的モデリングをサポートすることを示した。

関連論文リスト

• 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)
• 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)
• FACT-AUDIT: An Adaptive Multi-Agent Framework for Dynamic Fact-Checking Evaluation of Large Language Models [79.41859481668618]
  大規模言語モデル(LLM)はファクトチェック研究を大幅に進歩させた。 既存のファクトチェック評価手法は静的データセットと分類基準に依存している。 本稿では, LLMのファクトチェック機能を適応的かつ動的に評価するエージェント駆動型フレームワークであるFACT-AUDITを紹介する。
  論文  参考訳（メタデータ） (2025-02-25T07:44:22Z)
• Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach [3.9155346446573502]
  本稿では,5GおよびNextGプロトコル(AVRE)のための実世界プロンプトを用いた形式検証の自動モデリングを提案する。 AVREは次世代通信プロトコル(NextG)の正式な検証のために設計された新しいシステムである。
  論文  参考訳（メタデータ） (2023-12-28T20:41:24Z)
• FLIP: Fine-grained Alignment between ID-based Models and Pretrained Language Models for CTR Prediction [49.510163437116645]
  クリックスルーレート(CTR)予測は、パーソナライズされたオンラインサービスにおいてコア機能モジュールとして機能する。 CTR予測のための従来のIDベースのモデルは、表形式の1ホットエンコードされたID特徴を入力として取る。 事前訓練された言語モデル(PLM)は、テキストのモダリティの文を入力として取る別のパラダイムを生み出した。 本稿では,CTR予測のためのIDベースモデルと事前学習言語モデル(FLIP)間の細粒度特徴レベルのアライメントを提案する。
  論文  参考訳（メタデータ） (2023-10-30T11:25:03Z)
• DeforestVis: Behavior Analysis of Machine Learning Models with Surrogate Decision Stumps [46.58231605323107]
  複雑なMLモデルの振る舞いを要約する視覚解析ツールであるDeforestVisを提案する。 DeforestVisは、より多くの切り株をインクリメンタルに生成することで、複雑さとフィデリティのトレードオフを探索するのに役立つ。 DeforestVisの適用性と有用性について,2つのユースケースと,データアナリストとモデル開発者とのエキスパートインタビューで紹介する。
  論文  参考訳（メタデータ） (2023-03-31T21:17:15Z)

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

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