HUNYUANPROVER: Масштабируемая структура синтеза данных и направленный деревянный поиск для автоматизированного доказательства теорем.

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

December 30, 2024

Авторы: Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, Haitao Mi

cs.AI

Аннотация

Мы представляем HunyuanProver, языковую модель, донастроенную на основе Hunyuan 7B для интерактивного автоматического доказательства теорем с использованием LEAN4. Для уменьшения проблемы разреженности данных мы разработали масштабируемую структуру для итеративного синтеза данных с низкой стоимостью. Кроме того, разработаны направляемые алгоритмы поиска в дереве для обеспечения эффективного "мышления системы 2" доказывателя. HunyuanProver достигает передовых показателей (SOTA) на основных бенчмарках. В частности, он достигает процента успешных доказательств в размере 68.4% на тесте miniF2F по сравнению с 65.9%, текущими SOTA результатами. Он доказывает 4 утверждения IMO (imo_1960_p2, imo_1962_p2, imo_1964_p2 и imo_1983_p6) в тесте miniF2F. Для пользы сообщества мы предоставим в открытый доступ набор данных из 30 тыс. синтезированных примеров, где каждый пример содержит исходный вопрос на естественном языке, преобразованное утверждение с помощью автоформализации и доказательство с помощью 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.