- O modelo Gemini Deep Think do Google DeepMind atingiu a pontuação de medalha de ouro (35 pontos) na Olimpíada Internacional de Matemática (IMO) de 2025
- O modelo resolveu perfeitamente 5 dos 6 problemas e teve soluções matemáticas claras e precisas reconhecidas pela banca oficial de correção da IMO
- Representa um grande salto em relação ao nível de medalha de prata do ano passado (28 pontos) com AlphaProof e AlphaGeometry 2, compreendendo problemas oficiais em linguagem natural e concluindo provas como um humano em 4,5 horas
- O modo Deep Think aplica parallel thinking e aprendizado por reforço de ponta para explorar e combinar várias soluções ao mesmo tempo, sendo otimizado para resolver problemas no estilo da IMO
- O Google planeja ampliar a colaboração com matemáticos e avançar no desenvolvimento de uma próxima geração de AGI que combine raciocínio matemático e verificação formal
Breakthrough Performance at IMO 2025 with Gemini Deep Think
- O Gemini Deep Think do Google DeepMind recebeu 35 pontos no total (5 soluções perfeitas em 6 problemas) na Olimpíada Internacional de Matemática (IMO) de 2025, atingindo oficialmente o padrão de medalha de ouro
- A banca oficial de correção da IMO avaliou muito bem a clareza, precisão e facilidade de compreensão das soluções, e o presidente da IMO, Prof. Dr. Gregor Dolinar, publicou uma declaração oficial afirmando: "Confirmo que o Google DeepMind atingiu a pontuação de 35 pontos de medalha de ouro"
- No ano passado, AlphaGeometry e AlphaProof exigiam que especialistas traduzissem os problemas de linguagem natural para linguagens específicas de domínio (como Lean), e os cálculos levavam mais de dois dias. Neste ano, o Gemini concluiu todo o processo, da compreensão do problema à redação da prova, com base em linguagem natural e dentro do tempo da competição da IMO (4,5 horas)
Making the most of Deep Think mode
- O Gemini Deep Think é um modo de raciocínio aprimorado que aplica técnicas de pesquisa de ponta, como parallel thinking, explorando simultaneamente vários caminhos de solução para chegar à resposta ideal
- O modelo foi treinado com técnicas de aprendizado por reforço para resolver problemas matemáticos complexos e com diversos dados de provas no estilo da IMO, além de receber dicas e orientações gerais sobre abordagens para problemas da IMO
- Está previsto que uma versão de teste desse modelo Deep Think seja oferecida primeiro a alguns matemáticos e especialistas de confiança, com lançamento posterior para assinantes do Google AI Ultra
The Future of AI and Mathematics
- O Google DeepMind continua sua colaboração com a comunidade matemática e, além do raciocínio baseado em linguagem natural, também mantém pesquisas baseadas em sistemas formais como AlphaGeometry e AlphaProof
- No futuro, espera-se que uma IA que combine compreensão de linguagem natural e capacidade de raciocínio matemático formal e verificável se torne uma ferramenta central em matemática, ciência, engenharia e pesquisa
- O DeepMind avalia este resultado como um avanço importante no caminho rumo à AGI (inteligência artificial geral) e pretende enfrentar problemas matemáticos ainda mais complexos e de nível mais alto no futuro
Verificação das respostas e posição oficial da IMO
- O comitê organizador da IMO confirmou oficialmente que as respostas enviadas eram soluções completas e corretas
- No entanto, a IMO especificou que sua análise não inclui a validação do sistema, do processo ou do modelo base em si
- Para mais detalhes e para evitar interpretações ampliadas, consulte a declaração oficial da IMO (ver mais)
5 comentários
OpenAI anuncia desempenho de nível medalha de ouro na Olimpíada Internacional de Matemática (IMO) de 2025
Como a OpenAI anunciou isso primeiro há 2 dias, o impacto acabou sendo menor, e também vi comentários dizendo que foi falta de etiqueta o Alexander Wei, da OpenAI, ter falado antes sem sequer discutir com a IMO.
Como nem houve reconhecimento oficial por parte da IMO e eles já saíram anunciando, disseram também que isso acabou roubando as comemorações e o mérito dos participantes humanos, e não da IA.
Ou seja, graças a isso, a OAI ficou numa situação em que apenas o próprio painel dela validou, sem nem sequer receber a correção oficial da IMO. Além disso, vendo que muita gente considera que a qualidade das respostas do Gemini foi um pouco melhor... parece uma situação ainda mais constrangedora. Não assumir risco de reputação e, se der certo, anunciar; mas, se o resultado for ruim, cair fora (ainda por cima numa situação sem correção oficial), pode até ser aceitável em benchmark, mas não me parece a postura correta para mostrar numa competição em que os participantes competem colocando o próprio nome em jogo.
Mesmo que o desempenho dos LLMs do Google e da OpenAI seja mais ou menos equivalente, é aqui que aparece a diferença de experiência empresarial.
Comentários do Hacker News
AlphaGeometry e AlphaProof passavam por um processo de primeiro traduzir problemas em linguagem natural para uma linguagem específica de domínio como Lean e, depois, converter novamente o resultado da prova para linguagem natural, e os cálculos levavam de 2 a 3 dias; já o modelo Gemini deste ano usou uma abordagem end-to-end que gera diretamente a prova matemática a partir da descrição oficial do problema apenas em linguagem natural, ou seja, sem traduzir primeiro para Lean. Ainda assim, não está claro se internamente usou ferramentas como Lean, busca na internet, calculadora, Python etc. A OpenAI disse que em seu modelo essas ferramentas não foram usadas, mas não sei se essa afirmação vale exatamente para o Gemini também. Também queria saber a ordem de grandeza do uso de computação, ou seja, do custo, de cada sistema. Se o preço for enorme, isso significa que ainda é pouco prático. Como ainda não há informação pública, suponho que seja extremamente caro. E compartilham um link dizendo que foi confirmado “sem uso de ferramentas, sem conexão com a internet” https://x.com/FredZhang0/status/1947364744412758305
O modelo Gemini deste ano gera provas matemáticas diretamente a partir da descrição oficial do problema usando apenas linguagem natural, e todo o processo ocorreu dentro das 4,5 horas da competição, sem uso de ferramentas externas
Oficialmente dizem que ferramentas de verificação formal como Lean não são usadas para de fato resolver os problemas da IMO, mas fico curioso se elas são usadas durante o treinamento do modelo. No trabalho da Google sobre a IMO de 2024, existe uma técnica para converter provas em linguagem natural para uma linguagem formal verificável. Acho que o próximo passo natural seria usar isso em treinamento RLVR (verification-reward via reinforcement learning). Se todo raciocínio gerado por um LLM matemático pudesse ser traduzido e verificado para servir de sinal de recompensa, o sinal de recompensa ficaria muito mais denso. Conseguir uma prova formal perfeita ainda seria difícil, mas isso seria útil para orientar o modelo a evitar raciocínios errados ou frases impossíveis de interpretar. Com uma quantidade gigantesca de computação, isso poderia viabilizar a resolução de problemas no nível da IMO. Sistemas como o AlphaProof já mostraram que é possível resolver problemas desse nível navegando de forma eficiente pelo espaço de raciocínio ao alternar entre provas em Lean e saídas de LLM. Penso se, ao pular a etapa intermediária e ensinar o LLM a imitar raciocínio formal via RLVR, não seria possível obter eficiência e capacidade de resolução semelhantes
Também fico curioso sobre por que não usar Lean. Isso significa que usar Lean hoje em dia deixa a resolução fácil demais, ou será que o próprio Lean vira um fator de atrito?
Também queria saber se “sem uso de ferramentas, sem conexão com a internet” significa que ele poderia realmente rodar offline sem a infraestrutura do Google, ou seja, talvez ser implantado localmente se necessário
Dizem que neste ano um modelo Gemini mais avançado gerou diretamente provas matemáticas a partir das descrições oficiais dos problemas apenas em linguagem natural, mas pessoalmente acho até lamentável esse afastamento das técnicas de formalização. Se quisermos de fato automatizar matemática, ou por exemplo chegar ao nível de produzir mecanicamente provas com milhares de páginas, não vejo outro caminho além da formalização. Caso contrário, continuaremos precisando de revisores humanos e não haverá uma forma real de confiar nas provas
Se um LLM consegue produzir uma prova rigorosa em linguagem natural, então provar em uma linguagem formal como Lean também não deveria ser tão difícil. No AlphaProof, o uso de Lean era bastante limitado e especializado em certos tipos de problema matemático. Em contraste, se o mesmo for alcançado com RL e linguagem natural, isso pode se expandir para várias áreas em que a verificação é difícil
Também compartilham que a DeepMind está atualmente reunindo repositórios que registram problemas formalizados ainda em aberto https://github.com/google-deepmind/formal-conjectures
Sou matemático, embora não faça mais pesquisa, e queria dar um pouco de contexto sobre por que muitos matemáticos são pouco entusiasmados com métodos formais. Na prática, para produzir uma prova com milhares de páginas, claro que sem formalização isso é impossível, e concordo que, para “confiar” em algo, é preciso verificar formalmente. Mas o que os matemáticos realmente querem, na prática, é uma explicação de por que o resultado é verdadeiro. O produto real não é uma resposta de sim ou não, e sim sua interpretação e razão. Por exemplo, todo mundo acha que a hipótese de Riemann provavelmente é verdadeira, mas ninguém está simplesmente esperando pela resposta certa. Há inclusive muitos resultados do tipo “se a hipótese de Riemann for verdadeira, então este novo teorema vale”. O que se espera de uma prova é fundamentalmente um insight novo ou uma forma de fornecer compreensão profunda sobre teoria dos números. Se algo como Lean apenas verifica formalmente que é verdadeiro, mas nenhum humano consegue sequer entender, isso quase não tem valor
Como a formalização precisa tende a ser mais fácil do que resolver o problema, também é possível primeiro resolver o problema e depois formalizá-lo para verificação
Problemas da IMO são, desde o início, projetados para que humanos os resolvam sem ferramentas. Se formos fazer modelos resolverem problemas mais difíceis, aí sim dá para fornecer ferramentas suficientes. Pelo menos reproduzir primeiro a capacidade em nível humano sem ferramentas me parece um bom caminho
Comparando as respostas da OpenAI e do Gemini, o estilo de escrita do Gemini parece muito mais claro. A apresentação poderia ser um pouco melhor, mas o conteúdo da prova em si é fácil de acompanhar, e é composto por frases mais curtas e organizadas do que a resposta da OpenAI
A prova do Google talvez seja, na verdade, um resultado resumido a posteriori, e é possível que parte do mecanismo, como Tree of Thoughts, também envolva esse processo de resumo. Não parece ser apenas o resultado de um comando simples e passivo de “dê a resposta final”
Os resultados mencionados das provas da IMO da OpenAI e do Google podem ser vistos respectivamente em PDF da prova do Google e repositório de exemplos de provas da OpenAI
Tanto a OpenAI quanto o Google enfatizaram que “todo o processo terminou dentro das 4,5 horas da competição”, mas fico em dúvida sobre a relevância real dessa limitação. Na prática, eles poderiam ter rodado milhões de processos de raciocínio em paralelo ao mesmo tempo para encontrar a prova. Claro, isso exigiria também muito uso de computação para um modelo avaliador julgar os resultados e selecionar a prova final a ser enviada. Pode ter consumido, de fato, centenas de anos de GPU. Ainda assim, é impressionante que esse método encontre a resposta e que a paralelização seja possível nesse grau. No fim, independentemente de AGI ser alcançada ou não com mais computação, o cérebro humano não escala assim com facilidade, então o resultado tem significado claro
É muito interessante a mudança do sistema especializado em Lean do ano passado para um LLM geral baseado em linguagem natural + RL. Imagino que essa abordagem também vá contribuir para ganhos de desempenho em áreas além das olimpíadas de matemática. Estou curioso para ver até onde isso pode se expandir, e também parece que este sistema não é tão diferente do modelo/recurso “DeepThink” que deve ser lançado no verão
Neste momento parece que estamos vivendo, na competição matemática com máquinas, um momento equivalente à era Deep Blue vs. Kasparov. Houve um avanço enorme em relação a poucos anos atrás, mas ainda acho que estamos muito longe de um verdadeiro matemático de IA. Mesmo assim, é uma época realmente impressionante para se estar vivo
Em um podcast recente, Terrence Tao também demonstrou grande interesse em trabalhar com essas ferramentas. Ele comentou que, por enquanto, a melhor forma de uso provavelmente é o humano definir ideias/parâmetros e o LLM fazer exploração, provas etc. em paralelo. A analogia com motores de xadrez também faz sentido: no passado, os melhores enxadristas eram apoiados por equipes de especialistas na análise, mas hoje supercomputadores e softwares analisam inúmeras posições, escolhem as melhores ideias e as entregam ao jogador
Acho que está mais para um confronto entre o Deep Blue e uma criança prodígio. Participantes da IMO não são matemáticos de elite, e sim estudantes do ensino médio
A diferença aqui é que não dá para obter pontuação alta dentro do tempo apenas com brute force. É um verdadeiro marco técnico, diferente do “em princípio era possível” da época do Deep Blue
O problema 6 é intrigante: nem OpenAI nem DeepMind conseguiram apresentar uma resposta. Humanos ao menos dão uma solução parcial, então é estranho a IA não dar resposta nenhuma. Isso levanta a dúvida se o LLM percebeu por conta própria que falhou em resolver. Uma das limitações dos LLMs é “não saber que não sabe”, e, sendo assim, acho quase impossível verificar consistência lógica sem um solver
Provavelmente é porque ele não terminou de “pensar” dentro do limite de tempo da competição e não chegou à etapa de “saída”
Essa limitação vale apenas para a geração de texto de um LLM pré-treinado no formato mais básico. Também seria possível treinar adicionalmente um linear probe (uma camada simples de rede neural) para produzir um confidence score. Claro que isso não seria 100% confiável, mas ao menos em um domínio restrito como matemática talvez fosse bastante confiável
Sem ferramentas de verificação formal, ainda pode ser arriscado demais usar isso na prática. O antigo o3, embora não seja o mais recente, era forte em encontrar boas referências e propor novas desigualdades. Mas na etapa de prova propriamente dita, podia produzir respostas com aparência convincente, porém contendo proposições erradas nos detalhes ou erros algébricos. Quanto melhor o modelo fica, mais difícil pode ser encontrar esses erros sutis
Fico curioso sobre por que eles enfatizam tanto que não usaram um provador de teoremas. No fim das contas, não seria melhor usar qualquer ferramenta que aumente o desempenho do modelo? Além disso, o Gemini também foi especializado para a IMO: treinaram o modelo com reforço em dados de raciocínio em várias etapas, resolução de problemas e prova de teoremas, e ainda forneceram coletâneas de soluções matemáticas de alta qualidade e dicas sobre abordagens para problemas da IMO
Suspeito que a “versão avançada do Gemini Deepthink” na prática seja diferente do Deepthink que entrará no produto por assinatura Gemini Ultra quando for lançado, ou então tenha usado muito mais computação em tempo de teste. Ainda assim, é divertido ver OpenAI e Google competindo
Vou compartilhar o link do prompt de sistema de engenharia de contexto que resolveu todos os problemas de 1 a 6. Dá para usar com o o3 ou o Gemini 2.5; é só inserir o prompt inteiro, colocar a pergunta e pedir para resolver o problema. https://github.com/redcrash0721/freederia/blob/main/imo6kr.pdf