IA e Provas de Matemática: Uma Nova Abordagem

Escrever provas matemáticas formais pode ser tão complicado quanto tentar dobrar um lençol com elástico. Se você é humano ou computador, parece um quebra-cabeça sem fim. Recentemente, algumas pessoas inteligentes pensaram: "E se usássemos IA para nos ajudar?" Eles focaram em um tipo especial de problema matemático chamado problemas IMO da Olimpíada Internacional de Matemática.

Agora, esses problemas vão de moderados a verdadeiros quebra-cabeças. Sabe, aquele tipo de problema que te faz coçar a cabeça e se perguntar se você até sabe somar. A equipe queria escrever Provas Formais usando uma ferramenta chamada Lean, que é uma linguagem de programação para provas matemáticas. Eles queriam resolver alguns desses problemas complicados usando IA, e o que descobriram foi super interessante.

#O Desafio das Provas Matemáticas

Os humanos têm dificuldade para escrever provas matemáticas formais, e os computadores também não são exatamente gênios nisso. Até alguns modelos de IA considerados avançados se enrolam. O conjunto de dados miniF2F, que é usado como referência para a prova automatizada de teoremas, contém 20 problemas IMO, mas faltam provas formais para mais da metade deles. Então, por que isso é tão importante? Bem, quando um computador diz que pode resolver um problema mas não tem uma prova adequada para apoiar isso, é como afirmar que você é um cozinheiro incrível só porque aqueceu pizzas congeladas.

Muitos modelos de IA, como o GPT-4, têm dificuldade em provar corretamente esses problemas matemáticos. Eles podem dar sorte às vezes, mas quando chega nos problemas mais difíceis, é como ver uma criança pequena tentar amarrar os sapatos-muito esforço, mas pouco sucesso.

#Expandindo o Conjunto de Provas

Para ajudar a ter mais provas formais por aí, a equipe decidiu escrever provas originais para 13 dos 20 problemas IMO no conjunto de dados miniF2F, além de alguns extras de anos mais recentes. Isso resulta em um total de 5.150 linhas de prova-até mais longas que alguns romances! Esse esforço gigantesco facilita para futuros pesquisadores aprenderem e experimentarem com esses problemas.

Mas não pararam por aí. Eles também dividiram essas provas em partes menores, chamadas Lemas. Pense nesses lemas como os blocos de construção das provas matemáticas. A equipe criou cerca de 900 lemas com aproximadamente 25.500 linhas de código Lean. É um monte de blocos de matemática! Esses lemas são mais fáceis de trabalhar e oferecem um caminho mais claro para os modelos de IA aprenderem.

#Avaliando as Habilidades de Escrita de Provas da IA

Depois de gerar esses lemas, a equipe decidiu testar as habilidades de escrita de provas do GPT-4 neles. Spoiler: não foi tão bem quanto esperavam. A IA teve dificuldade em escrever provas corretas, o que foi surpreendente, considerando toda a tecnologia sofisticada por trás dela. Eles usaram várias técnicas de prompt, incluindo Zero-Shot prompting (pedindo para ir direto ao ponto) e Chain-of-Thought reasoning (guiando passo a passo). Mas mesmo assim, o robô não se destacou.

O que foi ainda mais interessante foi que o GPT-4 se saiu melhor nos problemas IMO mais antigos em comparação com os mais novos. Os problemas mais antigos pareciam ser um pouco mais amigáveis, como um dia de verão calmo, enquanto os mais novos eram mais como uma noite tempestuosa-desafiadores e difíceis de navegar.

#Por Que a IA Precisa de Dados de Alta Qualidade

Modelos de aprendizado de máquina, como uma pessoa faminta, precisam de dados de alta qualidade para prosperar. Quanto mais bons dados você fornecer, melhor eles vão performar. O sucesso de muitos sistemas de aprendizado de máquina geralmente pode ser rastreado de volta a uma abundância de dados de treinamento de qualidade. Por exemplo, o ImageNet teve um grande papel na visão computacional. Mas quando se trata de matemática, os recursos disponíveis são bem escassos.

O conjunto de dados miniF2F não tem provas de qualidade suficiente para muitos de seus problemas. A maioria dos modelos de IA falha porque carecem de exemplos sólidos para aprender. É como tentar aprender a andar de bicicleta sem nunca ter visto ninguém fazer isso primeiro. Quando um modelo tenta resolver um problema matemático e falha, é difícil saber onde errou, já que não há um bom ponto de referência.

#A Olimpíada de Matemática: Um Duro Osso

A Olimpíada Internacional de Matemática apresenta um desafio único. Os problemas são revelados apenas no dia da prova, e ficam mais difíceis a cada ano. Então, se um modelo de IA quer se destacar, precisa estar afiado e ser capaz de lidar com o desconhecido. Usar problemas anteriores como prática não é suficiente, porque a cada ano os alunos enfrentam novos desafios que são intencionalmente complicados.

Para preparar uma IA para a Olimpíada de Matemática, os pesquisadores precisam usar métodos de avaliação rigorosos. Eles precisam checar se a IA consegue generalizar seu aprendizado quando enfrenta um novo conjunto de problemas mais difíceis. Se você está tentando ganhar uma medalha de ouro e só praticou com algo fácil, pode acabar voltando para casa de mãos vazias.

#Status Atual dos Conjuntos de Dados Matemáticos

O conjunto de dados miniF2F consiste em vários teoremas matemáticos que os alunos são testados. Entre os 244 teoremas, 20 são da IMO, e sua dificuldade varia bastante. Alguns exigem prova em uma única linha, enquanto outros levam centenas de linhas. Ter sucesso em problemas mais fáceis não garante sucesso nos mais difíceis. Então, se um modelo diz que é bom, é essencial olhar além de simples porcentagens.

O atual campeão desse conjunto de dados, o LEGO-Prover, conseguiu provar apenas um dos problemas IMO. Enquanto isso, métodos como HTPS conseguem lidar com mais problemas, mas frequentemente enfrentam dificuldades com enunciados de problemas que são simplificados ou mal formulados. É como dizer que você pode ganhar uma corrida só porque conseguiu completar uma corrida curta.

#Uma Nova Abordagem para Decompor Provas

A equipe percebeu que para muitos problemas, provas formais não estavam disponíveis ao público. Então, eles enfrentaram esses problemas complicados e compartilharam suas provas formais em Lean. Eles dividiram cada prova em lemas menores. Esse processo tornou os desafios complexos mais gerenciáveis, permitindo que outros estudassem e aprendessem com eles.

Os lemas variam em dificuldade e cobrem uma variedade de tópicos. Enquanto alguns são simples e diretos, outros exigem um pensamento mais profundo. Eles até evitaram problemas fáceis que o Lean poderia provar automaticamente. Em vez disso, focaram em desafios reais onde a cabeça-humana ou de IA-precisaria ser colocada à prova.

#Testando o GPT-4: Esperando por Melhorias

Para ver se o GPT-4 poderia melhorar, a equipe pediu que ele escrevesse provas formais para seus lemas. Eles forneceram instruções detalhadas e revisaram as provas informais do GPT-4 ao lado das formais. Surpreendentemente, mesmo após muitos prompts e feedback, o GPT-4 ainda lutava com a precisão. Era como dizer a alguém repetidamente como fazer um sanduíche, e eles ainda acabavam te servindo uma salada.

Na maioria dos casos, o GPT-4 simplesmente não conseguiu fornecer as respostas certas. A equipe deu feedback e pediu que ele corrigisse os erros, mas parecia que estavam tentando ensinar um gato a buscar. Eles interagiram com o GPT-4 várias vezes, mas depois de dez rodadas, decidiram cortar suas perdas.

#Um Olhar Mais Atento aos Lemas

Cada um dos lemas no novo conjunto de dados tem uma prova formal em Lean, o que é crucial para qualquer um tentando aprender sobre esses problemas. A equipe construiu 907 lemas com níveis de dificuldade que variam de fáceis a complexos. Esses blocos de construção são essenciais para quem busca entender melhor a escrita de provas, pois fornecem um caminho para enfrentar problemas matemáticos mais intrincados.

Por exemplo, alguns lemas são relativamente simples, envolvendo a prova de propriedades básicas de números. Outros desafiam o solucionador a pensar criticamente sobre funções e relações entre números. Muitos ainda são difíceis, mesmo quando divididos, mas essa é a beleza da matemática-sempre há algo novo para aprender.

#Tornando as Provas Acessíveis

As provas formais criadas pela equipe foram compartilhadas com a comunidade para ajudar todo mundo a entender o trabalho que envolve escrever uma prova formal. Isso também pode ajudar a identificar erros em provas informais que circulam online. A equipe tem como objetivo mostrar quão benéficas e detalhadas as provas formais podem ser, especialmente ao olhar para assuntos mais complicados.

Ao tornar essas provas disponíveis, estão contribuindo para uma compreensão mais ampla da matemática. Não matemáticos podem ver o esforço envolvido nas provas formais, e matemáticos podem usá-las para aprimorar suas abordagens informais.

#Principais Conclusões

O projeto ajuda a esclarecer as dificuldades de formalizar provas e enfatiza a importância de dados de alta qualidade no treinamento de modelos de IA. Embora o GPT-4 tenha lutado bastante, esse trabalho lançou as bases para avanços futuros.

A equipe espera que, ao fornecer uma abundância de provas formais e trabalhar através dos lemas, possam incentivar mais sucessos na área da prova automatizada de teoremas. Eles veem isso como um passo à frente na longa jornada para construir IA capaz de enfrentar problemas matemáticos de alto nível, como os encontrados na Olimpíada de Matemática.

#Explorando Direções Futuras

Embora a equipe tenha enfrentado desafios com o GPT-4, eles permanecem otimistas. O objetivo de desenvolver um modelo que possa provar efetivamente os lemas em seu conjunto de dados ainda está vivo. Cada tentativa, mesmo que imperfeita, serve para informar o futuro da IA na matemática.

O projeto também abre caminhos para modelos de IA mais robustos que podem entender provas complexas e conectar ideias de maneiras novas. Não faltam desafios no mundo da matemática, e a IA pode desempenhar um papel crítico em empurrar esses limites ainda mais.

#Conclusão

Resumindo, o esforço para escrever provas formais para problemas IMO usando Lean oferece um grande potencial para trabalhos futuros em prova automatizada de teoremas. Embora a jornada seja complexa e cheia de obstáculos inesperados, cada passo dado nos aproxima de uma compreensão mais profunda de como a IA pode ajudar no mundo da matemática.

À medida que os pesquisadores continuam a refinar seus métodos e melhorar as capacidades dos modelos, em breve podemos ver sistemas de IA que podem lidar efetivamente com os problemas desafiadores das competições matemáticas-ou pelo menos se aproximar o suficiente para não passar vergonha diante da comunidade matemática. Quem sabe? Um dia, podemos ter uma IA que possa arrasar na Olimpíada de Matemática, mas até lá, teremos que continuar praticando essas provas, um lema de cada vez.