{"id":"arxiv:2610.30524","kind":"preprint","title":"LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification","authors":["Zhipeng Cao","Peiyang Song","Nikolaus Vertovec","Weiru Cui","Zhihao Yang","Mingkang Liu","Luxia Lin","Bai Xue","Alessandro Abate"],"author_count":9,"year":2026,"published":"2026-10-21","venue":null,"cited_by":0,"doi":null,"arxiv_id":"2610.30524","nct_id":null,"source_url":"https://arxiv.org/abs/2610.30524","archive_url":"https://space-kitty.com/papers/arxiv:2610.30524","updated":"2026-10-21","pmid":null,"pmcid":null,"openalex_id":"W7223386416","pdf_url":"https://arxiv.org/pdf/2610.30524","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.","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["eess.SY","cs.AI","cs.LG","math.OC"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[{"slug":"ai-mathematics","name":"AI for Mathematics & Formal Proof","domain_slug":"math-cs"}],"cited_in_dossiers":[]}