Reproduce “Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Tian-Shuo Liu, Shiyuan Zhang, Zijie Geng, Haoyu Liu, Runjie Xu, Pengyuan Wang, Lei Yuan, Yang Yu
The TOMAP framework addresses full-proof autoformalization by optimizing natural-language proof decomposition within a multi-agent LLM pipeline, demonstrating enhanced end-to-end Lean verification success and semantic faithfulness. This method achieved up to a 19.0% absolute improvement in combined syntactic correctness and semantic faithfulness on benchmarks like PROOFFLOWBENCH compared to previous approaches.
Key insights
- The quality of natural-language proof decomposition is a primary determinant of success for downstream formalization and proving in multi-agent autoformalization pipelines.
- Decomposing test-time optimization by using cheap, dense LLM-based rubric feedback to guide the search for better initial representations is more efficient than relying solely on expensive, sparse formal verifier feedback.
- A Pareto-guided evolutionary strategy combined with verification gating effectively balances solution quality improvement with computational cost in iterative optimization.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.