知识卡片：SemantEq：形式化陈述的忠实双向等价性

一句话结论

SemantEq 提出一种比“逻辑等价”更严格的形式化陈述等价关系，要求陈述之间只能经由允许的推理步骤（如逻辑重排、用库内等式重写）互相转化，从而在自动形式化中更忠实地判断形式陈述是否忠实翻译了自然语言原文。

事件概述或研究问题

• 背景：陈述自动形式化（statement autoformalization）把数学从自然语言翻译到 Lean 4 等证明助手，模型已能大规模执行。
• 问题转移：随着证明器变强，正确性负担从“证明”转向“陈述”——即形式陈述是否忠实翻译其来源。
• 现有检验的缺陷：给定可信参考形式化，自然的检验是逻辑等价，但逻辑等价“证得太多”。对库能证明的任意两个陈述 $P$、$Q$，$P \leftrightarrow Q$ 都平凡成立（各自可证，再经 $P \leftrightarrow \mathrm{True} \leftrightarrow Q$ 传递）。证明器越强，越多无关陈述对通过检验。
• 已有方法：限制证明器，并检查每个证明是否引用了对方陈述。
• 本文目标：提出更原则化的等价关系 SemantEq。

方法/产品要点

• SemantEq 关系：要求每个陈述只能通过一串允许步骤转化为另一个陈述，例如逻辑重排、用库自身等式重写。
• 判定依据：程序依据 Lean 检查的证明项（proof term）而非 tactic 脚本判定证明。
• SemantEq-Eval：无模型的搜索方法，用于评估等价性。
• SemantEq-ProofAudit：按从该关系导出的策略审计每个模型书写的证明。
• 设计思想：把等价性证明的“生成”与“接受”分离，使更强的证明器能提高召回率而不改变“接受”的含义。
• 开源：代码与数据见 https://github.com/hlxr89/SemantEq

主要结果或产业意义

• 在 ProofNetVerif 测试划分、按作者裁定的标签下：
  • SemantEq-Eval（无模型搜索）：精确率 100%、召回率 65.6%；BEq+ 为 95.8% 与 61.8%。
  • CPU 时间增加 8.9 倍，最多只多出三对。
• 语言模型能找出更多证明，但在四种提示中的两种下，会对约五分之二的非等价陈述对证明出双向等价。
• SemantEq-ProofAudit：在 104 对非等价陈述中一对都不接受；在最佳提示下把 407 对等价陈述的召回率从 65.4% 提升到 81.1%。
• 产业/研究意义：为自动形式化提供更可信的验收标准，使证明器能力提升不被“平凡等价”漏洞滥用。

为什么重要

• 自动形式化的瓶颈正从“能否证明”转向“陈述是否忠实”，SemantEq 直接针对这一验收环节。
• 通过分离证明生成与验收，兼顾召回率提升与验收标准稳定，对构建可信的数学形式化流水线有参考价值。
• 与既有卡片的关系：本卡片属于基础模型/形式化推理方向的新增脉络，未与所列已有卡片（MLIP 优化器、Embodied.cpp、VLA 忠实性）重复同一事实；其中“忠实性”主题与 VLA 忠实性卡片在概念上相关，但对象与方法不同。

局限与不确定性

• 摘要未说明 SemantEq 在更大规模或更多数学领域的泛化表现，待核实。
• “允许步骤”的具体形式化定义与策略细节需查阅全文，待核实。
• 语言模型在两成提示下对非等价对证明双向等价，说明生成端仍不可靠，需依赖审计环节，待核实其在不同模型上的稳定性。
• 作者裁定标签（adjudicated labels）的构建方式与规模待核实。

可用于图书/PPT/简报的角度

• “证明器越强，验收越难”：逻辑等价检验的漏洞与 SemantEq 的修复思路。
• 自动形式化的质量保证：从证明正确性到陈述忠实性的重心转移。
• 生成与验收分离的工程原则：更强证明器提升召回率而不改变验收语义。
• 形式化数学流水线中的“证明项 vs tactic 脚本”判定差异。

原始材料

• 标题：SemantEq: Faithful Bidirectional Equivalence of Formal Statements
• arXiv ID：2610.32919v1
• 作者：Xinrui Li, Pawan Sasanka Ammanamanchi, Siddharth Bhat, Rianna Jamdar, Yongxi Lin, Stella Biderman
• 发布：2026-10-23T17:20:12Z
• 分类：cs.AI（主）、cs.LG
• 摘要页：https://arxiv.org/abs/2610.32919v1
• PDF：https://arxiv.org/pdf/2610.32919v1
• 代码与数据：https://github.com/hlxr89/SemantEq