title: Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation
summary: 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.
paper_authors._id: 6717365cc613f45832d7cdf0
paper_authors.name: Shaonan Wu
paper_authors.status: claimed_verified
paper_authors.statusLastChangedAt: 2024-10-22T07:56:50.016Z
paper_authors._id: 653a3180863b9327f60e37b5
paper_authors.avatarUrl: /avatars/cd85a88e42167af1782128559d1f3354.svg
paper_authors.fullname: ShaonanWu
paper_authors.type: user
paper_authors.user: EurekaWu123
paper_authors._id: 6717365cc613f45832d7cdf1
paper_authors.name: Shuai Lu
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2024-10-22T09:39:28.701Z
paper_authors._id: 617a3066f5910ea887210d91
paper_authors.avatarUrl: /avatars/5193c5f523459f3d977defb257ef6f0d.svg
paper_authors.fullname: Shuai Lu
paper_authors.type: user
paper_authors.user: shuailu
paper_authors._id: 6717365cc613f45832d7cdf2
paper_authors.name: Yeyun Gong
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2024-10-22T09:39:23.194Z
paper_authors._id: 643f615aa16cd6d1f4c581de
paper_authors.avatarUrl: /avatars/47753a3e82b44f81881600c52e1e8495.svg
paper_authors.fullname: Yeyun Gong
paper_authors.type: user
paper_authors.user: yegong
paper_authors._id: 6717365cc613f45832d7cdf3
paper_authors.name: Nan Duan
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2024-10-22T09:39:17.629Z
paper_authors._id: 66422aede3e9eba09d3cb753
paper_authors.avatarUrl: /avatars/52a6292fcc3a37265062bdcfbea73441.svg
paper_authors.fullname: Nan Duan
paper_authors.type: user
paper_authors.user: opotle
paper_authors._id: 6717365cc613f45832d7cdf4
paper_authors.name: Ping Wei
paper_title: Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation
paper_summary: 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.
paper_ai_summary: Alchemy synthesizes formal theorems through symbolic mutation to augment Mathlib, enhancing performance on theorem proving benchmarks.
paper_ai_keywords: 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