Inteligência Artificial na Olimpíada Internacional de Matemática: Como AlphaProof e AlphaGeometry 2 Alcançaram o Padrão de Medalha de Prata

O raciocínio matemático é um aspecto vital das capacidades cognitivas humanas, impulsionando o progresso em descobertas científicas e desenvolvimentos tecnológicos. À medida que nos esforçamos para desenvolver inteligência artificial geral que iguale a cognição humana, equipar a IA com capacidades de raciocínio matemático avançadas é essencial. Embora os sistemas de IA atuais possam lidar com problemas matemáticos básicos, eles lutam com o raciocínio complexo necessário para disciplinas matemáticas avançadas, como álgebra e geometria. No entanto, isso pode estar mudando, pois a Google DeepMind fez avanços significativos no aprimoramento das capacidades de raciocínio matemático de um sistema de IA. Essa conquista foi alcançada na Olimpíada Internacional de Matemática (IMO) 2024. Estabelecida em 1959, a IMO é a mais antiga e prestigiosa competição de matemática, desafiando estudantes do ensino médio em todo o mundo com problemas em álgebra, combinatoria, geometria e teoria dos números. Cada ano, equipes de jovens matemáticos competem para resolver seis problemas muito desafiadores. Este ano, a Google DeepMind introduziu dois sistemas de IA: AlphaProof, que se concentra em raciocínio matemático formal, e AlphaGeometry 2, que se especializa em resolver problemas geométricos. Esses sistemas de IA conseguiram resolver quatro dos seis problemas, performando no nível de um medalhista de prata. Neste artigo, exploraremos como esses sistemas funcionam para resolver problemas matemáticos.

AlphaProof: Combinando IA e Linguagem Formal para Prova de Teoremas Matemáticos

AlphaProof é um sistema de IA projetado para provar declarações matemáticas usando a linguagem formal Lean. Ele integra Gemini, um modelo de linguagem pré-treinado, com AlphaZero, um algoritmo de aprendizado por reforço renomado por dominar xadrez, shogi e Go.

O modelo Gemini traduz declarações de problemas de linguagem natural para declarações formais, criando uma biblioteca de problemas com diferentes níveis de dificuldade. Isso serve a dois propósitos: converter linguagem natural imprecisa em linguagem formal precisa para verificar provas matemáticas e usar as capacidades preditivas do Gemini para gerar uma lista de soluções possíveis com precisão de linguagem formal.

Quando o AlphaProof encontra um problema, ele gera soluções potenciais e procura por etapas de prova em Lean para verificar ou refutar essas soluções. Isso é essencialmente uma abordagem neuro-simbólica, onde a rede neural, Gemini, traduz instruções de linguagem natural em linguagem formal simbólica Lean para provar ou refutar a declaração. Semelhante ao mecanismo de autojogo do AlphaZero, onde o sistema aprende jogando jogos contra si mesmo, o AlphaProof se treina tentando provar declarações matemáticas. Cada tentativa de prova refina o modelo de linguagem do AlphaProof, com provas bem-sucedidas reforçando a capacidade do modelo de lidar com problemas mais desafiadores.

Para a Olimpíada Internacional de Matemática (IMO), o AlphaProof foi treinado provando ou refutando milhões de problemas que abrangem diferentes níveis de dificuldade e tópicos matemáticos. Esse treinamento continuou durante a competição, onde o AlphaProof aprimorou suas soluções até encontrar respostas completas para os problemas.

AlphaGeometry 2: Integrando LLMs e IA Simbólica para Resolver Problemas Geométricos

AlphaGeometry 2 é a última iteração da série AlphaGeometry, projetada para lidar com problemas geométricos com precisão e eficiência aprimoradas. Construindo sobre a fundação de sua predecessora, a AlphaGeometry 2 emprega uma abordagem neuro-simbólica que combina modelos de linguagem grandes (LLMs) com IA simbólica. Essa integração combina lógica baseada em regras com a capacidade preditiva de redes neurais para identificar pontos auxiliares, essenciais para resolver problemas geométricos. O LLM na AlphaGeometry prevê novas construções geométricas, enquanto a IA simbólica aplica lógica formal para gerar provas.

Quando enfrenta um problema geométrico, o LLM da AlphaGeometry avalia numerousas possibilidades, prevendo construções cruciais para a resolução do problema. Essas previsões servem como pistas valiosas, orientando o motor simbólico em direção a deduções precisas e avançando em direção a uma solução. Essa abordagem inovadora permite que a AlphaGeometry aborde desafios geométricos complexos que se estendem além de cenários convencionais.

Uma das principais melhorias na AlphaGeometry 2 é a integração do LLM Gemini. Esse modelo é treinado desde o início com significativamente mais dados sintéticos do que sua predecessora. Esse treinamento extensivo o equipa para lidar com problemas geométricos mais difíceis, incluindo aqueles que envolvem movimentos de objetos e equações de ângulos, razões ou distâncias. Além disso, a AlphaGeometry 2 apresenta um motor simbólico que opera duas ordens de magnitude mais rápido, permitindo que explore soluções alternativas com velocidade sem precedentes. Esses avanços tornam a AlphaGeometry 2 uma ferramenta poderosa para resolver problemas geométricos intricados, estabelecendo um novo padrão no campo.

AlphaProof e AlphaGeometry 2 na IMO

Este ano, na Olimpíada Internacional de Matemática (IMO), os participantes foram testados com seis problemas diversificados: dois em álgebra, um em teoria dos números, um em geometria e dois em combinatoria. Pesquisadores da Google traduziram esses problemas para linguagem matemática formal para o AlphaProof e a AlphaGeometry 2. O AlphaProof lidou com dois problemas de álgebra e um problema de teoria dos números, incluindo o problema mais difícil da competição, resolvido por apenas cinco concorrentes humanos este ano. Enquanto isso, a AlphaGeometry 2 resolveu com sucesso o problema de geometria, embora não tenha resolvido os dois desafios de combinatoria.

Cada problema na IMO vale sete pontos, totalizando um máximo de 42 pontos. O AlphaProof e a AlphaGeometry 2 conquistaram 28 pontos, alcançando escores perfeitos nos problemas que resolveram. Isso os colocou no alto da categoria de medalha de prata. O limite para a medalha de ouro este ano foi de 29 pontos, alcançado por 58 dos 609 concorrentes.

Próximo Salto: Linguagem Natural para Desafios Matemáticos

O AlphaProof e a AlphaGeometry 2 demonstraram avanços impressionantes nas capacidades de resolução de problemas matemáticos da IA. No entanto, esses sistemas ainda dependem de especialistas humanos para traduzir problemas matemáticos em linguagem formal para processamento. Além disso, não está claro como essas habilidades matemáticas especializadas possam ser incorporadas a outros sistemas de IA, como para explorar hipóteses, testar soluções inovadoras para problemas de longa data e gerenciar aspectos demorados das provas de forma eficiente.

Para superar essas limitações, pesquisadores da Google estão desenvolvendo um sistema de raciocínio de linguagem natural baseado no Gemini e em sua última pesquisa. Esse novo sistema visa avançar as capacidades de resolução de problemas sem exigir a tradução de linguagem formal e é projetado para integrar-se suavemente com outros sistemas de IA.

O Ponto de Vista Final

O desempenho do AlphaProof e da AlphaGeometry 2 na Olimpíada Internacional de Matemática é um salto notável para a frente na capacidade da IA de lidar com raciocínio matemático complexo. Ambos os sistemas demonstraram desempenho no nível de medalha de prata, resolvendo quatro dos seis problemas desafiadores, demonstrando avanços significativos na prova formal e na resolução de problemas geométricos. Apesar de seus feitos, esses sistemas de IA ainda dependem de entrada humana para traduzir problemas em linguagem formal e enfrentam desafios de integração com outros sistemas de IA. Pesquisas futuras visam aprimorar esses sistemas ainda mais, possivelmente integrando raciocínio de linguagem natural para estender suas capacidades em uma gama mais ampla de desafios matemáticos.