证书不再只靠数值求解器：LLM2Cert 把 105 个动力系统里的 81 个验到核验通过
核心概要
动力系统的稳定性与安全性通常靠 Lyapunov 函数和屏障证书给出保证，而以往验证这些候选证书的数值求解器、区间方法和 SMT 求解器往往需要放宽条件，标准测试集也因此偏向低维多项式系统。LLM2Cert 让大模型提出候选证书，把每条证明义务按类型分派给 SMT 求解器或 Lean 证明助手，并只允许修补证明、不允许改动定理。在包含 105 个实例的 DynaCertBench 上，完整框架端到端验证了 81 个实例，而单次提议不做反馈时为 63 个。
深度剖析
证书验证的目标从“求解器能处理的放宽版本”改回原始未放宽的稳定性与安全条件，验证结果由 SMT 的不可满足判定或 Lean 内核检查过的证明给出。 以往流程依赖平方和规划、区间方法或 SMT 求解器，常需排除原点邻域、用 Taylor 近似替换超越项，或接受 -sat 这类只对弱化公式成立的结论。 在固定下来的 81 份证书和 296 条证明义务上，SMT 以不可满足判定解决了 253 条，占 85.5%，其余 43 条进入 Lean，其中 8 条来自 -sat、13 条来自超时、19 条由路由器直接指派、3 条为无 SMT 编码的径向无界性。
候选证书由大模型提出，被拒时收到的是反例或证明诊断，而不是被允许修改定理。 单次提议不接收任何反馈，在 DynaCertBench 上验证 63/105；只用 SMT 反馈为 57/105，只用 Lean 为 60/105。 完整框架在文献来源层、扩展层和新建层分别验证 66/80、7/11 和 8/14，合计 81/105，相对单次提议在这三层分别提高 15.0、27.3 和 21.4 个百分点。
Lean 的证明修复质量决定了昂贵后端能否收敛，结构化反馈把编译器错误分类、定位并附上 Mathlib 中的匹配引理。 在 19 个系统上首次证明失败的 26 条义务中，只报告失败的通用重试修复 1/26，返回原始编译器输出的方式修复 17/26。 结构化修复在同样预算下修复 21/26 条义务和 15/19 个系统，平均每条义务 2.19 轮、407.42 秒，而未修复义务按 900 秒预算计。
启示与展望
演示范围是 DynaCertBench 上连续时间与离散时间系统的稳定性、吸引域、前向不变集与安全性四类任务，且每个候选证书的定理陈述在验证过程中保持固定。作者把该基准描述为 105 个实例的精选集合而非穷尽样本，并把扩展到混合与不确定动力学列为后续方向。
作者指出当前形式化主要针对确定性动力系统，扩展到带随机扰动和概率保证的随机系统是下一步；合成循环针对给定验证域，并未显式优化被认证集合的大小。24 个未解决系统中，10 个止于 Lean 调用超时或共享截止时间耗尽，6 个在截止前没有解析出候选。