Durante quatro anos, o cientista da computação Trieu Trinh foi consumido por uma espécie de problema de metamatemática: como construir um modelo de IA que resolva problemas de geometria da Olimpíada Internacional de Matemática, a competição anual para os alunos do ensino médio com maior conhecimento matemático do mundo. .
Na semana passada, o Dr. Trinh defendeu com sucesso sua tese de doutorado sobre este tema na Universidade de Nova York; esta semana, ele descreveu o resultado de seu trabalho na revista Nature. Nomeado AlfaGeometriao sistema resolve problemas de geometria das Olimpíadas quase no nível de um medalhista de ouro humano.
Enquanto desenvolvia o projeto, o Dr. Trinh apresentou-o a dois cientistas pesquisadores do Google, e eles o contrataram como residente de 2021 a 2023. AlphaGeometry se junta à frota de sistemas de IA do Google DeepMind, que se tornou conhecido por enfrentar grandes desafios. Talvez o mais famoso, AlfaZero, um algoritmo de aprendizagem profunda, conquistou o xadrez em 2017. A matemática é um problema mais difícil, pois o número de caminhos possíveis para uma solução às vezes é infinito; o xadrez é sempre finito.
“Continuei entrando em becos sem saída, seguindo o caminho errado”, disse o Dr. Trinh, autor principal e força motriz do projeto.
Os coautores do artigo são o orientador de doutorado do Dr. Trinh, He He, na Universidade de Nova York; Yuhuai Wu, conhecido como Tony, cofundador da xAI (ex-Google) que em 2019 começou a explorar de forma independente uma ideia semelhante; Thang Luong, o investigador principal, e Quoc Le, ambos do Google DeepMind.
A perseverança do Dr. Trinh valeu a pena. “Não estamos fazendo melhorias incrementais”, disse ele. “Estamos dando um grande salto, um grande avanço em termos de resultado.”
“Só não exagere”, disse ele.
O grande salto
Trinh apresentou ao sistema AlphaGeometry um conjunto de testes de 30 problemas de geometria das Olimpíadas elaborados de 2000 a 2022. O sistema resolveu 25; historicamente, no mesmo período, o medalhista de ouro humano médio resolveu 25,9. Dr. Trinh também atribuiu os problemas a um sistema desenvolvido na década de 1970 que era conhecido por ser o mais forte provador de teorema de geometria; resolveu 10.
Nos últimos anos, o Google DeepMind realizou vários projetos investigando o aplicação de IA à matemática. E, de forma mais ampla, neste domínio de pesquisa, os problemas matemáticos das Olimpíadas foram adotados como referência; OpenAI e Meta AI alcançaram alguns resultados. Para motivação extra, há o Grande Desafio da IMOe um novo desafio anunciado em novembro, o Prêmio Olimpíada Matemática de Inteligência Artificialcom um pote de US$ 5 milhões indo para a primeira IA que ganhar o ouro nas Olimpíadas.
O artigo da AlphaGeometry abre com a afirmação de que a prova dos teoremas das Olimpíadas “representa um marco notável no raciocínio automatizado em nível humano”. Michael Barany, historiador da matemática e da ciência na Universidade de Edimburgo, disse que se perguntava se isso seria um marco matemático significativo. “O que a IMO está testando é muito diferente do que a matemática criativa parece para a grande maioria dos matemáticos”, disse ele.
Terence Tao, matemático da Universidade da Califórnia, em Los Angeles – e o mais jovem medalhista de ouro nas Olimpíadas, aos 12 anos – disse que achava que a AlphaGeometry era um “bom trabalho” e havia alcançado “resultados surpreendentemente fortes”. O ajuste fino de um sistema de IA para resolver problemas das Olimpíadas pode não melhorar as suas capacidades de investigação profunda, disse ele, mas neste caso a viagem pode revelar-se mais valiosa do que o destino.
Na opinião do Dr. Trinh, o raciocínio matemático é apenas um tipo de raciocínio, mas tem a vantagem de ser facilmente verificado. “A matemática é a linguagem da verdade”, disse ele. “Se você deseja construir uma IA, é importante construir uma IA confiável e que busque a verdade, em que você possa confiar”, especialmente para “aplicações críticas de segurança”.
Prova de conceito
AlphaGeometry é um sistema “neurossibólico”. Ele combina um modelo de linguagem de rede neural (bom em intuição artificial, como ChatGPT, mas menor) com um mecanismo simbólico (bom em raciocínio artificial, como uma espécie de calculadora lógica).
E é feito sob medida para geometria. “A geometria euclidiana é um bom campo de testes para o raciocínio automático, uma vez que constitui um domínio independente com regras fixas”, disse Heather Macbeth, geómetra da Universidade Fordham e especialista em raciocínio verificado por computador. (Quando adolescente, o Dr. Macbeth ganhou duas medalhas da IMO.) A AlphaGeometry “parece constituir um bom progresso”, disse ela.
O sistema possui dois recursos especialmente novos. Primeiro, a rede neural é treinada apenas com dados gerados por algoritmos – impressionantes 100 milhões de provas geométricas – sem usar exemplos humanos. O uso de dados sintéticos feitos do zero superou um obstáculo na prova automatizada de teoremas: a escassez de dados de treinamento à prova de humanos, traduzidos em uma linguagem legível por máquina. “Para ser honesto, inicialmente eu tinha algumas dúvidas sobre como isso teria sucesso”, disse o Dr.
Em segundo lugar, uma vez que o AlphaGeometry foi liberado para resolver um problema, o mecanismo simbólico começou a resolver; se travasse, a rede neural sugeria maneiras de aumentar o argumento da prova. O ciclo continuou até que uma solução se materializasse ou até o tempo acabar (quatro horas e meia). No jargão matemático, esse processo de aumento é chamado de “construção auxiliar”. Adicione uma linha, divida um ângulo, desenhe um círculo – é assim que os matemáticos, estudantes ou elite, mexem e tentam obter apoio em um problema. Nesse sistema, a rede neural aprendeu a fazer construções auxiliares, e de forma humana. Dr. Trinh comparou isso a enrolar um elástico em torno de uma tampa teimosa de frasco para ajudar a mão a segurar melhor.
“É uma prova de conceito muito interessante”, disse Christian Szegedy, cofundador da xAI que trabalhou anteriormente no Google. Mas “deixa muitas questões em aberto”, disse ele, e não é “facilmente generalizável para outros domínios e outras áreas da matemática”.
Dr. Trinh disse que tentaria generalizar o sistema em campos matemáticos e além. Ele disse que queria dar um passo atrás e considerar “o princípio subjacente comum” de todos os tipos de raciocínio.
Stanislas Dehaene, neurocientista cognitivo do Collège de France que tem um interesse de pesquisa em conhecimento geométrico básico, disse que ficou impressionado com o desempenho do AlphaGeometry. Mas ele observou que “não ‘vê’ nada sobre os problemas que resolve” – em vez disso, apenas utiliza codificações lógicas e numéricas de imagens. (Os desenhos no papel são para o benefício do leitor humano.) “Não há absolutamente nenhuma percepção espacial dos círculos, linhas e triângulos que o sistema aprende a manipular”, disse o Dr. Os pesquisadores concordaram que um componente visual poderia ser valioso; Luong disse que isso poderia ser adicionado, talvez dentro de um ano, usando o Gemini do Google, um sistema “multimodal” que ingere texto e imagens.
Soluções emocionantes
No início de dezembro, o Dr. Luong visitou seu antigo ensino médio na cidade de Ho Chi Minh, Vietnã, e mostrou AlphaGeometry ao seu ex-professor e treinador da IMO, Le Ba Khanh Trinh. Dr. Lê foi o maior medalhista de ouro na Olimpíada de 1979 e ganhou um prêmio especial por sua elegante solução geométrica. Lê analisou uma das provas da AlphaGeometry e achou-a notável, mas insatisfatória. Luong relembrou: “Ele achou-a mecânica e disse que lhe falta a alma, a beleza de uma solução que procura”.
Trinh já havia pedido a Evan Chen, estudante de doutorado em matemática no MIT – e treinador da IMO e medalhista de ouro nas Olimpíadas – para verificar alguns dos trabalhos da AlphaGeometry. Estava correto, disse Chen, e acrescentou que estava intrigado com a forma como o sistema encontrou as soluções.
“Gostaria de saber como a máquina está conseguindo fazer isso”, disse ele. “Mas, quero dizer, nesse caso, eu também gostaria de saber como os humanos também encontram soluções.”
