Алхимия: Увеличение Возможностей Теоремного Доказательства через Символическую Мутацию

Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation

October 21, 2024

Авторы: Shaonan Wu, Shuai Lu, Yeyun Gong, Nan Duan, Ping Wei

cs.AI

Аннотация

Формальные доказательства сложно написать даже опытным экспертам. Недавние успехи в области Нейронного Доказательства Теорем (NTP) показывают потенциал в ускорении этого процесса. Однако формальные корпуса, доступные в Интернете, ограничены по сравнению с общим текстом, что представляет собой значительную проблему нехватки данных для NTP. Для решения этой проблемы в данной работе предлагается Alchemy, общая структура для синтеза данных, которая создает формальные теоремы путем символической мутации. Конкретно, для каждой кандидатской теоремы в Mathlib мы определяем все вызываемые теоремы, которые могут быть использованы для переписывания или применения к ней. Впоследствии мы мутируем кандидатскую теорему, заменяя соответствующий терм в утверждении на его эквивалентную форму или предшествующее. В результате наш метод увеличивает количество теорем в Mathlib на порядок, с 110 тыс. до 6 млн. Кроме того, мы проводим непрерывное предварительное обучение и надзорное дообучение на этом расширенном корпусе для больших языковых моделей. Экспериментальные результаты демонстрируют эффективность нашего подхода, достигая улучшения производительности на 5% по абсолютному показателю на бенчмарке Leandojo. Кроме того, наши синтетические данные достигают улучшения производительности на 2.5% по абсолютному показателю на бенчмарке miniF2F вне распределения. Для предоставления дополнительных идей мы проводим всесторонний анализ состава синтетических данных и парадигмы обучения, предлагая ценное руководство для разработки надежного доказателя теорем.

English

Formal proofs are challenging to write even for experienced experts. Recent progress in Neural Theorem Proving (NTP) shows promise in expediting this process. However, the formal corpora available on the Internet are limited compared to the general text, posing a significant data scarcity challenge for NTP. To address this issue, this work proposes Alchemy, a general framework for data synthesis that constructs formal theorems through symbolic mutation. Specifically, for each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it. Subsequently, we mutate the candidate theorem by replacing the corresponding term in the statement with its equivalent form or antecedent. As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M. Furthermore, we perform continual pretraining and supervised finetuning on this augmented corpus for large language models. Experimental results demonstrate the effectiveness of our approach, achieving a 5% absolute performance improvement on Leandojo benchmark. Additionally, our synthetic data achieve a 2.5% absolute performance gain on the out-of-distribution miniF2F benchmark. To provide further insights, we conduct a comprehensive analysis of synthetic data composition and the training paradigm, offering valuable guidance for developing a strong theorem prover.