Certificates stop leaning on numerical solvers alone: LLM2Cert kernel-checks 81 of 105 dynamical systems
Synopsis
Stability and safety of dynamical systems are usually guaranteed by Lyapunov functions and barrier certificates, yet the numerical, interval and SMT solvers used to check candidates often need relaxations, and standard test suites drifted toward low-dimensional polynomial systems. LLM2Cert has a language model propose candidate certificates and routes each proof obligation to an SMT solver or to the Lean proof assistant, allowing only proof repair and never a change to the theorem. On the 105-instance DynaCertBench, the full framework verifies 81 instances end to end, against 63 for one-shot proposal without feedback.
Interpretation
Certificate verification is retargeted from a relaxed version the solver can handle back to the original, unrelaxed stability and safety conditions, with each result coming from an SMT unsatisfiability verdict or a Lean kernel-checked proof. Earlier pipelines relied on sum-of-squares programming, interval methods or SMT solvers, and often excluded a neighborhood of the origin, replaced transcendental terms by Taylor approximations, or accepted a -sat verdict that holds only for a weakened formula. On the 81 frozen certificates and their 296 obligations, SMT discharged 253 obligations (85.5%) by unsat and 43 reached Lean: 8 after -sat, 13 after timeout, 19 by direct router decision, and 3 radial-unboundedness obligations with no SMT encoding.
A language model proposes the candidate certificates, and a rejected candidate receives counterexamples or proof diagnostics rather than permission to alter the theorem. One-shot proposal takes no feedback and verifies 63/105 on DynaCertBench; SMT-only feedback reaches 57/105 and Lean-only reaches 60/105. The full framework verifies 66/80, 7/11 and 8/14 on the Literature-derived, Extended and New tiers, 81/105 overall, gains of 15.0, 27.3 and 21.4 percentage points over one-shot proposal on those tiers.
The quality of Lean proof repair decides whether the expensive backend converges, and structured feedback classifies and locates the compiler error and attaches matching Mathlib lemmas. Among 26 obligations that failed their first proof attempt across 19 systems, generic retry that reports only failure repaired 1/26, and returning raw compiler output repaired 17/26. Structured repair under the same budget repaired 21/26 obligations and 15/19 systems, at 2.19 rounds and 407.42 seconds per obligation, with unrepaired obligations charged the full 900-second budget.
Perspective
The demonstrated setting is the stability, region-of-attraction, forward-invariance and safety tasks for continuous- and discrete-time systems in DynaCertBench, with each candidate's theorem statement held fixed during verification. The authors describe the benchmark as a curated collection of 105 instances rather than an exhaustive sample, and list extension to hybrid and uncertain dynamics as future work.
The authors state that the present formulation focuses primarily on deterministic dynamical systems and that extending it to stochastic systems with random disturbances and probabilistic guarantees is a next step; the synthesis loop targets prescribed verification domains rather than explicitly optimizing the certified set. Of the 24 unresolved systems, 10 end at a Lean call timeout or shared-deadline exhaustion and 6 produce no parsed candidate before the deadline.