HUNYUANPROVER: Um Framework Escalável de Síntese de Dados e Busca de Árvore Guiada para Prova Automatizada 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

Resumo

Apresentamos o HunyuanProver, um modelo de linguagem ajustado a partir do Hunyuan 7B para demonstração automática interativa de teoremas com LEAN4. Para mitigar o problema de escassez de dados, projetamos um framework escalável para sintetizar iterativamente dados com baixo custo. Além disso, algoritmos de busca em árvore guiada são desenvolvidos para permitir um "pensamento do sistema 2" eficaz do provador. O HunyuanProver alcança desempenhos de ponta (SOTA) em importantes benchmarks. Especificamente, obtém uma taxa de aprovação de 68,4% no miniF2F-teste em comparação com 65,9%, os resultados SOTA atuais. Ele prova 4 declarações IMO (imo_1960_p2, imo_1962_p2, imo_1964_p2 e imo_1983_p6) no miniF2F-teste. Para beneficiar a comunidade, disponibilizaremos um conjunto de dados de 30 mil instâncias sintetizadas, onde cada instância contém a pergunta original em linguagem natural, a declaração convertida por autoformalização e a prova pelo 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.