Nemotron ganha ouro na IMO 2026 sem ferramentas

Prova de olimpíada não se resolve com autocomplete

Nemotron 3 Ultra acabou de furar uma barreira que parecia exclusiva de modelo fechado com tooling pesado. Resolver matemática de olimpíada em linguagem natural, sem provador formal, sem Python, sem internet, e ainda bater 30 de 42 pontos na IMO 2026, que é a faixa de ouro. Para quem constrói sistema de raciocínio, o recado é direto: o gargalo saiu do truque externo e voltou para o pós-treino e para o desenho de inferência. E isso muda a conta de quem opera LLM para tarefa difícil, porque agora o diferencial não é qual API de code execution você pluga, e sim como você treina, verifica e seleciona.

Quem já tentou colocar LLM para provar teorema sabe onde isso quebra. O modelo começa bem, define lemas, parece rigoroso, e no passo três escorrega em uma passagem sutil que invalida tudo. Em benchmark fácil, esse erro some na média. Na IMO, um salto lógico mal justificado zera a questão. É por isso que quase todo pipeline vencedor até aqui apelava para Lean, Isabelle ou execução de código para checar partes da prova. A NVIDIA foi no caminho oposto e bancou tudo em texto corrido. Se funciona em olimpíada, funciona em muito caso enterprise onde você não pode depender de ferramenta externa por latência, custo ou compliance.

O fato

A NVIDIA partiu do Nemotron 3 Ultra e treinou dois checkpoints especialistas, um com supervised fine-tuning e outro com reinforcement learning focado em provas matemáticas. Depois montou um pipeline de test-time compute que usa três checkpoints em conjunto: o modelo base de disponibilidade geral mais os dois especialistas. O sistema gera provas candidatas em linguagem natural, passa por uma etapa de verificação também em linguagem natural, refina o que parece promissor e repete o ciclo. No final, uma etapa separada com mais computação escolhe a submissão final para cada problema.

O resultado foi 30 de 42 pontos na IMO 2026, atingindo o corte de ouro. E o ponto mais relevante para a comunidade técnica: eles liberaram os dois checkpoints pós-treinados, os dados de treino, o código de treino e inferência, as soluções submetidas e ainda um benchmark novo chamado Nemotron-IMO-Bench, com 200 problemas inéditos em nível de olimpíada. Não é só anúncio de placar, é receita reproduzível. Dá para baixar os modelos conhecidos como Nemotron-3-Labs-Ultra-Math-RL e os datasets Nemotron-Math-Proofs-v3-SFT e RL, rodar o loop e auditar onde ele acerta e onde inventa.

Como funciona na visão de operador

Pensa na arquitetura como três papéis que se revezam. O gerador propõe soluções completas em texto, sem estrutura formal. O verificador lê como um corretor chato de olimpíada e aponta furos, passos faltantes, uso indevido de desigualdade ou indução mal ancorada. O refinador pega esse feedback e reescreve. Esse loop de gerar, verificar e refinar é test-time compute puro. Você troca latência e tokens por qualidade, o que na prática significa rodar dezenas a centenas de amostras por problema e podar agressivamente.

O pós-treino aqui é o que destrava o loop. O SFT provavelmente ensina o formato de prova longa, encadeamento lógico, estilo de justificativa que banca examinador humano. O RL entra depois para premiar provas que sobrevivem à verificação, não só as que parecem bonitas. É um sinal difícil de modelar, porque verificação em linguagem natural também erra. A sacada plausível, mesmo sem todos os hiperparâmetros abertos, é que eles calibraram o verificador para ser cético e usaram o RL para punir alucinação confiante. Em termos de API, imagina algo como três chamadas encadeadas com prompts distintos e temperatura diferente: geração com diversidade alta, verificação com temperatura baixa e refinamento condicionado ao critique.

Custo, latência e o detalhe que ninguém conta

Esse tipo de pipeline não é barato em inferência. Para chegar a ouro na IMO, estamos falando de busca iterativa pesada, provavelmente milhares de tokens por tentativa vezes N tentativas, mais passes de verificação e uma fase final de seleção com ainda mais compute. Em produção, isso se traduz em latência de minutos por problema difícil e custo de tokens facilmente 20x a 50x maior que uma chamada única. Funciona para olimpíada porque você tem horas por prova. Para um produto real, você vai precisar de early stopping, cache de raciocínio e um roteador que decide quando vale a pena ligar esse modo pesado.

Outro ponto de operador: rodar tudo sem ferramentas externas simplifica muito o deploy. Sem dependência de provador formal, sem sandbox de código, sem browsing. Isso reduz superfície de falha, evita timeout de tool e facilita rodar em VPC fechada ou em ambiente regulado. O preço é que você perde um verificador determinístico. A verificação vira probabilística, feita pelo próprio modelo. Então a confiabilidade final depende da qualidade da seleção. A etapa de alta computação no final é essencialmente um best-of-N com reranking crítico, e é ali que o sistema provavelmente queima mais FLOPs.

O que isso muda na prática

Quem ganha primeiro são times que precisam de raciocínio longo auditável em texto, como tutores de matemática avançada, copilotos para engenharia, revisão de provas e辅助 de pesquisa quantitativa. Ter checkpoints abertos e dados de SFT e RL permite fazer distilação para modelos menores ou adaptar o verificador para seu domínio. Quem perde um pouco de vantagem são stacks fechados que vendiam ouro em matemática como moat de sistema proprietário com tools secretas. Quando a receita é aberta, o moat vira execução e custo.

• Ação prática para testar hoje: baixe o checkpoint RL e o dataset SFT, separe 20 problemas difíceis do seu domínio e rode um loop simples de gerar, criticar e reescrever com três prompts separados antes de pensar em fine-tuning próprio.
• Ajuste de arquitetura: separe o verificador do gerador em serviços diferentes, com prompts, temperaturas e até modelos distintos, e registre taxa de descarte por rodada para calibrar custo por ponto de qualidade.
• Benchmark interno: use o Nemotron-IMO-Bench como referência de estresse para seu pipeline de raciocínio, mesmo que seu produto não seja matemática, porque ele expõe alucinação lógica melhor que muito benchmark de código.

Na prática, o que você precisa ajustar agora é sua estratégia de inferência. Muita equipe ainda investe 80 por cento do esforço em prompt único e modelo maior. Essa receita sugere inverter: modelo bom o suficiente mais verificação iterativa e seleção final forte. Para tarefas de alto valor onde erro custa caro, vale queimar mais tokens. Para tarefa de alto volume e baixa margem, você vai querer destilar o padrão de prova para uma chamada só.

A tensão que fica

A dúvida real é se isso escala sem quebrar economicamente. Fazer 30 pontos na IMO com busca massiva é impressionante, mas é um regime de seis problemas em dois dias. Levar esse mesmo loop para milhares de usuários simultâneos com SLA de segundos é outra história. O custo de test-time compute cresce rápido e a latência vira inimiga. Resolve ou só move o gargalo do treino para a inferência. Minha leitura é que resolve parcialmente: prova que linguagem natural sustenta rigor se houver verificação, mas empurra o problema para seleção e custo.

Tem outro incômodo técnico. Verificador em linguagem natural pode ser enganado por prova bem escrita e errada, o famoso fluente mas falso. Sem provador formal, você nunca tem garantia. O RL pode até reforçar esse viés se premiar prova que convence o verificador fraco. A NVIDIA mitigou com múltiplos checkpoints e estágio final de seleção, mas em produção isso pede calibração constante e avaliação humana. Aberto ajuda aqui, porque dá para inspecionar as soluções submetidas e ver exatamente que tipo de erro passou.

Conclusão

No fim, é uma receita aberta de ouro sem truque externo: pós-treino especializado mais busca iterativa de gerar, verificar, refinar e selecionar. Simples de entender, caro de rodar, poderoso quando bem calibrado. A pergunta que fica para quem opera é direta: no seu caso, quantos tokens extras por resposta valem um erro lógico a menos.