notícias

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Relatório do coração da máquina

Departamento Editorial de Coração de Máquina

Usando o modelo grande Gemini e o algoritmo de aprendizagem por reforço AlphaZero, você pode dominar geometria, álgebra e teoria dos números.

Para a IA, as Olimpíadas de Matemática não são mais um problema.

Na quinta-feira, a inteligência artificial do Google DeepMind completou uma façanha: usar IA para resolver a verdadeira questão da Olimpíada Internacional de Matemática IMO deste ano, e estava a apenas um passo de ganhar a medalha de ouro.

A competição da IMO que terminou na semana passada teve seis questões envolvendo álgebra, combinatória, geometria e teoria dos números. O sistema híbrido de IA proposto pelo Google acertou quatro questões e marcou 28 pontos, alcançando o patamar da medalha de prata.

No início deste mês, o professor titular da UCLA, Terence Tao, acabara de promover a Olimpíada de Matemática de IA (Prêmio de Progresso AIMO) com um prêmio de um milhão de dólares. Inesperadamente, o nível de resolução de problemas de IA melhorou para este nível antes de julho.

IMO, faça as perguntas simultaneamente e acerte as perguntas mais difíceis.

A IMO é a competição mais antiga, maior e mais prestigiada para jovens matemáticos, realizada anualmente desde 1959. Recentemente, a competição da IMO também foi amplamente reconhecida como um grande desafio no campo da aprendizagem automática, tornando-se uma referência ideal para medir as capacidades avançadas de raciocínio matemático dos sistemas de inteligência artificial.

Na competição IMO deste ano, AlphaProof e AlphaGeometry 2 desenvolvidos pela equipe DeepMind alcançaram em conjunto um marco histórico.

Entre eles, AlphaProof é um sistema de aprendizagem por reforço para raciocínio matemático formal, e AlphaGeometry 2 é uma versão melhorada do sistema de resolução de geometria AlphaGeometry da DeepMind.

Esta descoberta demonstra o potencial da inteligência artificial geral (AGI) com capacidades avançadas de raciocínio matemático para abrir novas áreas da ciência e da tecnologia.

Então, como o sistema de IA da DeepMind participou da competição da IMO?

Simplificando, esses problemas matemáticos são primeiro traduzidos manualmente para uma linguagem matemática formal para que o sistema de IA possa entendê-los. Na competição oficial, os competidores humanos submetem suas respostas em duas sessões (dois dias), com limite de tempo de 4,5 horas para cada sessão. O sistema de IA composto por AlphaProof+AlphaGeometry 2 resolveu um problema em poucos minutos, mas levou três dias para resolver outros problemas. Embora se você seguir estritamente as regras, o tempo limite do sistema DeepMind expirou. Algumas pessoas especulam que isso pode envolver muita quebra de força bruta.

AlphaProof resolveu dois problemas de álgebra e um problema de teoria dos números, determinando as respostas e provando sua correção, disse o Google. Estes incluem o problema mais difícil da competição, que apenas cinco concorrentes resolveram na IMO deste ano. E AlphaGeometry 2 prova um problema de geometria.

Solução fornecida pela IA: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html

O medalhista de ouro da IMO e medalhista Fields, Timothy Gowers, e duas vezes medalhista de ouro da IMO, Dr. Joseph Myers, presidente do Comitê de Seleção de Problemas da IMO 2024, pontuaram as soluções fornecidas pelo sistema combinado de acordo com as regras de pontuação da IMO.

Cada uma das seis questões vale 7 pontos, totalizando no máximo 42 pontos. O sistema da DeepMind recebeu uma pontuação final de 28, o que significa que todos os quatro problemas resolvidos receberam pontuações perfeitas – equivalente à pontuação mais alta na categoria medalha de prata. O limite da medalha de ouro deste ano foi de 29 pontos, e 58 dos 609 jogadores na competição oficial ganharam medalhas de ouro.

Este gráfico mostra o desempenho do sistema de inteligência artificial do Google DeepMind em relação aos concorrentes humanos na IMO 2024. O sistema marcou 28 pontos de um total de 42 pontos, alcançando o mesmo patamar do medalhista de prata da competição. Além disso, neste ano, 29 pontos podem valer a medalha de ouro.

AlphaProof: um método de raciocínio formal

Entre os sistemas híbridos de IA utilizados pelo Google, o AlphaProof é um sistema autotreinado que utiliza a linguagem formal Lean para provar afirmações matemáticas. Ele combina um modelo de linguagem pré-treinado com o algoritmo de aprendizagem por reforço AlphaZero.

Entre elas, as linguagens formais oferecem vantagens importantes para a verificação formal da correção das provas de raciocínio matemático. Até agora, isso tem sido de uso limitado no aprendizado de máquina porque a quantidade de dados escritos por humanos era muito limitada.

Em contraste, os métodos baseados em linguagem natural, apesar de terem acesso a maiores quantidades de dados, produzem etapas intermediárias de raciocínio e soluções que parecem razoáveis, mas são incorretas.

O Google DeepMind constrói uma ponte entre esses dois campos complementares, ajustando o modelo Gemini para traduzir automaticamente declarações de problemas em linguagem natural em declarações formais, criando assim uma grande biblioteca de problemas formais de dificuldade variada.

Dado um problema matemático, o AlphaProof gera soluções candidatas e depois as prova procurando possíveis etapas de prova no Lean. Cada solução de prova encontrada e verificada é usada para fortalecer o modelo de linguagem do AlphaProof e aprimorar sua capacidade de resolver problemas subsequentes mais desafiadores.

Para treinar o AlphaProof, o Google DeepMind provou ou refutou milhões de problemas matemáticos cobrindo uma ampla gama de dificuldades e tópicos nas semanas que antecederam a competição da IMO. Um ciclo de treinamento também é aplicado durante a competição para fortalecer a prova de variantes autogeradas do problema de competição até que uma solução completa seja encontrada.

Infográfico do processo de loop de treinamento de aprendizagem por reforço AlphaProof: Cerca de um milhão de problemas matemáticos informais são traduzidos para a linguagem matemática formal pela rede formal. O solucionador então procura na rede provas ou refutações do problema, treinando-se gradualmente para resolver problemas mais desafiadores usando o algoritmo AlphaZero.

AlphaGeometry 2 mais competitivo

AlphaGeometry 2 é uma versão significativamente melhorada do AlphaGeometry, a IA matemática que apareceu na revista Nature este ano. É um sistema híbrido neuro-simbólico em que o modelo de linguagem é baseado no Gemini e treinado do zero em uma ordem de grandeza com mais dados sintéticos do que seu antecessor. Isso ajuda o modelo a resolver problemas geométricos mais desafiadores, incluindo aqueles sobre movimento de objetos e equações de ângulos, proporções ou distâncias.

AlphaGeometry 2 apresenta um mecanismo simbólico duas ordens de magnitude mais rápido que seu antecessor. Quando novos problemas são encontrados, novos mecanismos de compartilhamento de conhecimento permitem combinações avançadas de diferentes árvores de busca para resolver problemas mais complexos.

Antes da competição deste ano, o AlphaGeometry 2 poderia resolver 83% de todos os problemas históricos de geometria da IMO nos últimos 25 anos, em comparação com apenas 53% do seu antecessor. No IMO 2024, o AlphaGeometry 2 resolveu o problema 4 em 19 segundos após receber sua formalização.

Um exemplo da questão 4 requer provar que a soma de ∠KIL e ∠XPY é igual a 180°. AlphaGeometry 2 propõe construir o ponto E na reta BI tal que ∠AEB = 90°. O ponto E ajuda a dar significado ao ponto médio L do segmento de reta AB, criando assim muitos pares de triângulos semelhantes, como ABE ~ YBI e ALE ~ IPC, para provar a conclusão.

O Google DeepMind também relata que, como parte do trabalho da IMO, os pesquisadores também estão experimentando um novo sistema de raciocínio em linguagem natural baseado no Gemini e um sistema de raciocínio em linguagem natural de última geração, na esperança de alcançar capacidades avançadas de resolução de problemas. O sistema não requer tradução de perguntas para linguagem formal e pode ser combinado com outros sistemas de IA. No teste das questões do concurso da IMO deste ano, “mostrou grande potencial”.

O Google continua explorando métodos de IA para aprimorar o raciocínio matemático e planeja divulgar mais detalhes técnicos sobre o AlphaProof em breve.

Estamos entusiasmados com um futuro em que os matemáticos usarão ferramentas de IA para explorar hipóteses, tentarão novas abordagens ousadas para resolver problemas de longa data e concluirão rapidamente elementos de provas demorados – e sistemas de IA como o Gemini farão a diferença na matemática e muito mais. O aspecto do raciocínio amplo torna-se ainda mais poderoso.

time de pesquisa

O Google disse que a nova pesquisa foi apoiada pela Olimpíada Internacional de Matemática e, além disso:

O desenvolvimento do AlphaProof foi liderado por Thomas Hubert, Rishi Mehta e Laurent Sartran; os principais colaboradores incluem Hussain Masoom, Aja Huang, Miklós Z. Horváth, Tom Zahavy, Vivek Veeriah, Eric Wieser, Jessica Yung, Lei Yu, Yannick Schroecker, Julian Schrittwieser, Ottavia Bertolli, Borja Ibarz, Edward Lockhart, Edward Hughes, Mark Rowland e Grace Margand.

Entre eles, Aja Huang, Julian Schrittwieser, Yannick Schroecker e outros membros também eram membros principais do jornal AlphaGo há 8 anos (2016). Há oito anos, o AlphaGo, que eles construíram com base no aprendizado por reforço, ficou famoso. Oito anos depois, o aprendizado por reforço brilha novamente no AlphaProof. Alguém lamentou no círculo de amigos: RL está de volta!

O trabalho de AlphaGeometry 2 e inferência de linguagem natural é liderado por Thang Luong. O desenvolvimento do AlphaGeometry 2 foi liderado por Trieu Trinh e Yuri Chervonyi, com importantes contribuições de Mirek Olšák, Xiaomeng Yang, Hoang Nguyen, Junehyuk Jung, Dawsen Hwang e Marcelo Menegali.

Além disso, David Silver, Quoc Le, Hassabis e Pushmeet Kohli são responsáveis ​​pela coordenação e gestão de todo o projeto.

Conteúdo de referência:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/