HUNYUANPROVER: un framework scalabile di sintesi dati e ricerca guidata dell'albero per la dimostrazione automatica dei teoremi

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

December 30, 2024

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

cs.AI

Abstract

Introduciamo HunyuanProver, un modello linguistico ottimizzato a partire dal Hunyuan 7B per dimostrazioni automatiche interattive con LEAN4. Per affrontare il problema della scarsità di dati, progettiamo un framework scalabile per la sintesi iterativa di dati a basso costo. Inoltre, sono stati progettati algoritmi di ricerca guidata nell'albero per abilitare un efficace "pensiero di sistema 2" del dimostratore. HunyuanProver raggiunge prestazioni all'avanguardia (SOTA) su importanti benchmark. In particolare, ottiene un punteggio del 68,4% nel miniF2F-test rispetto al 65,9%, attuale risultato SOTA. Dimostra 4 affermazioni IMO (imo_1960_p2, imo_1962_p2, imo_1964_p2 e imo_1983_p6) nel miniF2F-test. Per beneficiare la comunità, renderemo open-source un dataset di 30k istanze sintetizzate, in cui ogni istanza contiene la domanda originale in linguaggio naturale, l'affermazione convertita tramite autoformalizzazione e la dimostrazione di 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.