LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification

LLM2Cert. LLM Synthesis of Certificates with SMT/Lean Verification. By Zhipeng Cao and eight others, from the Institute of Software, Chinese Academy of Sciences, the University of Chinese Academy of Sciences, and five other institutions. Published on the twenty-first of October. Its code repository is worked out: about seventy source files, with a readme and a licence.

Lyapunov functions and barrier certificates are how you guarantee, over a whole state space, that a system is stable or that it stays safe. Finding one and then verifying it is still an open challenge, most of all for nonlinear, high-dimensional systems. Existing pipelines check candidates with numerical solvers such as sum-of-squares programs, with interval methods, or with satisfiability-modulo-theories solvers, known as SMT solvers. Those tools often need relaxations, are conservative, or scale poorly as dimension and nonlinearity grow.

The authors point to a second effect of the same limits. Benchmarks have been shaped by them. Standard test suites are dominated by low-dimensional polynomial systems, picked because solvers can handle them, not because engineering applications look like that.

The paper answers both halves. On the measuring side, it builds a harder benchmark. On the solving side, it lets a language model propose certificates, and then does not trust the proposal: every candidate is checked against the proof obligations it has to meet, and each obligation can go to whichever verifier suits it.

The benchmark is DynaCertBench, with one hundred and five instances. Eighty of them are non-redundant systems curated from the literature. Those are extended with high-dimensional variants, control-constrained variants, and new nonlinearly coupled systems, and the tasks cover stability, region of attraction, forward invariance and safety.

The framework is LLM2Cert. A language model synthesizes a candidate certificate, and the candidate is verified obligation by obligation. Each obligation is routed either to an SMT solver or directly to the Lean Proof-Repair agent, so a condition that a solver struggles with has another path to a proof.

On DynaCertBench, LLM2Cert verifies eighty-one of the one hundred and five instances, which is seventy-seven point one percent. That is a seventeen point one percentage point improvement over one-shot proposal without feedback. A second comparison isolates the routing. Holding the eighty-one certificates fixed, LLM2Cert verifies twenty-two of them that an All-SMT setup leaves unresolved. Code and data are released.

Before this, a certificate had to survive whatever single solver the pipeline was built on, and the benchmarks were drawn to match. Here the candidate comes from a language model, each proof obligation is sent where it can actually be discharged, and the test set is widened toward the systems engineers face.

LLM2Cert. LLM Synthesis of Certificates with SMT/Lean Verification. By Zhipeng Cao and eight others, from the Institute of Software, Chinese Academy of Sciences, the University of Chinese Academy of Sciences, and five other institutions. Published on the twenty-first of October. This is the long version: the whole paper rather than the abstract.

Before a robot, a vehicle or an aircraft controller is trusted, someone wants a guarantee that holds for every state, not just the ones that were simulated. For dynamical systems, that guarantee is a certificate. A Lyapunov function certifies stability by decreasing along every trajectory. A barrier certificate certifies safety by drawing a boundary that trajectories from the initial set can never cross into the unsafe one. Finding such a function is hard, and proving that it really works is harder. The paper's complaint is that the field has quietly bent the target to fit the tools. Verifiers exclude a small neighbourhood of the origin, swap cosines for Taylor approximations, or accept a solver verdict that only holds for a slightly weakened formula. Benchmarks followed suit, chosen for what solvers can handle.

Two kinds of checker matter here. An SMT solver works by hunting for a counterexample. It is handed the negation of a condition, and if it answers unsat, no counterexample exists and the condition holds. It can also answer sat, which hands back a violating state, or time out. One solver, dReal, can also answer delta-sat, which only says that a slightly loosened version of the query is satisfiable. That neither proves nor refutes anything. Lean works the other way round: it checks a proof term against a small trusted kernel. When it accepts, the exact mathematical statement is proven. The cost is that writing those proofs is slow. Soundness then has two layers. The authors proved in Lean that each task's certificate conditions really imply the property. The framework's job is the second layer: showing that a particular candidate satisfies those conditions, with nothing relaxed.

The loop has three parts. A Proposal Agent, a language model, reads a typed specification of the system and its sets, and proposes a symbolic certificate, plus a feedback policy when the system has control inputs. The task's theorem turns the candidate into a list of proof obligations, one per premise. From that point the candidate and its obligations are frozen. Only proofs are searched for. Fast screening comes next: each obligation is evaluated on sampled states, and any violation goes straight back to the proposer as a counterexample. Passing the screen proves nothing, so every obligation still goes to formal verification.

A Verification Router sends each obligation either to SMT or directly to Lean. Obligations with no SMT encoding, such as radial unboundedness, go straight to Lean. Solvers get thirty seconds per obligation. Anything that ends in delta-sat or a timeout is escalated to the Lean Proof-Repair Agent. That agent may write only the proof body; the definitions and theorem stay fixed. When an attempt fails, it gets structured feedback: the kind of failure, such as an unknown identifier or an unsolved goal, where it happened, the remaining goal, and for unknown names, matching lemmas found by searching Mathlib. Accepted proofs must type-check and pass an audit that rejects placeholders and any nonstandard axiom. The running example, System 88, shows the whole path. Three of its four safety obligations fall to SMT. The fourth contains a cosine on an unbounded domain, so only one solver can try it, and it times out. Lean's third proof attempt succeeds, showing the barrier's derivative stays above three tenths on the boundary.

DynaCertBench has a hundred and five instances: eighty curated from two hundred and thirty-three literature records, eleven extended and fourteen new. Curation is revealing in itself. Of twenty-nine nominally high-dimensional records, only seven survived, because the rest were duplicates, padded with decoupled states, or linearised by feedback. The new tiers raise that count to twenty-five. The full framework verifies eighty-one instances, seventy-seven point one percent. One-shot proposal manages sixty-three. SMT alone with feedback reaches fifty-seven and Lean alone sixty, so neither backend recovers the combination.

The cleaner test of the thesis freezes the eighty-one verified certificates and their two hundred and ninety-six obligations, then varies only the verifier. All-SMT verifies fifty-nine; All-Lean verifies sixty-four. On polynomial systems SMT already covers everything Lean does, and fast: under two seconds per system against roughly five hundred and twelve for Lean. On non-polynomial systems Lean verifies thirty-four of forty, SMT only eighteen. Routing gets all eighty-one, with SMT discharging two hundred and fifty-three obligations and only forty-three reaching Lean. A third experiment replays twenty-six failed first Lean attempts. Generic Retry repaired one, Raw Diagnostics seventeen, Structured Repair twenty-one.

The paper has a limitations section, in its appendix, and it names three. DynaCertBench is a curated hundred and five instances, not an exhaustive sample. The framework handles deterministic systems, not stochastic ones with probabilistic guarantees. And it verifies the sets that candidates induce rather than enlarging regions of attraction or invariant sets. The evidence adds caveats of its own. The results come with no repeated runs or error bars, and with a single proposal model. Lean adds no coverage on polynomial systems. Among the twenty-four unresolved systems, ten ended on a Lean timeout or the shared deadline and six never produced a parsed candidate, so many failures are budget failures rather than mathematical ones. Against existing pipelines, comparisons cover only fifty-one compatible systems, and the baselines still verified two that the framework did not.

The idea to carry away is a division of labour with a fixed contract. The language model is free to guess, and its guesses can be wrong as often as they like, because nothing it writes can change what is being proved. A fast solver clears the easy obligations, a proof assistant takes the hard ones, and every answer that counts is either an exact unsat or a kernel-checked proof. What used to be relaxed to suit the verifier is now simply proved.