A visão de um matemático sobre a capacidade matemática da IA

• O novo modelo de linguagem o3 da OpenAI marcou 25% no difícil benchmark de matemática FrontierMath, reacendendo a dúvida sobre se a IA matemática pode ultrapassar o nível de graduação
• O FrontierMath é um conjunto de dados privado criado pela Epoch AI, composto por centenas de problemas difíceis de matemática que exigem respostas numéricas verificáveis automaticamente, em vez de “provas de teoremas”
• As 5 amostras públicas não eram fáceis nem para matemáticos pesquisadores; Tao as classificou como “extremamente desafiadoras”, mas Borcherds considerou que produzir uma resposta numérica não é o mesmo que uma prova original
• Como Elliot Glazer, da Epoch AI, revelou que 25% dos problemas eram do tipo “IMO/estilo graduação”, é difícil confirmar, por causa da natureza privada do conjunto de dados, até que nível de dificuldade o resultado de 25% do o3 realmente chegou
• Para os matemáticos, o objetivo mais importante do que “encontre este número” é provar corretamente um teorema e explicá-lo de forma compreensível para humanos, e abordagens baseadas em modelos de linguagem e em Lean têm limitações diferentes

---

o3 e FrontierMath abalaram a linha de base

• o3 é o novo modelo de linguagem da OpenAI e obteve 25% no FrontierMath
• Desde o ChatGPT, os modelos de linguagem públicos vêm melhorando rapidamente, e sua capacidade de resolver problemas de matemática está sendo avaliada dentro desse movimento
• FrontierMath é um conjunto de dados privado de problemas de matemática criado pela Epoch AI; o resumo do artigo diz que ele contém “centenas” de problemas difíceis
• Se o conjunto de dados for tornado público, os modelos de linguagem podem aprender os problemas e as respostas, por isso até informações básicas, como o número de questões, estão sendo tratadas com cautela
  • Se problemas e respostas forem divulgados, o modelo pode simplesmente reproduzir respostas que já viu
  • Por isso, é difícil verificar de fora a dificuldade real e a representatividade de um benchmark privado

Formato e dificuldade dos problemas do FrontierMath

• Os problemas do FrontierMath são mais próximos do formato “encontre este número” do que de “prove este teorema”
• Os problemas precisam ter respostas claras e computáveis, e sua verificação deve ser automática
• As respostas das 5 questões de amostra divulgadas são todas inteiros positivos
  • Entre os exemplos de resposta estão 9811 e 367707
  • As outras três respostas são maiores, projetadas para dificultar acertos por chute aleatório
• As amostras públicas não são triviais nem para matemáticos pesquisadores
  • O autor afirma que entendeu os enunciados das 5 questões
  • A terceira questão pôde ser resolvida relativamente rápido, e para a quinta ele conhecia um método padrão usando as Weil conjectures for curves, mas não calculou a resposta de 13 dígitos
  • Ele julgou não conseguir resolver a primeira e a segunda, e achou que talvez pudesse avançar na quarta com esforço, mas leu a solução sem tentar
• Um aluno de graduação de matemática inteligente, em geral, pode ter dificuldade para resolver sequer uma dessas questões
  • A primeira questão provavelmente exigiria nível de doutorado ou superior em teoria analítica dos números

Vantagens e limites de benchmarks com resposta numérica

• O principal motivo de o FrontierMath usar problemas com resposta numérica é o custo de correção
• Para avaliar centenas de respostas do tipo “prove este teorema”, seria preciso contar com especialistas humanos
  • Em 2024, considera-se difícil delegar esse nível de correção a máquinas
• Já uma lista de respostas numéricas pode ser comparada muito rapidamente por um computador
• Borcherds considera que matemáticos pesquisadores passam a maior parte do tempo buscando provas e ideias, e não números
• Ainda assim, o FrontierMath tem valor na área de IA matemática
  • Há escassez extrema de conjuntos de dados difíceis
  • Criar conjuntos assim é muito difícil ou muito caro
  • Um texto recente de Frieder e outros discute mais profundamente as limitações dos conjuntos de dados de IA matemática

Por que os 25% do o3 surpreenderam

• A percepção anterior era de que a IA matemática estava mais próxima do nível de graduação ou anterior à graduação
• A IA está ficando muito forte em problemas de olimpíada resolvidos por estudantes brilhantes do ensino médio
• Parece claro que, dentro de um ano, a IA conseguirá passar em provas de matemática de graduação
  • Provas de graduação às vezes incluem problemas padronizados que um aluno com entendimento básico do curso consegue resolver
  • Máquinas podem acertar esse tipo de problema com facilidade
• Mas o salto além da reutilização de ideias padronizadas rumo a ideias inovadoras de nível avançado de graduação ou início de doutorado parece grande
• Respostas recentes do ChatGPT para a prova Putnam ficaram aquém do esperado
  • Apenas a questão B4 pareceu ter sido respondida de forma apropriada pela máquina
  • A maioria das outras respostas foi vista como algo entre 1 e 2 pontos em 10
• Por isso, esperava-se que o FrontierMath fosse praticamente inalcançável por alguns anos

A incerteza deixada por um conjunto de dados privado

• Elliot Glazer, da Epoch AI, declarou no Reddit que 25% dos problemas do FrontierMath eram do tipo IMO/estilo graduação
• Essa afirmação não parece combinar bem com as 5 questões públicas
  • Até a mais fácil das amostras públicas envolvia uma abordagem com as Weil conjectures for curves
  • Ou então poderia exigir uma dolorosa busca exaustiva para fatorar um polinômio cúbico de grau 10^12 sobre um corpo finito
• Essa informação deixa dúvidas sobre a dificuldade real do conjunto de dados privado e se as 5 questões públicas são uma amostra representativa
• Como o conjunto de dados é privado, essas dúvidas não são fáceis de verificar
• Se 25% forem problemas de nível de graduação, então os 25% do o3 podem ser menos surpreendentes
• O grande avanço esperado seria o momento em que a IA mostrar desempenho significativo nos 50% seguintes de problemas descritos como nível de “qual”

“Prove este teorema” continua sendo outro problema

• Na pesquisa em matemática, a pergunta importante costuma ser “prove este teorema”
• Mesmo que surjam máquinas com desempenho sobre-humano em problemas de encontrar números, sua aplicabilidade pode continuar limitada em muitas áreas da matemática de pesquisa
• O maior caso de sucesso de 2024 é apontado como o AlphaProof da DeepMind
  • O AlphaProof resolveu 4 dos 6 problemas da IMO 2024
  • Os problemas eram do tipo “prove este teorema” ou “encontre o número e prove que ele está correto”
  • Três deles foram produzidos como provas totalmente formalizadas em Lean
• Lean é um provador de teoremas interativo, e o mathlib é uma biblioteca matemática que inclui várias técnicas necessárias para resolver problemas da IMO e mais
• As soluções do sistema da DeepMind foram verificadas por humanos e validadas como respostas de “nota máxima”
• Ainda assim, embora os problemas da IMO sejam muito difíceis, suas soluções usam apenas técnicas de nível escolar, o que significa uma volta a problemas de nível de ensino médio
• A expectativa é que em 2025 as máquinas mostrem desempenho de nível de medalha de ouro na IMO

Quem vai corrigir as respostas da máquina?

• É possível imaginar que, em julho de 2025, na IMO, não apenas estudantes humanos, mas também máquinas participem
• Os sistemas de máquina podem se dividir em dois tipos
  • Sistemas que enviam respostas em linguagens de verificação de prova por computador, como Lean, Rocq e Isabelle
  • Modelos de linguagem que enviam respostas em linguagem humana
• Respostas enviadas em linguagem de verificador de provas exigem apenas confirmar se o enunciado foi traduzido corretamente
  • Depois disso, se a prova compilar, já se sabe na prática que é uma resposta de “nota máxima”
• Já modelos de linguagem que enviam respostas em linguagem natural são diferentes
  • Mesmo que a resposta pareça plausível, um corretor humano precisa lê-la e avaliá-la com cuidado
  • Não há garantia de que seja uma resposta de nota máxima
• Considera-se que os modelos de linguagem ainda são pelo menos uma ordem de grandeza menos precisos do que especialistas humanos em raciocínio lógico
• Há a preocupação de que uma “prova” do modelo de linguagem para a hipótese de Riemann possa misturar afirmações ambíguas ou imprecisas no meio de 10 páginas de matemática correta
• Já os provadores de teoremas, ao contrário, seriam pelo menos uma ordem de grandeza mais precisos
  • Nos casos vistos pelo autor em que o Lean não aceitou um argumento da literatura matemática humana, o lado humano estava errado

Objetivo restante: prova correta e compreensão humana

• O que os matemáticos querem não é apenas “prove este teorema”, mas uma prova correta e uma explicação compreensível para humanos
• Na abordagem com modelos de linguagem, a “correção” continua sendo a grande preocupação
• Na abordagem com provadores de teoremas, a preocupação é se isso ocorre de um modo compreensível para humanos
• Ainda há muito trabalho a fazer
• O ritmo de progresso é rápido, mas ninguém sabe quando a barreira da graduação será superada