LLM2Cert：利用大语言模型合成证书，并通过 SMT/Lean 验证
李雅普诺夫函数和屏障证书可为动态系统提供稳定性与安全性保证，但在非线性、高维系统中，合成和验证仍然困难。研究团队推出包含 105 个多样化案例的基准 DynaCertBench，以及 LLM2Cert 框架。该框架生成候选证书，并通过 SMT 求解器或 Lean 检查其证明义务。LLM2Cert 在 105 个案例中验证了 81 个（77.1%），比无反馈的一次性提案高出 17.1 个百分点。在 81 个固定证书中，它验证了 All-SMT 未能解决的 22 个。代码和数据已公开。
本文来源：Hugging Face，仅供学习参考，版权归原作者所有。