机械检查与LLM评审结合可降低形式化验证的接受错误率
资讯摘要
论文提出一种超越LLM评判忠实度的Lean形式化验证方法，将LLM语义审查与机械的数值检查和空泛性检查结合，提供可核查反馈并发现LLM评审遗漏的错误。作者将该方法与Extract-Verify-Proof自动形式化流程用于构建FLMF，即NIST DLMF的部分形式化。在三个标注数据集上，该方法在已评估方法中接受错误率最低；专家审查还发现现有数据集存在翻译与来源缺陷。
要点速读
- 方法结合LLM语义审查与机械数值、空泛性检查，提供可核查反馈
- 与Extract-Verify-Proof流程结合构建FLMF，对NIST DLMF做部分形式化
- 三个标注数据集上接受错误率在已评估方法中最低，专家审查发现现有数据集缺陷
中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/24 08:00:37（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。