# Aligning Faithfulness for Theory-Scale Autoformalization

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 45 of its 57 references that are in the map.
- First posted on arXiv 13 Oct 2026.

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

- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [Language Models (Mostly) Know What They Know](https://mlsanity.com/paper/2207.05221/) (2022)
- [Know What You Don't Know: Unanswerable Questions for SQuAD](https://mlsanity.com/paper/1806.03822/) (2018)
- [FEVER: a large-scale dataset for Fact Extraction and VERification](https://mlsanity.com/paper/1803.05355/) (2018)
- [FActScore: Fine-grained Atomic Evaluation of Factual Precision in Long Form Text Generation](https://mlsanity.com/paper/2305.14251/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [AmbigQA: Answering Ambiguous Open-domain Questions](https://mlsanity.com/paper/2004.10645/) (2020)
- [ProcessBench: Identifying Process Errors in Mathematical Reasoning](https://mlsanity.com/paper/2412.06559/) (2024)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Understanding Factuality in Abstractive Summarization with FRANK: A Benchmark for Factuality Metrics](https://mlsanity.com/paper/2104.13346/) (2021)
- [RAGTruth: A Hallucination Corpus for Developing Trustworthy Retrieval-Augmented Language Models](https://mlsanity.com/paper/2401.00396/) (2023)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [SimAlign: High Quality Word Alignments without Parallel Training Data using Static and Contextualized Embeddings](https://mlsanity.com/paper/2004.08728/) (2020)
- [Fine-grained Hallucination Detection and Editing for Language Models](https://mlsanity.com/paper/2401.06855/) (2024)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [We're Afraid Language Models Aren't Modeling Ambiguity](https://mlsanity.com/paper/2304.14399/) (2023)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Know Your Limits: A Survey of Abstention in Large Language Models](https://mlsanity.com/paper/2407.18418/) (2024)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://mlsanity.com/paper/2403.18120/) (2024)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [Benchmarking and Improving Text-to-SQL Generation under Ambiguity](https://mlsanity.com/paper/2310.13659/) (2023)
- [Reliable Evaluation and Benchmarks for Statement Autoformalization](https://mlsanity.com/paper/2406.07222/) (2024)
- [FormalAlign: Automated Alignment Evaluation for Autoformalization](https://mlsanity.com/paper/2410.10135/) (2024)
- [Consistent Autoformalization for Constructing Mathematical Libraries](https://mlsanity.com/paper/2410.04194/) (2024)
- [Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph](https://mlsanity.com/paper/2510.04520/) (2025)
- [ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization](https://mlsanity.com/paper/2510.24592/) (2025)

## Abstract (arXiv)

Autoformalization (AF) requires more than compilation: formal statements must preserve the meaning of their informal sources, a property known as faithfulness. An emerging frontier is the automated evaluation of this property, yet most existing methods operate at the statement level and produce whole-item verdicts, failing to reveal how individual expressions correspond or which contextual interpretations support the judgment. This omission is consequential because AF is inherently theory-scale: target statements derive their meaning from surrounding mathematical material and unstated conventions. We formulate faithfulness evaluation as a context-aware align-then-label problem: identifying phrase-level correspondences between informal and formal statements and assigning a faithfulness label to each under explicitly specified contextual interpretations and assumptions. We also introduce FaithAlign, the first theory-scale faithfulness benchmark comprising 460 items and 4,982 annotated phrase-level links, alongside FaithAlign-Gap, a companion set of 146 items with informal context and assumptions withheld. Each FaithAlign item includes the target statement pair, relevant context, formal dependencies, and, where needed, assumptions specifying one given interpretation. Across 8 models, GPT-6 Astra achieves the highest defect F1 at 47.8% and identifies all defects in only 4.5% of items with two or more defects. On FaithAlign-Gap, Astra identifies only 28.2% of undecidable items as such. These results show the difficulty of recovering context-dependent correspondences, establishing FaithAlign as a testbed for fine-grained, context-aware faithfulness evaluation.