LLM2Cert：让大模型生成可验证的稳定性与安全性证明

导语

在机器人控制、自动驾驶和复杂工程系统中，仅靠仿真观察系统“似乎稳定”或“没有越界”并不够。研究者通常需要 Lyapunov 函数或 barrier certificate，将稳定性、安全性等性质转化为可以严格检查的数学证明。然而，对于高维、强非线性的动态系统，如何找到合适的证书、再确认它满足全部证明条件，始终是自动化验证中的难题。

论文《LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification》尝试把大语言模型引入这一流程，但并没有让模型直接充当最终裁判，而是将其定位为候选证书生成器，并把结论交给形式化工具核验。

核心要点

• 基准不再局限于低维多项式系统。 作者提出 DynaCertBench，共包含 105 个实例。其中有 80 个来自文献、经过筛选的非冗余系统，同时加入高维变体、控制约束变体以及新的非线性耦合系统，覆盖稳定性、吸引域、前向不变性和安全性等任务。
• 模型负责提出，工具负责证明。 LLM2Cert 根据动态系统和目标性质生成候选 Lyapunov 函数或 barrier certificate，并将相关证明义务路由到 SMT 求解器，或直接交给 Lean Proof-Repair agent。
• 反馈机制是关键。 如果候选证书未能通过检查，验证结果会反馈给模型，用于后续修改，而不是停留在一次性生成。这样的闭环减少了“表达看似合理、但无法形式化证明”的候选结果。
• 结果显示出组合式流程的价值。 在 DynaCertBench 上，LLM2Cert 验证了 105 个实例中的 81 个，成功率为 77.1%，比没有反馈的一次性提案高 17.1 个百分点。在已经修正的 81 个证书中，还有 22 个是 All-SMT 未能解决的案例。

意义与影响

这项工作的重要性不只是“让 LLM 写出数学表达式”，而是探索了生成模型与形式化验证器之间更合理的分工：模型负责搜索复杂、开放式的候选结构，SMT 和 Lean 则负责提供可检查的逻辑约束。对于证书合成而言，这种分工有望减少完全依赖人工构造函数的成本，也能缓解传统数值方法在高维和强非线性问题上的扩展瓶颈。

同时，DynaCertBench 也提醒研究者，评估自动证明系统不能只看容易被现有求解器处理的低维算例。更接近真实工程条件的高维、耦合和控制约束任务，才能检验方法是否具备实际适用性。当然，77.1% 的验证率并不意味着所有系统都能自动获得证明；剩余实例以及形式化工具的计算开销，仍是后续研究需要解决的问题。更准确地说，LLM2Cert 展示的是一种可迭代的“生成—验证—修复”路线，而不是用语言模型取代数学证明。

来源：Hugging Face Daily Papers