SemantEq 提出形式化语句双向等价判定新方法
本条为 AI 依据下方公开信源自动整理生成的摘要，不构成转载，可能存在偏差，请以原文为准。整理者：贝果科技 AI 资讯助手。
全文梳理
AI 摘要依据下方信源原文自动整理，非原文转载等价判据为何失效
论文关注的是语句自动形式化：把自然语言数学翻译成 Lean 4 这类证明助手中的形式语句，模型已能大规模完成这一步。随着证明器变强，正确性的压力从「证明是否成立」转移到「形式语句是否忠实于原文」。在有可信参照形式化的情况下，直觉上的检验方式是逻辑等价，但这一判据证明得太多：对库中任意两条可证语句 P 和 Q，证明器可以分别证明二者，再经由 P↔True↔Q 得到 P↔Q。证明器越强，被误判为等价的无关语句对就越多。此前的方法通过限制证明器能力、并要求每个证明显式引用另一条语句来收紧条件。
允许步骤链与证明项判定
SemantEq 换了一种更讲道理的关系定义：每条语句必须仅通过一串被允许的步骤转换为另一条，例如逻辑重排，以及用库自身的等式进行改写。实现上，程序判断的是 Lean 实际检查的证明项，而不是模型写出的策略脚本，因此判定标准不随证明器强弱漂移。作者据此构建了无需模型的搜索方案 SemantEq-Eval，在 ProofNetVerif 测试划分、按其裁定标签下取得 100% 精确率与 65.6% 召回率，对比对象 BEq+ 为 95.8% 与 61.8%；把 CPU 时间放大到 8.9 倍，结果最多只增加三对，说明精度并非靠算力堆出。
模型写证明的审计结果
语言模型能找出更多等价证明，但论文报告：在四种提示中的两种下，模型对约五分之二的非等价语句对给出了双向证明，即把不该等价的语句判成了等价。为此作者给出 SemantEq-ProofAudit，按由该关系导出的策略逐条审计模型写出的证明，在 104 对非等价语句上一条也未接受；在最佳提示下，它把 407 对等价语句上的召回率从 65.4% 提升到 81.1%。这种把「生成等价证明」与「接受等价证明」分开的设计，使得换用更强的证明器可以抬高召回率，而接受的含义保持不变。论文共 37 页、4 幅图、6 张表，代码与数据已放出。
为什么值得看
自动形式化的瓶颈已从证明转向语句本身是否忠实，本文给出可判定的等价关系与审计工具，直接关系 Lean 形式化数据的可靠…
信源1 家
关键事实
相关 · 论文
本页内容由 AI 自动聚合公开信源生成，仅供了解行业动态参考，不构成任何投资或决策建议。如需引用请以原文出处为准。