PaperlayerView exact revision on arXiv

Source-linked AI summary

PAT-Agent: Autoformalization for Model Checking

Xinyue Zuo, Yifan Zhang, Hongshu Wang, Yufan Cai, Zhe Hou, Jing Sun, Jin Song Dong

arXiv:2509.23675v1cs.SE

TL;DR

Formal modeling remains difficult because of the learning curve and complexity of formal languages, while LLM-based synthesis faces hallucinations and logical inconsistencies. PAT-Agent combines structured LLM planning with PAT verification and feedback-guided repair; across 40 tasks, it reports a 100% verification success rate.

  • Problem

    Formal methods are difficult to adopt because of steep learning curves and complex formal languages, while LLM synthesis can produce hallucinated or logically inconsistent models.

    Source: §I · p. 1

  • Method

    PAT-Agent uses semantic-prompt planning to guide LLM model synthesis, checks models with PAT, and uses verification feedback for iterative repair.

    Source: §I · p. 2

  • Results

    100% verification success rate across 40 tasks.

    Source: §IX · p. 11

  • Takeaways & Limitations

    A user study confirms that the interface is usable and accessible for non-experts building and verifying formal models.

    Source: §I · p. 2

    Ambiguous or incomplete inputs can yield incorrect or underspecified models, and highly entangled control logic or intricate data-dependent behavior may not decompose cleanly into the semantic-prompt structure.

    Source: §VII · p. 11

Abstract

from arXiv · show

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.

I. INTRODUCTION

PAT-Agent combines LLM-based synthesis with formal verification to address the expertise and accessibility barriers of formal modeling. It uses structured planning and verification-guided repair, alongside an interface intended to help non-experts build and verify models.

I. INTRODUCTION

  • Formal methods’ broader adoption is limited by steep learning curves, inaccessible tooling, and complex formal languages, despite their use in safety-critical and concurrent domains..Source: §I · p. 1
  • LLMs offer a route from informal requirements to formal specifications, but hallucinations, logical inconsistencies, and limited success with direct generation challenge reliable model synthesis.Prior LLM work emphasized fine-grained formulas or simpler system models, while rule-based synthesis is labor-intensive and difficult to generalize.Source: §I · p. 1
  • PAT-Agent uses semantic-prompt planning and verification-guided repair to synthesize formal models, with an ablation study confirming both components’ effectiveness.The framework is evaluated on 40 diverse tasks and compared with direct LLM baselines and alternative model combinations.Source: §I · p. 2
  • A web-based interface supports guided modeling, verification, and repair, and a user study confirms its usability and accessibility for non-experts.Users can input descriptions, inspect and edit intermediate representations, review verification results, and apply automatic corrections.Source: §I · p. 2

A. The PAT Framework

  • PAT provides state-space exploration and LTL verification for concurrent and real-time systems, but building correct models remains expertise-intensive.PAT’s CSP# language extends CSP with imperative C# statements and typed variables.Source: A. The PAT Framework · p. 2

B. Syntax and Semantics of CSP#

The paper presents the CSP# process syntax and PAT assertion forms used to model systems and check requirements. Requirements pair natural-language properties with expected verification outcomes, which PAT results are checked against.

B. Syntax and Semantics of CSP#

  • CSP# processes are built from events, imperative statements, choice, conditionals, sequencing, and parallel or interleaved composition.The passage describes a process as a labelled transition system.Source: B. Syntax and Semantics of CSP# · p. 2
  • CSP# sequential composition runs one process after another, external choice lets the environment select an offered branch, and parallel composition can synchronize on an alphabet.Interleaving executes both operands independently without event synchronization.Source: B. Syntax and Semantics of CSP# · p. 2

C. Assertions and Verification in PAT

  • PAT assertions check deadlock-freedom, reachability, or whether all execution traces satisfy an LTL formula.A requirement is satisfied when PAT’s result for an autoformalized assertion matches the user’s expected VALID or INVALID outcome.Source: C. Assertions and Verification in PAT · p. 2

III. APPROACH

PAT-Agent structures natural-language-to-model synthesis as a pipeline that combines planning, code generation, PAT verification, and feedback-driven repair. Its formal objective is to construct a well-formed PAT model from a natural-language specification and requirements.

III. APPROACH

  • PAT-Agent integrates LLMs with PAT to synthesize and formally verify system models from natural-language descriptions.The framework is organized around four core components.Source: §III · pp. 2–3
  • The Planning LLM extracts semantic elements and creates a detailed code-generation plan, which the Code Generation LLM converts into PAT models.The plan guides formal model construction; the generated models aim for syntactic correctness and semantic fidelity to user intent.Source: §III · p. 3
  • PAT checks generated models against user requirements and provides diagnostic feedback when a requirement is not satisfied.The Repair Loop uses counterexamples and violation traces to guide iterative model revisions.Source: §III · p. 3
  • The formal objective is to construct a well-formed PAT model from a natural-language specification and finite requirements set.The pipeline stages are formalized as possibly stochastic transformers.Source: §III · p. 3

A. Planning LLM

The Planning LLM uses reusable semantic prompts to extract structured modeling elements and turn them into a detailed plan for code generation. Prompt structure and validation rules constrain what the model extracts and how it is represented.

A. Planning LLM

  • Semantic prompts replace direct free-form code generation with an intermediate planning step built around reusable, parameterized modeling prompts.Each prompt includes a role specification, supporting context, structural guidance, and targeted instructions with validation rules.Source: A. Planning LLM · p. 3
  • The extraction prompts specify structured fields for constants, variables, and processes, including names, values or types, initial values, actions, and guards.The prompts also require unique, non-conflicting names and prescribe declaration ordering for constants and variables.Source: A. Planning LLM · p. 3
  • The planning transformer extracts typed variables, constants, and guarded actions into JSON-serializable elements for later stages.These elements are supplied to subsequent semantic prompts to create a detailed natural-language model-generation plan.Source: A. Planning LLM · pp. 3–4

B. Code-Generation LLM

PAT-Agent uses a line-by-line natural-language plan, augmented with PAT syntax guidance and retrieved examples, to generate formal models. PAT checks user requirements, and counterexamples guide localized repair until expectations match or the iteration cap is reached.

B. Code-Generation LLM

  • The Code-Generation LLM translates a line-by-line natural-language plan into PAT syntax, using syntax guidance and a retrieved plan-code example to improve robustness.The exemplar is selected for similarity to the plan; if none is close, it serves as a one-shot illustration.Source: B. Code-Generation LLM · p. 4

C. Model Checker (PAT)

  • PAT checks each user requirement with deadlock detection, reachability, or LTL, compares outcomes with expected results, and returns counterexamples for mismatches.The pipeline aggregates matches and mismatches into a verdict vector.Source: C. Model Checker (PAT) · p. 4

D. Verification-Repair Loop

  • Repair uses counterexample traces to prioritize likely faulty actions and issue targeted edits, then stops when all verdicts match or after five iterations.Directives are fed back to code generation without rerunning the full planning pipeline; if the cap is reached, the latest model and trace are returned.Source: D. Verification-Repair Loop · p. 4

E. Interactive Interface

The interface supports guided, interactive formalization, from reusing verified examples to gathering requirements, inspecting generated models, and repairing failures. The running example illustrates how semantic prompts guide model planning and how verification feedback drives targeted revision.

E. Interactive Interface

  • The interface first checks for similar verified systems, supports clarification when descriptions are ambiguous, and lets users customize reusable examples or start fresh synthesis.Its repository adds newly synthesized models after successful verification.Source: E. Interactive Interface · pp. 4–5
  • Users can review and revise extracted constructs, specify requirements through guided controls, inspect plans and code, and view verification outcomes and counterexamples.The repair dashboard also allows code edits or automatic repair and provides human-readable update summaries.Source: E. Interactive Interface · p. 5

F. Running Example

  • In the car example, semantic prompts use descriptions and extracted elements to infer action conditions, such as requiring the engine on, sufficient fuel, and the owner present before driving.The resulting plan maps natural-language annotations to formal constructs.Source: F. Running Example · p. 5
  • The car model passes P1 and P2 but fails P3; counterexample-guided repair targets implicated actions, such as tightening start_driving preconditions when no driver is present.The example links the verification failure to possible ambiguity or generation inaccuracies in the initial model.Source: F. Running Example · p. 6

IV. EVALUATION

The evaluation is organized around pipeline effectiveness, the contribution of planning and repair, and processing time. The supplied passages state these research questions but do not report their results.

IV. EVALUATION

  • RQ1 asks whether PAT-Agent generates verified systems from natural-language descriptions more effectively than alternative strategies.Source: §IV · p. 6
  • RQ2 examines how the Planning LLM and Repair Loop affect overall pipeline performance.Source: §IV · p. 6
  • RQ3 asks how processing time varies across pipeline stages and model configurations.Source: §IV · p. 6

A. Datasets and Baselines

The evaluation covers 40 tasks across three datasets and compares direct LLM generation with alternative pipeline pairings. PAT-Agent achieves a 100% full-pass rate across all systems after repair.

A. Datasets and Baselines

B. Metrics

  • CSR tracks syntax compilation, FPR tracks systems passing all assertions, and APR gives assertion-level correctness across systems.Source: B. Metrics · pp. 6–7

C. Results of RQ1: Effectiveness of Formal Model Generation

D. Results of RQ2: Impact of Components

The ablations show that planning and verification-guided repair both contribute to verification performance. Removing either component reduces performance, with the largest drop when both are removed.

D. Results of RQ2: Impact of Components

  • Removing either planning or repair reduces verification performance, with the most severe degradation when both are disabled.The study compares the full pipeline with variants that disable planning, repair, or both.Source: D. Results of RQ2: Impact of Components · p. 8
  • Removing the Repair Loop alone maintains 100% compilation, while the full-pass rate drops to 0.7500 and the average pass rate drops to 0.8045.Source: D. Results of RQ2: Impact of Components · p. 8
  • Across repair rounds, performance improves from initial generation and reaches 100% in the final repair process.The breakdown covers Round 0, intermediate rounds 1–2, and final Round 5.Source: Table VI · p. 8, D. Results of RQ2: Impact of Components · p. 9
  • Without the Planning LLM, compilation success falls to 0.7500, the full-pass rate to 0.6000, and the average pass rate to 0.7594.Without structured, semantics-aware planning, the Code Generation LLM struggles to produce syntactically valid code and align models with user intent.Source: D. Results of RQ2: Impact of Components · p. 9
  • Together, planning provides structural guidance for code generation, while repair iteratively corrects models to achieve final verification success.The ablation results affirm the importance of both components.Source: D. Results of RQ2: Impact of Components · p. 9

E. Results of RQ3: Time Efficiency

The <o3, Claude> pipeline combines strong verification performance with competitive efficiency, reaching the lowest reported median runtime. In a user study, participants using PAT-Agent completed tasks faster and achieved stronger assertion and system accuracy than the control group, while reporting that the interface was easy to inspect and modify.

E. Results of RQ3: Time Efficiency

  • The <o3, Claude> pipeline combines the highest verification performance with competitive efficiency across processing stages.o3 outperforms R1 in planning steps, while Claude has the lowest code-generation latency.Source: E. Results of RQ3: Time Efficiency · p. 9
  • Repair runtimes are low and stable for <o3, Claude>, while near-zero repair time in <o3, R1> and <o3, o3> accompanies lower overall verification coverage.Verification time remains consistently low across configurations; a small number of cases have elevated repair times.Source: E. Results of RQ3: Time Efficiency · p. 9
  • 4.34 minutes per system is the lowest median runtime reported, achieved by the <o3, Claude> pipeline.The pipeline also achieves strong end-to-end performance with high time efficiency.Source: E. Results of RQ3: Time Efficiency · p. 9

V. USER STUDY

  • Experimental-group users completed tasks faster than control-group users, although the reported comparison gives no task-time value.The difference suggests users spent time validating intermediate outputs and interpreting verification results through the interface.Source: §V · p. 10
  • 0.9958 assertion accuracy was achieved by experimental-group users, significantly outperforming the control group.Models produced by the experimental group also had significantly higher system accuracy; on simpler tasks, all reached 1.0000 accuracy.Source: §V · p. 10
  • Experimental-group users found the interface intuitive for understanding model construction and inspecting or modifying specific components.Control-group participants reported challenges prompting LLMs and writing correct PAT code.Source: §V · p. 10

VI. DISCUSSION

The discussion notes that CSP# lacks public corpora and prior end-to-end translators, limiting the available basis for a strong autoformalization baseline. It also presents the workflow as potentially adaptable beyond PAT and CSP#, while emphasizing the additional resources such adaptations require.

VI. DISCUSSION

  • CSP# lacks public corpora and prior end-to-end translators, and no existing work is known to cover an NL-to-CSP# pipeline with concurrent constructs, shared variables, and refinement assertions.Building a comparative baseline would require re-engineering the contribution itself.Source: §VI · p. 11
  • The workflow may generalize beyond CSP# and PAT to other model checkers and languages, including PEPA and Petri nets.The authors describe this as potential generalization.Source: §VI · p. 11
  • Adapting the workflow to CSP-style variants or other languages requires corresponding syntax documentation, example corpora, and verification-feedback integration.For CSP-style variants such as tock-CSP and model checkers such as FDR, most prompts and guidance are reusable.Source: §VI · p. 11

VII. THREATS TO VALIDITY

PAT-Agent’s validity is bounded by input clarity, model complexity, generation stochasticity, and repair heuristics tuned to observed safety and liveness errors. The paper contrasts its broader model-checking goal with prior work and concludes with a 100% verification success rate across 40 tasks and plans for broader support.

VII. THREATS TO VALIDITY

  • Ambiguous or incomplete inputs, entangled control logic, intricate data-dependent behavior, and stochastic generation constrain model fidelity; repair heuristics may not generalize beyond observed safety and liveness errors.The authors mitigate stochasticity by fixing LLM versions with timestamps and using multiple PAT-feedback repair iterations.Source: §VII · p. 11

VIII. RELATED WORK

  • Unlike work focused on translating natural language into temporal-logic formulae, PAT-Agent synthesizes and improves system models until they pass assertions, a more complex task.The related work also notes that LTL is only one type of assertion supported in PAT-Agent.Source: §VIII · p. 11
  • Prior Alloy and B-method work targets simpler system models or fine-grained formulae and directly maps natural language to code; PAT-Agent instead structures synthesis and targets model checking.The paper distinguishes its model-checking focus from neuro-symbolic work on interactive theorem proving, with PAT automatically discharging temporal-logic obligations after an LLM populates PAT’s process.Source: §VIII · p. 11

IX. CONCLUSION AND FUTURE WORK

  • PAT-Agent achieved a 100% verification success rate across 40 tasks; future work would extend semantic prompts to probabilistic, real-time, and hybrid systems and generalize the architecture to Event-B and Alloy.Source: §IX · p. 11

Related papers

Loading 2509.23675v1…