arXiv Artificial Intelligence· Zhipeng Cao, Peiyang Song, Nikolaus Vertovec, Weiru Cui, Zhihao Yang, Mingkang Liu, Luxia Lin, Bai Xue, Alessandro Abate·· 4 小时前AI 评分38
LLM2Cert：用 LLM 合成证书并经 SMT/Lean 验证
LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification
AI 导读
LLM2Cert 让 LLM 合成 Lyapunov 函数与屏障证书，并把每项证明义务分派给 SMT 求解器或 Lean Proof-Repair 智能体验证。在 105 个实例的 DynaCertBench 上，该框架验证通过 81 个（77.1%），比无反馈的一次性提议高 17.1 个百分点；在 81 个固定证书上，它验证了 All-SMT 未能解决的 22 个。
来源：arXiv Artificial Intelligence · arxiv.org