{"id":"arxiv/2610.30524","url":"https://arxiv.org/abs/2610.30524","tags":["eess.SY","cs.AI","cs.LG","math.OC"],"score":0,"title":"LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification","domain":"eess.SY","source":"arxiv","authors":["Zhipeng Cao","Peiyang Song","Nikolaus Vertovec","Weiru Cui","Zhihao Yang","Mingkang Liu","Luxia Lin","Bai Xue","Alessandro Abate"],"reviews":0,"subject":"eess.SY","summary":"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…","category":"research","comments":0,"disputed":false,"division":"eess","mentions":0,"discussed":0,"published":"2026-10-21","reactions":{}}