Alchemie: Versterking van de stellingbewijsmogelijkheid door symbolische mutatie

Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation

October 21, 2024

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

cs.AI

Samenvatting

Het schrijven van formele bewijzen is zelfs voor ervaren experts uitdagend. Recente vooruitgang in Neuraal Stellingen Bewijzen (NSB) toont belofte om dit proces te versnellen. Echter, de formele corpora die beschikbaar zijn op het internet zijn beperkt in vergelijking met de algemene tekst, wat een aanzienlijke uitdaging vormt vanwege de schaarste aan data voor NSB. Om dit probleem aan te pakken, stelt dit werk Alchemie voor, een algemeen kader voor gegevenssynthese dat formele stellingen construeert door symbolische mutatie. Specifiek identificeren we voor elke kandidaatstelling in Mathlib alle oproepbare stellingen die kunnen worden gebruikt om deze te herschrijven of toe te passen. Vervolgens muteren we de kandidaatstelling door het overeenkomstige term in de verklaring te vervangen door de equivalente vorm of antecedent. Als gevolg hiervan vergroot onze methode het aantal stellingen in Mathlib met een orde van grootte, van 110k naar 6M. Bovendien voeren we voortdurende voortraining en begeleide fijnafstemming uit op dit uitgebreide corpus voor grote taalmodellen. Experimentele resultaten tonen de effectiviteit van onze aanpak aan, met een absoluut prestatieverbetering van 5% op de Leandojo benchmark. Daarnaast behalen onze synthetische gegevens een absoluut prestatievoordeel van 2.5% op de out-of-distribution miniF2F benchmark. Om verdere inzichten te bieden, voeren we een uitgebreide analyse uit van de samenstelling van synthetische gegevens en het trainingsparadigma, waarbij waardevolle richtlijnen worden geboden voor de ontwikkeling van een sterke stellingenbewijzer.

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.