# Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization arXiv: https://arxiv.org/abs/2607.11307 ยท HTML: https://mlsanity.com/paper/2607.11307/ ## Key facts - Cited by 2 papers in the map (data through 14 Oct 2026). - Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. - Builds on 32 of its 36 references that are in the map. - First posted on arXiv 13 Jul 2026. ## Placed in - LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/) ## Builds on (most cited first, 30 of 32) - [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023) - [Qwen2.5 Technical Report](https://mlsanity.com/paper/2412.15115/) (2024) - [Reflexion: Language Agents with Verbal Reinforcement Learning](https://mlsanity.com/paper/2303.11366/) (2023) - [MetaGPT: Meta Programming for A Multi-Agent Collaborative Framework](https://mlsanity.com/paper/2308.00352/) (2023) - [CAMEL: Communicative Agents for "Mind" Exploration of Large Language Model Society](https://mlsanity.com/paper/2303.17760/) (2023) - [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022) - [Large Language Models Are Human-Level Prompt Engineers](https://mlsanity.com/paper/2211.01910/) (2022) - [Large Language Models as Optimizers](https://mlsanity.com/paper/2309.03409/) (2023) - [Promptbreeder: Self-Referential Self-Improvement Via Prompt Evolution](https://mlsanity.com/paper/2309.16797/) (2023) - [GEPA: Reflective Prompt Evolution Can Outperform Reinforcement Learning](https://mlsanity.com/paper/2507.19457/) (2025) - [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021) - [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023) - [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022) - [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025) - [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022) - [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025) - [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025) - [A Survey on Large Language Models for Mathematical Reasoning](https://mlsanity.com/paper/2506.08446/) (2025) - [Seed-Coder: Let the Code Model Curate Data for Itself](https://mlsanity.com/paper/2506.03524/) (2025) - [Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience](https://mlsanity.com/paper/2512.17260/) (2025) - [A Survey of Progress on Cooperative Multi-agent Reinforcement Learning in Open Environment](https://mlsanity.com/paper/2312.01058/) (2023) - [Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs](https://mlsanity.com/paper/2506.19923/) (2025) - [The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs](https://mlsanity.com/paper/2506.21621/) (2025) - [Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically](https://mlsanity.com/paper/2411.01829/) (2024) - [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025) - [ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization](https://mlsanity.com/paper/2510.24592/) (2025) - [ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings](https://mlsanity.com/paper/2510.15681/) (2025) - [M2F: Automated Formalization of Mathematical Literature at Scale](https://mlsanity.com/paper/2602.17016/) (2026) - [WHALE: Towards Generalizable and Scalable World Models for Embodied Decision-making](https://mlsanity.com/paper/2411.05619/) (2024) - [Monotonic Reference-Free Refinement for Autoformalization](https://mlsanity.com/paper/2601.23166/) (2026) ## Built on by (most cited first, 2 of 2) - [VALG: An Agentic System for ML Theory Research](https://mlsanity.com/paper/2608.13060/) (2026) - [AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness](https://mlsanity.com/paper/2610.05367/) (2026) ## Abstract (arXiv) Full-proof autoformalization bridges extensive mathematical proofs in natural language with formally validated reasoning, offering a pathway to elevate the ceiling of verifiable mathematical reasoning. Unlike statement-level formalization, proof autoformalization is a long-horizon challenge requiring coordination of claims, contexts, and dependencies across many proof steps, yet has only recently come under focused study. Current approaches either rely on costly model training or apply excessive, unguided repair at inference time. To this end, we introduce ToMap, a multi-agent framework that structures proof autoformalization as a Decomposer-Formalizer-Prover pipeline with efficient test-time optimization guided by formal verification and semantic rubrics for proof quality. Rather than distributing test-time compute across all agents, we perform bottleneck analysis and identify the Decomposer as the critical bottleneck: the quality of its atomic, self-contained proof units directly determines whether downstream agents can successfully formalize and prove each step. ToMap therefore treats the Formalizer and Prover as downstream executors and efficiently focuses test-time compute on Decomposer refinement. This refinement follows a loop inspired by GEPA, evolving prompts over candidate decompositions and using formal verification progress together with semantic proof rubrics to define a Pareto frontier that guides the next decomposition update. Experiments on ProofFlowBench show that ToMap improves over the best previous method by 19.0% when evaluated by both syntactic correctness and semantic faithfulness, while requiring lower test-time cost. Scaling analysis shows that most gains emerge within a few iterations of decomposition evolution, guiding test-time budget selection.