Suche
Mein Konto
Depois que o Google DeepMind derrotou os humanos em tudo, desde Jogue Vá para jogos de tabuleiro de estratégia,
agora afirma estar prestes a vencer os melhores alunos do mundo na resolução de problemas de matemática.
A sede em Londres Aprendizado de máquina A empresa anunciou em 25 de julho que seus sistemas de inteligência artificial (IA) resolveram quatro dos seis problemas apresentados aos alunos na Olimpíada Internacional de Matemática (IMO) de 2024 em Bath, no Reino Unido. A IA forneceu provas rigorosas e passo a passo avaliadas por dois matemáticos renomados e alcançou uma pontuação de 28/42 – apenas um ponto fora do território da medalha de ouro.
“É obviamente um avanço muito significativo”, diz Joseph Myers, um matemático de Cambridge, Reino Unido, que, juntamente com Tim Gowers, medalhista Fields, revisou as soluções e ajudou a selecionar os problemas originais para a IMO deste ano.
A DeepMind e outras empresas estão na corrida para fornecer às máquinas evidências importantes Resolva questões de pesquisa em matemática. Os problemas apresentados na IMO, a principal competição mundial para jovens matemáticos, tornaram-se uma referência para o progresso rumo a esse objetivo e são considerados um “grande desafio” para o aprendizado de máquina, disse a empresa.
“Esta é a primeira vez que um sistema de IA alcança desempenho de nível de medalha”, disse Pushmeet Kohli, vice-presidente de IA em ciência da DeepMind, em uma coletiva de imprensa. “Este é um marco importante na construção de investigadores de evidências avançados”, disse Kohli.
Extensão
Há apenas alguns meses, em janeiro, o sistema DeepMind Conquistas de nível de medalha AlphaGeometry alcançado na resolução de um tipo de problemas da IMO, nomeadamente os da geometria euclidiana. A primeira IA a ter um desempenho medalha de ouro no teste geral – incluindo questões de álgebra, combinatória e teoria dos números, geralmente consideradas mais desafiadoras do que geometria – será elegível para receber um prêmio de US$ 5 milhões, o AI Mathematics Olympiad Prize (AIMO). (O prêmio tem critérios rígidos, como divulgar o código-fonte e trabalhar com poder computacional limitado, o que significa que os esforços atuais da DeepMind não seriam qualificados.)
Na sua última tentativa, os investigadores usaram o AlphaGeometry2 para resolver o problema de geometria em menos de 20 segundos; a IA é uma versão melhorada e mais rápida de seu sistema de registro, diz Thang Luong, especialista em informática da DeepMind.
Para os demais tipos de questões, a equipe desenvolveu um sistema totalmente novo denominado AlphaProof. AlphaProof resolveu dois problemas de álgebra na competição e um de teoria dos números, o que durou três dias. (Os participantes do próprio IMO têm duas sessões de 4,5 horas cada.) Não foi possível resolver os dois problemas de combinatória, outra área da matemática.
Os pesquisadores obtiveram resultados mistos ao responder questões matemáticas usando modelos de linguagem – o tipo de sistema que alimenta chatbots como o ChatGPT. Às vezes, os modelos dão a resposta certa, mas não conseguem explicar racionalmente o seu raciocínio, e às vezes eles falam bobagens.
Na semana passada, uma equipe de pesquisadores das empresas de software Numina e HuggingFace usou um modelo de linguagem para ganhar um “prêmio de progresso” intermediário da AMIO baseado em versões simplificadas de problemas da IMO. As empresas tornaram todos os seus sistemas de código aberto e os disponibilizaram para download por outros pesquisadores. Mas os vencedores disseramNatureza, que os modelos de linguagem por si só provavelmente não seriam suficientes para resolver problemas mais difíceis.
Somente aula
AlphaProof combina um modelo de linguagem com tecnologia de aprendizado por reforço que usa o mecanismo “AlphaZero” que a empresa usou com sucesso para jogos de ataque como Go e alguns problemas matemáticos específicos usado. Na aprendizagem por reforço, uma rede neural aprende por tentativa e erro. Isto funciona bem quando suas respostas podem ser avaliadas usando um padrão objetivo. Para tanto, o AlphaProof foi treinado para ler e escrever provas em uma linguagem formal chamada Lean, que é usada no pacote de software 'Proof Assistant' de mesmo nome, popular entre os matemáticos. Para fazer isso, AlphaProof testou se suas saídas estavam corretas executando-as no pacote Lean, o que ajudou a preencher algumas etapas do código.
Treinar um modelo de linguagem requer grandes quantidades de dados, mas poucas provas matemáticas estavam disponíveis no Lean. Para superar esse problema, a equipe desenvolveu uma rede adicional que tentou traduzir um registro existente de um milhão de problemas escritos em linguagem natural, mas sem soluções escritas por humanos, para Lean, diz Thomas Hubert, pesquisador de aprendizado de máquina da DeepMind que co-liderou o desenvolvimento do AlphaProof. “Nossa abordagem foi: podemos aprender a provar mesmo que não tenhamos treinado originalmente em provas escritas por humanos?” (A empresa adotou uma abordagem semelhante ao Go, onde sua IA aprendeu a jogar jogando contra si mesma, e não da maneira como os humanos o fazem.)
Chaves mágicas
Muitas das traduções Lean não faziam sentido, mas foram suficientes para levar o AlphaProof ao ponto em que pudesse iniciar seus ciclos de aprendizagem por reforço. Os resultados foram muito melhores do que o esperado, disse Gowers na coletiva de imprensa. "Muitos problemas na IMO têm esta propriedade de chave mágica. O problema parece difícil no início, até que você encontre uma chave mágica que o abra", disse Gowers, que trabalha no Collège de France, em Paris.
Em alguns casos, o AlphaProof parecia ser capaz de fornecer aquele passo extra de criatividade, fornecendo um passo correto a partir de uma solução possível infinitamente grande. Mas é necessária uma análise mais aprofundada para determinar se as respostas foram menos surpreendentes do que pareciam, acrescentou Gowers. Um discurso semelhante surgiu após o surpreendente 'Trem 37', o bot DeepMinds AlphaGo em seu famosa vitória de 2016 sobre o melhor jogador humano de Go do mundo feito – um ponto de viragem para a IA.
Ainda não se sabe se as técnicas podem ser aperfeiçoadas para funcionar em nível de pesquisa em matemática, disse Myers na coletiva de imprensa. “Poderá expandir-se para outros tipos de matemática que podem não ter milhões de problemas treinados?”
"Estamos no ponto em que eles podem provar não apenas problemas de pesquisa abertos, mas também problemas que são muito desafiadores para os melhores jovens matemáticos do mundo", disse David Silver, especialista em computação da DeepMind, que foi o principal pesquisador do desenvolvimento do AlphaGo em meados da década de 2010.