Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation
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.
6717365cc613f45832d7cdf0
Shaonan Wu
claimed_verified
2024-10-22T07:56:50.016Z
653a3180863b9327f60e37b5
/avatars/cd85a88e42167af1782128559d1f3354.svg
ShaonanWu
user
EurekaWu123
6717365cc613f45832d7cdf1
Shuai Lu
admin_assigned
2024-10-22T09:39:28.701Z
617a3066f5910ea887210d91
/avatars/5193c5f523459f3d977defb257ef6f0d.svg
Shuai Lu
user
shuailu
6717365cc613f45832d7cdf2
Yeyun Gong
admin_assigned
2024-10-22T09:39:23.194Z
643f615aa16cd6d1f4c581de
/avatars/47753a3e82b44f81881600c52e1e8495.svg
Yeyun Gong
user
yegong
6717365cc613f45832d7cdf3
Nan Duan
admin_assigned
2024-10-22T09:39:17.629Z
66422aede3e9eba09d3cb753
/avatars/52a6292fcc3a37265062bdcfbea73441.svg
Nan Duan
user
opotle
6717365cc613f45832d7cdf4
Ping Wei
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation
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.
Alchemy synthesizes formal theorems through symbolic mutation to augment Mathlib, enhancing performance on theorem proving benchmarks.
Neural Theorem Proving NTP data synthesis symbolic mutation invocable theorems theorem rewriting equivalent form antecedent continual pretraining supervised finetuning large language models Leandojo benchmark miniF2F benchmark synthetic data