'Prova por intimidação': IA resolve problemas matemáticos 'impossíveis' com confiança. Mas pode convencer os melhores matemáticos?

Estados Unidos - Agência de Notícias Ekhbary

'Prova por intimidação': IA resolve problemas matemáticos 'impossíveis' com confiança. Mas pode convencer os melhores matemáticos?

No intrincado mundo da matemática, onde a precisão é primordial, o rápido avanço da inteligência artificial (IA) apresenta um desafio novo e desconcertante. Modelos de IA sofisticados, como o 'o4-mini' da OpenAI, são agora capazes de gerar demonstrações matemáticas complexas que parecem notavelmente convincentes, impressionando até mesmo os matemáticos de ponta. No entanto, essa conquista levanta uma questão fundamental: podemos realmente confiar nessas demonstrações geradas por máquinas, especialmente quando parecem 'corretas', mas podem ocultar falhas sutis ou ser muito intrincadas para verificação humana?

Em uma reunião secreta em 2025, alguns dos matemáticos mais proeminentes do mundo se reuniram para testar rigorosamente o mais recente modelo de linguagem grande da OpenAI, o 'o4-mini'. Os especialistas presentes ficaram maravilhados com a semelhança impressionante das saídas do modelo com o raciocínio de um matemático humano ao apresentar uma demonstração complexa. Ken Ono, um distinto professor de teoria dos números na Universidade da Virgínia, comentou sobre o desempenho do modelo: "Eu nunca vi esse tipo de raciocínio em modelos antes. É isso que um cientista faz."

No entanto, essa admiração inicial foi rapidamente temperada por uma crescente apreensão. A IA estava recebendo mais crédito do que merecia? E corremos o risco de aceitar demonstrações derivadas de IA sem compreender totalmente suas implicações? O próprio Professor Ono reconheceu o potencial do modelo para fornecer respostas confiantes, mas possivelmente incorretas. "Se você diz algo com autoridade suficiente, as pessoas simplesmente ficam assustadas", observou Ono. "Eu acho que o o4-mini dominou a arte da prova por intimidação; ele diz tudo com tanta confiança."

Historicamente, a confiança e a aparência de um argumento sólido eram indicadores confiáveis, pois apenas os matemáticos mais habilidosos podiam construir argumentos convincentes, e seu raciocínio era tipicamente robusto. Esse paradigma mudou. O renomado matemático Terry Tao, vencedor da Medalha Fields da UCLA, destacou a crescente capacidade da IA de imitar a correção. "Infelizmente, a IA é muito melhor em parecer que tem a resposta certa do que em realmente obtê-la... certa ou errada; elas sempre parecerão convincentes", explicou Tao à Live Science. "Se você fosse um matemático terrível, também seria um escritor matemático terrível e enfatizaria as coisas erradas. Mas a IA quebrou esse sinal."

Consequentemente, os matemáticos estão cada vez mais preocupados com a possibilidade de a IA inundar o campo com demonstrações aparentemente plausíveis que contenham erros sutis, difíceis de serem detectados por humanos. O Professor Tao alertou contra a aceitação acrítica de argumentos gerados por IA devido à sua aparência rigorosa. "Infelizmente, a IA é muito melhor em parecer que tem a resposta certa do que em realmente obtê-la... certa ou errada; elas sempre parecerão convincentes", reiterou. Ele instou a uma abordagem cautelosa em relação às 'provas' da IA, afirmando: "Uma coisa que aprendemos ao usar IAs é que, se você lhes der um objetivo, elas trapacearão loucamente para atingir esse objetivo."

Embora a questão de saber se podemos realmente "provar" conjecturas matemáticas altamente técnicas sem entender as demonstrações possa parecer abstrata, suas implicações são profundas. Afinal, se uma demonstração não pode ser confiável, a base para um maior desenvolvimento matemático desmorona. Considere o problema P versus NP, um grande desafio em aberto na matemática computacional. Essencialmente, pergunta se problemas cujas soluções são fáceis de verificar também são fáceis de resolver. Uma prova definitiva poderia revolucionar o planejamento, a logística, o design de chips e a descoberta de medicamentos. Por outro lado, uma prova verificável poderia minar a segurança da maioria dos sistemas criptográficos atuais. Estas não são questões obscuras; elas carregam um risco significativo no mundo real.

Pode surpreender os não matemáticos descobrir que as demonstrações matemáticas derivadas de humanos sempre foram, em certa medida, construções sociais – sobre convencer outros no campo da validade dos argumentos. Afinal, uma demonstração matemática é frequentemente aceita como verdadeira quando outros matemáticos a analisam e a consideram correta. Isso significa que a aceitação generalizada não garante uma verdade irrefutável. Andrew Granville, um matemático da Universidade de Montreal, suspeita que até mesmo algumas das demonstrações humanas mais conhecidas e rigorosamente examinadas podem conter erros.

Há algumas evidências que apoiam essa afirmação. "Houve alguns artigos famosos que estão errados por causa de pequenas questões linguísticas", disse Granville à Live Science. Talvez o exemplo mais conhecido seja a prova do Último Teorema de Fermat de Andrew Wiles. O teorema afirma que, embora existam números inteiros onde a soma de dois quadrados é igual a um terceiro quadrado (por exemplo, 3² + 4² = 5²), não existem números inteiros que façam o mesmo para cubos ou potências superiores. Wiles passou notoriamente sete anos trabalhando em quase completo isolamento e, em 1993, apresentou sua prova em uma série de palestras em Cambridge, com grande alarde. Quando Wiles terminou sua última palestra com a imortal linha 'Acho que vou parar por aqui', a audiência explodiu em aplausos estrondosos e champanhe foi servido para celebrar a conquista. Jornais ao redor do mundo proclamaram a vitória do matemático sobre o problema de 350 anos. No entanto, durante o processo de revisão por pares, um revisor detectou uma falha significativa na prova de Wiles. Ele passou mais um ano trabalhando no problema e eventualmente o corrigiu. Mas por um curto período, o mundo acreditou que a prova havia sido resolvida, quando na verdade não havia sido.

Para evitar esse tipo de problema – onde uma prova é aceita sem estar realmente correta – há um movimento para reforçar as provas com o que os matemáticos chamam de 'linguagens de verificação formal'. Esses programas de computador, o mais conhecido dos quais é 'Lean', exigem que os matemáticos traduzam suas provas para um formato muito preciso. O computador então percorre cada etapa, aplicando lógica matemática rigorosa para confirmar que o argumento está 100% correto. Se o computador encontrar uma etapa na prova que não lhe agrada, ele a sinaliza e não a deixa passar. Essa formalização codificada não deixa espaço para as incompreensões linguísticas que Granville teme terem atormentado provas anteriores.

Kevin Buzzard, um matemático do Imperial College London e um dos principais proponentes da verificação formal, disse: "Eu comecei neste negócio porque estava preocupado que as provas humanas fossem incompletas e incorretas e que nós, humanos, estávamos fazendo um trabalho ruim ao documentar nossos argumentos."

Além de verificar provas humanas existentes, a IA, trabalhando em conjunto com programas como Lean, pode ser transformadora, disseram os matemáticos. "Se forçarmos a saída da IA a produzir coisas em uma linguagem formalmente verificada, então isso, em princípio, resolve a maioria do problema" de a IA gerar provas de aparência convincente, mas em última análise incorretas, disse Tao. Ele acrescentou: "Existem artigos em matemática onde ninguém entende o artigo inteiro. Sabe, há um artigo com 20 autores e cada autor entende sua parte. Ninguém entende a coisa toda. E tudo bem. É assim que funciona." Buzzard concordou: "Você gostaria de pensar que talvez possamos obter..."

Agência de Notícias Ekhbary