O Congresso Internacional de Matemáticos, realizado em Filadélfia, viu o matemático Jacob Tsimerman afirmar que o mundo muda e que a carreira acadêmica matemática não sobreviverá na forma atual. A discussão foca na necessidade de formalizar saídas de inteligência artificial para garantir a precisão de sistemas.
O avanço da inteligência artificial gera descobertas contínuas, mudando o gargalo histórico que era a descoberta. Hoje, a confirmação humana se torna o recurso escasso. A solução apontada é a formalização, que traduz resultados de IA em formas exatas passíveis de checagem automática. Construir essa infraestrutura de verificação é um desafio de engenharia nacional.
Os riscos se estendem além da matemática. Sistemas de hospitais, bancos e redes elétricas operam com códigos vulneráveis. Em abril, uma empresa de IA revelou que seu modelo encontrou falhas em sistemas operacionais. Posteriormente, engenheiros de uma grande empresa identificaram noventa falhas críticas em um produto amplamente usado.
O desenvolvimento de código por IA permite que equipes construam rapidamente, mas também gera volumes de código que poucos entendem completamente. Pesquisadores defendem o uso de métodos formais, que provam matematicamente que um software fará exatamente o que foi projetado. Isso valida o resultado da IA, mas a definição correta do que o sistema deve fazer ainda depende do julgamento humano.
A União Matemática Internacional alertou que a IA ameaça a verificabilidade de provas. Os especialistas argumentam que a matemática fornece a infraestrutura para aumentar a confiança na IA. Empresas que gerenciam infraestrutura crítica devem incorporar garantias formais desde o início, focando na lógica dos sistemas, e não apenas em correções reativas.
