Da Prata ao 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 apenas um ano. Após conquistar a medalha de prata na Olimpíada Internacional de Matemática (IMO) em 2024, seu sistema de IA conquistou a medalha de ouro em 2025. Esse rápido avanço destaca as crescentes capacidades da inteligência artificial em lidar com problemas complexos e abstratos que exigem criatividade e insights semelhantes aos humanos. Este artigo explicará como a DeepMind alcançou essa transformação, as escolhas técnicas e estratégicas por trás dela e as implicações mais amplas desses avanços.

A importância da OMI

A Olimpíada Internacional de Matemática, fundada em 1959, é reconhecida mundialmente como a principal competição de matemática para estudantes do ensino médio. A cada ano, os melhores alunos do mundo enfrentam seis problemas desafiadores em álgebra, geometria, teoria dos números e combinatória. Resolver esses problemas exige muito mais do que cálculos; os participantes devem demonstrar criatividade matemática genuína, raciocínio lógico rigoroso e a capacidade de construir provas elegantes.

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

A conquista da medalha de prata em 2024

Em 2024, a DeepMind introduzido 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ólico”IA, combinando os pontos fortes dos grandes modelos de linguagem (LLMs) com o rigor da lógica simbólica.

AlphaProof foi projetado para provar afirmações matemáticas usando Lean, uma linguagem matemática formal. Ela combinava Gemini, o grande modelo de linguagem da DeepMind, com AlfaZero, um mecanismo de aprendizado por reforço conhecido por seu sucesso em jogos de tabuleiro. Nesse cenário, o papel do Gemini era traduzir problemas de linguagem natural para Lean e tentar comprová-los gerando etapas lógicas. O AlphaProof foi treinado em milhões de problemas de amostra, abrangendo diferentes disciplinas e dificuldades matemáticas. O sistema se aprimorou ao tentar comprovar afirmações cada vez mais complexas, semelhante a como o AlphaZero aprendia jogando contra si mesmo.

AlfaGeometria 2 foi projetado para resolver problemas de geometria. Aqui, a compreensão da linguagem do Gemini permitiu que a IA previsse construções auxiliares úteis, enquanto um mecanismo de raciocínio simbólico gerenciava as deduções lógicas. Essa abordagem híbrida permitiu AlfaGeometria para abordar problemas geométricos muito além do escopo do raciocínio tradicional das máquinas.

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 teve alcançado o nível de medalha de prata na IMO. No entanto, esse sucesso dependia fortemente de especialistas humanos para traduzir problemas em linguagens matemáticas formais. Eles também exigiam recursos computacionais massivos, o que levava dias de processamento para cada problema.

Inovações técnicas por trás da medalha de ouro

A transição da DeepMind de uma prata para uma medalha de ouro o desempenho foi impulsionado por diversas melhorias técnicas significativas.

1. A linguagem natural como meio para provas

A mudança mais significativa foi a transição de sistemas que exigiam traduções especializadas para linguagens formais para o tratamento da linguagem natural como meio para demonstrações. Essa mudança é alcançada por meio de uma versão aprimorada do Gemini. equipado com Capacidades de 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. Aprendizado por reforço a partir de feedback humano (RLHF) foi usado para recompensar soluções que fossem logicamente consistentes, breves e bem 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. Segundo, ele utiliza raciocínio paralelo, onde centenas de threads especulativos são gerados para diferentes soluções potenciais. Um supervisor leve então classifica e promove os caminhos mais promissores, tomando emprestados conceitos de Pesquisa em árvore Monte Carlo mas aplicada ao texto. Essa abordagem imita como equipes humanas fazem brainstorming, descartam ideias improdutivas e convergem para soluções elegantes.

2. Treinamento e Aprendizagem por Reforço

O treinamento do Gemini Deep Think envolveu o ajuste fino do modelo para prever os próximos passos em vez das respostas finais. Para isso, foi compilado um corpus com 100,000 soluções de alta qualidade para olimpíadas e concursos de graduação. O corpus foi coletado principalmente de fóruns públicos de matemática, pré-impressões do arXiv e conjuntos de problemas de faculdade. Mentores humanos revisaram os exemplos de treinamento para filtrar provas ilógicas ou incompletas. O aprendizado por reforço ajudou a refinar o modelo, levando-o a produzir provas concisas e precisas. As primeiras versões produziam provas excessivamente detalhadas, mas as penalidades por frases redundantes ajudaram a reduzir a produção.

Ao contrário do ajuste fino convencional, que frequentemente enfrenta dificuldades com recompensas esparsas em que o feedback é binário, ou a prova está correta ou não. A DeepMind implementou um sistema de recompensas gradual, em que cada sublema verificado contribui para a pontuação geral. Esse mecanismo de recompensa guia o Gemini mesmo quando a prova completa é rara. O processo de treinamento durou três meses e utilizou aproximadamente 25 milhões de horas TPU.

3. Paralelização Massiva

A paralelização também desempenhou um papel crucial na evolução da DeepMind, da categoria prata para a categoria ouro. Cada problema gerava múltiplas ramificações de raciocínio em paralelo, com recursos migrando dinamicamente para caminhos mais promissores quando outros estagnavam. Esse escalonamento dinâmico foi particularmente benéfico para problemas combinatórios, que possuem grandes espaços de solução. A abordagem é semelhante à que humanos usam para testar desigualdades auxiliares antes de se comprometerem com uma indução completa. Embora essa técnica fosse computacionalmente dispendiosa, era administrá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 o vazamento de problemas oficiais para o conjunto de treinamento. Eles também filtraram dados contendo soluções para questões olímpicas inéditas.

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

O Gemini Deep Think obteve notas máximas nos cinco primeiros problemas. A questão final, que era um quebra-cabeça combinatório desafiador, no entanto, surpreendeu tanto a IA quanto 94% dos participantes humanos. Apesar disso, a IA terminou com uma pontuação total de 35/42, garantindo a medalha de ouro. Essa pontuação foi sete pontos a mais que a prata do ano anterior. Observadores posteriormente descreveram as provas da IA ​​como "diligentes" e "completas", observando que elas seguiram as rigorosas justificativas esperadas de competidores humanos.

Implicações para IA e Matemática

A conquista da DeepMind é um marco significativo tanto para a IA quanto para a matemática. Para a IA, dominar a IMO é um passo em direção à inteligência artificial geral (IAG), onde os sistemas podem executar qualquer tarefa intelectual que um humano possa. Resolver problemas matemáticos complexos requer raciocínio e compreensão, componentes fundamentais da inteligência geral. Esse sucesso indica que a IA está avançando em direção a habilidades cognitivas mais semelhantes às humanas.

Para a matemática, sistemas de IA como o Gemini Deep Think podem se tornar ferramentas inestimáveis para matemáticos. Eles podem auxiliar na exploração de novas áreas, na verificação de conjecturas e até mesmo na descoberta de novos teoremas. Ao automatizar os aspectos mais tediosos da construção de provas, a IA libera matemáticos humanos para se concentrarem em trabalhos conceituais de nível superior. Além disso, as técnicas desenvolvidas para esses sistemas de IA podem inspirar novos métodos de pesquisa matemática que talvez não fossem possíveis apenas com o esforço humano.

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 seu envolvimento pode alterar a natureza da educação e das competições matemáticas.

Olhando para o futuro

Conquistar o ouro da OMI é um marco significativo, mas muitos desafios matemáticos ainda permanecem fora do alcance dos sistemas de IA atuais. No entanto, o rápido avanço da prata para o ouro em apenas um ano destaca o ritmo acelerado das inovações e desenvolvimentos em IA. Se esse ritmo continuar, os sistemas de IA poderão em breve resolver alguns dos problemas não resolvidos mais famosos da matemática. Embora a questão de se a IA substituirá ou aprimorará a criatividade humana permaneça sem resposta, a OMI de 2025 é uma indicação clara de que a inteligência artificial fez avanços significativos no raciocínio lógico.