LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification

AI summary

Overview

Research area: Formal verification and safe control of dynamical systems, combining LLM-based certificate synthesis with SMT solvers and the Lean theorem prover.

Technical level: Advanced. The paper assumes familiarity with Lyapunov functions, barrier certificates, satisfiability modulo theories (SMT), and interactive theorem proving.

Scope: The paper introduces DynaCertBench, a 105-instance benchmark of stability, region-of-attraction, forward-invariance, and safety tasks, and LLM2Cert, an agentic framework that proposes Lyapunov/barrier certificates and verifies every proof obligation by SMT or a kernel-checked Lean proof.

What This Paper Is About

Lyapunov functions and barrier certificates are mathematical witnesses that a system is stable or safe, but finding them and rigorously checking them is hard, especially for nonlinear, high-dimensional systems. Existing checkers rely on numerical solvers, interval methods, or SMT solvers that often need relaxations (excluding a neighborhood of the origin, Taylor approximations, or accepting δ-sat answers) and scale poorly. The paper's goal is to keep the original, unrelaxed certificate conditions as a fixed target, verify them end to end with SMT plus Lean, and evaluate on a benchmark that restores the high-dimensional and control-constrained systems earlier test suites left out.

Key Contributions

1. DynaCertBench benchmark. 105 instances: 80 non-redundant systems curated from the literature, plus Extended variants (scaled dimension, larger domains, added control constraints or perturbations) and New high-dimensional, nonlinearly coupled systems. It covers stability, region-of-attraction, forward-invariance, and safety tasks for continuous- and discrete-time systems, each posed with its exact, unrelaxed certificate conditions.

2. SMT-plus-Lean verification paradigm. To the authors' knowledge, this is the first work to integrate the Lean theorem prover into end-to-end synthesis and verification of Lyapunov and barrier certificates for both continuous- and discrete-time systems. Obligations SMT cannot discharge (δ-sat, timeout, or no SMT encoding) are escalated to Lean, removing the need for Taylor approximations, δ-satisfiability, or excluding a neighborhood of the origin.

3. LLM2Cert agentic framework. A Proposal Agent generates a candidate certificate (and feedback policy); a Verification Router assigns each obligation to SMT or Lean; a Lean Proof-Repair Agent constructs kernel-checked proofs using structured compiler feedback; counterexamples and unresolved obligations are fed back into the next proposal round.

4. Soundness argument. Each certificate condition is proved in Lean to imply the corresponding theorem, and a candidate is accepted only when every obligation has an SMT unsat verdict or a kernel-checked Lean proof, giving an end-to-end chain from proposed candidate to verified candidate to theorem.

Main Findings

• End-to-end coverage: LLM2Cert verifies 81 of 105 DynaCertBench instances (77.1%), a 17.1 percentage point improvement over one-shot proposal without feedback (63/105).
• Ablation by tier: Full LLM2Cert verifies 66/80 Literature-derived, 7/11 Extended, and 8/14 New instances, versus 54/80, 4/11, and 5/14 for one-shot proposal, an improvement of 15.0, 27.3, and 21.4 percentage points respectively.
• Backends are complementary: SMT-only verifies 57/105 and Lean-only 60/105, while the full framework reaches 81/105. On the 81 fixed certificates with 296 obligations, All-SMT verifies 59/81 and All-Lean 64/81.
• Lean's gains concentrate on non-polynomial systems: All-Lean verifies 34/40 non-polynomial certificates versus 18/40 for All-SMT, while on polynomial systems SMT covers all 41/41 certificates that Lean verifies (Lean: 30/41).
• Routing is efficient: The routed strategy verifies all 81 fixed certificates. SMT discharges 253 of 296 obligations (85.5%) by unsat; 43 reach Lean (14.5%) — 21 after a non-unsat SMT result (8 δ-sat, 13 timeout), 19 by direct router decision, and 3 with no SMT encoding (radial unboundedness).
• Cost profile: All-SMT verifies 58 of the 81 certificates within 30 s per obligation and only 59 at 900 s. Mean times: All-SMT 1.65 s (polynomial) and 8.30 s (non-polynomial); All-Lean 511.99 s and 638.44 s; Routed 2.49 s and 239.05 s.
• Against external pipelines: On the 51 systems supported by at least one baseline, baselines verify 19/51 natively and only 11/19 of those natively verified certificates pass a strict recheck, while LLM2Cert verifies 40/51. LLM2Cert verifies 23 systems no baseline verifies natively and 17 that a baseline also verifies; baselines verify two systems LLM2Cert leaves unresolved.
• Unsolved BarrierBench cases: LLM2Cert verifies 8 of the 10 systems that Taheri et al. (2025) report as unsolved.
• Repair feedback matters: On 26 obligations that failed their first Lean attempt, Structured Repair fixes 21/26 and 15/19 systems in 2.19 rounds and 407.42 s per obligation, versus Raw Diagnostics 17/26, 13/19, 2.35 rounds, 491.02 s, and Generic Retry 1/26, no complete system, 3.58 rounds, 873.66 s.
• Illustrative case: In the Extend-S011 safety example, cvc5 times out on the barrier's Lie-derivative obligation; Lean proves it using ring and nlinarith to establish a lower bound of 3/10 > 0, and the final label is hybrid_verified.
• Reported numbers on Lean's exclusive coverage differ slightly by section: the abstract states LLM2Cert verifies 22 certificates that All-SMT leaves unresolved, while the fixed-candidate analysis (RQ1) states All-Lean verifies 21 that All-SMT leaves unresolved.

Methodology in Plain English

The system works as a loop. A language model is given a typed specification of the system, its domain, initial and unsafe sets, control bounds, and the task type, and proposes a symbolic candidate certificate plus, for controlled systems, a feedback policy. That candidate is parsed into a typed expression tree, and each premise of the relevant theorem becomes a separate proof obligation, with the original constraints left unchanged.

Before expensive verification, cheap sampling checks each obligation for obvious violations; a violation rejects the candidate and the offending samples become counterexample feedback. A router then sends each obligation either to an SMT solver (Z3, cvc5, Yices, dReal, with a 30 s timeout per obligation) or directly to Lean when no SMT encoding exists. An SMT unsat verifies the obligation; sat produces a counterexample; δ-sat or timeout is inconclusive and escalates to Lean.

In Lean, the theorem statement and definitions are fixed and the agent may only write the proof body. Failed attempts return classified errors, source locations, remaining goals, and matching Mathlib declarations, which the agent uses to repair its proof. Proofs are accepted only if they type-check and pass an audit rejecting the sorry placeholder and any axiom beyond Lean's standard ones. Candidates and obligations stay frozen throughout, so the framework never relaxes the target statement.

The loop allows up to 5 candidates per system, 6 Lean rounds per obligation within 900 s, and 2400 s total per system. The full run took 2.5 h; the fixed-certificate runs took 0.25 h (All-SMT), 1.4 h (All-Lean), and 2.1 h (repair sweep), about 6.2 h in total, recording 7.83 M model tokens.

Why This Matters

Research impact. The paper argues that benchmark design has been silently shaped by solver limitations: standard suites are dominated by low-dimensional polynomial systems with excluded origin neighborhoods or Taylor approximations. By holding the exact conditions fixed and using a proof assistant as the final arbiter, the work separates "the solver accepted a relaxed surrogate" from "the theorem is true," and shows where SMT and Lean each fall short.

Real-world applications (from the paper's framing of safety-critical autonomous systems):

• Robotic platforms needing stability and safety guarantees beyond simulation.
• Autonomous vehicles, where barrier certificates separate reachable states from unsafe regions.
• Aerospace systems requiring formal assurances for controllers.
• Controlled systems with input constraints, where the framework verifies a certificate against a specific feedback policy on the closed loop.

Industry relevance. The hybrid SMT/Lean routing gives a practical cost profile: fast solver checks where they apply, and expensive but sound proof search only where needed (Routed averages 2.49 s per polynomial system and 239.05 s per non-polynomial one, versus 511.99 s and 638.44 s for All-Lean). Machine-checkable certificates are more defensible in certification and assurance arguments than numeric tolerance-based verdicts.

Future Directions

• Broader benchmark coverage. DynaCertBench is a curated 105-instance collection; extending it to more high-dimensional, hybrid, and uncertain dynamics is stated as future work.
• Stochastic systems. The current formulation targets deterministic dynamics; extending to random disturbances with probabilistic guarantees is named as an important next step.
• Optimizing the certified region. The loop verifies the set induced by a proposed candidate rather than maximizing it; adding region-size objectives could formally synthesize larger regions of attraction and invariant sets.
• Combining neural synthesis with LLM verification. The authors note that pairing neural certificate synthesis with LLM2Cert is a promising direction, motivated by the two systems baselines verify but LLM2Cert does not, and by the 24 unresolved systems analyzed in the appendix.

Target Audience

Researchers and graduate students in formal methods, safe control, and verification of learned or nonlinear controllers; practitioners building certified safety cases for autonomous systems; and LLM-agent researchers interested in tool-augmented theorem proving and solver-in-the-loop synthesis. Readers without background in Lyapunov/barrier theory or SMT will find the verification sections dense, though the framework description is accessible.

Authors’ abstract

Lyapunov functions and barrier certificates give state-space guarantees of stability and safety, but synthesizing and verifying them---especially for nonlinear, high-dimensional systems---remains an open challenge. Existing pipelines verify candidates with numerical solvers (sum-of-squares programs), interval methods, or satisfiability-modulo-theories (SMT) solvers, which often require relaxations, are conservative, or scale poorly with model dimension and nonlinearity. These limitations have also shaped benchmark design: standard test suites are dominated by low-dimensional polynomial systems chosen to suit what solvers can handle rather than what engineering applications require. We address both sides of this challenge. First, we introduce DynaCertBench, a benchmark of 105 instances: 80 non-redundant systems curated from the literature, extended with high-dimensional and control-constrained variants and new nonlinearly coupled systems, comprehensively spanning stability, region-of-attraction, forward-invariance, and safety tasks. Second, we present LLM2Cert, an LLM-driven framework that synthesizes candidate certificates and verifies them against their proof obligations: each obligation is routed to an SMT solver or directly to the Lean Proof-Repair agent. On DynaCertBench, LLM2Cert verifies 81 of 105 instances ($77.1\%$), a $17.1$ percentage point improvement over one-shot proposal without feedback. On the 81 fixed certificates, LLM2Cert verifies 22 that All-SMT leaves unresolved. Code and data are available at https://github.com/FormalCert-AI/llm2cert.