Google DeepMind avança na conquista da matemática de alto nível

Embora computadores sejam reconhecidos por superar humanos em cálculos, a matemática de alto nível ainda era um domínio exclusivamente humano. No entanto, um avanço da Google DeepMind trouxe sistemas de inteligência artificial (IA) mais perto do que nunca de superar os melhores matemáticos humanos em seu próprio jogo.

Dois novos sistemas, chamados AlphaProof e AlphaGeometry 2, trabalharam juntos para enfrentar questões da Olimpíada Internacional de Matemática, uma competição global para estudantes do ensino médio que ocorre desde 1959. A olimpíada consiste em seis questões extremamente desafiadoras por ano, cobrindo áreas como álgebra, geometria e teoria dos números. Ganhar uma medalha de ouro coloca você entre os melhores jovens matemáticos do mundo.

Os esforços combinados dos dois sistemas da DeepMind não alcançaram exatamente esse nível. Após suas respostas serem corrigidas pelo Prof. Timothy Gowers – ganhador do equivalente matemático do Prêmio Nobel, a Medalha Fields, e também medalhista de ouro na olimpíada –, a equipe da DeepMind marcou 28 de 42 pontos – suficiente para uma medalha de prata, mas a um ponto da de ouro.

Diferentemente de um matemático humano, os sistemas eram perfeitos ou completamente perdidos. Em cada uma das questões que resolveram, obtiveram pontuação máxima, mas em duas das seis questões, foram incapazes até mesmo de começar a trabalhar em uma resposta. Além disso, a DeepMind, diferentemente dos competidores humanos, não teve limite de tempo. Enquanto os estudantes têm nove horas para enfrentar os problemas, os sistemas da DeepMind levaram três dias trabalhando ininterruptamente para resolver uma questão, apesar de resolver outra em segundos.

Os dois sistemas que trabalharam no desafio eram muito diferentes um do outro. O AlphaProof, que resolveu três dos problemas, funciona combinando um grande modelo de linguagem – do tipo usado em chatbots de consumo – com uma abordagem especializada de “aprendizado por reforço”, semelhante à usada pela DeepMind para enfrentar o jogo de Go. O truque está em aproveitar uma abordagem preexistente chamada “matemática formal”, um conjunto de regras que permite escrever uma prova matemática como um programa que só pode ser executado se for verdadeiro.

“O que tentamos fazer é construir uma ponte entre essas duas esferas”, disse Thomas Hubert, líder do AlphaProof, “para que possamos aproveitar as garantias que vêm com a matemática formal e os dados disponíveis na matemática informal”. Depois de ser treinado em um vasto número de problemas matemáticos escritos em inglês, o AlphaProof usou seu conhecimento para tentar gerar provas específicas na linguagem formal. Como essas provas podem ser verificavelmente verdadeiras ou falsas, é possível ensinar o sistema a se melhorar. A abordagem pode resolver problemas difíceis, mas nem sempre é rápida: embora seja muito melhor do que simples tentativa e erro, levou três dias para encontrar o modelo formal correto para uma das questões mais difíceis do desafio.

O outro sistema, AlphaGeometry 2, combina de forma semelhante um modelo de linguagem com uma abordagem mais inclinada para a matemática. Mas seu sucesso no campo mais restrito dos problemas de geometria foi surpreendente: ele resolveu seu problema em apenas 16 segundos. E, segundo Gowers, escolheu uma rota surpreendente para fazê-lo. “Houve alguns exemplos lendários de provas [auxiliadas por computador] que são mais longas que a Wikipédia. Esse não foi o caso: estamos falando de um resultado muito curto, no estilo humano”.

O líder do AlphaGeometry 2, Thang Luong, descreveu a saída como semelhante à famosa “jogada 37” na histórica vitória da DeepMind no Go, quando o sistema de IA fez uma jogada que nenhum humano teria pensado e continuou a vencer. A prova do AlphaGeometry 2 envolveu construir um círculo em torno de outro ponto e, em seguida, usar esse círculo para provar a resposta geral. “No início, nosso especialista não entendeu muito bem por que ele construiu aquele ponto”, disse Luong. “Mas depois de olhar para a solução, ele realmente conecta muitos triângulos e eles acharam que a solução era realmente bastante elegante”.

Leia também: