Stability
Do states converge to the equilibrium?
26 problemsRESEARCH PROJECT · 2026
LLM2Cert
LLM Synthesis of Certificates
with SMT/Lean Verification
Language models propose Lyapunov functions, barrier certificates, and feedback policies. SMT solvers and Lean check the exact proof obligations.
105benchmark problems
77.1%verified end to end
+17.1 ppover one-shot proposal
22Full certificates beyond All-SMT
ABSTRACT
Synthesis with exact verification targets
Lyapunov functions and barrier certificates give state-space guarantees of stability and safety, but synthesizing and verifying them remains challenging for nonlinear, high-dimensional systems. Solver limitations have also shaped benchmarks toward low-dimensional polynomial systems.
We introduce DynaCertBench, a benchmark of 105 instances spanning stability, region of attraction, forward invariance, and safety. LLM2Cert synthesizes candidate certificates and routes each proof obligation to an SMT solver or the Lean proof-repair agent. A certificate is accepted only when all required obligations are discharged.
LLM2Cert verifies 81 of 105 instances, a 17.1 percentage point improvement over one-shot proposal. On the 81 fixed certificates, the integrated framework verifies 22 that All-SMT leaves unresolved.
FRAMEWORK
From a task to a checked certificate
The definitions, hypotheses, and theorem statement remain fixed during Lean proof repair. Failed proof attempts return compiler feedback for the next attempt.
DYNACERTBENCH
Four tasks, 105 problems
80 literature-derived systems, 11 extensions, and 14 newly constructed systems. The benchmark includes continuous- and discrete-time dynamics.
Region of attraction
Which initial states converge?
12 problemsForward invariance
Do trajectories remain inside the set?
13 problemsSafety
Do trajectories avoid unsafe states?
54 problemsRESULTS
Main experiment and research questions
MAIN
End-to-end synthesis and verification
The full framework verifies 81/105 systems. On the 51 systems supported by the external baselines, Full verifies 40; the baseline union verifies 19 natively and 11 under Strict accounting.
Main runs and model outputs ↗| Configuration | Verified systems |
|---|---|
| One-shot proposal | 63/105 |
| SMT-only | 57/105 |
| Lean-only | 60/105 |
| Full | 81/105 |
The one-shot reference is reconstructed from successful Full traces that required no feedback.
RQ1 / RQ2
Backend coverage and routing cost
Comparisons use the same 81 frozen certificates and 296 active obligations. Full discharges 253 obligations through SMT and 43 through Lean.
| Strategy | Verified | Mean time (s) |
|---|---|---|
| All-SMT | 59/81 | 3.68 |
| All-Lean | 64/81 | 579.17 |
| Routed (Full) | 81/81 | 119.31 |
| SMT-first + Lean | 80/81 | 94.28 |
Time averages use verified certificates. Full is observed; SMT-first + Lean composes saved SMT and independent Lean records.
RQ3
Compiler-guided proof repair
Three feedback strategies start from the same 26 failed first attempts from 19 systems. Structured Repair repairs 21 obligations and has the lowest mean timeout-charged repair time.
Repair trajectories and compiler logs ↗| Feedback | Repaired | Mean time (s) |
|---|---|---|
| Generic Retry | 1/26 | 873.66 |
| Raw Diagnostics | 17/26 | 491.02 |
| Structured Repair | 21/26 | 407.42 |
Unrepaired obligations are charged the full 900-second budget.
CITATION
Cite LLM2Cert
@misc{cao2026llm2certllmsynthesiscertificates,
title={LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification},
author={Zhipeng Cao and Peiyang Song and Nikolaus Vertovec and Weiru Cui and Zhihao Yang and Mingkang Liu and Luxia Lin and Bai Xue and Alessandro Abate},
year={2026},
eprint={2610.30524},
archivePrefix={arXiv},
primaryClass={eess.SY},
url={https://arxiv.org/abs/2610.30524},
}
For setup and new experiments, see the running guide. For questions, use GitHub Issues.