LeanDojo é uma plataforma de código aberto para provar teoremas matemáticos usando modelos de linguagem.
A prova automatizada de teoremas (ATP) é uma tarefa que gera provas para teoremas formulados na lógica formal. É ú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 é desafiadora devido ao seu grande espaço de busca. Por isso, a Prova Interativa de Teoremas (ITP) surgiu como uma alternativa. Na ITP, as provas são geradas por matemáticos que interagem com ferramentas de software chamadas assistentes de prova.
A aprendizagem de máquina poderia automatizar esse processo, abrindo um novo caminho para provar teoremas.
Grandes modelos de linguagem podem automatizar a prova de teoremas
Grandes modelos de linguagem combinados com assistentes de prova, como o Lean, são candidatos para esse processo.
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.
Para resolver isso, eles criaram o LeanDojo, uma plataforma de código aberto para provar teoremas matemáticos usando modelos de linguagem.
O LeanDojo e o ReProver abrem as portas para pesquisas adicionais
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, o LeanDojo é a primeira ferramenta capaz de interagir de forma confiável com o Lean, o que deve reduzir significativamente erros de prova.
O LeanDojo também aborda um gargalo importante na prova de teoremas: seleção de premissas. A equipe demonstra isso com o 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.
De acordo com a equipe, 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. O ReProver também pode provar teoremas para os quais ainda não há prova no Lean, tornando-se uma ferramenta útil para ampliar as bibliotecas matemáticas existentes no Lean.
Modelos de linguagem como coautores de matemática até 2026?
A equipe também está lançando um benchmark construído com o LeanDojo, que inclui quase 97.000 teoremas do Mathlib, além de um plugin para o ChatGPT.
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. O LeanDojo e o ReProver mostram como essas ferramentas poderiam ser e agora oferecem a outros pesquisadores uma base para melhorias.
Mais informações estão disponíveis no site do LeanDojo.
