证书不再只靠数值求解器：LLM2Cert 把 105 个动力系统里的 81 个验到核验通过
动力系统的稳定性与安全性通常靠 Lyapunov 函数和屏障证书给出保证，而以往验证这些候选证书的数值求解器、区间方法和 SMT 求解器往往需要放宽条件，标准测试集也因此偏向低维多项式系统。LLM2Cert 让大模型提出候选证书，把每条证明义务按类型分派给 SMT 求解器或 Lean 证明助手，并只允许修补证明、不允许改动定理。在包含 105 个实例的 DynaCertBench 上，完整框架端到端验证了 81 个实例，而单次提议不做反馈时为 63 个。