SemantEq：形式化陈述的忠实双向等价性

陈述自动形式化将自然语言表述的数学内容转换为 Lean 4 等证明助手中的形式化表达，如今模型已能大规模完成这一任务。随着证明器能力增强，正确性保障的重心从证明转向陈述，即形式化陈述是否忠实地翻译了其来源。在给定可信参考形式化表达的情况下，自然的检验标准是逻辑等价，但这一标准过于宽泛。对于库中可证的任意两个陈述 $P$ 和 $Q$，$P \leftrightarrow Q$ 都平凡成立，因为证明器可以分别证明二者，再通过 $P \leftrightarrow \mathrm{True} \leftrightarrow 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%。将等价性证明的生成与验收分离，使更强的证明器能够提高召回率，而不改变通过验收所代表的含义。我们在以下地址发布代码和数据：https://github.com/hlxr89/SemantEq