# Monotonic Reference-Free Refinement for Autoformalization

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 26 of its 42 references that are in the map.
- First posted on arXiv 30 Jan 2026.

## Builds on (most cited first, 26 of 26)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [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)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [ReACC: A Retrieval-Augmented Code Completion Framework](https://mlsanity.com/paper/2203.07722/) (2022)
- [Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad](https://mlsanity.com/paper/2503.21934/) (2025)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Seed-Coder: Let the Code Model Curate Data for Itself](https://mlsanity.com/paper/2506.03524/) (2025)
- [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://mlsanity.com/paper/2505.02735/) (2025)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning](https://mlsanity.com/paper/2505.23754/) (2025)
- [Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://mlsanity.com/paper/2502.12065/) (2025)
- [Consistent Autoformalization for Constructing Mathematical Libraries](https://mlsanity.com/paper/2410.04194/) (2024)
- [DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems](https://mlsanity.com/paper/2510.10815/) (2025)
- [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)
- [Improving Autoformalization Using Direct Dependency Retrieval](https://mlsanity.com/paper/2511.11990/) (2025)

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

- [Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization](https://mlsanity.com/paper/2607.11307/) (2026)

## Abstract (arXiv)

While statement autoformalization has advanced rapidly, full-theorem autoformalization remains largely unexplored. Existing iterative refinement methods in statement autoformalization typically improve isolated aspects of formalization, such as syntactic correctness, but struggle to jointly optimize multiple quality dimensions, which is critical for full-theorem autoformalization. We introduce a reference-free iterative monotonic process at inference time for full-theorem autoformalization that leverages complementary feedback from theorem provers and LLM-based judges, without access to ground-truth or existing formalizations and without human intervention. Our approach optimizes a masked composite objective over Formal Validity, Logical Preservation, Mathematical Consistency, and Formal Quality, guided by a responsiveness map that indicates how different LLMs acting as different roles preferentially improve each dimension. We further propose an acceptance policy that guarantees certified monotonic improvement, and provide conditions ensuring convergence and termination. Empirical experiments demonstrate the proposed process enables simultaneous improvement across multiple dimensions, achieving 100.00% formal validity and a 90.27% overall score on miniF2F, and 77.96% formal validity and a 52.45% overall score on ProofNet.