LLM improves verification of safety certificates in complex systems
LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification
Artificial IntelligenceMachine Learning
Summary
Guaranteeing that complex systems remain safe and stable is hard, especially when systems are nonlinear and have many parts. Traditional tools struggle with these challenges or only work well on simpler examples. The authors created a new testing set of tougher examples and built a method that uses large language models (LLMs) to suggest safety proofs and verify them automatically. Their method checks more cases successfully than previous approaches, making it easier to trust complex systems in real-life uses.
What this means in practice
- •For control engineers: Automate the verification of stability and safety certificates for high-dimensional nonlinear control systems to reduce manual proof effort.
- •For formal verification teams: Use an LLM-guided framework to integrate SMT solvers and proof assistants to verify complex system properties beyond current solver capabilities.
Authors
Zhipeng Cao, Peiyang Song, Nikolaus Vertovec, Weiru Cui, Zhihao Yang, Mingkang Liu, Luxia Lin, Bai Xue, Alessandro Abate
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.