Um novo teste de sistemas de prova de teoremas com IA aponta uma divisão clara entre responder corretamente a uma questão de matemática e produzir uma prova formal que passa pela checagem do Lean 4. No benchmark MathAdv, a maior acurácia reportada em Lean 4 foi de 21,88%, alcançada pelo Goedel-Prover-V2; o DeepSeek-Prover-V1.5 RL com RMaxTS ficou em 16,56%.
O que o MathAdv mede
O benchmark foi construído para separar habilidades que, vistas de fora, parecem a mesma coisa: resolver o problema, formalizar a solução e generalizar o raciocínio para problemas novos. Um modelo pode acertar a resposta numérica e ainda assim falhar ao expressar o mesmo argumento em uma linguagem de prova formal que um assistente como o Lean 4 aceita sem erro.
Por que isso importa
A formalização é o elo entre o raciocínio de um modelo e a verificação confiável de que a matemática está correta. Se os modelos continuam abaixo de 22% em precisão formal, há uma distância considerável até o ponto em que IAs possam, de forma autônoma, produzir provas verificáveis em pesquisa ou em verificação de software. O resultado reforça que “acertar a resposta” não é o mesmo que “provar que está certo”.
Leitura cuidadosa
Os números vêm de um preprint (ainda não revisado por pares) e de um único benchmark. A acurácia formal baixa não significa ausência de progresso — a taxa saltou nos últimos modelos — mas indica onde está o gargalo atual do campo.
Descubra mais sobre noticiAI
Assine para receber nossas notícias mais recentes por e-mail.
