Ferramenta encontrou soluções pa questões complexas usando linguagem especializada.
A ferramenta de inteligência artificial AxiomProver, desenvolvida pela startup Axiom, encontrou soluções para quatro problemas matemáticos que permaneciam sem resposta até então. O anúncio foi feito pela empresa, que criou um sistema capaz de verificar provas matemáticas utilizando uma linguagem especializada chamada Lean.
Entre os problemas solucionados está uma conjectura proposta pelos matemáticos Dawei Chen e Quentin Gendron, que enfrentavam obstáculos em uma área da geometria algébrica relacionada a diferenciais.
De acordo com a Wired, os pesquisadores não conseguiam justificar uma fórmula da teoria dos números necessária para avançar em seu trabalho.
A solução surgiu após um encontro entre Chen e Ken Ono, matemático que recentemente deixou a Universidade da Virgínia, nos EUA, para integrar a equipe da Axiom. O encontro ocorreu durante uma conferência matemática em Washington, nos EUA, no mês passado. Depois que Chen explicou o problema, Ono apresentou uma prova gerada pelo AxiomProver no dia seguinte.
“Tudo se encaixou naturalmente depois disso”, afirma Chen, que trabalhou com a Axiom para documentar a prova.
A ferramenta de IA identificou uma conexão entre o problema e um fenômeno numérico estudado inicialmente no século XIX. A prova desenvolvida e verificada pelo sistema está disponível no repositório arXiv.
“O que o AxiomProver encontrou foi algo que todos os humanos haviam perdido”, explica Ono.
Outros problemas resolvidos
Além da conjectura Chen-Gendron, o AxiomProver solucionou outros três problemas matemáticos complexos. Um deles foi a Conjectura de Fel, relacionada a syzygies (expressões matemáticas onde números se alinham em álgebra). Esta conjectura envolve fórmulas encontradas originalmente no caderno do matemático indiano Srinivasa Ramanujan há mais de 100 anos.
O terceiro problema resolvido pela IA aborda um modelo probabilístico de “becos sem saída” na teoria dos números.
Já o quarto utiliza ferramentas matemáticas originalmente desenvolvidas para solucionar o Último Teorema de Fermat.
“Este é um novo paradigma para provar teoremas”, afirma Ono sobre a prova gerada por IA para a conjectura Chen-Gendron.
Tecnologia e aplicações
A Axiom, cofundada por Carina Hong (atual CEO), combina modelos de linguagem grandes com o sistema proprietário AxiomProver. A empresa treinou a tecnologia para raciocinar através de problemas matemáticos e chegar a soluções comprovadamente corretas.
“A matemática é realmente o grande campo de testes e sandbox para a realidade”, diz Hong. “Acreditamos que existem muitos casos de uso bastante importantes de alto valor comercial.”
Em 2024, o Google apresentou uma ideia semelhante com um sistema chamado AlphaProof. No entanto, segundo Hong, o AxiomSolver incorpora avanços significativos e técnicas mais recentes.
As técnicas desenvolvidas pela Axiom podem ter aplicações além da matemática pura. Isso porque a mesma abordagem poderia ser utilizada para desenvolver software mais resistente a certos tipos de ataques cibernéticos, usando IA para verificar que o código é comprovadamente confiável.
Impacto na comunidade científica
Scott Kominers, professor da Harvard Business School familiarizado com a tecnologia da Axiom, expressa seu entusiasmo: “Mesmo como alguém que tem acompanhado de perto a evolução das ferramentas matemáticas de IA por anos e trabalhado com elas, acho isso bastante surpreendente. Não é apenas o fato de que o AxiomProver conseguiu resolver um problema como este de forma totalmente automatizada e instantaneamente verificada, o que por si só é incrível, mas também a elegância e beleza da matemática que produziu.”
Para Ono, a tecnologia também oferece insights sobre o próprio processo matemático: “Estou interessado em tentar entender se você pode tornar esses momentos de descoberta previsíveis. E estou aprendendo muito sobre como provei alguns dos meus próprios teoremas.”
Chen, por outro lado, vê a IA como uma ferramenta complementar ao trabalho dos matemáticos: “Os matemáticos não esqueceram as tabuadas após a invenção da calculadora. Acredito que a IA servirá como uma nova ferramenta inteligente (ou talvez ‘parceiro inteligente’ seja mais apropriado) abrindo horizontes mais ricos e amplos para a pesquisa matemática.”
Por: Giz_br
