Em 2025, a startup Axiom, com apenas sete meses de vida, resolveu todas as 12 questões do exame Putnam, um dos testes de matemática mais difíceis para graduandos. A pontuação 12/12 supera a média humana (mediana zero) e outros sistemas de IA, como o DeepSeek (103/120). O feito impressiona, mas o que realmente importa não é a nota — é o método.
O fato
Axiom atingiu 12/12 no Putnam dentro do tempo limite, enquanto o melhor humano teve 110/120 com tempo extra. O exame é conhecido por sua dificuldade: a mediana costuma ser 0 ou 1 ponto. Isso coloca a IA em um patamar nunca visto em raciocínio matemático informal. Mas o que está por trás desse resultado?
Como funciona: visão de operador
A Axiom usa verificação formal como sinal de recompensa no treinamento por reforço. Em vez de depender de RLHF ou GRPO (que usam aproximações estatísticas), eles alimentam o modelo com provas matemáticas escritas em Lean, uma linguagem de verificação formal. O modelo gera código e prova de correção — e o Lean verifica se a prova é válida. Isso é análogo a compilar e testar código durante o RL, mas para matemática. O resultado: a Axiom alcançou 99% (187/189) no benchmark ProofGen, muito acima de qualquer outro sistema conhecido.
Na prática, isso significa que o sinal de reforço é muito mais preciso. Enquanto métodos estatísticos dão recompensas aproximadas (baseadas em similaridade com dados de treino), a verificação formal dá um veredito binário: certo ou errado. Isso acelera o aprendizado e reduz a necessidade de dados humanos rotulados.
O que isso muda na prática
Para quem constrói sistemas de IA, a lição é clara: integrar verificadores formais (Lean, Isabelle, Coq) pode turbinar o RL em domínios onde a correção pode ser verificada automaticamente. Código já se beneficia disso, mas matemática abre um novo campo. A Axiom mostrou que é possível ir além de benchmarks de código e atacar problemas abertos de raciocínio.
Para quem usa IA em educação ou pesquisa, isso significa que ferramentas de prova assistida por IA podem se tornar muito mais confiáveis. Imagine um assistente que não apenas sugere passos, mas verifica formalmente cada um. A Axiom abriu o toolkit AXLE justamente para isso.
Tensão e reflexão
Mas a pergunta que fica: isso escala? Verificação formal é cara e lenta. A própria CEO da Axiom, Carina Hong, vê o código como um marco necessário, mas insuficiente. O gargalo é a tradução de problemas informais (como os enunciados do Putnam) para uma linguagem formal. Se a IA não consegue entender a intenção humana por trás do problema, a verificação formal se torna um beco sem saída. O Putnam 12/12 é impressionante, mas ainda é um ambiente controlado. O verdadeiro teste será em problemas abertos, onde não há uma formulação formal pré-definida.
Outra tensão é o custo. A Axiom não divulga o custo computacional, mas provavelmente é alto. Para startups menores, replicar essa abordagem pode ser inviável. A verificação formal é um atalho poderoso, mas só funciona se você tiver os recursos para gerar e verificar provas em larga escala.
Conclusão
A Axiom provou que verificação formal pode levar IA a superar humanos em matemática. O feito é real, mas o caminho para AGI ainda exige resolver o problema da informalidade — traduzir o mundo real para linguagens formais. Por enquanto, o Putnam foi vencido. O próximo desafio é sair do exame.
Nenhum comentário ainda. Seja o primeiro a comentar!
Deixe seu comentário