Google AI quase perde medalha de ouro na IMO: resolve problema em 19 segundos, chocando juízes, habilidade geométrica supera humanos

O mais recente modelo matemático da DeepMind conquistou uma medalha de prata na Olimpíada Internacional de Matemática (IMO), com um desempenho excepcional. O modelo resolveu perfeitamente 4 das 6 questões, ficando a apenas 1 ponto da medalha de ouro. Particularmente na questão 4, o modelo apresentou uma solução em apenas 19 segundos, impressionando os avaliadores humanos com sua velocidade e qualidade de resolução.

AlphaProof

AlphaProof é um sistema capaz de provar proposições matemáticas na linguagem formal Lean. Ele combina um modelo de linguagem grande pré-treinado com o algoritmo de aprendizado por reforço AlphaZero.

Para superar as limitações das linguagens formais na aprendizagem de máquina devido aos dados limitados escritos por humanos, os pesquisadores preencheram a lacuna entre a linguagem natural e as declarações formais:

  1. Ajustando o modelo Gemini para traduzir automaticamente enunciados de problemas em linguagem natural para declarações formais
  2. Criando uma grande biblioteca de problemas formalizados de dificuldade variada

Ao resolver problemas, o AlphaProof gera soluções candidatas e as prova ou refuta buscando possíveis etapas de prova no Lean.

AlphaGeometry 2

AlphaGeometry 2 é um sistema híbrido neural-simbólico treinado do zero usando o modelo de linguagem Gemini. Ele pode resolver problemas de geometria mais difíceis que seu antecessor, incluindo aqueles envolvendo movimento de objetos, ângulos, proporções e equações de distância.

Melhorias principais incluem:

  1. Treinamento em dados sintéticos uma ordem de magnitude maior que a versão anterior
  2. Um mecanismo simbólico duas ordens de magnitude mais rápido que antes
  3. Um novo mecanismo de compartilhamento de conhecimento permitindo combinações avançadas de diferentes árvores de busca para resolver problemas mais complexos

O AlphaGeometry 2 demonstrou capacidades impressionantes, resolvendo 83% dos problemas de geometria da IMO dos últimos 25 anos, em comparação com 53% de seu antecessor. Na IMO deste ano, resolveu o Problema 4 em apenas 19 segundos após receber a questão formalizada.

O desempenho da IA na IMO demonstra progresso significativo nas capacidades de raciocínio matemático, aproximando a IA da resolução de problemas em nível humano em matemática avançada.