arXiv · ML· Zhipeng Cao, Peiyang Song, Nikolaus Vertovec, Weiru Cui, Zhihao Yang, Mingkang Liu, Luxia Lin, Bai Xue, Alessandro Abate·· 6 小时前AI 评分28
LLM2Cert：LLM 合成证书及 SMT/Lean 验证框架
LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification
AI 导读
研究提出 LLM2Cert 框架，通过 LLM 合成 Lyapunov 函数与屏障证书，并利用 SMT 求解器或 Lean 代理进行验证。该框架基于新基准 DynaCertBench（含 105 个实例）测试，成功验证 81 个实例，准确率达 77.1%，比无反馈的一次性提案提升 17.1 个百分点。 LLM2Cert 能验证 22 个 All-SMT 无法解决的固定证书实例，代码与数据已开源。
来源：arXiv · ML · arxiv.org