自动形式化把自然语言中的数学翻译成 Lean 4 等交互式证明助手，近年来已经能够大规模运行。随着证明器能力提升，正确性的关注点从证明本身转向陈述本身——即形式化陈述是否忠实地对应其来源。给定可信的参考形式化，最直接的检验是逻辑等价，但这往往过于宽松。只要库中能够分别证明 $P$ 和 $Q$，就可以得到 $P \leftrightarrow \mathrm{True} \leftrightarrow Q$，从而任意两条语句都满足 $P \leftrightarrow Q$。证明器越强，越多无关的语句对会被误判为等价。早期方法通过限制证明器并要求每个证明显式引用另一条语句来缓解此问题。
我们提出 SemantEq，一种更为原则性的等价关系：每条语句只能通过一系列允许的步骤（如逻辑重排、使用库中已有等式进行重写）转化为另一条语句。判定依据是 Lean 实际检查的证明项，而非 tactic 脚本。基于此，我们实现了 SemantEq‑Eval，一种不依赖模型的搜索方法，在 ProofNetVerif 测试集上实现了 100% 精确率和 65.6% 召回率，优于 BEq+（95.8% 精确率、61.8% 召回率），且仅增加约 8.9 倍的 CPU 时间，却只多加入了三对等价。
语言模型可以发现更多证明，但在四个提示中有两个只能在约二分之一的非等价对上同时证明两个方向。我们进一步构建 SemantEq‑ProofAudit，依据关系导出的策略审计模型生成的证明，成功拒绝了所有 104 条非等价对，并在 407 条等价对上将召回率从 65.4% 提升至 81.1%（最佳提示下）。将等价证明的生成与接受分离，使得更强的证明器能够提升召回率，而不改变接受标准的含义。
代码与数据已开源：https://github.com/hlxr89/SemantEq
点评