# Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 20 of its 28 references that are in the map.
- First posted on arXiv 8 Jun 2026.

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

- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [Reflexion: Language Agents with Verbal Reinforcement Learning](https://mlsanity.com/paper/2303.11366/) (2023)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [Constitutional AI: Harmlessness from AI Feedback](https://mlsanity.com/paper/2212.08073/) (2022)
- [Optimization Methods for Large-Scale Machine Learning](https://mlsanity.com/paper/1606.04838/) (2016)
- [Solving math word problems with process- and outcome-based feedback](https://mlsanity.com/paper/2211.14275/) (2022)
- [e-SNLI: Natural Language Inference with Natural Language Explanations](https://mlsanity.com/paper/1812.01193/) (2018)
- [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)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought](https://mlsanity.com/paper/2210.01240/) (2022)
- [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)
- [Do Natural Language Explanations Represent Valid Logical Arguments? Verifying Entailment in Explainable NLI Gold Standards](https://mlsanity.com/paper/2105.01974/) (2021)
- [Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations](https://mlsanity.com/paper/2505.24264/) (2025)
- [Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning](https://mlsanity.com/paper/2506.10903/) (2025)
- [The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee](https://mlsanity.com/paper/2512.02080/) (2025)

## Abstract (arXiv)

Autoformalization (AF) requires both prover acceptance and fidelity to an informal source, but prover acceptance alone cannot establish fidelity, and expert-validated reference formalizations are costly to obtain. We introduce a reference-free proxy-judge framework, which separates correctness into grounding, statement faithfulness, coverage, and inference, and a theory of how imperfect checks shape iterative refinement. We establish three results. First, for a fixed sequence of candidates, an added proxy's false-positive and false-negative rates bound its effect on the pass-but-wrong rate. Second, damage to a correct formalization requires a false rejection that exposes it to further refinement, and harmful revisions are then retained through unguarded changes, missed changes, or prover progress that overrides judge warnings. Third, a decomposition of the final pass rate distinguishes continued refinement, generation of new candidates, and their success in passing the checks. We instantiate the framework with eight proxies and test these predictions on ProofNet and miniF2F in Lean~4 and on e-SNLI and ProntoQA in Isabelle/HOL. Under single-proxy removal, no prediction written before the runs is contradicted, and all traced breaks follow the identified failure routes. The results connect proxy reliability to the benefits, risks, and limits of refinement without reference formalizations.