Num salto significativo para a inteligência artificial, uma equipa de investigação da Universidade de Pequim desenvolveu um sistema de IA capaz de resolver problemas matemáticos complexos e não resolvidos por si só. O sistema abordou com sucesso uma conjectura de álgebra de uma década, marcando uma mudança da IA como um mero assistente para a IA como um pesquisador autônomo.
Quebrando a conjectura da álgebra
O problema central desta descoberta foi uma conjectura de álgebra proposta pela primeira vez em 2014 pelo falecido Dan Anderson, ex-professor da Universidade de Iowa. Durante dez anos, o problema permaneceu um desafio aberto no campo da álgebra comutativa.
Ao contrário dos modelos anteriores de IA que requerem orientação humana constante, este novo sistema processou décadas de literatura matemática para resolver a conjectura e, o que é crucial, verificou as suas próprias descobertas sem intervenção humana. Todo o processo foi concluído em 80 horas de execução.
A Arquitetura da Autonomia: Rethlas e Archon
Para superar as limitações tradicionais da IA em matemática, os pesquisadores se afastaram dos Grandes Modelos de Linguagem (LLMs) padrão, que são frequentemente propensos a “alucinações” ou erros lógicos. Em vez disso, eles construíram uma estrutura de agente duplo projetada para imitar o fluxo de trabalho rigoroso dos matemáticos humanos:
- O Agente Raciocinador (Rethlas): Este sistema atua como o “pensador”. Ele utiliza um mecanismo de busca de teoremas chamado Matlas para explorar várias estratégias e caminhos matemáticos para resolver um problema.
- O Agente de Formalização (Arconte): Assim que uma prova potencial for encontrada, o Arconte assume o controle. Usando LeanSearch, ele traduz o raciocínio informal em um formato formal e verificável por máquina.
- O Verificador (Lean 4): O sistema usa o Lean 4, uma linguagem de programação especializada e um provador de teoremas interativo, para garantir que a prova seja matematicamente sólida e livre de erros.
Por que isso é importante: da assistência à automação
As tendências atuais da IA mostram um enorme impulso em direção a modelos de treinamento em matemática, mas a maioria ainda luta com a “lacuna de rigor”. Embora os humanos possam escrever provas, eles podem cometer erros; embora os LLMs possam gerar texto rapidamente, muitas vezes falta-lhes a precisão lógica necessária para matemática de alto nível.
Este estudo da Universidade de Pequim aborda essa lacuna integrando o raciocínio em linguagem natural com a verificação formal. Esta abordagem dupla garante que a IA não apenas “adivinha” uma resposta, mas constrói uma prova que pode ser provada matematicamente como correta.
Além disso, os pesquisadores observaram que a IA demonstrou uma capacidade única de executar tarefas que normalmente exigem colaboração interdisciplinar, atuando efetivamente como vários especialistas trabalhando em conjunto.
O Futuro da Pesquisa Matemática
Embora o sistema funcionasse de forma autónoma, os investigadores notaram que a intervenção humana ainda pode funcionar como um acelerador. Um matemático guiando o agente “Arconte” pode acelerar o processo de formalização, sugerindo um futuro onde os humanos e a IA trabalharão em um ciclo simbiótico de alta velocidade.
“Este trabalho fornece um exemplo concreto de como a pesquisa matemática pode ser substancialmente automatizada usando IA”, afirmaram os pesquisadores.
Conclusão
Ao combinar o raciocínio com uma verificação formal rigorosa, esta nova estrutura leva a IA além da simples computação e para o domínio da descoberta científica autónoma. Este avanço abre caminho para que a IA resolva problemas cada vez mais complexos em matemática e outros campos científicos altamente técnicos.
