A maioria das aplicações práticas de inteligência artificial faz uso de princípios matemáticos que são incorporados ao sistema, de forma que basta à IA seguir o fluxo lógico da resolução de equações para atingir seu objetivo. A prova de teoremas matemáticos é mais complexa, pois exige o uso de raciocínio simbólico e a exploração de um número infinito de possíveis soluções. Um ser humano consegue provar um teorema se valendo em grande parte da intuição e da criatividade, habilidades mentais que têm se mostrado mais difíceis de incorporar em máquinas.
Mas no início do mês, a Meta anunciou um novo método que quebrou os recordes atuais de sistemas inteligentes artificiais na tarefa de provar teoremas matemáticos. Batizado de HyperTree Proof Search (HTPS), o sistema é treinado em um dataset de provas matemáticas bem sucedidas, aprendendo a generalizar o tipo de raciocínio envolvido para novos problemas.
As tentativas atuais de realizar essa tarefa têm aplicado uma abordagem que busca encontrar a solução em um “único passo”, mas os pesquisadores da Meta buscaram inspiração na maneira como um ser humano resolve o problema, quebrando-o em porções menores e fazendo progresso incremental, para desenvolver o novo sistema. O modelo foi desenhado para aplicar aprendizagem por reforço junto com os chamados assistentes de prova de conceito, que implementam um mecanismo de raciocínio passo-a-passo. Assim, cada etapa na resolução do problema, chamada nesse contexto de estado, é interpretado como um nó em um grafo. A partir deste ponto, é possível utilizar técnicas que já se mostraram bem sucedidas na implementação de IAs capazes de jogar xadrez ou Go.
Ao final do desenvolvimento, o desempenho do HTPS foi avaliado frente ao IMO, uma competição matemática para alunos do ensino médio que contém problemas em álgebra, análise combinatória, teoria numérica e geometria. As questões são tão desafiadoras que a maioria dos estudantes não consegue resolvê-las. A IA da Meta conseguiu solucionar 10 problemas, superando as 2 questões resolvidas por outras inteligências artificiais. O sistema ainda bateu o recorde de outros dois benchmarks matemáticos em pelo menos 10%.
A evolução dessa área deverá ajudar em tarefas práticas como a verificação de software, criptografia, e na área aeroespacial, que depende de simulações para maximizar a garantia da segurança.
O artigo que apresenta o modelo pode ser acessado aqui, e o modelo pode ser testado através de um plugin para VSCode.
