SemantEq: Faithful Bidirectional Equivalence of Formal Statements
Statement autoformalization translates mathematics from natural language into a proof assistant such as Lean 4, and models now do it at scale. As provers get stronger, the burden of correctness shifts from the proof to the statement, that is, to whether the formal statement faithfully translates its source. Given a trusted reference formalization, the natural test is logical equivalence, and it proves too much. $P \leftrightarrow Q$ holds trivially for any two statements $P$ and $Q$ that the library proves, because a prover can prove each separately and pass through $P \leftrightarrow \mathrm{True} \leftrightarrow Q$. The stronger the prover, the more unrelated pairs pass. Earlier methods restrict the prover and check that each proof names the other statement. We introduce SemantEq, a more
提出 SemantEq 模型，提高形式化语句间的双向等价性。
- 核心方法
- 通过引入 SemantEq 模型，使用逻辑等价测试但限制证明工具的能力，确保形式化语句忠实于自然语言来源。
- 适合谁读
- 研究者 / 工程师
- 要解决的问题
- 当证明工具变得更强大时，形式化语句的正确性验证从证明转移到语句本身的忠实性转换。
- 关键实验
- 未提供具体实验数据，但描述了方法的有效性验证过程。
- 主要贡献
- 提供了一个有效的方法来验证形式化语句的忠实性，避免了传统方法中因证明工具太强而造成的误判。
- 意义与局限
- 提高了数学语句自动形式化过程的可靠性和准确性，但可能受限于当前证明工具的能力。