SemantEq ensures correct math translation between natural and formal language
SemantEq: Faithful Bidirectional Equivalence of Formal Statements
Artificial IntelligenceMachine Learning
Summary
Translating math from everyday language into a formal system that computers can verify is tricky because the computer might accept false matches as correct. The authors designed SemantEq, a method that only accepts two math statements as equivalent if one can be rigorously transformed into the other through allowed logical steps. This method catches mismatches that simpler checks miss and verifies proofs more reliably. Their approach separates proof generation from verification, improving accuracy without changing what counts as proof.
What this means in practice
- •For software engineers using proof assistants: Validate that automatically translated math statements truly match their natural language originals before using them in verification.
- •For developers building math ai tools: Audit AI-generated proofs of math statement equivalence to reduce errors in automated formalization systems.
Authors
Xinrui Li, Pawan Sasanka Ammanamanchi, Siddharth Bhat, Rianna Jamdar, Yongxi Lin, Stella Biderman
Abstract
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 principled relation that instead requires each statement to turn into the other only through a chain of allowed steps, such as logical rearrangement and rewriting with the library's own equations. Our programs judge a proof by the proof term Lean checks, not by its tactic script. SemantEq-Eval, a search without a model, reaches 100% precision and 65.6% recall on the ProofNetVerif test split under our adjudicated labels, against 95.8% and 61.8% for BEq+, and an 8.9-fold increase in its CPU time adds at most three pairs. A language model finds more proofs, but under two of four prompts it proves both directions of about two in five of the non-equivalent pairs. SemantEq-ProofAudit audits each model-written proof under a policy derived from the relation and accepts none of the 104 non-equivalent pairs, and it raises recall on 407 equivalent pairs from 65.4% to 81.1% under the best prompt. Separating the generation of equivalence proofs from their acceptance lets a stronger prover raise recall without changing what an acceptance means. We release code and data at: https://github.com/hlxr89/SemantEq