# FormalAlign: Automated Alignment Evaluation for Autoformalization

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

## Key facts

- Cited by 24 papers in the map (data through 14 Oct 2026).
- Builds on 39 of its 61 references that are in the map.
- First posted on arXiv 14 Oct 2024.

## Builds on (most cited first, 30 of 39)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [BERTScore: Evaluating Text Generation with BERT](https://mlsanity.com/paper/1904.09675/) (2019)
- [Mistral 7B](https://mlsanity.com/paper/2310.06825/) (2023)
- [G-Eval: NLG Evaluation using GPT-4 with Better Human Alignment](https://mlsanity.com/paper/2303.16634/) (2023)
- [Microsoft COCO Captions: Data Collection and Evaluation Server](https://mlsanity.com/paper/1504.00325/) (2015)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [Don't Give Me the Details, Just the Summary! Topic-Aware Convolutional Neural Networks for Extreme Summarization](https://mlsanity.com/paper/1808.08745/) (2018)
- [Get To The Point: Summarization with Pointer-Generator Networks](https://mlsanity.com/paper/1704.04368/) (2017)
- [ChatEval: Towards Better LLM-based Evaluators through Multi-Agent Debate](https://mlsanity.com/paper/2308.07201/) (2023)
- [BARTScore: Evaluating Generated Text as Text Generation](https://mlsanity.com/paper/2106.11520/) (2021)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [PandaLM: An Automatic Evaluation Benchmark for LLM Instruction Tuning Optimization](https://mlsanity.com/paper/2306.05087/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Aligning with Human Judgement: The Role of Pairwise Preference in Large Language Model Evaluators](https://mlsanity.com/paper/2403.16950/) (2024)
- [UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression](https://mlsanity.com/paper/2212.02746/) (2022)
- [Skywork: A More Open Bilingual Foundation Model](https://mlsanity.com/paper/2310.19341/) (2023)
- [TrueTeacher: Learning Factual Consistency Evaluation with Large Language Models](https://mlsanity.com/paper/2305.11171/) (2023)
- [Automatic Evaluation of Attribution by Large Language Models](https://mlsanity.com/paper/2305.06311/) (2023)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [FIMO: A Challenge Formal Dataset for Automated Theorem Proving](https://mlsanity.com/paper/2309.04295/) (2023)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data](https://mlsanity.com/paper/2402.08957/) (2024)
- [Multilingual Mathematical Autoformalization](https://mlsanity.com/paper/2311.03755/) (2023)

## Built on by (most cited first, 24 of 24)

- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (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)
- [Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization](https://mlsanity.com/paper/2606.31002/) (2026)
- [Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving](https://mlsanity.com/paper/2606.29493/) (2026)
- [Towards a Common Framework for Autoformalization](https://mlsanity.com/paper/2509.09810/) (2025)
- [Uncovering Hidden Correctness in LLM Causal Reasoning via Symbolic Verification](https://mlsanity.com/paper/2601.21210/) (2026)
- [MathAtlas: A Benchmark for Autoformalization in the Wild](https://mlsanity.com/paper/2605.14061/) (2026)
- [FormalRx: Rectify and eXamine Semantic Failures in Autoformalization](https://mlsanity.com/paper/2607.04655/) (2026)
- [Translating Informal Proofs into Formal Proofs Using a Chain of States](https://mlsanity.com/paper/2512.10317/) (2025)
- [Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs](https://mlsanity.com/paper/2608.15432/) (2026)
- [KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment](https://mlsanity.com/paper/2507.08665/) (2025)
- [Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization](https://mlsanity.com/paper/2604.16347/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference](https://mlsanity.com/paper/2607.22511/) (2026)
- [Beyond Solver Verdicts: Generative Reward Models for Autoformalization](https://mlsanity.com/paper/2609.11085/) (2026)
- [ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization](https://mlsanity.com/paper/2609.34960/) (2026)
- [Sage: Formalization with Semantic Correction](https://mlsanity.com/paper/2609.35790/) (2026)
- [Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization](https://mlsanity.com/paper/2609.39228/) (2026)
- [AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness](https://mlsanity.com/paper/2610.05367/) (2026)
- [SpecGuard: Proving a Task Is Broken Before the Agent Cheats](https://mlsanity.com/paper/2610.09159/) (2026)
- [claimcheck: Measuring and Improving Specification Faithfulness](https://mlsanity.com/paper/2610.17358/) (2026)
- [Aligning Faithfulness for Theory-Scale Autoformalization](https://mlsanity.com/paper/2610.18498/) (2026)
- [Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization](https://mlsanity.com/paper/2610.20573/) (2026)

## Abstract (arXiv)

Autoformalization aims to convert informal mathematical proofs into machine-verifiable formats, bridging the gap between natural and formal languages. However, ensuring semantic alignment between the informal and formalized statements remains challenging. Existing approaches heavily rely on manual verification, hindering scalability. To address this, we introduce textscFormalAlign, the first automated framework designed for evaluating the alignment between natural and formal languages in autoformalization. textscFormalAlign trains on both the autoformalization sequence generation task and the representational alignment between input and output, employing a dual loss that combines a pair of mutually enhancing autoformalization and alignment tasks. Evaluated across four benchmarks augmented by our proposed misalignment strategies, textscFormalAlign demonstrates superior performance. In our experiments, textscFormalAlign outperforms GPT-4, achieving an Alignment-Selection Score 11.58% higher on forml-Basic (99.21% vs. 88.91%) and 3.19% higher on MiniF2F-Valid (66.39% vs. 64.34%). This effective alignment evaluation significantly reduces the need for manual verification. Both the dataset and code can be accessed via~urlhttps://github.com/rookie-joe/FormalAlign.