# Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency

arXiv: https://arxiv.org/abs/2410.20936 · HTML: https://mlsanity.com/paper/2410.20936/

## Key facts

- Cited by 41 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Oct 2024.

## Built on by (most cited first, 30 of 41)

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://mlsanity.com/paper/2502.12065/) (2025)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [Theorem Prover as a Judge for Synthetic Data Generation](https://mlsanity.com/paper/2502.13137/) (2025)
- [miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward](https://mlsanity.com/paper/2511.03108/) (2025)
- [Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization](https://mlsanity.com/paper/2507.07399/) (2025)
- [ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity](https://mlsanity.com/paper/2509.22246/) (2025)
- [MerLean: An Agentic Framework for Autoformalization in Quantum Computation](https://mlsanity.com/paper/2602.16554/) (2026)
- [Faithful Autoformalization via Roundtrip Verification and Repair](https://mlsanity.com/paper/2604.25031/) (2026)
- [Towards a Common Framework for Autoformalization](https://mlsanity.com/paper/2509.09810/) (2025)
- [Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning](https://mlsanity.com/paper/2506.10903/) (2025)
- [MASA: LLM-Driven Multi-Agent Systems for Autoformalization](https://mlsanity.com/paper/2510.08988/) (2025)
- [Automated Formalization via Conceptual Retrieval-Augmented LLMs](https://mlsanity.com/paper/2508.06931/) (2025)
- [OpInf-LLM: Parametric PDE Solving with LLMs via Operator Inference](https://mlsanity.com/paper/2602.01493/) (2026)
- [Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance](https://mlsanity.com/paper/2606.14000/) (2026)
- [LeanTutor: Towards a Verified AI Mathematical Proof Tutor](https://mlsanity.com/paper/2506.08321/) (2025)
- [FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean](https://mlsanity.com/paper/2604.23002/) (2026)
- [Theory-Scale Auto-Formalization of Logics for Computer Science](https://mlsanity.com/paper/2606.26525/) (2026)
- [Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs](https://mlsanity.com/paper/2508.15878/) (2025)
- [A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants](https://mlsanity.com/paper/2508.18587/) (2025)
- [Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs](https://mlsanity.com/paper/2507.04719/) (2025)
- [Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure](https://mlsanity.com/paper/2509.09726/) (2025)
- [Can Large Language Models Autoformalize Kinematics?](https://mlsanity.com/paper/2509.21840/) (2025)
- [Monotonic Reference-Free Refinement for Autoformalization](https://mlsanity.com/paper/2601.23166/) (2026)
- [Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory](https://mlsanity.com/paper/2606.20642/) (2026)
- [ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers](https://mlsanity.com/paper/2607.19407/) (2026)
- [CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference](https://mlsanity.com/paper/2607.22511/) (2026)
- [TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition](https://mlsanity.com/paper/2510.11944/) (2025)
- [Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification](https://mlsanity.com/paper/2511.00202/) (2025)

## Abstract (arXiv)

Autoformalization, the task of automatically translating natural language descriptions into a formal language, poses a significant challenge across various domains, especially in mathematics. Recent advancements in large language models (LLMs) have unveiled their promising capabilities to formalize even competition-level math problems. However, we observe a considerable discrepancy between pass@1 and pass@k accuracies in LLM-generated formalizations. To address this gap, we introduce a novel framework that scores and selects the best result from k autoformalization candidates based on two complementary self-consistency methods: symbolic equivalence and semantic consistency. Elaborately, symbolic equivalence identifies the logical homogeneity among autoformalization candidates using automated theorem provers, and semantic consistency evaluates the preservation of the original meaning by informalizing the candidates and computing the similarity between the embeddings of the original and informalized texts. Our extensive experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy, achieving up to 0.22-1.35x relative improvements across various LLMs and baseline methods.