EFFICIENT TEST-TIME OPTIMIZATION FOR MULTI-AGENT PROOF AUTOFORMALIZATION

Full-proof autoformalization aims to translate entire natural-language mathematical proofs into formal, machine-verifiable Lean code. Unlike statement-level formalization, this is a long-horizon task requiring the coordination of complex dependencies and intermediate claims. The authors investigate how to perform efficient test-time optimization in a multi-agent pipeline to maximize verification success without relying on costly model retraining or unguided, trial-and-error repair.

The authors propose ToMap, a multi-agent framework consisting of a Decomposer, a Formalizer, and a Prover. Through a bottleneck analysis, they identify the Decomposer as the critical stage: the quality of its atomic, self-contained proof units dictates the success of all downstream agents. ToMap optimizes this stage by maintaining a pool of candidate decompositions and iteratively evolving them using a reflective loop. This loop is guided by cheap, dense rubric scores (measuring semantic faithfulness, atomicity, and Lean-friendliness) rather than expensive Lean verification. A Pareto frontier of these scores determines which candidates are refined, and only those meeting a specific quality threshold are passed to the downstream Formalizer and Prover for final verification.

ToMap significantly outperforms existing methods, achieving a 19.0% improvement on the ProofFlowBench dataset in terms of combined syntactic correctness and semantic faithfulness. The bottleneck analysis confirms that revising the Decomposer's output yields higher end-to-end verification gains compared to revising the Formalizer or Prover. Furthermore, the authors demonstrate that most performance gains occur within a few iterations of decomposition evolution, allowing for an efficient allocation of the test-time budget.