Alchimie : Amplification de la capacité de prouver des théorèmes grâce à la mutation symbolique

Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation

October 21, 2024

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

cs.AI

Résumé

Les preuves formelles sont difficiles à rédiger, même pour des experts expérimentés. Les progrès récents en Proving Neural Theorem (PNT) montrent des promesses pour accélérer ce processus. Cependant, les corpus formels disponibles sur Internet sont limités par rapport au texte général, ce qui pose un défi important de pénurie de données pour le PNT. Pour résoudre ce problème, ce travail propose Alchemy, un cadre général pour la synthèse de données qui construit des théorèmes formels par mutation symbolique. Plus précisément, pour chaque théorème candidat dans Mathlib, nous identifions tous les théorèmes invoquables qui peuvent être utilisés pour le réécrire ou l'appliquer. Ensuite, nous mutons le théorème candidat en remplaçant le terme correspondant dans l'énoncé par sa forme équivalente ou son antécédent. Ainsi, notre méthode augmente le nombre de théorèmes dans Mathlib d'un ordre de grandeur, passant de 110k à 6M. De plus, nous effectuons un pré-entraînement continu et un affinage supervisé sur ce corpus augmenté pour de grands modèles de langage. Les résultats expérimentaux démontrent l'efficacité de notre approche, atteignant une amélioration de performance absolue de 5% sur le benchmark Leandojo. De plus, nos données synthétiques réalisent un gain de performance absolu de 2,5% sur le benchmark miniF2F hors distribution. Pour fournir des perspectives supplémentaires, nous menons une analyse approfondie de la composition des données synthétiques et du paradigme d'entraînement, offrant des orientations précieuses pour le développement d'un puissant prouveur de théorèmes.

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.