De Prata a Ouro: Como a IA da DeepMind Conquistou a Olimpíada de Matemática

A IA da DeepMind fez um progresso notável no raciocínio matemático em um curto período de apenas um ano.  Depois de ganhar uma medalha de prata na Olimpíada Internacional de Matemática (IMO) em 2024, o sistema de IA da empresa conquistou a medalha de ouro em 2025. Essa rápida evolução destaca as crescentes capacidades da inteligência artificial em lidar com problemas complexos e abstratos que exigem criatividade e insights humanos. Este artigo irá mostrar como a DeepMind alcançou essa transformação, as escolhas técnicas e estratégicas por trás disso e as implicações mais amplas desses avanços.

A Importância da IMO

A Olimpíada Internacional de Matemática, estabelecida em 1959, é reconhecida globalmente como a principal competição de matemática para estudantes do ensino médio. Todos os anos, os melhores estudantes de todo o mundo enfrentam seis problemas desafiadores em álgebra, geometria, teoria dos números e combinação. Resolver esses problemas exige muito mais do que cálculos; os participantes devem mostrar criatividade matemática real, pensamento lógico rigoroso e a capacidade de construir provas elegantes.

Para a inteligência artificial, a IMO apresenta um desafio único. Embora a IA tenha dominado o reconhecimento de padrões, análise de dados e até mesmo jogos complexos como Go e xadrez, a matemática olímpica exige raciocínio criativo e abstrato e a síntese de novas ideias, habilidades tradicionalmente consideradas marcas da inteligência humana. Como resultado, a IMO se tornou um local de teste natural para avaliar quão perto a IA está de alcançar um raciocínio verdadeiramente humano.

A Quebra da Medalha de Prata de 2024

Em 2024, a DeepMind apresentou dois sistemas de IA para lidar com problemas de nível IMO: AlphaProof e AlphaGeometry 2. Ambos os sistemas são exemplos de “neuro-simbólica” IA, combinando as forças de grandes modelos de linguagem (LLMs) com a rigidez da lógica simbólica.

AlphaProof foi projetado para provar declarações matemáticas usando Lean, uma linguagem matemática formal. Ele combinou Gemini, o grande modelo de linguagem da DeepMind, com AlphaZero, que é um motor de aprendizado por reforço conhecido por seu sucesso em jogos de tabuleiro. Nesse cenário, o papel de Gemini era traduzir problemas de linguagem natural para Lean e tentar provas gerando etapas lógicas. O AlphaProof foi treinado em milhões de problemas de amostra que abrangem diferentes disciplinas matemáticas e dificuldades. O sistema melhorou a si mesmo tentando provar declarações cada vez mais complexas, semelhante à forma como o AlphaZero aprendeu jogando jogos contra si mesmo.

AlphaGeometry 2 foi projetado para resolver problemas de geometria. Aqui, a compreensão da linguagem de Gemini permitiu que a IA predissesse construções auxiliares úteis, enquanto um motor de raciocínio simbólico gerenciava as deduções lógicas. Essa abordagem híbrida permitiu que o AlphaGeometry lidasse com problemas geométricos bem além do alcance do raciocínio tradicional da máquina.

Juntos, esses sistemas resolveram quatro dos seis problemas da IMO: dois em álgebra, um em teoria dos números e um em geometria, alcançando uma pontuação de 28 em 42. Esse desempenho foi um marco significativo, pois foi a primeira vez que uma IA atingiu o nível de medalha de prata na IMO. No entanto, esse sucesso dependeu fortemente de especialistas humanos para traduzir problemas em linguagens matemáticas formais. Eles também exigiram recursos computacionais massivos, que levaram dias de tempo de processamento para cada problema.

Inovações Técnicas por trás da Medalha de Ouro

A transição da DeepMind de uma performance de medalha de prata para uma performance de medalha de ouro foi impulsionada por várias melhorias técnicas significativas.

1. Linguagem Natural como Meio para Provas

A mudança mais significativa foi a transição de sistemas que exigiam traduções de especialistas em linguagens formais para tratar a linguagem natural como o meio para provas. Essa mudança foi alcançada por meio de uma versão aprimorada do Gemini equipada com capacidades Deep Think. Em vez de converter problemas em Lean, o modelo processa o texto diretamente, gera esboços informais, formaliza internamente etapas críticas e produz uma prova refinada em inglês. O aprendizado por reforço a partir de feedback humano (RLHF) foi usado para recompensar soluções que eram logicamente consistentes, breves e apresentadas.

O Gemini Deep Think difere da versão pública do Gemini em dois aspectos principais. Primeiro, ele aloca janelas de contexto mais longas e mais tokens de computação por consulta, o que permite que o modelo mantenha cadeias de pensamento de várias páginas. Em segundo lugar, ele usa raciocínio paralelo, onde centenas de threads especulativas são geradas para diferentes soluções potenciais. Um supervisor leve então classifica e promove os caminhos mais promissores, emprestando conceitos da busca em árvore de Monte Carlo mas aplicados a texto. Essa abordagem imita como equipes humanas brainstorm, descartam ideias improdutivas e convergem para soluções elegantes.

2. Treinamento e Aprendizado por Reforço

O treinamento do Gemini Deep Think envolveu ajustar o modelo para prever as próximas etapas em vez de respostas finais. Para esse propósito, um corpus de 100.000 soluções de alta qualidade de competições de matemática e olímpicas foi compilado. O corpus foi principalmente coletado de fóruns de matemática públicos, pré-impressões do arXiv e conjuntos de problemas de faculdade. Mentores humanos revisaram exemplos de treinamento para filtrar provas ilógicas ou incompletas. O aprendizado por reforço ajudou a refinar o modelo, empurrando-o em direção à produção de provas concisas e precisas. Versões iniciais produziram provas verbosas demais, mas penalidades em frases redundantes ajudaram a cortar a saída.

Ao contrário do ajuste convencional, que frequentemente luta com recompensas esparsas, onde o feedback é binário, ou a prova é correta ou não. A DeepMind implementou um sistema de recompensa passo a passo, onde cada sub-lemma verificado contribuiu para a pontuação geral. Esse mecanismo de recompensa orienta o Gemini, mesmo quando a prova completa é infrequente. O processo de treinamento durou três meses e utilizou aproximadamente 25 milhões de horas de TPU.

3. Paralelização Maciça

A paralelização também desempenhou um papel crítico no avanço da DeepMind de prata para ouro. Cada problema gerou múltiplas ramificações de raciocínio em paralelo, com recursos dinamicamente mudando para avenidas mais promissoras quando outras estagnavam. Essa programação dinâmica foi particularmente benéfica para problemas de combinação, que têm grandes espaços de solução. A abordagem é semelhante à forma como os humanos testam desigualdades auxiliares antes de se comprometer com uma indução completa. Embora essa técnica fosse computacionalmente cara, foi gerenciável usando os clusters TPU v5 da DeepMind.

DeepMind na IMO 2025

Para manter a integridade da competição, a DeepMind congelou os pesos do modelo três semanas antes da IMO para evitar a fuga de problemas oficiais para o conjunto de treinamento. Eles também filtraram os dados que continham soluções para questões olímpicas não publicadas anteriormente.

Durante a competição, o Gemini Deep Think foi fornecido com os seis problemas oficiais em formato de texto puro, sem acesso à internet. O sistema operou em um cluster configurado para simular o poder computacional de um laptop padrão por processo. O processo de resolução de problemas foi concluído em menos de três horas, bem dentro dos limites de tempo. As provas geradas foram submetidas aos coordenadores da IMO sem alterações.

O Gemini Deep Think obteve pontuações perfeitas nos cinco primeiros problemas. A última questão, que era um quebra-cabeça de combinação desafiador, no entanto, enganou tanto a IA quanto 94% dos participantes humanos. Apesar disso, a IA terminou com uma pontuação total de 35/42 para garantir a medalha de ouro. Essa pontuação foi sete pontos mais alta do que a performance de prata do ano anterior. Observadores mais tarde descreveram as provas da IA como ‘diligentes’ e ‘completas’, observando que elas seguiram as justificativas rigorosas esperadas dos concorrentes humanos.

Implicações para a IA e a Matemática

O feito da DeepMind é um marco significativo para a IA e a matemática. Para a IA, dominar a IMO é um passo em direção à inteligência artificial geral (IAG), onde os sistemas podem realizar qualquer tarefa intelectual que um humano possa. Resolver problemas matemáticos complexos exige raciocínio e compreensão, que são componentes fundamentais da inteligência geral. Esse sucesso indica que a IA está fazendo progressos em direção a capacidades cognitivas mais humanas.

Para a matemática, sistemas de IA como o Gemini Deep Think podem se tornar ferramentas inestimáveis para os matemáticos. Eles podem ajudar a explorar novas áreas, verificar conjecturas e até descobrir novos teoremas. Ao automatizar os aspectos mais tediosos da construção de provas, a IA libera os matemáticos humanos para se concentrar em trabalho conceitual de nível superior. Além disso, as técnicas desenvolvidas para esses sistemas de IA podem inspirar novos métodos em pesquisa matemática que podem não ser possíveis por meio do esforço humano sozinho.

No entanto, o progresso da IA na matemática também levanta questões sobre o papel da IA em ambientes educacionais e competições. À medida que as capacidades da IA continuam a crescer, haverá debates sobre como a participação da IA pode alterar a natureza da educação e competição matemática.

Olhando para o Futuro

Ganhar a medalha de ouro da IMO é um marco significativo, mas muitos desafios matemáticos ainda estão fora do alcance dos sistemas de IA atuais. No entanto, a rápida evolução de prata para ouro em apenas um ano destaca o ritmo acelerado das inovações e desenvolvimentos da IA. Se esse ritmo continuar, os sistemas de IA podem em breve lidar com alguns dos problemas matemáticos mais famosos não resolvidos. Embora a questão de a IA substituir ou melhorar a criatividade humana permaneça sem resposta, a IMO de 2025 é um claro indicador de que a inteligência artificial fez progressos significativos no raciocínio lógico. ments. Se esse ritmo continuar, os sistemas de IA podem em breve lidar com alguns dos problemas matemáticos mais famosos não resolvidos. Embora a questão de a IA substituir ou melhorar a criatividade humana permaneça sem resposta, a IMO de 2025 é um claro indicador de que a inteligência artificial fez progressos significativos no raciocínio lógico.