OpenAI anuncia dez avanços matemáticos gerados pelo modelo Astra

Astra produziu resultados em dez problemas abertos

Os resultados incluem novos limites para empacotamento de esferas e códigos binários e esféricos em altas dimensões. O modelo também teria construído grupos não-sofic, refutado a conjectura de rigidez de Connes e obtido novos limites inferiores para calcular o permanente com circuitos e fórmulas aritméticas. Nesse último caso, a OpenAI cita um limite inferior para fórmulas aritméticas de ordem n 4/log n.

A lista ainda traz um teorema de repetição paralela exponencial para jogos quânticos de dois jogadores. O trabalho sobre o problema do vetor mais próximo estabelece uma dureza de aproximação por fator polinomial, ligada à criptografia pós-quântica. A empresa também afirma ter determinado, em toda dimensão, o maior volume possível de um corpo convexo cujo centróide é seu único ponto de rede interior.

Os dois últimos resultados tratam de combinatória extremal. A OpenAI diz ter obtido um limite inferior superexponencial para números de Ramsey de triângulos com várias cores, resolvendo o problema 183 de Erdős, além de resultados sobre as conjecturas de compactação e degenerescência em teoria extremal dos grafos, associados aos problemas 146 e 180 de Erdős.

O comunicado não apresenta esses achados como uma simples execução automática de provas. Humanos transformaram os argumentos produzidos pelo Astra em manuscritos, e o modelo formalizou cada argumento em um certificado Lean. A OpenAI liberou os certificados no repositório openai/ten-proofs e também a narração do processo de raciocínio do modelo para cada solução.

A empresa libera certificados, não o Astra

A OpenAI afirma que encontrar as soluções consumiu tokens cujo custo ficaria em torno de $2,000 nas tarifas da Sol API. Esse valor mede o gasto estimado pela empresa para gerar os resultados, não um preço de acesso ao modelo. O Astra aparece no comunicado como uma versão interna e o texto não anuncia sua liberação pública.

A validação também tem um limite claro. A OpenAI diz que assume a responsabilidade pela correção dos resultados e que ajudou a preparar os manuscritos e a formalizar as provas, mas reconhece que os argumentos matemáticos vieram do sistema. A confirmação independente pela comunidade matemática ainda precisa situar os resultados e avaliar suas consequências.

O anúncio faz parte de um movimento da própria OpenAI para usar modelos em pesquisa. A empresa anunciou o ChatGPT for Academic Researchers, que oferece acesso gratuito aos melhores modelos do ChatGPT para 100,000 cientistas e matemáticos. Em May, durante a avaliação de um modelo não lançado, a OpenAI também divulgou uma refutação gerada por IA para a conjectura de Erdős sobre distâncias unitárias.

Esses casos mostram uma mudança em relação ao uso do modelo apenas para responder perguntas ou escrever código: a empresa o apresenta como gerador de argumentos para problemas de pesquisa. O comunicado, porém, fornece os resultados e os certificados, mas não detalha uma avaliação externa, o histórico completo de tentativas ou a comparação com técnicas humanas anteriores.