SemantEq checks faithful Lean 4 statement equivalence
Original title: SemantEq: Faithful Bidirectional Equivalence of Formal Statements
A model-free search hits 100% precision and 65.6% recall; proof auditing accepts none of 104 non-equivalent pairs.
SemantEq defines a bidirectional equivalence for mathematical statements formalized in Lean 4, requiring each statement to become the other only through allowed steps such as logical rearrangement and library equations. Judgments use the Lean-checked proof term rather than the tactic script. SemantEq-Eval, a search without a model, reaches 100% precision and 65.6% recall on the ProofNetVerif test split under adjudicated labels, versus 95.8% and 61.8% for BEq+. SemantEq-ProofAudit accepts none of 104 non-equivalent pairs and raises recall on 407 equivalent pairs from 65.4% to 81.1% under the best prompt. Code and data are released on GitHub.
Unconfirmed: Precision and recall figures use the authors' adjudicated labels on the ProofNetVerif test split.
- SemantEq-Eval reports 100% precision and 65.6% recall on ProofNetVerif.
- BEq+ is cited at 95.8% precision and 61.8% recall on the same split.
- Under two of four prompts, a model proved both directions of about two in five non-equivalent pairs.
- ProofAudit accepts none of 104 non-equivalent pairs.
- Recall on 407 equivalent pairs rises from 65.4% to 81.1% under the best prompt.
From the original article
1 min read at arxiv.orgStatement 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.
By Xinrui Li · arxiv.org
A short excerpt; the article and its images belong to the publisher. Summary, key facts and assessment above are AI-written from the article and can be wrong.