LLM2Cert：基于 LLM 的证书合成与 SMT/Lean 验证

arXiv:2610.30524v1 公告类型：交叉发布 摘要：Lyapunov 函数和屏障证书可在状态空间中提供稳定性与安全性保证，但其合成与验证——尤其是针对非线性高维系统——仍是一项尚未解决的挑战。现有流程使用数值求解器（平方和规划）、区间方法或可满足性模理论（SMT）求解器来验证候选证书，这些方法往往需要松弛处理、具有保守性，或在模型维度和非线性程度增加时扩展性较差。这些局限也影响了基准设计：标准测试集主要由低维多项式系统构成，选择这些系统是为了适应求解器的处理能力，而非满足工程应用的需求。我们从两个方面应对这一挑战。首先，我们推出 DynaCertBench，这是一个包含 105 个实例的基准：以从文献中精选的 80 个非冗余系统为基础，加入高维变体、受控制约束的变体以及新的非线性耦合系统，全面覆盖稳定性、吸引域、前向不变性和安全性任务。其次，我们提出 LLM2Cert，这是一个由 LLM 驱动的框架，用于合成候选证书，并依据其证明义务进行验证：每项证明义务被分派给 SMT 求解器，或直接交给 Lean Proof-Repair 智能体。在 DynaCertBench 上，LLM2Cert 成功验证了 105 个实例中的 81 个（$77.1\%$），比无反馈的单次候选生成方式提高了 $17.1$ 个百分点。对于这 81 个固定证书，LLM2Cert 成功验证了其中 All-SMT 未能解决的 22 个。代码和数据可在 https://github.com/FormalCert-AI/llm2cert 获取。