A OpenAI divulgou esta semana centenas de soluções alegadas para problemas matemáticos difíceis, numa tentativa de demonstrar a capacidade dos seus modelos de lidar com questões avançadas. Mas a divulgação não cumpriu integralmente as orientações estabelecidas por um grupo consultivo de pesquisadores de matemática, reabrindo a questão fundamental: basta que os modelos produzam uma solução passível de formalização computacional, ou ela também deve ser compreensível e auditável por matemáticos?
O grupo Advisory Group on Mathematics and Artificial Intelligence (AGMAI) reúne nove pesquisadores renomados e é sediado pelo Instituto de Estudos Avançados da Universidade de Princeton. O grupo publicou, no fim de setembro, orientações para os laboratórios que desenvolvem modelos avançados para resolver problemas matemáticos.
Cumprimento parcial das orientações dos pesquisadores
A AGMAI indicou que a avaliação do cumprimento das suas recomendações cabe, em última instância, à comunidade matemática. Entre as suas principais recomendações está deixar de testar problemas matemáticos avançados em modelos comercialmente proprietários, enquanto a OpenAI afirmou explicitamente que utiliza problemas de pesquisa abertos para avaliar os seus próprios modelos.
A OpenAI seguiu alguns dos princípios, como publicar os resultados rapidamente e fornecer informações sobre como os modelos chegaram às suas conclusões. No entanto, apenas 10 manuscritos de um total de 719 incluíram as cadeias de raciocínio do modelo. Além disso, 42% das provas publicadas não foram formalizadas.
O grupo considera que as provas difíceis de compreender para os seres humanos devem ser convertidas para uma forma formal. Mas também destacou a responsabilidade do laboratório de garantir que a divulgação dos resultados seja acompanhada de uma compreensão humana deles, e propôs financiar matemáticos que ajudem a tornar esses resultados efetivamente dotados de significado científico.
Lacuna entre a linguagem natural e o código Lean
Os modelos geralmente começam criando uma explicação em linguagem natural e depois tentam convertê-la para Lean, uma linguagem de programação cujo compilador pode confirmar a consistência da prova numa forma executável. No entanto, a conversão automática pode alterar o conteúdo da prova ou criar uma separação entre o que a explicação afirma e o que o código demonstra.
Um artigo publicado por matemáticos da Universidade de Cambridge e do King’s College London documentou pelo menos duas diferenças entre uma prova em linguagem natural e o código Lean associado a uma solução apresentada pela OpenAI para um problema derivado das equações de Navier-Stokes sobre o comportamento de fluidos complexos. Essas diferenças não provam necessariamente que uma das soluções esteja errada, mas levantam dúvidas sobre permitir que os modelos formalizem as suas próprias soluções sem intervenção humana.
A AGMAI também pediu a inclusão de metadados legíveis por máquina que estabeleçam uma ligação entre a prova textual e a versão formal, algo que a OpenAI não forneceu nestas divulgações. Os autores do artigo, conhecido como “lost in translation”, concluíram que as provas textuais e as provas de Lean convertidas automaticamente não devem ser aceites, em princípio, sem revisão por pares e uma auditoria semelhantes às realizadas com outras provas.
Por que esta notícia é importante?
O problema não diz respeito apenas a demonstrar que o código é compilado com sucesso, mas a demonstrar que o código representa efetivamente a ideia matemática explicada pelo texto. Na pesquisa tradicional, os cientistas assumem a responsabilidade pelos seus resultados e discutem-nos por meio de artigos, palestras e seminários, num processo que ajuda a detetar erros e a compreender métodos reutilizáveis.
Quando os modelos produzem uma solução para um problema difícil, porém, essa compreensão humana pode não estar disponível no momento da publicação. Por isso, os resultados atuais da OpenAI parecem mais próximos do início de um processo de validação científica do que do fim do problema; a revisão humana e a ligação entre as saídas textuais e formais continuam a ser duas condições pendentes antes que essas provas sejam adotadas pela comunidade matemática.