aiqbench analysis
FormalEvolve reframes autoformalization as a budgeted test-time search problem, utilizing an archive of diverse formal statements generated via LLM-driven mutation and symbolic AST rewrites. This approach significantly improves semantic hit rates on CombiBench and ProofNet while enhancing downstream theorem proving under fixed computational budgets. The method demonstrates that structural diversity in generated formalizations is critical for efficient proof discovery, moving beyond single-output evaluation limits.
FormalEvolve: Neuro-Symbolic Evolutionary Search for Diverse Autoformalization
arXiv:2603.19828v4 Announce Type: replace Abstract: Autoformalization aims to produce formal statements that compile and faithfully preserve the intended meaning of informal mathematics. Yet standard single-output evaluation collapses this many-to-many structure into a single prediction. For downstream proving, this granularity is too coarse: a formal statement is not merely a faithful translation endpoint, but also a prover-facing interface whose structure can alter proof search under a fixed budget. We therefore recast autoformalization as budgeted test-time search: FormalEvolve maintains a compilation-feasible archive for reuse and returns a deduplicated, semantically accepted repertoire for evaluation and downstream proving. It expands the archive with LLM-driven mutation, crossover, bounded patch repair, and symbolic abstract syntax tree (AST) rewrites for structural diversity. Under a generator-call budget of T=100 with a fixed LLM semantic judge, FormalEvolve reaches SH@100 of 58.0% on CombiBench and 84.9% on ProofNet, improving over all no-archive controls while reducing the cross-problem concentration of semantic successes. Under a fixed B=64 prover budget, these repertoires improve theorem-complete proving over the matched no-archive control. Additional stronger-base statement-generation experiments show that archive-search gains persist with stronger seed and repair models.
Abstract:Autoformalization aims to produce formal statements that compile and faithfully preserve the intended meaning of informal mathematics. Yet standard single-output evaluation collapses this many-to-many structure into a single prediction. For downstream proving, this granularity is too coarse: a formal statement is not merely a faithful translation endpoint, but also a prover-facing interface whose structure can alter proof search under a fixed budget. We therefore recast autoformalization as budgeted test-time search: FormalEvolve maintains a compilation-feasible archive for reuse and returns a deduplicated, semantically accepted repertoire for evaluation and downstream proving. It expands the archive with LLM-driven mutation, crossover, bounded patch repair, and symbolic abstract syntax tree (AST) rewrites for structural diversity. Under a generator-call budget of T=100 with a fixed LLM semantic judge, FormalEvolve reaches SH@100 of 58.0% on CombiBench and 84.9% on ProofNet, improving over all no-archive controls while reducing the cross-problem concentration of semantic successes. Under a fixed B=64 prover budget, these repertoires improve theorem-complete proving over the matched no-archive control. Additional stronger-base statement-generation experiments show that archive-search gains persist with stronger seed and repair models.
29 pages, 13 figures. Accepted to Findings of EMNLP 2026. Revised camera-ready version
Artificial Intelligence (cs.AI)
arXiv:2603.19828 [cs.AI]
(or arXiv:2603.19828v4 [cs.AI] for this version)
https://doi.org/10.48550/arXiv.2603.19828 Focus to learn more arXiv-issued DOI via DataCite
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Full text under the publisher's open licence · 282 words
Related coverage
Academia is for Ambition — Alex Zhang, MIT
Latent Space · Oct 2, 2026
Shared Symbolic Backbones for Physically Consistent Multi-Output Symbolic Regression
arXiv · Jul 31, 2026
FunctionEvolve: Structure-Guided Symbolic Regression with LLMs
arXiv · Jun 9, 2026
Deliberate Evolution: Agentic Reasoning for Sample-Efficient Symbolic Regression with LLMs
arXiv · Jun 5, 2026