Em uma notícia recente que causou sensação no mundo da matemática, um grupo de ex-alunos da Tsinghua, com o auxílio da IA, conseguiu provar 162 teoremas matemáticos que antes eram insolúveis. Ainda mais impressionante, essa inteligência artificial, chamada LeanAgent, também superou o desafio proposto por Terence Tao para a formalização do problema da conjectura de Freiman-Ruzsa polinomial! Isso nos leva a acreditar que os métodos de pesquisa em ciências básicas foram completamente transformados pela IA.
Como sabemos, os atuais modelos de linguagem (LLMs), apesar de impressionantes, são na maioria estáticos e não conseguem aprender novos conhecimentos online; provar teoremas de matemática avançada é ainda mais difícil. No entanto, o LeanAgent, desenvolvido em conjunto por equipes da Caltech, Stanford e da Universidade de Washington, é um assistente de IA com capacidade de aprendizado contínuo, capaz de aprender e provar teoremas continuamente.
O LeanAgent utiliza um caminho de aprendizagem cuidadosamente projetado para lidar com diferentes níveis de dificuldade matemática, utilizando um banco de dados dinâmico para gerenciar o fluxo constante de conhecimento matemático, garantindo que ele não esqueça as habilidades já adquiridas ao aprender novos conhecimentos. Os experimentos mostraram que ele conseguiu provar 162 teoremas matemáticos antes insolúveis a partir de 23 diferentes repositórios de código Lean, um desempenho 11 vezes superior ao dos grandes modelos tradicionais, o que é realmente surpreendente!
Esses teoremas abrangem várias áreas da matemática avançada, incluindo problemas complexos de álgebra abstrata e topologia algébrica. O LeanAgent não só consegue começar com conceitos simples e gradualmente resolver temas complexos, mas também demonstra excelente desempenho em estabilidade e transferência inversa.
No entanto, o desafio de Terence Tao ainda representa um obstáculo para a IA. Embora os verificadores interativos de teoremas (ITPs), como o Lean, desempenhem um papel importante na formalização e verificação de provas matemáticas, a construção desse processo de prova costuma ser complexa e demorada, exigindo passos minuciosos e uma grande quantidade de bibliotecas de código matemático. Grandes modelos avançados como o o1 e o Claude, quando confrontados com provas não formalizadas, tendem a cometer erros, o que destaca as deficiências dos LLMs em termos de precisão e confiabilidade na demonstração matemática.
Pesquisas anteriores tentaram usar LLMs para gerar passos completos de prova; por exemplo, o LeanDojo é um verificador de teoremas criado treinando grandes modelos em um conjunto de dados específico. No entanto, os dados para provas formais de teoremas são extremamente escassos, limitando a ampla aplicabilidade desse método. Outro projeto, o ReProver, é um modelo otimizado para a biblioteca de código de prova de teoremas Lean mathlib4; embora abranja mais de 100.000 teoremas e definições matemáticas formalizadas, ele se limita à matemática de nível universitário, portanto, apresenta desempenho inferior quando confrontado com problemas mais complexos.
É importante notar que a natureza dinâmica da pesquisa matemática apresenta desafios ainda maiores para a IA. Os matemáticos geralmente trabalham em vários projetos simultaneamente ou alternadamente; Terence Tao, por exemplo, trabalha em várias áreas de pesquisa, incluindo a conjectura PFR e a média simétrica de números reais. Esses exemplos mostram uma deficiência crucial nos métodos atuais de prova de teoremas por IA: a falta de um sistema de IA capaz de aprender e melhorar de forma adaptativa em diferentes áreas da matemática, especialmente com dados Lean limitados.
Por esse motivo, a equipe do LeanDojo criou o LeanAgent, uma nova estrutura de aprendizado contínuo projetada para resolver os problemas mencionados acima. O fluxo de trabalho do LeanAgent inclui a dedução da complexidade dos teoremas para elaborar um currículo de aprendizagem, o treinamento gradual para equilibrar a estabilidade e a flexibilidade durante o processo de aprendizagem e a utilização da busca em árvore de melhor prioridade para encontrar teoremas ainda não comprovados.
O LeanAgent pode ser usado com qualquer grande modelo, utilizando a "recuperação" para melhorar sua capacidade de generalização. Sua inovação reside no uso de um banco de dados dinâmico personalizado para gerenciar o conhecimento matemático em constante expansão e na estratégia de aprendizagem baseada em currículo na estrutura de prova Lean, auxiliando no aprendizado de conteúdo matemático mais complexo.
Para lidar com o problema do esquecimento catastrófico da IA, os pesquisadores utilizaram um método de treinamento gradual, permitindo que o LeanAgent se adaptasse continuamente a novos conhecimentos matemáticos sem esquecer o aprendizado anterior. Esse processo envolve treinamento incremental em cada novo conjunto de dados, garantindo o melhor equilíbrio entre estabilidade e flexibilidade.
Por meio desse treinamento gradual, o LeanAgent demonstrou um desempenho excepcional na prova de teoremas, conseguindo provar 162 problemas ainda não resolvidos por humanos, especialmente em teoremas desafiadores de álgebra abstrata e topologia algébrica. Sua capacidade de provar novos teoremas é 11 vezes maior do que a do ReProver estático, mantendo ao mesmo tempo a capacidade de provar teoremas conhecidos.
O LeanAgent demonstrou características de aprendizagem gradual no processo de prova de teoremas, passando de teoremas simples para teoremas mais complexos, demonstrando a profundidade de seu conhecimento matemático. Por exemplo, ele provou teoremas de estruturas algébricas básicas relacionadas à teoria dos grupos e anéis, mostrando uma compreensão profunda da matemática. Em resumo, o LeanAgent, com sua poderosa capacidade de aprendizado contínuo e melhoria, traz perspectivas empolgantes para o mundo da matemática!
Endereço do artigo: https://arxiv.org/pdf/2410.06209
