HUNYUANPROVER: Een Schaalbaar Gegevenssynthesekader en Begeleide Boomzoekopdracht voor Geautomatiseerd Stellingbewijs

HUNYUANPROVER: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving

December 30, 2024

Auteurs: Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, Haitao Mi

cs.AI

Samenvatting

We introduceren HunyuanProver, een taalmodel dat is gefinetuned vanuit de Hunyuan 7B voor interactief automatisch stellingen bewijzen met LEAN4. Om het probleem van data-schaarste te verlichten, hebben we een schaalbaar kader ontworpen om iteratief data te synthetiseren met lage kosten. Bovendien zijn begeleide boomzoekalgoritmes ontworpen om effectief "systeem 2 denken" van de bewijzer mogelijk te maken. HunyuanProver behaalt state-of-the-art (SOTA) prestaties op belangrijke benchmarks. Specifiek behaalt het een slagingspercentage van 68,4% op de miniF2F-test in vergelijking met 65,9%, de huidige SOTA-resultaten. Het bewijst 4 IMO-verklaringen (imo_1960_p2, imo_1962_p2, imo_1964_p2 en imo_1983_p6) in de miniF2F-test. Om de gemeenschap ten goede te komen, zullen we een dataset van 30k gesynthetiseerde gevallen open-source maken, waarbij elk geval de oorspronkelijke vraag in natuurlijke taal bevat, de omgezette verklaring door autoformalisering, en het bewijs door HunyuanProver.

English

We introduce HunyuanProver, an language model finetuned from the Hunyuan 7B for interactive automatic theorem proving with LEAN4. To alleviate the data sparsity issue, we design a scalable framework to iterative synthesize data with low cost. Besides, guided tree search algorithms are designed to enable effective ``system 2 thinking`` of the prover. HunyuanProver achieves state-of-the-art (SOTA) performances on major benchmarks. Specifically, it achieves a pass of 68.4% on the miniF2F-test compared to 65.9%, the current SOTA results. It proves 4 IMO statements (imo_1960_p2, imo_1962_p2}, imo_1964_p2 and imo_1983_p6) in miniF2F-test. To benefit the community, we will open-source a dataset of 30k synthesized instances, where each instance contains the original question in natural language, the converted statement by autoformalization, and the proof by HunyuanProver.