Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization¶

🕒 Published (v1): 2026-07-13 09:21 UTC · Source: Arxiv · link

Why this paper was selected

Multi-agent proof autoformalization with test-time optimization; novel orchestration for formal reasoning

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

TL;DR¶

TOMAP is a multi-agent framework for full-proof autoformalization (informal math proofs → Lean 4) that structures the task as a Decomposer–Formalizer–Prover pipeline and concentrates test-time compute on the Decomposer, which a causal bottleneck analysis identifies as the highest-leverage stage. It uses a GEPA-style Pareto-guided evolution loop with cheap LLM rubric feedback to refine decompositions, gating expensive Lean verification calls for only the most promising candidates. On ProofFlowBench it improves SC∧SF by 19.0% over the best prior method at lower wall-clock cost.

Problem¶

Full-proof autoformalization is a long-horizon task requiring coordinated translation of claims, dependencies, and side conditions across many proof steps. Existing training-based methods are costly, while training-free inference-time approaches apply unguided repair: Lean verifier feedback arrives only after a full generation chain, yields a binary pass/fail signal, and does not reveal which upstream stage caused failure. This makes efficient allocation of test-time compute an open problem.

Method¶

The pipeline is formalized as $\Psi_\theta = P_{\theta_P} \circ F_{\theta_F} \circ D_{\theta_D}$, where $D$ decomposes the informal proof into atomic proof units $n_i = (q_i, u_i, a_i, d_i, \kappa_i)$, $F$ formalizes each into a Lean statement, and $P$ closes each goal with tactics. The Lean verifier $V$ is external.

Bottleneck analysis. Three matched-intervention conditions (D-Intervene, F-Intervene, P-Intervene) each receive the same Lean diagnostic trace and identical correction budget, varying only which stage is editable. D-Intervene reaches 51.1% full-proof accuracy at pass 5 vs. 45.1% (F) and 33.7% (P), confirming the Decomposer as the critical bottleneck.

TOMAP optimization loop. Each candidate decomposition $z$ is scored by a three-dimensional rubric vector $$\rho(z) = \bigl(\rho_\text{faithful}(z),\; \rho_\text{provable}(z),\; \rho_\text{Leanfriendly}(z)\bigr) \in [0,1]^3$$ evaluated by an LLM judge. A candidate pool $Z_t$ of size $K$ is maintained; the Pareto frontier $\mathcal{F}_t = \{z \in Z_t \mid \nexists\, z' \text{ s.t. } \rho(z') \succ \rho(z)\}$ selects parents. A reflective LLM proposer generates critiques and revised decompositions, updating the pool by discarding dominated candidates. A candidate is committed to the downstream Formalizer–Prover executor only when $\min_{j \in R} \rho_j(z) \geq \epsilon$; otherwise the GEPA loop continues. The Formalizer and Prover parameters $\theta_F, \theta_P$ are frozen throughout.

Key Contributions¶

Causal bottleneck analysis via matched stage-intervention experiments, identifying decomposition quality as the dominant failure mode in multi-agent proof pipelines.
TOMAP: a two-level test-time optimizer that decouples cheap Pareto-guided decomposition search from expensive Lean verification, concentrating budget where recoverability is highest.
Multi-objective rubric scoring (semantic faithfulness, provability, Lean-friendliness) providing dense proxy feedback without executing the full pipeline.
Verification gate ($\min_j \rho_j(z) \geq \epsilon$) that reserves Lean calls for candidates meeting all quality criteria, rather than retrying uniformly.
Scaling analysis showing most gains emerge within a few decomposition-evolution iterations, providing practical budget-selection guidance.

Results¶

ProofFlowBench (184 problems, undergraduate level):
TOMAP-Gemini: SC = 63.59%, SF = 51.09%, SC∧SF = 40.22% (+19.0 pp over best prior method PROOFFLOW at 15.76%)
TOMAP-Qwen30B: SC = 66.30%, SF = 27.71%, SC∧SF = 21.10%
TOMAP-Gemini wall-clock: 850.27 s/problem vs. PROOFFLOW 2348.48 s/problem
miniF2F (244 problems, competition level):
TOMAP-Gemini: SC = 82.79%, SF = 63.93%, SC∧SF = 55.74% (+8.2 pp over PROOFFLOW at 47.54%)
Bottleneck analysis: D-Intervene 51.1% vs. F-Intervene 45.1% vs. P-Intervene 33.7% at pass 5 on 184 samples (baseline 29.9%).
Training-based ProofBridge (ProofFlowBench): SC = 92.93%, SC∧SF = 9.24% — high syntactic pass rate but poor semantic faithfulness.

Limitations¶

Rubric scores are LLM-as-judge proxies (Qwen3-235B-A22B), not ground-truth verifiability measures; rubric–Lean alignment is assumed but not formally bounded.
Budget comparison across baselines is approximate due to heterogeneous pipeline structures, parallelism, and prompt lengths.
Gate threshold $\epsilon = 1$ (all rubric dimensions at maximum) is strict; suboptimal settings are only briefly explored via ablation.
Evaluation is Lean 4-specific; generalization to other proof assistants (Isabelle, Coq) is not demonstrated.
Proof-unit decomposition granularity is controlled by natural-language rubrics, not by a formal notion of atomicity.
The paper text available is truncated, so any limitations stated in later sections may be missing here.

Relevance to Harnesses / Meta-Harnesses¶

TOMAP is a concrete implementation of a meta-harness pattern: an outer optimization loop that governs when and how to invoke an inner agent pipeline, treating the Formalizer–Prover–Verifier chain as a black-box executor. The two-level design — cheap proxy evaluation driving the bulk of the search, with expensive oracle calls gated by quality thresholds — is the canonical harness efficiency heuristic (proxy-first, oracle-second). The bottleneck-analysis methodology (matched stage-intervention under fixed budget) is a generalizable framework for diagnosing where to invest test-time compute in any multi-stage agent harness, not just proof pipelines. The GEPA-style prompt evolution loop, with Pareto-frontier selection and reflective proposal, provides a reusable meta-harness template applicable to any task where a decomposition or planning stage precedes expensive downstream execution.