A OpenAI lançou, esta semana, centenas de supostas resoluções para alguns dos problemas matemáticos mais difíceis do mundo. Para evitar controvérsias como as que surgiram quando um de seus modelos resolveu um problema em aberto, a empresa recorreu a um grupo consultivo formado por matemáticos de prestígio. Esse grupo, denominado AGMAI (Advisory Group on Mathematics and Artificial Intelligence), é sediado pelo Instituto de Estudos Avançados da Universidade de Princeton e reúne nove pesquisadores de instituições ao redor do globo. No final de setembro, o AGMAI publicou diretrizes para laboratórios de fronteira que resolvem problemas matemáticos, pedindo, entre outras coisas, que não se testem problemas avançados em modelos proprietários.
No entanto, a OpenAI não atendeu a todos os requisitos recomendados. A empresa seguiu alguns princípios, como a divulgação imediata dos resultados e a inclusão de informações sobre o processo de raciocínio dos modelos. Ainda assim, apenas 10 dos 719 manuscritos liberaram a chamada "cadeia de pensamento" do modelo. Além disso, os matemáticos haviam sugerido que as provas fossem formalizadas em uma linguagem de verificação, como a Lean; apenas 42% das provas apresentadas passaram por esse processo de formalização. O grupo consultivo também não respondeu aos pedidos da imprensa para uma avaliação mais detalhada dos lançamentos.
O AGMAI chegou a sugerir que a OpenAI ajudasse a financiar o trabalho de matemáticos humanos que seriam necessários para tornar as soluções realmente significativas. Terence Tao, renomado matemático que já havia criticar a abordagem da empresa, comentou em redes sociais que os "prompters" de IA resolvem problemas de forma autônoma, sem interesse na comunidade e sem comprender suficientemente a saída do modelo para explicar os resultados em palestras ou debates.
Uma pesquisa publicada esta semana por mathematicians das universidades de Cambridge e do King's College de Londres reforça essas preocupações. O estudo identificou pelo menos duas discrepâncias entre a explicação em linguagem natural e o código em Lean correspondente a uma solução derivada das equações de Navier‑Stokes, que descrevem o comportamento de fluidos. Tais diferenças não invalidam necessariamente as resoluções, mas levantam dúvidas sobre a confiabilidade de confiar apenas nos próprios modelos para formalizar suas provas.
O AGMAI havia pedido que a OpenAI incluísse metadados legíveis por máquina que correlacionassem os artefatos em linguagem natural e os formais. Essa solicitação não foi atendida na actual liberação. O artigo "lost in translation" conclui que as provas em linguagem natural da OpenAI e outras provas auto‑formalizadas em Lean não devem ser confiadas sem o mesmo processo de revisão por pares e escrutínio aplicado a outras demonstrações matemáticas.
Matemáticos enfatizam que, quando resultados são descobertos por humanos, os próprios autores assumem a responsabilidade e se engajam com a comunidade por meio de artigos, palestras e seminários. Esse processo amplia a compreensão das soluções, revela estratégias aplicáveis a outros problemas e permite a transferência do conhecimento para áreas práticas. Melanie Wood, professora de matemática da Universidade Harvard, declarou à imprensa que, no momento da divulgação por um modelo, ainda não existe compreensão humana das provas – e que, a partir daí, o verdadeiro trabalho começa.
Fonte: TechCrunch
