A Resolution, startup de segurança de IA anteriormente conhecida como Sequent, publicou um relato técnico sobre como empregou agentes de IA para formalizar automaticamente a resolução de singularidades de Hironaka, um resultado clássico da geometria algébrica. O material foi destacado na edição 478 da newsletter Import AI, de 26 de outubro de 2026, assinada por Jack Clark.
Segundo a empresa, o trabalho de formalização "abre caminho para pesquisas automatizadas sobre a relação entre a geometria da paisagem de perda e a generalização" dos modelos.
Como o processo foi conduzido
A abordagem não foi um único pedido a um modelo, mas uma operação dividida em camadas. Um pesquisador da Resolution começou colaborando com agentes para produzir dois planos: uma versão de alto nível, legível por humanos, e um plano detalhado de 112 páginas, quebrado em etapas atômicas e alinhado à literatura existente.
Em seguida, esse pesquisador delegou a execução a um agente orquestrador, que criou subagentes para fazer matemática no papel, escrever provas em Lean e desempenhar funções de apoio, como verificar se o trabalho seguia o plano original. De acordo com a empresa, a fase de execução exigiu pouca estrutura adicional além do plano inicial e de algumas habilidades de agente destiladas de esforços internos anteriores de autoformalização.
O custo e a escala do esforço
Os números dão a dimensão do que foi feito. O trabalho levou cerca de uma semana e consumiu algo na ordem de 100 bilhões de tokens de entrada — dos quais 90% foram leituras de cache, e aproximadamente 300 milhões de tokens de saída.
O gasto estimado em tokens ficou em US$ 135 mil. O produto final foi um conjunto de cerca de 600 mil linhas de código Lean. É um volume que dificilmente seria produzido por uma equipe humana no mesmo prazo, e o relato torna transparente uma questão que costuma ficar fora das discussões sobre pesquisa com IA: o preço computacional de se formalizar matemática avançada.
Por que isso importa para a segurança de IA
A conexão entre matemática de fronteira e segurança de modelos passa pela teoria da aprendizagem singular. Com a biblioteca formalizada, a Resolution afirma já ter obtido ganhos ao estender partes dessa teoria, por exemplo, para entender melhor o processo de amostragem, compreensão que, segundo a empresa, permite moldar como os modelos aprendem, objetivo do que ela chama de "patterning".
A aposta declarada é que a "industrialização da matemática" viabilize "uma nova e rigorosa ciência de automação de pesquisa". O ponto central é que tarefas antes caras demais em tempo humano para entrar no roteiro de uma startup agora se tornam executáveis, o que muda o cálculo de prioridades de laboratórios de segurança.
ProgramBench: de 0% a 18,5% em poucos meses
A mesma edição traz outro dado sobre ritmo de progresso. O Claude Opus 5.5, na configuração xhigh, alcançou 18,5% de tarefas resolvidas no ProgramBench, benchmark lançado em maio deste ano que, na época, viu todos os modelos testados marcarem 0%.
O ProgramBench avalia a capacidade de sistemas de IA de reconstruir programas de software a partir de um executável compilado e de sua documentação. As 200 tarefas incluem interpretadores de linguagem (PHP, Lua, tinycc), bancos de dados (DuckDB, SQLite), utilitários de mídia e compressão (FFmpeg, zstd, xz) e ferramentas de desenvolvimento (ripgrep, fzf, jq).
A métrica que mudou de patamar
Quando foi lançado, o melhor sistema era o Claude Opus 4.7, com 0% de tarefas resolvidas, a fração das 200 tarefas em que todos os testes passam, e 3% na categoria "quase", reservada aos casos em que mais de 95% dos testes passam. O cenário atual é outro: o Claude Opus 5.5 chega a 18,5% de tarefas resolvidas e a 70,5% na faixa "quase".
A leitura da newsletter é que 2027 verá grandes volumes de software construídos de ponta a ponta por sistemas de IA, desenvolvendo autonomamente o que for necessário para as tarefas a que forem designados. Avaliações como o ProgramBench funcionam, nesse contexto, como termômetro da velocidade dessa mudança.
O que observar daqui para frente
Para o leitor brasileiro que acompanha adoção de IA, dois fios se destacam. O primeiro é metodológico: o relato da Resolution descreve um padrão de trabalho, plano detalhado, orquestrador, subagentes especializados e verificação contínua, que pode ser replicado em outros domínios que exigem rigor formal, não apenas em matemática.
O segundo é econômico: o custo explícito de US$ 135 mil em tokens por uma semana de formalização oferece uma referência concreta para estimar orçamentos de pesquisa assistida por IA. Do outro lado, o salto do ProgramBench indica que a reconstrução autônoma de software deixou de ser um limite intransponível, ainda que 18,5% de tarefas plenamente resolvidas esteja longe de domínio completo.
Fontes e links
- Import AI
- Formalizing Hironaka's Resolution of Singularities (Resolution)
- Import AI 461: alignment is not on track, FrontierCode, and synthetic research interns
