HUNYUANPROVER: Un marco escalable de síntesis de datos y búsqueda guiada de árboles para la demostración automática de teoremas

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

December 30, 2024

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

cs.AI

Resumen

Presentamos HunyuanProver, un modelo de lenguaje ajustado finamente a partir del Hunyuan 7B para demostración automática interactiva de teoremas con LEAN4. Para mitigar el problema de la escasez de datos, diseñamos un marco escalable para sintetizar datos de forma iterativa con bajo costo. Además, se diseñaron algoritmos de búsqueda de árbol guiados para habilitar un efectivo "pensamiento del sistema 2" del demostrador. HunyuanProver logra un rendimiento de vanguardia (SOTA) en importantes puntos de referencia. Específicamente, alcanza un 68.4% de aprobación en la miniF2F-test en comparación con el 65.9%, los resultados SOTA actuales. Demuestra 4 declaraciones IMO (imo_1960_p2, imo_1962_p2, imo_1964_p2 e imo_1983_p6) en la miniF2F-test. Para beneficiar a la comunidad, compartiremos de forma abierta un conjunto de datos de 30k instancias sintetizadas, donde cada instancia contiene la pregunta original en lenguaje natural, la declaración convertida por autoformalización y la demostración realizada por 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.