LLM2Cert：用LLM合成证书并经SMT/Lean验证

LLM2Cert结合LLM生成与SMT/Lean验证，在自建基准上验证通过率77.1%。

资讯摘要

论文提出LLM2Cert框架，由大模型生成Lyapunov函数与屏障证书候选，再将证明义务分派给SMT求解器或Lean证明修复代理进行验证。作者同时构建DynaCertBench基准，含105个实例，覆盖稳定性、吸引域、前向不变性与安全性任务，并加入高维、控制约束及非线性耦合系统。作者报告在DynaCertBench上验证通过81/105（77.1%），较无反馈的一次性生成提升17.1个百分点。

要点速读

1. 论文提出LLM2Cert，将证书证明义务路由至SMT求解器或Lean Proof-Repair代理验证。
2. 作者构建DynaCertBench，含105个实例，覆盖稳定性、吸引域、前向不变性与安全性任务。
3. 作者报告验证通过81/105（77.1%），比无反馈一次性生成高17.1个百分点；在81个固定证书上多验证22个All-SMT未解决的实例。

中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/24 08:00:37（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。