Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization

• URL: http://arxiv.org/abs/2607.11307v1
• Date: Mon, 13 Jul 2026 09:21:15 GMT
• Title: Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization
• Abstract summary: ToMap is a framework that structures proof autoformalization as a Decomposer-Formalizer-Prover pipeline.<n>We show that ToMap improves over the best previous method by 19.0% when evaluated by both syntactic correctness and semantic faithfulness.
• Score: 20.22828310618122
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• From Verdict to Process: Agentic Reinforcement Learning for Multi-Stage Fact Verification [4.539896456749749]
  We propose ProFact, an agentic reinforcement learning framework for end-to-end optimization of multi-stage fact verification trajectories.<n>ProFact trains a unified policy to coordinate claim decomposition, evidence seeking, answer generation, and verdict prediction.<n> Empirical evaluation shows that ProFact consistently outperforms strong baselines in both verification performance and inference efficiency.
  arXiv  Detail & Related papers  (2026-06-11T12:17:18Z)
• Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries [18.744562922743405]
  PRoSFI (Process Reward over Structured Formal Intermediates) is a novel reward method that enhances reasoning reliability without compromising accuracy.<n>Only fully validated reasoning chains receive high rewards.<n>The integration of formal verification guides the model towards generating step-by-step machine-checkable proofs.
  arXiv  Detail & Related papers  (2026-03-31T09:42:13Z)
• Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
  Large language models (LLMs) have demonstrated significant potential in formal theorem proving.<n>We exploit an informative structure in formal verification: the observation that compilers map a vast space of diverse proof attempts.<n>We introduce a learning-to-refine framework that leverages this compression to perform efficient learning and proof exploration.
  arXiv  Detail & Related papers  (2026-03-13T01:33:20Z)
• Decompose-and-Formalise: Recursively Verifiable Natural Language Inference [34.505373718498014]
  Large language models (LLMs) with theorem provers (TPs) in neuro-symbolic pipelines helps with entailment verification and proof-guided refinement of explanations for natural language inference (NLI)<n>We propose a decompose-and-formalise framework that decomposes premise-hypothesis pairs into an entailment tree of atomic steps.<n>We also introduce $$-substitution in an event-based logical form to enforce consistent argument-role bindings.
  arXiv  Detail & Related papers  (2026-01-27T13:43:30Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Provable Benefit of Curriculum in Transformer Tree-Reasoning Post-Training [76.12556589212666]
  We show that curriculum post-training avoids the exponential complexity bottleneck.<n>Under outcome-only reward signals, reinforcement learning finetuning achieves high accuracy with sample complexity.<n>We establish guarantees for test-time scaling, where curriculum-aware querying reduces both reward oracle calls and sampling cost from exponential to order.
  arXiv  Detail & Related papers  (2025-11-10T18:29:54Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)
• ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization [10.021930888250546]
  Current approaches fail to preserve semantic meaning and logical structure of the original human-written argument.<n>We introduce ProofFlow, a novel pipeline that treats structural fidelity as a primary objective.<n>We present a new benchmark of 184 undergraduate-level problems, manually annotated with step-by-step solutions.<n>We also introduce ProofScore, a new composite metric to evaluate syntactic correctness, semantic faithfulness, and structural fidelity.
  arXiv  Detail & Related papers  (2025-10-13T10:20:11Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  Autoformalization addresses the scarcity of data for Automated Theorem Proving (ATP) by translating mathematical problems from natural language into formal statements.<n>Existing formalizer still struggles to consistently generate valid statements that meet syntactic validity and semantic consistency.<n>We propose the Autoformalizer with Tool Feedback (ATF), a novel approach that incorporates syntactic and consistency information as tools into the formalization process.
  arXiv  Detail & Related papers  (2025-10-08T10:25:12Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  This work proposes Alchemy, a framework for data synthesis that constructs formal theorems through symbolic mutation.<n>For each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it.<n>As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M.
  arXiv  Detail & Related papers  (2024-10-21T08:04:21Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.