PaperlayerView exact revision on arXiv

Source-linked AI summary

Formal Model Construction Guided by Model-Based Proof Sketches

Hongshu Wang, Xinyue Zuo, Yufan Cai, Neeraj Kumar Singh, Yamine Ait Ameur, Jin Song Dong

arXiv:2609.29870v1cs.SE

TL;DR

Formal model construction is labor-intensive, and existing LLM approaches rely on verification feedback that can be difficult to use for consistent repairs across a model. ProGS uses hierarchical proof sketches to structure model construction and repair; across 27 formal systems, it reports high proof-level verifiability, competitive runtime, and fewer LLM requests than existing approaches incorporating proof information.

  • Problem

    Formal modeling requires substantial expertise and effort, while existing autoformalization approaches provide model- or event-level feedback that can be limited for fault localization or miss dependencies among related events.

    Source: §1 · p. 2, §2.2 · p. 4

  • Method

    ProGS uses LLM-generated model-based proof sketches as a hierarchical intermediate representation, checks sketch structure and leaf proof obligations, and maps failures to subtrees for repair.

    Source: §1 · p. 2, §3.3 · p. 7

  • Results

    Across 27 formal systems, ProGS achieves high proof-level verifiability and competitive runtime, resolving proof failures with fewer LLM requests than existing approaches that incorporate proof information.

    Source: §1 · p. 3

  • Takeaways & Limitations

    The evaluation suggests that proof sketches provide more effective verification feedback and a more appropriate repair granularity than flat generate-and-repair workflows.

    Source: §1 · p. 3

    Proof-discharge-based verifiability depends on the underlying tools, so an unproven obligation may reflect prover limitations rather than an incorrect model, and expert intervention may still be needed.

    Source: §5.1.1 · p. 15

Abstract

from arXiv · show

Formal modeling provides strong guarantees about system correctness, but developing and repairing formal models remains labor-intensive and requires substantial expertise in logic and formal reasoning. Recent LLM-based autoformalization agents seek to reduce this burden by generating candidate formal models and revising them using feedback from formal tools. However, the existing approaches follow a generate-and-repair paradigm, in which repairs are driven by verification failures of the generated model and therefore depend heavily on both the granularity of the feedback and the LLM's repair capability. As a consequence, a repair targeting one level of verification may invalidate properties at another level, which requires reasoning over the complete set of event guards. To address these limitations, we propose Proof-Sketch-Guided Formal Model Synthesis (ProGS), an autoformalization method centered on model-based proof sketches. A model-based proof sketch represents the proof structure of the target formal system as a tree. Internal nodes capture case splits and inductive reasoning steps, while leaf nodes correspond to concrete state-transition events that realize individual subgoals. ProGS uses LLMs to generate and repair these sketches, with verification failures mapped back to specific nodes and subtrees to provide structured guidance for iterative repair. Our evaluation on a benchmark of 27 formal systems shows that ProGS improves over state-of-the-art agentic formal modeling approaches in syntactic validity, deductive verifiability, and behavioral correctness, demonstrating the benefit of organizing formal model construction around hierarchical proof sketches.

1 Introduction

Formal model construction is labor-intensive and requires expertise, while existing LLM approaches rely on verification feedback whose granularity can make consistent repairs difficult. ProGS organizes construction and repair around hierarchical proof sketches, and its evaluation reports strong verification results and reduced modeling effort.

1 Introduction

  • Formal modeling remains labor-intensive because translating requirements into models and diagnosing failed verification require expertise in logic, specification languages, and formal reasoning.Existing LLM methods generate candidate models and repair them from tool feedback, but effectiveness depends on feedback granularity and repair capability.Source: §1 · p. 2
  • ProGS uses tree-structured model-based proof sketches to connect hierarchical proof structure with state-transition events, localize failures, and guide repairs of related model components.Internal nodes capture case splits and inductive reasoning; leaves correspond to transition events for proof subgoals.Source: §1 · p. 2
  • Across 27 formal systems, ProGS achieves high proof-level verifiability, competitive runtime, and resolves proof failures with fewer LLM requests than existing approaches that incorporate proof information.The evaluation also reports that baselines tend to improve one performance aspect at the cost of another.Source: §1 · p. 3
  • The paper introduces a hierarchical intermediate representation and ProGS, integrates the method into the Rodin IDE, and evaluates it on 27 formal systems.Its contribution summary reports improvements in syntactic validity and deductive verifiability.Source: §1 · p. 3

2 Background and Motivation

The section defines state-based formal models and their verification obligations, then explains why flat, independently repaired components can undermine coherent system-level behavior. A selection-sort example motivates ProGS’s use of proof sketches to organize events and repair related failures.

2.1 Preliminary

  • A state-based model consists of an environment model Γ and events; each event has a guard and an action, and deadlock-freeness requires an enabled event in every reachable state.The environment contains constants, sets, axioms, variables, invariants, and variants.Source: §2.1.1 · p. 3, §2.1.2 · p. 3

2.1.2 Verification Obligations.

  • Invariant preservation requires every event to preserve the global invariant, which may be decomposed into less complex obligations for individual event-invariant pairs.This decomposition distributes checking across event-invariant pairs.Source: §2.1.2 · p. 3, §2.1.3 · p. 3

2.1.3 Modeling Efforts.

  • Unlike decomposable invariant-preservation checks, deadlock-freeness uses a disjunction of event guards, so failures provide limited localization and can make repair costly.Table 1 presents a subset of selection-sort safety requirements and their formalizations.Source: §2.1.3 · p. 4, Table 1 · p. 4

2.2 Problem Statement

  • Flat model-level feedback offers limited fault localization, while independently repairing event-level failures can overlook dependencies; repair groups should cover events sharing a structural cause without unnecessary changes.The section frames effective repair as intermediate in granularity between repairing one event and repairing the entire model.Source: §2.2 · p. 4

2.3 Motivating Example

  • The motivating comparison shows that a missing guard can leave prefix-sortedness unproved, while guards added to discharge a proof obligation can over-constrain place_minimum and cause deadlocks.ProGS instead decomposes minimum search into cases and refines the place_minimum node while retaining behavioral coverage.Source: §2.3 · pp. 5–6
  • In the selection-sort example, ProGS refines an incomplete place_minimum node into four cases, adding a critical guard while retaining cases where that guard does not hold.The cases include a successful swap, abnormal cases, and successful termination.Source: §2.3 · p. 6

3.1 Overview

ProGS constructs an environment model, generates and validates a proof sketch, and synthesizes a formal model from the validated sketch. It maps verification failures to subtrees to focus repairs.

3.1 Overview

  • ProGS constructs an environment model, generates and validates a model-based proof sketch, then synthesizes a formal model while mapping verification failures to problematic subtrees for focused repair.The sketch is refined using deadlock-freeness and parent-child guard checks, and its leaf events are verified through event-level proof obligations.Source: §3.1 · p. 6

3.2 Environment Model Construction

ProGS constructs a well-formed environment model, identifies relationships among invariants and variants, and validates those relationships through proof obligations. The validated dependencies guide proof-sketch construction, including case splits and induction.

3.2 Environment Model Construction

  • ProGS prompts an LLM to construct an environment model from requirements, then repairs compilation and typing errors until it is well-formed.The sorting example's model includes constants, variables, invariants, and variants.Source: §3.2 · p. 6
  • Requirements are represented as condition-gated invariants; using TRUE as the condition makes a requirement a global invariant.Prefix sortedness is an example whose property is expected to hold when fs = TRUE.Source: §3.2 · pp. 6–7
  • ProGS identifies equivalence, implication, case-split, and induction dependencies, which respectively capture redundant or subsumed invariants, branching opportunities, and inductive relations.An induction dependency links a hypothesis, conclusion, and decreasing variant; the hypothesis establishes the conclusion in the inductive step.Source: §3.2 · p. 7
  • The dependencies are validated through proof obligations for equivalence, implication, case splits, and induction, with induction checked at a terminal variant value.In the sorting example, n-k reaching zero lets the sorted-prefix invariant imply that the entire array is sorted.Source: §3.2 · p. 7
  • For selection sort, n-k tracks progress toward the final sorted state, while r-l tracks termination of the inner minimum-search loop.The sorted prefix serves as the induction hypothesis.Source: §3.2 · p. 7

3.3 Model-Based Proof Sketch

A model-based proof sketch is a tree connecting proof conditions to state-transition events. ProGS normalizes and checks the sketch, then uses a structural cost score to select and repair candidates.

3.3 Model-Based Proof Sketch

  • A proof sketch is a tree whose internal nodes encode guarded proof or case-splitting conditions and whose leaves contain guards and actions for concrete state-transition events.An LLM generates the initial sketch from requirements, the environment model, and invariant dependencies; structural checks then guide iterative repair.Source: §3.3 · p. 7

3.3.1 Sketch Cleaning.

  • Sketch cleaning removes non-executable leaves, merges unary branches, and factors shared sibling guards into an abstract parent.Factoring common guards makes subtree structure more explicit for later fault localization and repair.Source: §3.3.1 · pp. 7–8

3.3.2 Structural Checks of a Model-Based Proof Sketch.

  • Structural checks require child branches to cover their parent’s guards and each child’s guards to imply its parent’s, supporting invariant preservation from leaves up to the root.The checks can be decomposed into smaller proof obligations, including obligations at the edge level.Source: §3.3.1 · p. 8, §3.3.2 · p. 8

3.3.3 Model-Based Proof Sketch Structural Cost.

  • The Structural Cost Score favors sketches with fewer structural-check failures, greater depth, and more leaf nodes; ProGS selects the lowest-scoring of three candidates.The selected sketch and failed checks are supplied to the LLM for repair until the checks pass or the trial limit is reached.Source: §3.3.3 · p. 9

3.4 Formal Model Synthesis and Subtree-Based Repair

ProGS translates validated proof-sketch leaves into formal-model events and checks their proof obligations. When obligations fail, it maps failures to sketch leaves and can repair related subtrees together.

3.4 Formal Model Synthesis and Subtree-Based Repair

  • Each leaf of a validated proof sketch becomes a state-transition event, and the events are combined with the environment model to form the formal model.Source: §3.4.1 · p. 9

3.4.1 Formal Model Construction.

  • In the selection-sort example, Case 1 and Case 2 search for the minimum in the unsorted suffix, while place_minimum swaps it into position.Case 1 advances l when l < r and g(l) > g(r).Source: §3.4.1 · p. 9
  • ProGS generates event-level obligations for guard well-definedness, invariant preservation, and variant decrease, then applies automated provers and SMT solvers.Source: §3.4.1 · p. 9

3.4.2 Failure Localization and Subtree-Based Repair.

  • When an invariant or variant obligation fails, ProGS maps the failure to sketch leaves and groups leaves that fail the same obligation under a common subtree.The LLM is prompted to repair that subtree rather than each failed event independently.Source: §3.4.2 · p. 9
  • In the example, failed prefix-sortedness proofs at both leaves under place_minimum lead ProGS to request a repair of the whole subtree.That subtree corresponds to the events Inductive Case 4 and Termination 3.Source: §3.4.2 · p. 9
  • Structural checking and subtree repair repeat until the sketch is structurally valid and its derived model discharges all generated obligations.The validated sketch can then be deterministically translated into events that avoid unexpected deadlocks and satisfy invariant-encoded user properties.Source: §3.4.2 · p. 9

4 Evaluation

The evaluation compares ProGS with agentic modeling baselines on 27 formal systems, measuring model quality, construction effort, and component contributions. ProGS is best or second-best across all reported metrics, while ablations assess structural checks and subtree-based repair.

4.1 Experimental Setup and Implementation

  • The comparison uses Event-B as a common language, with Rodin for compilation and proof checks and ProB for model checking.All methods use the same LLM, GPT 5.4 mini, and receive Event-B documentation and rules for a fair comparison.Source: §4.1 · p. 10

4.2 Benchmarks

  • The benchmark contains 27 Event-B Agent examples spanning sequential algorithms, concurrent systems, and distributed systems.Requirements specify constants, variables, behavior, and safety properties; three concrete constant assignments per system provide traces for runtime metrics.Source: §4.2 · p. 10

4.3 Baselines

  • The three baselines range from basic generation and repair to planning with retrieval and event-level proof-guided model repair.Basic Modeling Agent, PAT-Agent, and adapted Event-B Agent are compared in Event-B.Source: §4.3 · p. 11

4.4 Metrics

  • Model quality is assessed through syntax correctness, runtime coverage, trace conformance, Proof Discharge Rate, and Requirement Fulfillment Rate.The evaluation omits Invariant Correctness because Requirement Fulfillment Rate is proof-based and accounts for multiple invariants per requirement.Source: §4.4 · p. 11

4.5 RQ1. Overall Performance

  • Across 27 formal systems, ProGS is best or second-best across all metrics and achieves the highest Trace Conformance score (0.697), exceeding PAT-Agent, Event-B Agent, and Basic Modeling Agent by 0.395, 0.210, and 0.068, respectively.Source: §4.5 · pp. 11, 13, Table 2 · p. 11

4.6 RQ2. Efficiency and Modeling Efforts

  • ProGS averages 2.366 LLM requests per discharged proof obligation, fewer than Event-B Agent, and also has lower average runtime and LLM-call counts.Event-B Agent averages 7.148 requests per discharged obligation; ProGS's subtree-level failure localization supplies more informative repair guidance.Source: §4.6 · pp. 13–14, Table 4 · p. 13

4.7 RQ3. Ablation Study

  • Ablations indicate that structural checks improve runtime semantics, while subtree-based repair improves both proof-level and runtime performance.Structural checks can slightly reduce proof-level performance by ruling out over-restrictive shortcuts, while helping keep sketches valid and parent-child relations semantically consistent.Source: §4.7 · pp. 14–15

5 Discussion

The discussion qualifies ProGS’s verification guarantees by the limits of automated proof discharge, LLM variability, and the benchmark’s partial environment information. The authors describe mitigations and boundaries for interpreting the evaluation.

5.1 Threats to Validity

  • Proof discharge is a proxy for model verifiability, and valid obligations may remain unproven when tools lack domain-specific lemmas, hints, or interactive reasoning.An unproven obligation therefore does not necessarily indicate an incorrect model; ProGS reduces rather than eliminates expert intervention.Source: §5.1.1 · p. 15

5.1.1 Construct Validity.

  • LLM nondeterminism can change generated sketches, repair decisions, model quality, and the number of synthesis or repair iterations.Prompt design, decoding parameters, and model choice may also affect measured performance; additional models and settings would strengthen evidence of stability.Source: §5.1.2 · p. 15

5.1.2 Internal Threats.

  • The benchmark supplies partial environment information, including constant and variable names and types, which constrains the formal models LLMs may generate.That information is needed to compute Runtime Coverage and Trace Conformance, and all evaluated methods receive it uniformly.Source: §5.1.3 · p. 15

6 Related Work

Prior work applies LLMs to individual formal-methods tasks and to formal model generation, while ProGS structures the broader modeling process around proof sketches. Unlike theorem-proving sketches used to guide proof generation, ProGS sketches are model-based artifacts that encode state-transition events and are themselves verified and repaired.

6.1 Autoformalization

  • LLMs have been applied to theorem proving [12] [13] [20] [24] [27] [28], specification generation [15] [23], and verifiable code generation.Interactive modeling assistants such as ModelWisdom leave substantial modeling decisions to users, while later work studies automatic model construction [3] [11] and verification-guided agentic approaches [21].Source: §6.1 · p. 16
  • Formal modeling spans construction, verification, validation, and iterative repair, whereas ProGS uses proof sketches to structure construction, decompose checks, and guide repair hierarchically.The cited agentic approaches largely treat generated model components as a flat collection of artifacts.Source: §6.1 · p. 16

6.2 Theorem Proving with Proof Sketches

  • Theorem-proving sketches typically draft informal proofs or sequences of subgoals to guide formal proof generation [12] [13] [20] [27] [28], rather than serving as verified and repaired model-based artifacts.ProGS sketches encode both proof subgoals and the state-transition events that discharge them.Source: §6.2 · p. 16

7 Conclusion

The conclusion presents ProGS as a hierarchical approach to state-based formal modeling, using model-based proof sketches to decompose verification and guide repair. It identifies extensions to formal checks and study of refinement and trace validation as future work.

7 Conclusion

  • ProGS uses model-based proof sketches to decompose global verification into edge- and node-level checks and aggregate related failures through subtrees for repair.The conclusion frames this as an alternative to flat collections of model components and says it produces high-quality models whose correctness can be more easily verified.Source: §7 · p. 16
  • The conclusion identifies additional edge- and subtree-level formal checks, and the relationship of proof sketches to model refinement and trace validation, as future research directions.Source: §7 · p. 16
  • The authors describe model-based proof sketches as an opportunity to design structural and modular verification beyond what flat formal models support.Source: §7 · p. 16
Loading 2609.29870v1…