HUNYUANPROVER: Ein skalierbares Daten-Synthese-Framework und geführter Baum-Suchalgorithmus für automatisches Beweisen von Theoremen.

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

December 30, 2024

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

cs.AI

Zusammenfassung

Wir stellen HunyuanProver vor, ein Sprachmodell, das vom Hunyuan 7B für interaktives automatisches Beweisen von Theoremen mit LEAN4 feinabgestimmt wurde. Um das Problem der Datenknappheit zu mildern, entwerfen wir ein skalierbares Framework zur iterativen Synthese von Daten mit geringen Kosten. Darüber hinaus wurden geleitete Baum-Suchalgorithmen entwickelt, um ein effektives "System 2-Denken" des Beweisers zu ermöglichen. HunyuanProver erzielt Spitzenleistungen (SOTA) auf wichtigen Benchmarks. Speziell erreicht es eine Erfolgsquote von 68,4% im miniF2F-Test im Vergleich zu 65,9%, den aktuellen SOTA-Ergebnissen. Es beweist 4 IMO-Aussagen (imo_1960_p2, imo_1962_p2, imo_1964_p2 und imo_1983_p6) im miniF2F-Test. Um der Gemeinschaft zu nutzen, werden wir einen Datensatz von 30.000 synthetisierten Instanzen als Open Source veröffentlichen, wobei jede Instanz die ursprüngliche Frage in natürlicher Sprache, die umgewandelte Aussage durch Autoformalisierung und den Beweis durch HunyuanProver enthält.

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.