SemantEq 用受限步骤链判定形式化陈述是否忠实等价。
资讯摘要
论文提出 SemantEq，用于判断自然语言数学陈述的形式化翻译是否忠实于可信参考形式化。作者指出，仅用逻辑等价 P↔Q 判定会因证明器过强而误判：任意两条可证命题都能经由 True 互推。SemantEq 要求两条陈述只能通过逻辑重排、库内等式重写等允许步骤互相转化，并按 Lean 校验的证明项而非策略脚本判定。作者报告 SemantEq-Eval 在 ProofNetVerif 测试集上精确率 100%、召回率 65.6%，并发布代码与数据。
要点速读
- 论文指出逻辑等价判定在强证明器下会误判：任意两条可证命题均可经 P↔True↔Q 互推。
- SemantEq 要求陈述仅通过逻辑重排、库内等式重写等允许步骤互相转化，并按 Lean 校验的证明项判定。
- 作者报告 SemantEq-Eval 在 ProofNetVerif 测试集上精确率 100%、召回率 65.6%，SemantEq-ProofAudit 在最佳提示下将 407 对等价陈述的召回率从 65.4% 提升至 81.1%。
中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/27 08:00:28（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。