Astra: quando a IA começa a produzir matemática verificável
Astra: quando a IA começa a produzir matemática verificável
A OpenAI revelou que uma versão interna do Astra, descrito como a próxima grande família de modelos da empresa, produziu avanços em dez problemas abertos de matemática e ciência da computação teórica. Não se trata de uma demonstração sobre responder a perguntas ou gerar código.. são na realidade resultados que incidem directamente sobre questões de investigação com décadas de história.
Os problemas abrangem áreas muito diferentes, incluindo geometria de alta dimensão, teoria de códigos, teoria de grupos, complexidade de circuitos, jogos quânticos, criptografia. Entre os resultados divulgados está a construção de grupos não-sofic, uma questão central da teoria de grupos, bem como uma refutação da conjectura de rigidez de Connes. Foram igualmente apresentados novos limites para o empacotamento de esferas em dimensões elevadas e avanços relativos a problemas colocados por Paul Erdős.
Uma alegação especialmente relevante é que o sistema chegou a argumentos novos. A OpenAI disponibilizou certificados em Lean para cada resultado. Lean é um assistente de prova que permite verificar formalmente, passo a passo, se uma demonstração respeita as regras lógicas definidas. Essa formalização não substitui a apreciação científica humana, mas reduz de forma substancial a dificuldade de auditar provas complexas.
O custo estimado para encontrar as soluções foi de cerca de 2.000 dólares, calculado com base nas tarifas de API indicadas pela empresa. O número deve ser lido com cautela, porque não representa todo o investimento necessário para treinar, avaliar e operar um modelo de fronteira. Ainda assim, ilustra como uma capacidade de investigação antes reservada a equipas especializadas pode tornar-se mais acessível quando é distribuída por ferramentas computacionais.
Há apenas alguns anos, modelos de linguagem cometiam erros elementares em aritmética e falhavam cadeias curtas de raciocínio formal. A passagem para resultados auditáveis em problemas abertos não significa que o erro tenha desaparecido, mas mostra uma mudança de escala! O objetivo agora já não é apenas automatizar tarefas conhecidas, mas explorar hipóteses e construir argumentos em territórios onde não existe uma resposta estabelecida.
Esta evolução também reforça a importância dos agentes de IA capazes de trabalhar durante períodos mais longos. Em vez de produzir uma resposta isolada, um sistema poderá dividir um problema, procurar literatura, formular conjecturas, testar contra-exemplos, formalizar resultados e rever a própria abordagem. A utilidade real dependerá menos de uma única resposta brilhante e mais da fiabilidade de todo esse processo.
O potencial para a ciência é considerável. Matemática, descoberta de materiais, física, biologia e engenharia contêm problemas cuja dificuldade não decorre da falta de talento, mas do tempo limitado disponível para explorar possibilidades. Ferramentas que acelerem essa exploração podem ampliar o trabalho dos investigadores, desde que os resultados permaneçam transparentes, reproduzíveis e sujeitos a escrutínio independente.
O Astra ainda não foi lançado publicamente e a OpenAI não confirmou se será associado a uma futura versão GPT ou a uma designação autónoma. Por isso, qualquer previsão sobre disponibilidade, funcionalidades finais ou desempenho fora deste contexto permanece especulativa.
A IA já começa a ser avaliada não apenas pela fluidez com que comunica, mas pela sua capacidade de contribuir para descobertas que possam ser verificadas...
