Monotonic Reference-Free Refinement for Autoformalization

TL;DR

This paper introduces a novel reference-free iterative refinement method for full-theorem autoformalization, leveraging feedback from theorem provers and LLMs to improve multiple quality dimensions simultaneously.

Contribution

It proposes a monotonic inference process that guarantees improvement across multiple formalization quality metrics without human intervention.

Findings

Achieves 100% formal validity on miniF2F

Attains 90.27% overall score on miniF2F

Achieves 77.96% formal validity on ProofNet

Abstract

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.