Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation
Shaonan Wu, Shuai Lu, Yeyun Gong, Nan Duan, Ping Wei
2024-10-22
Summary
This paper introduces Alchemy, a new method that enhances the ability of AI to prove mathematical theorems by creating new theorems through a process called symbolic mutation.
What's the problem?
Writing formal proofs in mathematics is difficult, even for experts. Current methods using Neural Theorem Proving (NTP) help speed up this process, but there isn't enough formal data available online for training these AI models effectively. This lack of data makes it hard for the models to learn and produce accurate proofs.
What's the solution?
To overcome this challenge, the authors developed Alchemy, which generates new formal theorems by modifying existing ones using symbolic mutation. They take candidate theorems from a database called Mathlib and identify related theorems that can be used to rewrite or enhance them. By replacing terms in the original theorems with equivalent expressions, they significantly increase the number of available theorems from 110,000 to 6 million. They then use this expanded dataset to train large language models, leading to improved performance in theorem proving tasks.
Why it matters?
This research is important because it addresses the data scarcity issue in training AI for mathematical proofs. By creating a larger and more diverse set of theorems, Alchemy enhances the capabilities of AI systems in formal reasoning. This can lead to advancements in fields that rely on precise mathematical proofs, such as computer science, engineering, and mathematics education.
Abstract
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.