Monotonic Reference-Free Refinement for Autoformalization

While statement autoformalization has advanced rapidly, full-theorem autoformalization remains largely unexplored. Existing iterative refinement methods for statement autoformalization typically improve isolated aspects of formalization quality, such as syntactic correctness, but struggle to jointly optimize multiple dimensions of quality, a key requirement for full-theorem autoformalization. We introduce a reference-free iterative monotonic process for full-theorem autoformalization at inference time that leverages complementary feedback from theorem provers and LLM-based judges, without access to existing formalizations or human intervention. Our approach optimizes a masked composite objective over a hard dimension, formal validity as determined by a theorem prover, and a set of soft dimensions. We introduce an acceptance policy over candidate formalizations that provides a certified notion of monotonic progress, ensuring at each iteration that either the true objective does not decrease or its lower confidence bound increases, while establishing conditions for convergence and termination. We also propose a responsiveness map that characterizes how different LLMs, acting in different roles, preferentially improve these dimensions, enabling principled generator selection. Experiments show that our method simultaneously improves multiple dimensions of formalization quality, achieving overall scores of 90.27% on miniF2F and 52.45% on ProofNet.