Structure aware equivalence improves math statement evaluation accuracy
Structure-Aware Equivalence for Evaluating Autoformalized Statements
Programming Languages
Summary
Figuring out if a computer’s version of a math statement really means the same thing as the original is hard. The authors present a new way to check meaning that looks at how each part of the statement plays a role, not just if the whole thing is logically equal. Their method, called SAE, catches when math statements change meaning even if they look equivalent logically. They built a tool named ACE that uses this to confidently say if statements match or differ, doing better than previous methods in tests.
What this means in practice
- •For automated theorem proving teams: Provide finer checks for whether auto-generated mathematical statements maintain intended meaning beyond simple logical equivalence.
- •For mathematical knowledge management teams: Improve quality control in systems that transform informal math into formal statements by detecting subtle meaning changes.
Authors
Yi Yu, Yu-Hsuan Wu, Guang Lin, Yuhui Zhang, Yuxiang Peng
Abstract
Evaluating autoformalized mathematical statements requires determining whether a candidate preserves the mathematical claim intended by a trusted reference. Existing methods approach this problem from complementary directions: reference-free learned evaluators estimate semantic agreement but are not constrained to a formal equivalence relation, while reference-based proof methods typically employ whole-statement logical equivalence to provide formal certificates, which is too coarse for translation fidelity and may identify mathematically unrelated statements. We introduce Structure-Aware Equivalence (SAE), a role-preserving formal equivalence relation between syntactic and whole-statement logical equivalence that allows formally justified reformulations while preserving translation-relevant mathematical structure. We operationalize SAE in the Autoformalization Correctness Evaluator (ACE), which provides certified equivalence or inequivalence judgments and reports Inconclusive otherwise. On ProofNetVerif, a benchmark introduced with BEq+, ACE retains substantial equivalent-case coverage while remaining highly conservative in certifying disputed or inequivalent pairs. On targeted diagnostics, BEq+ accepts 94-96% of unrelated but whole-statement logically equivalent pairs, while Mathesis LeanScorer accepts 42% of localized meaning-changing perturbations; ACE accepts none of either set as equivalent.