LLM2Cert 框架发布：LLM 合成动力系统安全证书并自动验证

CMU 研究者发布 LLM2Cert 框架，号称首个将 Lean 定理证明器引入智能体式合成与验证的端到端系统，用于为非线性动力系统生成稳定性与安全性证书，包括 Lyapunov 函数、Barrier 函数和策略。框架由 LLM 负责合成证书，再通过 SMT 求解器与 Lean 自动验证，在 105 个系统的评测中通过率达 77%。

2026-10-27 ~ 2026-10-27 · 2 条相关

• CMU 提出 LLM2Cert：LLM 生成证书，SMT/Lean 自动验证 — CarnegieMellonU · 2026-10-27
• LLM2Cert 发布:LLM+Lean 自动合成安全证书,105 个系统通过 77% — wellecks · 2026-10-27