Alchemie: Verstärkung der Beweisfähigkeit durch symbolische Mutation

Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation

October 21, 2024

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

cs.AI

Zusammenfassung

Das Verfassen formaler Beweise ist selbst für erfahrene Experten eine Herausforderung. Die jüngsten Fortschritte im Bereich des Neuralen Theorembeweises (NTP) zeigen vielversprechende Ansätze zur Beschleunigung dieses Prozesses. Allerdings sind die formalen Korpora, die im Internet verfügbar sind, im Vergleich zum allgemeinen Text begrenzt, was eine erhebliche Datenknappheit für den NTP darstellt. Um dieses Problem zu lösen, schlägt diese Arbeit Alchemy vor, ein allgemeines Rahmenwerk für die Datensynthese, das formale Sätze durch symbolische Mutation konstruiert. Konkret identifizieren wir für jeden Kandidatensatz in Mathlib alle aufrufbaren Sätze, die zur Umformulierung oder Anwendung darauf verwendet werden können. Anschließend mutieren wir den Kandidatensatz, indem wir den entsprechenden Term in der Aussage durch seine äquivalente Form oder den Antezedens ersetzen. Auf diese Weise erhöht unsere Methode die Anzahl der Sätze in Mathlib um eine Größenordnung, von 110k auf 6M. Darüber hinaus führen wir kontinuierliches Pretraining und überwachtes Feintuning an diesem erweiterten Korpus für große Sprachmodelle durch. Experimentelle Ergebnisse zeigen die Wirksamkeit unseres Ansatzes, der eine absolute Leistungssteigerung von 5% beim Leandojo-Benchmark erzielt. Darüber hinaus erzielen unsere synthetischen Daten einen absoluten Leistungsgewinn von 2,5% beim out-of-distribution miniF2F-Benchmark. Um weitere Einblicke zu bieten, führen wir eine umfassende Analyse der Zusammensetzung synthetischer Daten und des Schulungsparadigmas durch, die wertvolle Anleitungen für die Entwicklung eines starken Theorembeweisers bieten.

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.