연금술: 상징적 돌연변이를 통해 정리 증명 능력을 증폭하기

Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation

October 21, 2024

저자: Shaonan Wu, Shuai Lu, Yeyun Gong, Nan Duan, Ping Wei

cs.AI

초록

형식적인 증명은 경험이 풍부한 전문가들에게도 쓰기 어려운 과제입니다. 최근 신경 정리 증명(Neural Theorem Proving, NTP)의 발전은 이 과정을 가속화하는 데 유망성을 보여줍니다. 그러나 인터넷에서 이용 가능한 형식적 말뭉치는 일반 텍스트에 비해 제한적이어서 NTP에 대한 중요한 데이터 부족 도전을 제기합니다. 본 연구는 이 문제에 대응하기 위해 데이터 합성을 위한 일반적인 프레임워크인 Alchemy를 제안합니다. 이 프레임워크는 상징적 돌연변이를 통해 형식적 정리를 구축합니다. 구체적으로, Mathlib의 각 후보 정리에 대해 해당 정리를 다시 쓰거나 적용할 수 있는 모든 호출 가능한 정리를 식별합니다. 그 후, 후보 정리를 해당 문장의 대응하는 용어를 동등한 형태나 선행으로 대체함으로써 돌연변이를 일으킵니다. 결과적으로, 우리의 방법은 Mathlib의 정리 수를 11만 개에서 600만 개로 10배 증가시킵니다. 더불어, 우리는 이 보강된 말뭉치에 대해 대규모 언어 모델을 위한 지속적인 사전 훈련 및 지도된 미세 조정을 수행합니다. 실험 결과는 우리의 접근 방식의 효과를 입증하며, 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.