Alquimia: Ampliando la Capacidad de Demostración de Teoremas a través de la Mutación Simbólica

Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation

October 21, 2024

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

cs.AI

Resumen

Las demostraciones formales son difíciles de redactar incluso para expertos experimentados. El progreso reciente en la Demostración de Teoremas Neurales (DTN) muestra promesas para acelerar este proceso. Sin embargo, las corpora formales disponibles en Internet son limitadas en comparación con el texto general, lo que plantea un desafío significativo de escasez de datos para la DTN. Para abordar este problema, este trabajo propone Alquimia, un marco general para la síntesis de datos que construye teoremas formales a través de mutaciones simbólicas. Específicamente, para cada teorema candidato en Mathlib, identificamos todos los teoremas invocables que se pueden utilizar para reescribirlo o aplicarlo. Posteriormente, mutamos el teorema candidato reemplazando el término correspondiente en la declaración con su forma equivalente o antecedente. Como resultado, nuestro método aumenta el número de teoremas en Mathlib en un orden de magnitud, de 110k a 6M. Además, realizamos un preentrenamiento continuo y un ajuste fino supervisado en este corpus aumentado para modelos de lenguaje grandes. Los resultados experimentales demuestran la efectividad de nuestro enfoque, logrando una mejora de rendimiento absoluta del 5% en el benchmark de Leandojo. Además, nuestros datos sintéticos logran una ganancia de rendimiento absoluto del 2.5% en el benchmark miniF2F fuera de la distribución. Para proporcionar más información, realizamos un análisis exhaustivo de la composición de datos sintéticos y el paradigma de entrenamiento, ofreciendo orientación valiosa para el desarrollo de un potente demostrador de teoremas.

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.