一句话：提出 PAT-Agent，结合 LLM 规划、代码生成、PAT 模型检测与反例修复，实现自然语言到可验证形式模型的端到端自动形式化。
LLM 用于形式验证仍受规约语言复杂、输出幻觉及自然语言到形式逻辑的语义鸿沟制约。本文提出 PAT-Agent，一个端到端的自然语言自动形式化与形式模型修复框架：规划 LLM 先用语义提示提取建模元素并生成计划，指导代码生成 LLM 合成语法正确、语义忠实的形式模型；模型由 PAT 模型检测器对用户指定性质验证，出现偏差时触发修复循环，用反例迭代修正。作者还提供 Web 界面，使非形式方法专家能通过人机交互描述、定制并验证系统行为。在 40 个系统上，PAT-Agent 持续优于基线，以更高效率取得高验证成功率；消融研究确认规划与修复组件均重要，用户研究显示界面对有限形式方法经验者亦易用有效。
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 Anal y sis 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.
DOI 原文 ·
@inproceedings{paperbot9496,
title = {PAT-Agent: Autoformalization for Model Checking},
author = {Xinyue Zuo and Yifan Zhang and Hongshu Wang and Yufan Cai and Zhe Hou and Jing Sun and Jin Song Dong},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00176}
}