Alquimia: Ampliando a Capacidade de Prova de Teoremas por meio de Mutação 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

Resumo

Provas formais são desafiadoras de serem escritas, mesmo para especialistas experientes. O progresso recente em Prova de Teoremas Neurais (PTN) mostra promessa em acelerar esse processo. No entanto, os corpora formais disponíveis na Internet são limitados em comparação com o texto geral, apresentando um desafio significativo de escassez de dados para PTN. Para lidar com esse problema, este trabalho propõe Alquimia, um framework geral para síntese de dados que constrói teoremas formais por meio de mutação simbólica. Especificamente, para cada teorema candidato em Mathlib, identificamos todos os teoremas invocáveis que podem ser usados para reescrevê-lo ou aplicá-lo. Posteriormente, mutamos o teorema candidato substituindo o termo correspondente na afirmação por sua forma equivalente ou antecedente. Como resultado, nosso método aumenta o número de teoremas em Mathlib em uma ordem de magnitude, de 110k para 6M. Além disso, realizamos pré-treinamento contínuo e ajuste fino supervisionado neste corpus ampliado para grandes modelos de linguagem. Resultados experimentais demonstram a eficácia de nossa abordagem, alcançando uma melhoria de desempenho absoluto de 5% no benchmark Leandojo. Adicionalmente, nossos dados sintéticos alcançam um ganho de desempenho absoluto de 2,5% no benchmark miniF2F fora da distribuição. Para fornecer mais insights, realizamos uma análise abrangente da composição dos dados sintéticos e do paradigma de treinamento, oferecendo orientações valiosas para o desenvolvimento de um forte provador 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.