Um novo estudo da ETH Zurich e do INSAIT mostrou que os modelos atuais de IA que simulam o raciocínio e resolvem de forma confiável problemas matemáticos padrão são quase incapazes de formular provas completas no nível da Olimpíada de Matemática dos Estados Unidos (USAMO) de 2025. Esses resultados questionam a possibilidade de raciocínio matemático profundo em modelos modernos de IA.
Fonte da imagem: Imkara Visual / Unsplash
Em março de 2025, uma equipe de pesquisa da ETH Zurique e do Instituto de Ciência da Computação, Inteligência Artificial e Tecnologia (INSAIT) da Universidade de Sófia, liderada por Ivo Petrov e Martin Vechev, publicou um preprint de um artigo científico intitulado “Prova ou Blefe? Avaliando LLMs na Olimpíada de Matemática dos EUA de 2025”. O trabalho visa avaliar a capacidade de modelos de grandes linguagens (LLMs) que simulam o raciocínio de gerar provas matemáticas completas para problemas de Olimpíada.
Seis problemas do USAMO de 2025, organizado pela Mathematical Association of America, foram usados para a análise. Os modelos de IA foram testados imediatamente após a publicação das tarefas para minimizar o risco de vazamento de dados nas amostras de treinamento. O desempenho médio em todos os modelos de IA na geração de evidências completas foi inferior a 5% da pontuação máxima possível. Os sistemas foram avaliados em uma escala de 0 a 7 pontos por tarefa, levando em consideração créditos parciais dados por especialistas. Apenas um modelo, o Gemini 2.5 Pro do Google, teve um desempenho significativamente melhor, marcando 10,1 de 42 pontos possíveis, o equivalente a cerca de 24%. Os outros modelos ficaram significativamente atrás: DeepSeek R1 e Grok 3 receberam 2,0 pontos cada, Gemini Flash Thinking – 1,8 pontos, Claude 3.7 Sonnet – 1,5 pontos, Qwen QwQ e OpenAI o1-pro – 1,2 pontos cada. O modelo de IA o3-mini-high da OpenAI obteve apenas 0,9. Das quase 200 soluções geradas, nenhuma recebeu nota máxima.
O estudo destaca uma diferença fundamental entre resolver problemas e construir provas matemáticas. Problemas padrão, como calcular o valor de uma expressão ou encontrar uma variável, exigem apenas uma resposta correta final. Em contraste, as provas exigem argumentação lógica consistente que explique a verdade de uma afirmação para todos os casos possíveis. Essa diferença qualitativa torna os problemas do nível USAMO significativamente mais exigentes em termos de profundidade de raciocínio.
Captura de tela da Tarefa nº 1 do USAMO 2025 e sua solução no site AoPSOnline. Fonte da imagem: AoPSOnline
Os autores do estudo identificaram padrões de erro característicos no trabalho da IA. Uma delas era a incapacidade de manter conexões lógicas corretas ao longo de toda a cadeia de inferência. No exemplo do Problema 5 do USAMO de 2025, os modelos de IA foram solicitados a encontrar todos os valores naturais de k para os quais uma certa soma de coeficientes binomiais elevada à k-ésima potência permanece um inteiro para qualquer n positivo. O modelo Qwen QwQ cometeu um erro grosseiro ao excluir possíveis valores não inteiros permitidos pelas condições do problema, o que levou a uma conclusão final incorreta apesar da definição correta das condições nos estágios intermediários.
Uma característica do comportamento dos modelos era que, mesmo em caso de erros lógicos graves, eles formulavam suas decisões de forma afirmativa, sem quaisquer sinais de dúvida ou indícios de possíveis contradições. Essa propriedade de simular o raciocínio indica a ausência de mecanismos internos de autoverificação e correção de saída em modelos de IA.
Métricas de precisão para modelos de IA em cada tarefa do USAMO 2025. Fonte da imagem: MathArena
Apesar das limitações identificadas, a implementação de métodos de cadeia de pensamento e raciocínio simulado teve um efeito positivo na formação de etapas lógicas intermediárias no processo de inferência de modelos de IA. O mecanismo de escalonamento computacional do estágio de inferência permite que a IA construa um raciocínio local mais coerente. Entretanto, um problema fundamental permanece: os modernos modelos de grandes linguagens (LLMs) na arquitetura Transformer continuam a operar como sistemas de reconhecimento de padrões, em vez de sistemas autônomos de raciocínio conceitual.
O desempenho aprimorado do modelo Gemini 2.5 Pro sugere o potencial de diminuir a lacuna entre o raciocínio simulado e o real no futuro. No entanto, para alcançar progresso qualitativo, é necessário treinar modelos de IA em conexões multidimensionais mais profundas no espaço latente e dominar os princípios de construção de novas estruturas lógicas, e não apenas copiar padrões existentes de amostras de treinamento.