LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification

Zhipeng Cao, Peiyang Song, Nikolaus Vertovec +6

Lyapunov functions and barrier certificates give state-space guarantees of stability and safety, but synthesizing and verifying them---especially for nonlinear, high-dimensional sy…