A OpenAI tornou público nesta terça-feira, 6, um conjunto de 722 manuscritos matemáticos produzidos por um modelo de inteligência artificial que ainda não está disponível ao público. Os documentos foram publicados no GitHub, acompanhados de materiais que permitem examinar as demonstrações apresentadas.
O acervo está organizado em 372 grupos de resultados relacionados, que podem incluir um teorema principal, corolários ou provas alternativas. A avaliação dos trabalhos envolveu cerca de quatro mil problemas. A empresa alerta que os manuscritos se encontram em diferentes estágios de verificação e que alguns resultados ainda não formalizados podem conter erros.
Verificação e formalização em Lean
Parte das demonstrações foi expressa em Lean, uma linguagem de programação combinada com um assistente de provas que permite ao computador confirmar a validade de argumentos matemáticos. No processo, a prova é escrita em uma linguagem formal, com definições e etapas que o sistema pode checar para garantir que a conclusão decorre das premissas e das regras utilizadas.
A OpenAI informou que continuará a adicionar novas formalizações ao repositório à medida que elas forem criadas, mantendo versões anteriores acessíveis e registrando correções. A verificação das provas é considerada um ponto crucial para o avanço da inteligência artificial na matemática, já que confirmar a correção de uma demonstração e compreender as ideias subjacentes são tarefas distintas do trabalho científico.
Recomendações do Grupo Consultivo de Matemática e IA
A divulgação foi orientada pelo Grupo Consultivo de Matemática e Inteligência Artificial, um comitê independente sediado no Institute for Advanced Study. Em recomendações publicadas em 29 de setembro, o grupo defendeu que laboratórios compartilhem descobertas relevantes com documentação detalhada, referências, informações sobre o processo e provas formalizadas sempre que possível.
O documento também pediu que sejam destinados recursos para que pesquisadores possam entender e incorporar os resultados, com iniciativas lideradas pela comunidade matemática. O grupo, porém, não endossa a prática de testar problemas avançados em modelos proprietários inacessíveis e solicita que os laboratórios interrompam essa abordagem.
Para os membros do comitê, a capacidade das máquinas de produzir argumentos não elimina a necessidade de compreensão humana, verificação colaborativa e responsabilidade pelo conteúdo publicado.
Contexto e implicações
Cada resultado publicado consumiu, em média, uma quantidade de computação equivalente a aproximadamente três horas de raciocínio do ChatGPT Pro. A empresa afirma que está trabalhando para disponibilizar o modelo publicamente e que financiará workshops, conferências e programas dedicados à análise dos resultados.
A iniciativa representa um marco na interação entre inteligência artificial e pesquisa matemática, mas também levanta questões sobre a confiabilidade de provas geradas por sistemas opacos e sobre a melhor forma de integrar esses avanços ao trabalho científico tradicional.
