Alchimia: Amplificare la Capacità di Dimostrazione Teorematica tramite Mutazione Simbolica

Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation

October 21, 2024

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

cs.AI

Abstract

Le dimostrazioni formali sono difficili da scrivere anche per esperti esperti. I recenti progressi nel Prova Teoremi Neurale (PTN) mostrano promesse nel velocizzare questo processo. Tuttavia, i corpora formali disponibili su Internet sono limitati rispetto al testo generale, presentando una significativa sfida legata alla scarsità di dati per il PTN. Per affrontare questo problema, questo lavoro propone Alchimia, un framework generale per la sintesi dei dati che costruisce teoremi formali attraverso mutazioni simboliche. In particolare, per ciascun teorema candidato in Mathlib, identifichiamo tutti i teoremi invocabili che possono essere utilizzati per riscriverlo o applicarlo. Successivamente, mutiamo il teorema candidato sostituendo il termine corrispondente nella formulazione con la sua forma equivalente o antecedente. Di conseguenza, il nostro metodo aumenta il numero di teoremi in Mathlib di un ordine di grandezza, da 110k a 6M. Inoltre, eseguiamo un preaddestramento continuo e un raffinamento supervisionato su questo corpus ampliato per modelli di linguaggio di grandi dimensioni. I risultati sperimentali dimostrano l'efficacia del nostro approccio, ottenendo un miglioramento delle prestazioni assoluto del 5% sul benchmark Leandojo. Inoltre, i nostri dati sintetici raggiungono un guadagno di prestazioni assoluto del 2,5% sul benchmark miniF2F out-of-distribution. Per fornire ulteriori approfondimenti, conduciamo un'analisi approfondita della composizione dei dati sintetici e del paradigma di addestramento, offrendo preziose indicazioni per lo sviluppo di un forte dimostratore di teoremi.

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.