Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Monotonic Reference-Free Refinement for Autoformalization

Lan Zhang, Marco Valentino, André Freitas

TL;DR

This work defines full-theorem autoformalization and introduces a reference-free, monotonic test-time optimization that jointly optimizes Formal Validity, Logical Preservation, Mathematical Consistency, and Formal Quality. By leveraging a masked composite objective and a lower-confidence-bound based acceptance policy, the framework combines information from theorem provers and diverse LLM judges through specialized generator roles (One-Off, FV-Repairer, Recurrent) guided by a responsiveness map. Empirical results on miniF2F and ProofNet demonstrate monotonic improvement, achieving high Formal Validity and substantial overall quality gains while showing robustness to judge noise and model biases. The approach offers a principled path toward reliable, scalable autoformalization without extensive ground-truth libraries, with potential impact on formal verification pipelines and mathematical knowledge automation.

Abstract

While statement autoformalization has advanced rapidly, full-theorem autoformalization remains largely unexplored. Existing iterative refinement methods in statement autoformalization typicall improve isolated aspects of formalization, such as syntactic correctness, but struggle to jointly optimizing multiple quality dimensions, which is critical for full-theorem autoformalization. We introduce a reference-free iterative monotonic process for full-theorem autoformalization that leverages complementary feedback from theorem provers and LLM-based judges, without access to ground-truth proofs or existing formalizations at inference time. 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 93.44% formal validity and a 78.22% overall score on miniF2F, and 44.09% formal validity and a 29.79% overall score on ProofNet.

Monotonic Reference-Free Refinement for Autoformalization

TL;DR

This work defines full-theorem autoformalization and introduces a reference-free, monotonic test-time optimization that jointly optimizes Formal Validity, Logical Preservation, Mathematical Consistency, and Formal Quality. By leveraging a masked composite objective and a lower-confidence-bound based acceptance policy, the framework combines information from theorem provers and diverse LLM judges through specialized generator roles (One-Off, FV-Repairer, Recurrent) guided by a responsiveness map. Empirical results on miniF2F and ProofNet demonstrate monotonic improvement, achieving high Formal Validity and substantial overall quality gains while showing robustness to judge noise and model biases. The approach offers a principled path toward reliable, scalable autoformalization without extensive ground-truth libraries, with potential impact on formal verification pipelines and mathematical knowledge automation.

Abstract

While statement autoformalization has advanced rapidly, full-theorem autoformalization remains largely unexplored. Existing iterative refinement methods in statement autoformalization typicall improve isolated aspects of formalization, such as syntactic correctness, but struggle to jointly optimizing multiple quality dimensions, which is critical for full-theorem autoformalization. We introduce a reference-free iterative monotonic process for full-theorem autoformalization that leverages complementary feedback from theorem provers and LLM-based judges, without access to ground-truth proofs or existing formalizations at inference time. 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 93.44% formal validity and a 78.22% overall score on miniF2F, and 44.09% formal validity and a 29.79% overall score on ProofNet.
Paper Structure (37 sections, 3 theorems, 17 equations, 6 figures, 3 tables, 2 algorithms)

This paper contains 37 sections, 3 theorems, 17 equations, 6 figures, 3 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Monotonic Test-Time Optimization for Full-Theorem Autoformalization
  3. Problem Statement
  4. Dimension Scores.
  5. Masked Composite Objective.
  6. Approximation with LLM Judges
  7. The Monotonic Optimization Process
  8. Candidate Generation
  9. One-Off Generator (OOG).
  10. FV-Repairer (FVR).
  11. Recurrent Generator (REG).
  12. The Acceptance Policy
  13. Conservative Acceptance Policy.
  14. Summary of Choice Coherence
  15. Empirical Experiments
  16. ...and 22 more sections

Key Result

Theorem 2.2

Assuming that the evaluations of LP, MC and FQ are independent, there exists a lower confidence bound for the masked composite objective $J_\mathrm{OA}(x)$ given by: with uncertainty level $\delta=1-(1-\delta_\mathrm{LP})(1-\delta_\mathrm{MC})(1-\delta_\mathrm{FQ})$.

Figures (6)

  • Figure 1: Schematic illustration of the monotonic process with a running example. In this process, One-Off Generators (OOGs) produce formalizations from scratch, Recurrent Generators (REGs) refine the current best formalization using feedback from LLM judges, and FV-Repairers (FVRs) correct formally invalid candidates generated by OOGs and REGs. The acceptance policy retains only the formalization estimated to have the highest quality among all candidates and the previous best.
  • Figure 2: Performance of the monotonic process on miniF2F and ProofNet test split. (GPT-Eval): soft-dimensions are estimated by GPT-4.1-mini judges; (Qwen-Eval): soft-dimensions are estimated by Qwen2.5-Coder-7B judges; (Mono): the monotonic process.
  • Figure 3: Performance of iterative self-refinement (ISR) using DeepSeek-Prover-V2-7B with error feedback and no acceptance policy.
  • Figure 4: Average of local responsiveness (%)for LLMs as different generators.
  • Figure 5: Average and Cohen's d of improvements using different feedback on each dataset.
  • ...and 1 more figures

Theorems & Definitions (10)

  • Theorem 2.2: Lower Confidence Bound of $J_\mathrm{OA}$
  • proof
  • Definition 2.3: Responsiveness Map
  • Theorem 2.4: Certified Monotonicity
  • proof
  • Theorem 2.5
  • proof
  • proof
  • proof
  • proof