SemantEq：形式化数学语句的双向等价新方法

当AI模型大规模地将自然语言数学翻译成Lean 4等证明助手中的形式化语句时，正确性的重心正从证明本身转移到语句上——形式化语句是否忠实于原文。近日，一篇题为《SemantEq: Faithful Bidirectional Equivalence of Formal Statements》的研究提出了一个更严格的双向等价关系，旨在解决现有逻辑等价测试过于宽松的问题。

逻辑等价测试的困境

给定一个可信的参考形式化，最自然的测试是逻辑等价性，但研究发现这“证明得太多了”。对于库中任何两个可证语句P和Q，由于证明器可以分别证明它们，并通过P ↔ True ↔ Q传递，P ↔ Q会轻易成立。证明器越强，不相关的语句对通过测试的就越多。

据论文所述，早先的方法通过限制证明器并检查每个证明是否引用了另一个语句来应对。然而，这种方法不够原则化。SemantEq则要求每个语句仅通过一系列允许的步骤（如逻辑重排、使用库自身等式重写）变成另一个语句。

SemantEq示意图

证明项与策略脚本：在Lean 4等基于依赖类型论的证明助手中，策略脚本（tactic script）是用户编写的、指导证明搜索的命令序列，而证明项（proof term）是这些策略执行后由内核检查通过的实际证明对象。策略脚本可能包含自动化搜索、宏展开或非终止循环，其写法因人和工具而异；证明项则是类型论中的项，具有规范的结构，且其正确性由小型可信内核独立验证。因此，基于证明项判断等价性，可以避免因策略风格不同或证明器自动化程度差异而导致的判定偏差，使等价关系更接近语句本身的语义内容。

SemantEq的核心设计

SemantEq的核心创新在于：程序通过Lean检查的证明项（proof term）来判断证明，而非其策略脚本（tactic script）。这意味着判断标准不依赖于生成证明的方式，而是证明本身的结构。

该关系定义了“允许的步骤”链：每个语句必须通过逻辑重排、重写等操作转化为另一个语句。这种设计确保了等价性不是通过证明器的强大能力“作弊”实现的，而是基于语句间的实质性联系。

重写与逻辑重排：SemantEq允许的步骤包括逻辑重排（如交换合取项、调整量词顺序等保持经典逻辑等价的句法变换）和使用库自身等式进行重写（将语句中的子项替换为库中已证明相等的表达式）。这些步骤构成一条从语句P到语句Q的变换链，每一步都可由Lean内核验证。与一般逻辑等价不同，该链限制了证明器可以“自由发挥”的空间：不能引入与库中无关的辅助引理，也不能利用证明器的强自动化能力跨越语义鸿沟。因此，SemantEq捕捉的是语句在库上下文中的实质性可转换性，而非仅凭经典逻辑真值相同的宽松等价。

评估与结果

研究团队构建了SemantEq-Eval，一个无需模型的搜索方法。在ProofNetVerif测试集上，根据人工裁决的标签，SemantEq-Eval达到了100%的精确率和65.6%的召回率，而BEq+的精确率和召回率分别为95.8%和61.8%。有意思的是，将CPU时间增加8.9倍，最多只增加三对新的等价语句，表明该方法的高效性。

语言模型可以找到更多证明，但在四种提示中的两种下，对于约五分之二的非等价语句对，模型会证明两个方向。SemantEq-ProofAudit则根据关系推导出的策略审计每个模型编写的证明，在104个非等价语句对中拒绝了所有，并在最佳提示下将407个等价语句对的召回率从65.4%提升到81.1%。

精确率与召回率：在等价性检测任务中，精确率指被判定为等价的语句对中真正等价的比例，召回率指所有真正等价的语句对中被成功找出的比例。SemantEq-Eval达到100%精确率，意味着其判定的等价对全部正确，没有误报；65.6%的召回率则表明它找出了约三分之二的等价对。相比之下，BEq+精确率95.8%、召回率61.8%，说明SemantEq在保持更高准确性的同时覆盖了更多等价语句。高精确率对于验证场景尤为关键，因为误判等价可能导致形式化语句与原文含义偏离却未被发现。

分离生成与接受

SemantEq的一个重要理念是将等价证明的生成与接受分开：更强的证明器可以提高召回率，而不会改变“接受”的含义。这为形式化数学的验证提供了更稳健的框架，使得随着证明器能力的提升，验证的可靠性不会因此降低。

研究团队已开源代码和数据，地址为：https://github.com/hlxr89/SemantEq。

ProofAudit的审计机制：SemantEq-ProofAudit利用SemantEq关系对语言模型生成的等价证明进行审计。具体而言，当模型声称语句P与Q等价并给出证明时，审计器检查该证明是否能被分解为SemantEq允许的步骤链；若不能，则拒绝该证明。在104个非等价语句对上，审计器拒绝了所有模型证明，说明它有效过滤了基于证明器强大能力“作弊”的虚假等价。同时，在最佳提示下，它将407个等价语句对的召回率从65.4%提升到81.1%，表明审计机制在严格把关的同时，仍能接受模型找到的合法等价证明，从而兼顾可靠性与覆盖率。