Доказательство Гёделя: модель фронтового уровня для автоматизированного доказательства теорем с открытым исходным кодом

Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving

February 11, 2025

Авторы: Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, Chi Jin

cs.AI

Аннотация

Мы представляем Goedel-Prover, открытую модель большого языка (LLM), которая достигает передовой производительности в автоматическом создании формальных доказательств для математических задач. Основным вызовом в этой области является дефицит формализованных математических утверждений и доказательств, с которым мы справляемся следующим образом. Мы обучаем формализаторы утверждений для перевода естественноязычных математических задач из Numina на формальный язык (Lean 4), создавая набор данных из 1,64 миллиона формальных утверждений. LLM используются для проверки того, что формальные утверждения точно сохраняют содержание исходных естественноязычных задач. Затем мы итеративно создаем большой набор данных формальных доказательств, обучая серию доказывателей. Каждый доказыватель успешно доказывает множество утверждений, которые предыдущие не могли, и эти новые доказательства добавляются в обучающий набор данных для следующего доказывателя. Финальный доказыватель превосходит все существующие модели с открытым исходным кодом в создании полных доказательств. На мини-тесте miniF2F он достигает успеха в 57,6% случаев (Pass@32), превосходя предыдущую лучшую модель с открытым исходным кодом на 7,6%. На тесте PutnamBench Goedel-Prover успешно решает 7 задач (Pass@512), занимая первое место в рейтинге. Более того, он генерирует 29,7 тыс. формальных доказательств для задач Lean Workbook, почти вдвое больше, чем 15,7 тыс., созданных ранее.

English

We introduce Goedel-Prover, an open-source large language model (LLM) that achieves the state-of-the-art (SOTA) performance in automated formal proof generation for mathematical problems. The key challenge in this field is the scarcity of formalized math statements and proofs, which we tackle in the following ways. We train statement formalizers to translate the natural language math problems from Numina into formal language (Lean 4), creating a dataset of 1.64 million formal statements. LLMs are used to check that the formal statements accurately preserve the content of the original natural language problems. We then iteratively build a large dataset of formal proofs by training a series of provers. Each prover succeeds in proving many statements that the previous ones could not, and these new proofs are added to the training set for the next prover. The final prover outperforms all existing open-source models in whole-proof generation. On the miniF2F benchmark, it achieves a 57.6% success rate (Pass@32), exceeding the previous best open-source model by 7.6%. On PutnamBench, Goedel-Prover successfully solves 7 problems (Pass@512), ranking first on the leaderboard. Furthermore, it generates 29.7K formal proofs for Lean Workbook problems, nearly doubling the 15.7K produced by earlier works.