錬金術：象徴的変異を通じた定理証明能力の増幅

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における重要なデータ不足の課題が生じています。この問題に対処するため、本研究では、形式的定理をシンボリックな変異を通じて構築するデータ合成のための一般的なフレームワークであるアルケミーを提案します。具体的には、Mathlib内の各候補定理について、それを書き換えたり適用したりするために使用できるすべての呼び出し可能な定理を特定します。その後、候補定理を、その文に対応する項を等価形式または前提で置き換えることで変異させます。その結果、当社の手法により、Mathlib内の定理の数が110kから6Mにオーダー増加します。さらに、この拡張されたコーパスに対して大規模言語モデルの継続的な事前学習と教師あり微調整を行います。実験結果は、当社のアプローチの効果を示し、Leandojoベンチマークで5%の絶対性能向上を達成しています。さらに、当社の合成データは、分布外のminiF2Fベンチマークで2.5%の絶対性能向上を達成しています。さらなる洞察を提供するために、合成データの構成とトレーニングパラダイムの包括的な分析を行い、強力な定理証明器の開発に有益なガイダンスを提供しています。

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.