LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification
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.
Related
- Birnbaum's principles in Venn diagrams: Extended version with Lean verification
- Aligning Information Theory and Formal Verification: A Lean Formalization of Rate-Distortion Theory
- Four-arm polyominoes in Golomb's hierarchy: A complete classification with Lean verification
- A Lean 4 Verification Report for Completing the Arakawa--Moreau Conjecture on Maximal Ideals of Affine Vertex Algebras
- Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
BibTeX
@misc{cao2026llm2cert,
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},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.30524},
eprint = {2610.30524},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.30524},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification
AU - Zhipeng Cao
AU - Peiyang Song
AU - Nikolaus Vertovec
AU - Weiru Cui
AU - Zhihao Yang
AU - Mingkang Liu
AU - Luxia Lin
AU - Bai Xue
AU - Alessandro Abate
PY - 2026
DA - 2026/10/21
PB - arXiv
DO - 10.48550/arxiv.2610.30524
UR - https://arxiv.org/abs/2610.30524
AB - 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.
ER -