LeanDojo usa modelos de linguagem para automatizar provas e ampliar bibliotecas matemáticas
LeanDojo é uma plataforma de código aberto para provar teoremas matemáticos usando modelos de linguagem. A iniciativa reúne ferramentas de aprendizado de máquina e assistentes de prova para enfrentar um dos desafios clássicos da matemática formal: transformar enunciados formais em demonstrações verificáveis.
A prova automatizada de teoremas, conhecida como ATP, é uma tarefa que gera provas para teoremas formulados na lógica formal. Esse tipo de tecnologia é útil para a matemática formal e suporta a verificação formal, que garante a correção e segurança de aplicações de alto risco. No entanto, a ATP esbarra em um grande espaço de busca, o que torna o problema computacionalmente exigente.
Por que LeanDojo muda o jogo
Para driblar esse gargalo, surgiu a Prova Interativa de Teoremas, ou ITP, na qual o cientista interage com um assistente de prova. A novidade do projeto é combinar ITP com modelos de linguagem avançados, criando um fluxo onde os LLMs colaboram com ferramentas formais. Nesse contexto, o conjunto de funções do projeto se destaca: o LeanDojo oferece duas características principais para a prova de teoremas baseada em aprendizado: extração de dados e interação programática de modelos com o Lean, um assistente de prova amplamente utilizado.
Segundo os pesquisadores por trás do projeto, o LeanDojo é a primeira ferramenta capaz de interagir de forma confiável com o Lean, o que deve reduzir significativamente erros de prova. Esse ponto é crucial, porque minimizar interações inválidas ou passos de prova incorretos aumenta a chance de gerar demonstrações que passam na verificação formal sem intervenção humana intensiva.
ReProver: estratégia de recuperação e prova
Uma contribuição prática importante do ecossistema LeanDojo é o ReProver. A equipe descreve o sistema como ReProver (Retrieval-Augmented Prover), um provador baseado em modelo de linguagem que gera uma estratégia de prova com base em algumas premissas recuperadas da biblioteca matemática do Lean. Em outras palavras, o ReProver não tenta provar um teorema a partir do nada, ele pesquisa premissas relevantes na biblioteca Mathlib e usa essas informações para esboçar uma estratégia de demonstração.
De acordo com os pesquisadores, o ReProver supera alguns outros métodos, provando uma porcentagem significativa de teoremas no benchmark do LeanDojo, assim como em dois conjuntos de dados existentes, o MiniF2F e o ProofNet. Além disso, o ReProver pode provar teoremas para os quais ainda não há prova no Lean, o que o torna uma ferramenta potencialmente valiosa para ampliar bibliotecas matemáticas existentes.
Os autores também lançaram um benchmark construído com a plataforma, que inclui quase 97.000 teoremas do Mathlib, além de um plugin para o ChatGPT, criando um ambiente reprodutível e acessível para pesquisadores testarem novas abordagens.
Impactos, desafios e o que vem a seguir
Apesar das promessas, os próprios autores apontam limitações do estado da arte. Eles afirmam que “No entanto, os métodos existentes são difíceis de reproduzir ou evoluir devido a códigos proprietários, dados e altos requisitos computacionais, de acordo com uma equipe de pesquisadores do Caltech, Nvidia, MIT, UC Santa Barbara e UT Austin.” O lançamento do LeanDojo tenta mitigar esse problema ao oferecer uma base open source.
Essas ferramentas entram em um debate maior sobre o papel dos modelos de linguagem na pesquisa científica. O matemático Terence Tao recentemente previu que “modelos de linguagem utilizando ferramentas externas poderiam se tornar coautores confiáveis em matemática e outras ciências até 2026.” A combinação de ambientes programáticos como o Lean e sistemas de recuperação e prova como o ReProver mostra um caminho concreto para essa visão.
Para pesquisadores e desenvolvedores, o apelo do projeto é duplo: por um lado, há a promessa de ampliar a produção de provas formais, por outro, a plataforma aberta facilita a reprodução e evolução das técnicas. Com o benchmark e o plugin para ChatGPT, a comunidade ganha ferramentas para medir progresso e integrar modelos grandes de linguagem nas rotinas de prova.
Em resumo, o desenvolvimento do LeanDojo e do ReProver mostra como a junção entre assistentes formais e LLMs pode acelerar a prova de teoremas e enriquecer bibliotecas matemáticas, ao mesmo tempo em que cria um ambiente mais reprodutível para pesquisa. A tendência é que, à medida que esses sistemas amadureçam, matemáticos e engenheiros adquiram parceiros digitais cada vez mais capazes de colaborar na construção de demonstrações formais.
Deixe um comentário