O Apocalipse Matemático da IA
A IA talvez tenha mudado a Matemática para sempre. E tudo isso passa por uma invenção de um pesquisador brasileiro.
A OpenAI soltou um artigo semana passada apresentando 372 famílias de resultados matemáticos gerados por IA, incluindo alguns sobre problemas que a comunidade tenta resolver há décadas. Parte desses resultados já foi verificada formalmente por computadores, outros ainda precisam de mais escrutínio e alguns manuscritos já foram até retirados pela OpenAI.
O volume de resultados é sem precedentes. Isso é uma nova forma de "fazer matemática", que a comunidade ainda está tentando assimilar. Um dos teóricos mais importantes da ciência da computação, Scott Aaronson, chamou essa fase de Mathocalypse (Matemáticalipse). O engraçado é que a própria esposa dele, a professora Dana Moshkovitz, também uma teórica da computação, passou décadas atacando um dos problemas que foi supostamente resolvido.
Uma das questões mais importantes é que resultados matemáticos podem influenciar a segurança dos algoritmos que usamos para criptografar nossos dados. Isso porque boa parte da criptografia depende de certos problemas matemáticos serem extremamente difíceis de resolver. A segurança desses algoritmos se apoia na convicção de que ninguém consiga realizar os cálculos necessários para quebrá-los em tempo hábil. E essa convicção vem de décadas de pesquisa matemática e de fortes evidências de que esses problemas são difíceis de resolver. O uso da IA pode permitir que um governo, uma organização ou um indivíduo descubra novos algoritmos que tornem viáveis cálculos antes considerados impraticáveis, e isso comprometeria a segurança dos nossos sistemas.
Uma coisa estranha que está gerando um vuco-vuco na bolha tech é a ausência de resultados ligados à criptografia no conjunto divulgado pela OpenAI. Isso, somado a relatos de pesquisadores, gerou especulações de que as empresas de IA estejam investigando em privado problemas mais sensíveis, como possíveis maneiras de quebrar sistemas criptográficos.
Os especialistas em criptografia estão divididos sobre quão urgente deve ser o preparo da comunidade de criptografia e da sociedade, mas há amplo reconhecimento de que essa nova capacidade da IA de gerar resultados matemáticos é algo sério que deve ser acompanhado de perto.
E existe algo ainda mais profundo. A Matemática ficou por milênios limitada ao raciocínio humano. Claro que ferramentas de cálculo acompanham a Matemática desde muito cedo, auxiliando os matemáticos nas tarefas mais tediosas e sujeitas a erros. A própria concepção do computador de propósito geral por Charles Babbage, no século XIX, nasceu de trabalhos para automatizar cálculos e evitar erros humanos. Na época, havia grande demanda por tabelas de logaritmos e outras funções matemáticas, usadas, por exemplo, na navegação. Sua Máquina Analítica, um projeto de computador universal, nunca chegou a ser construída, mas isso é história pra outro post.
Um dos grandes avanços do uso da computação na Matemática foi a verificação automática de provas matemáticas. Hoje, um matemático pode usar uma linguagem formal como Lean, criada pelo pesquisador brasileiro Leonardo de Moura, que recentemente deu uma entrevista excelente ao podcast Machine Learning Street Talk. Moura é bem rigoroso e cauteloso e nos lembra, por exemplo, do cuidado que se deve ter com esses resultados. Ele conta um episódio em que uma suposta prova matemática explorava bugs nos próprios sistemas responsáveis por verificá-la, possivelmente com ajuda de IA.
Na linguagem Lean, pode-se escrever teoremas e demonstrações, e o computador verifica formalmente se a demonstração é válida a partir dos axiomas, definições e teoremas anteriores. Essas linguagens podem ajudar os modelos de IA em duas etapas: durante o treinamento, fornecendo feedback sobre a validade das provas que tentam produzir; e depois, verificando formalmente as provas que conseguem gerar.
Domínios em que é possível verificar se uma resposta está correta, como Matemática, programação e jogos com regras bem definidas, têm sido fundamentais para a evolução da IA. Nessas áreas, os modelos podem tentar resolver um problema, verificar o resultado e aprender com os erros. Esse ciclo de tentativa e verificação foi um dos fatores que ajudaram os modelos a evoluir de chatbots para agentes de IA. Ferramentas que ajudam humanos a verificar provas ou testar programas agora também podem ajudar máquinas a aprender a produzi-los.
Mas a verificação formal também tem seus limites. Um artigo recente de pesquisadores das universidades de Cambridge e King's College London encontrou discrepâncias entre uma demonstração sobre as equações de Navier–Stokes apresentada pela OpenAI e sua tradução para Lean. O problema é sutil: o Lean verifica rigorosamente uma demonstração formalizada, mas isso, por si só, não garante que ela corresponda exatamente ao argumento matemático escrito originalmente. Isso não significa que o resultado da OpenAI esteja errado, mas que a verificação formal, por si só, não resolve o problema de traduzir fielmente o raciocínio matemático humano para a linguagem do computador.
Vale lembrar que resolver um problema matemático envolve, sim, produzir uma prova, mas vai muito além disso. Ao atacar um problema, matemáticos frequentemente criam novos conceitos, muitos deles frutíferos para outros resultados ou para uma compreensão mais profunda da própria Matemática. Como lembrou o grande matemático Terence Tao em entrevista recente, uma das medidas da importância de um resultado é a quantidade de novos conceitos e conexões que ele gera.
Tao vai mais além, cunhando a ideia da Matemática 2.0. Segundo ele, a cultura matemática atual dá importância excessiva a quem resolve primeiro um problema aberto. Com a IA assumindo parte desse trabalho, seria necessário valorizar ainda mais outras contribuições: desenvolver novas teorias, explicar resultados, estabelecer conexões e aplicar a Matemática a problemas do mundo real.
O que segue, então, é fascinante e um pouco perturbador: a IA consegue usar poder computacional para gerar diversos resultados matemáticos, alguns com provas formalmente verificadas, muito mais rápido do que os humanos conseguem digerir. É a tal indigestão matemática de que fala Tao. O que acontece quando temos esse novo tipo de inteligência, que funciona de maneira opaca e gera resultados que não são palatáveis aos humanos? Em alguns casos, os humanos já recorrem à própria IA para ajudar a entender resultados matemáticos produzidos por IA. O que ainda não sabemos é por quanto tempo a criação de novas teorias continuará em nossas mãos.