HUNYUANPROVER : un cadre de synthèse de données évolutif et une recherche arborescente guidée pour la démonstration automatique de théorèmes

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

Résumé

Nous présentons HunyuanProver, un modèle de langage affiné à partir du Hunyuan 7B pour la démonstration automatique interactive de théorèmes avec LEAN4. Pour pallier le problème de rareté des données, nous concevons un cadre évolutif pour la synthèse itérative de données à faible coût. De plus, des algorithmes de recherche arborescente guidée sont conçus pour permettre une "pensée du système 2" efficace du prouveur. HunyuanProver atteint des performances de pointe (SOTA) sur les principaux bancs d'essai. Plus précisément, il obtient un taux de réussite de 68,4 % sur le miniF2F-test par rapport à 65,9 %, les résultats SOTA actuels. Il prouve 4 énoncés IMO (imo_1960_p2, imo_1962_p2, imo_1964_p2 et imo_1983_p6) dans le miniF2F-test. Pour bénéficier à la communauté, nous mettrons à disposition un ensemble de données de 30 000 instances synthétisées, où chaque instance contient la question originale en langage naturel, l'énoncé converti par autoformalisation et la preuve par 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.