CMU 提出 LLM2Cert：用 LLM 生成证书并通过 SMT/Lean 自动验证

卡内基梅隆大学提出 LLM2Cert 框架，让 LLM 为非线性动力系统合成 Lyapunov 函数、Barrier 函数和策略，并由 SMT 求解器与 Lean 证明修复 agent 自动验证。流程涵盖提案 agent、快速筛查、SMT/Lean 路由及失败重试，可为稳定性、ROA、不变性与安全性提供认证保证；配套 benchmark 显示验证成功率显著提升。