IA da DeepMind resolve problemas da Olimpíada Internacional de Matemática em nível de medalha de prata

(deepmind.google)

3 pontos por GN⁺ 2024-07-26 | 3 comentários | Compartilhar no WhatsApp

No IMO 2024, uma das principais provas de raciocínio matemático avançado, o AlphaProof e o AlphaGeometry 2, do Google DeepMind, resolveram 4 de 6 problemas, alcançando pela primeira vez para uma IA uma pontuação equivalente à faixa de medalha de prata
Obtiveram 28 pontos de um total de 42; todos os problemas resolvidos receberam pontuação máxima, ficando apenas 1 ponto abaixo do corte da medalha de ouro de 2024, que foi 29
A avaliação foi conduzida por matemáticos segundo as regras de correção da IMO; álgebra e teoria dos números ficaram a cargo do AlphaProof, enquanto geometria ficou com o AlphaGeometry 2, combinando diferentes métodos de raciocínio
Os problemas foram primeiro traduzidos manualmente para uma linguagem matemática formal; enquanto a competição estudantil tem duas sessões de 4,5 horas, o sistema levou de alguns minutos em um problema a até 3 dias nos demais
O resultado mostra que a IA para matemática foi além do simples cálculo e se aproximou da busca e verificação de provas, mas a entrada formalizada e o longo tempo de resolução ainda permanecem como limitações importantes

Pontuação na faixa de medalha de prata na IMO 2024

O Google DeepMind apresentou o sistema de raciocínio matemático AlphaProof e a versão aprimorada do sistema de resolução de problemas de geometria, AlphaGeometry 2
Os dois sistemas resolveram 4 dos 6 problemas da International Mathematical Olympiad de 2024
- AlphaProof: resolveu 2 problemas de álgebra e 1 de teoria dos números
- AlphaGeometry 2: provou 1 problema de geometria
- 2 problemas de combinatória não foram resolvidos
Cada problema vale no máximo 7 pontos, com pontuação total de 42
- O sistema recebeu pontuação máxima nos 4 problemas resolvidos, obtendo 28 pontos
- Isso corresponde à parte superior da faixa de medalha de prata na IMO 2024
- O corte para medalha de ouro em 2024 foi 29 pontos, e na competição oficial 58 de 609 participantes alcançaram a faixa de medalha de ouro
É o primeiro caso em que um sistema de IA obteve na IMO um desempenho equivalente ao de um medalhista de prata

Método de avaliação e condições de resolução

Foram usados os problemas da competição fornecidos pelos organizadores da IMO
As respostas foram avaliadas de acordo com as regras de pontuação da IMO
- Os avaliadores foram o Prof Sir Timothy Gowers, medalhista de ouro da IMO e vencedor da Fields Medal, e o Dr Joseph Myers, duas vezes medalhista de ouro da IMO e presidente do Problem Selection Committee da IMO 2024
Para que o sistema pudesse entender os problemas, todos eles foram primeiro traduzidos manualmente para uma linguagem matemática formal
Na competição oficial, os estudantes enviam respostas durante duas sessões de 4,5 horas
- O sistema de IA resolveu um problema em poucos minutos, enquanto os demais levaram até 3 dias
Entre os problemas resolvidos pelo AlphaProof estava o mais difícil da IMO 2024, resolvido por apenas 5 participantes

AlphaProof: raciocínio formal baseado em Lean

AlphaProof é um sistema treinado para provar proposições matemáticas na linguagem formal Lean
Combina um modelo de linguagem pré-treinado com o algoritmo de aprendizado por reforço AlphaZero
- AlphaZero é o algoritmo usado para aprender sozinho xadrez, shogi e Go
O uso de uma linguagem formal permite a verificação de correção de provas que incluem raciocínio matemático
Até então, havia muito poucos dados de provas formais escritas por humanos, o que limitava o uso de linguagens formais em machine learning
Abordagens baseadas em linguagem natural podem usar muito mais dados, mas também podem gerar etapas intermediárias de raciocínio ou respostas que parecem plausíveis, porém estão incorretas
A DeepMind ajustou modelos Gemini para traduzir automaticamente problemas em linguagem natural para proposições formais e criou uma biblioteca de problemas formais de vários níveis de dificuldade
Quando recebe um problema, o AlphaProof gera candidatos de resposta e então explora, no Lean, etapas de prova possíveis para prová-los ou refutá-los
- Provas descobertas e verificadas são usadas para reforçar o modelo de linguagem do AlphaProof
- Esse processo iterativo é usado para aumentar sua capacidade de resolver problemas mais difíceis
Durante a preparação para a IMO, o sistema aprendeu por várias semanas provando ou refutando milhões de problemas
- Durante a competição, também foi aplicado um loop de aprendizado que reforçava provas de variantes autogeradas dos problemas enquanto buscava uma solução completa

AlphaGeometry 2: expansão para problemas de geometria mais difíceis

AlphaGeometry 2 é uma versão amplamente aprimorada do AlphaGeometry anterior
O sistema tem uma arquitetura híbrida neuro-simbólica, combinando redes neurais e raciocínio simbólico
- O modelo de linguagem é baseado no Gemini
- Foi treinado do zero com uma ordem de grandeza a mais de dados sintéticos do que a versão anterior
Graças a mais dados e a um modelo melhorado, passou a lidar com problemas de geometria mais difíceis que incluem movimento de objetos e equações de ângulos, razões e distâncias
O motor simbólico do AlphaGeometry 2 é dezenas de vezes mais rápido que o da versão anterior
Ao receber um novo problema, ele usa um novo mecanismo de compartilhamento de conhecimento para aproveitar combinações avançadas de diferentes árvores de busca e tratar problemas mais complexos
Taxa de resolução de problemas de geometria da IMO nos últimos 25 anos: {b:83,53}
- Antes da competição de 2024, o AlphaGeometry 2 conseguia resolver 83% dos problemas de geometria da IMO dos últimos 25 anos
- A taxa de resolução do AlphaGeometry anterior era de 53%
Na IMO 2024, resolveu o Problem 4 em 19 segundos após a entrada formalizada

Raciocínio em linguagem natural e usos futuros

Como parte do trabalho com a IMO, a DeepMind também experimentou um sistema de raciocínio em linguagem natural baseado no Gemini e em pesquisas recentes
Esse sistema não precisa traduzir problemas para uma linguagem formal e pode ser combinado com outros sistemas de IA
A abordagem também foi testada nos problemas da IMO 2024, e os resultados foram avaliados como promissores
A metodologia mais técnica do AlphaProof foi publicada em um artigo na Nature
A DeepMind mira um futuro em que matemáticos possam explorar hipóteses com ferramentas de IA, tentar novas abordagens para problemas antigos e concluir rapidamente partes demoradas de provas

3 comentários

chabulhwi 2024-07-26

Quanto mais matemáticos contribuírem para o desenvolvimento de bibliotecas de matemática formal, mais fácil será criar IAs matemáticas com bom desempenho. Até onde eu sei, atualmente há 3 coreanos transferindo para a Mathlib, a biblioteca matemática do Lean, teorias matemáticas que eles próprios formalizaram na linguagem do assistente de provas Lean.

No ano passado, participei um pouco do trabalho de migração da Mathlib do Lean 3 para o Lean 4 e, neste ano, provei um teorema em aberto na biblioteca Batteries do Lean 4.

GN⁺ 2024-07-26

Opiniões do Hacker News

Estou realmente muito animado com esse anúncio, mas não está claro quanto trabalho está embutido na frase “primeiro os problemas foram traduzidos manualmente para uma linguagem matemática formal, para que o sistema pudesse entendê-los”
Todos os problemas que não eram de geometria tinham a forma “encontre todos os X tais que...”, e a afirmação do teorema tinha a forma “mostre que o conjunto de todos os X é {foo}”
Só olhando as soluções para download em https://storage.googleapis.com/deepmind-media/DeepMind.com/B..., é difícil saber se, na etapa de tradução, uma pessoa definiu {foo} ou se o computador o encontrou. Quero acreditar que foi o computador, mas não encontrei uma base para confirmar
- O computador encontrou a resposta diretamente. Ou seja, no P1 ele encontrou inteiros pares, no P2 {1,1} e no P6 2, e em cada caso também apresentou uma prova em Lean
- De modo geral, essa etapa de tradução é muito mais fácil do que a etapa de prova. O problema da tradução automática é que o resultado da tradução pode estar errado
  Isso também acontece com frequência quando humanos lidam diretamente com métodos formais, então os pesquisadores provavelmente concluíram que, seja com LLMs ou outras ferramentas, no fim todas as traduções teriam de ser auditadas
- A página vinculada diz que “os enunciados dos problemas foram formalizados em Lean por humanos, mas as respostas dentro dos enunciados foram geradas e formalizadas pelo agente”
  Ainda assim, não fica claro que forma inicial foi dada ao agente para que essa etapa fosse possível
- É interessante que houvesse uma ferramenta de formalização usada para criar os dados de treinamento, mas que ela não tenha sido usada aqui. Talvez ainda não fosse confiável o suficiente
- Pelo que entendi da explicação, “dado um problema, o AlphaProof gera uma candidata a solução e então busca, no Lean, possíveis passos de prova para demonstrá-la ou refutá-la”
  Ou seja, seja qual for o tipo de “problema” que o AlphaProof recebe, e seja como ele tenha formalizado “encontre todos os X tais que...”, parece que ele provavelmente gera teoremas candidatos em Lean. Por exemplo, poderia ser algo como o conjunto ter a forma {n: P(n)} para alguma fórmula P. Depois disso, ele busca a prova
  Se o AlphaProof não encontrou {foo}, mas isso foi dado a ele, então afirmar que ele resolveu o problema pareceria bastante absurdo. Mesmo assim, estou muito animado com esse resultado
É certamente impressionante, mas é preciso cuidado quando a IMO é mencionada. Medalhas são concedidas a 50% dos participantes, isto é, estudantes do ensino médio, e a proporção entre ouro, prata e bronze é 1:2:3, então os medalhistas de ouro e prata ficam entre os 25% melhores de todos os participantes
Portanto, a formulação seria “a IA resolveu problemas da IMO melhor do que 75% dos estudantes”, o que na verdade também pode ser mais impressionante
Mas a condição de “um problema em alguns minutos, os demais em até 3 dias cada” é diferente das 9 horas que os estudantes recebem, então é difícil ver isso como uma comparação verdadeira. Se os estudantes também tivessem recebido até 15 dias em vez de 9 horas, mais pessoas teriam igualado ou superado essa pontuação
Na prática, a IA resolveu apenas um problema dentro das 9 horas dadas aos estudantes, então provavelmente teria ficado longe da faixa de medalhas. Fico me perguntando se há necessidade de ofuscar um resultado tão impressionante com uma comparação entre maçãs e laranjas
De forma mais objetiva, bastaria informar que levou mais tempo, mas resolveu X% do total de problemas, ou que obteve X pontos de N possíveis
- Já conheci participantes da IMO, e eles são absurdamente inteligentes. Antes de ter contato com um grupo desses, eu não imaginava que pessoas pudessem ser tão inteligentes. Então é preciso pensar neles como algo próximo dos 25% melhores dentro dos 0,01% melhores de todos os estudantes do ensino médio
  Aqui, o tempo não é um eixo tão interessante. Humanos não usam uma CPU equivalente a um enorme cluster de GPUs. A dicotomia mais interessante é “com recursos suficientes, consegue chegar à solução?”, e para GPT/Claude a resposta era claramente não
- A frase “medalhas são concedidas a 50% dos participantes do ensino médio” pode ser confusa, porque os estudantes do ensino médio mencionados aqui não são uma amostra de estudantes comuns. Pelo que sei, são equipes nacionais compostas por cerca de 6 pessoas que são os maiores craques em resolver problemas de olimpíada em cada país
- Pessoalmente, e esta não é a posição do Google, acho que o único motivo pelo qual não ganhou medalha de ouro este ano foi a má sorte na seleção dos problemas e o fato de não ter buscado pontuação parcial em P3/P5
  Ficou muito perto do corte, e normalmente até um pequeno progresso já pode render 1 ponto. Dito isso, não teria sido bom ver matérias dizendo que ganhou ouro por razões técnicas, então parece que se contentaram com uma prata sem controvérsia
- A diferença central entre dar mais tempo a humanos e dar mais tempo a um programa de computador é que, historicamente, tivemos muito mais sucesso em fazer este último rodar mais rápido
- A maior parte da pesquisa da DeepMind é um centro de custos do ponto de vista da empresa. Comunicados de imprensa como este ajudam a justificar o investimento contínuo perante investidores e o público
Isso é real. O AlphaGeometry resolveu um conjunto muito limitado de problemas com muita busca por força bruta
Este método é muito mais amplo, e acho que terá um grande impacto na forma como se faz matemática. Ele vai da matemática em linguagem natural para a matemática formalizada e, a partir daí, implementa de fato um pipeline autoalimentado capaz de treinar tanto a formalização quanto as provas
Em princípio, esse pipeline também pode aprender construção teórica básica, como gerar definições auxiliares e lemas. É algo próximo do cálice sagrado da assistência a provas, e acho que permitirá formalizar a maior parte da matemática que produzimos naturalmente. Humanos trabalharão no modo de rigorizar a posteriori, e as máquinas ajudarão a preencher os detalhes
- Concordo. É um grande avanço. Problemas de geometria pertencem a outra categoria, porque podem ser traduzidos para sistemas de equações polinomiais e resolvidos com algoritmos de álgebra computacional bem conhecidos
  Em contraste, esse tipo de formalização aberta era uma área em que o progresso vinha sendo muito lento e incremental. Trabalhei em uma área adjacente há 5 anos, e dá para dizer que este resultado está em um nível inalcançável por técnicas tradicionais de raciocínio automático
  Prova automática de teoremas de verdade é útil de forma muito mais ampla do que apenas na matemática pura. Por exemplo, é possível escrever em Lean a semântica axiomática de uma pequena linguagem de programação e fazer perguntas como “mostre que existe um programa que satisfaz esta especificação”
  Se esta abordagem escalar, ela será mais importante do que qualquer aplicação de aprendizado de máquina lançada nos últimos anos
- Não se deve subestimar a busca. Pode parecer força bruta, mas a busca superou o nível humano no go e chegou ao nível de medalha de prata da IMO
  A evolução que nos criou também é uma busca movida por enormes tentativas de força bruta, e a pesquisa no método científico também é essencialmente busca
- Já há pessoas trabalhando nessa área
  https://leandojo.org/
  https://machine-learning-for-theorem-proving.github.io/
  https://www.youtube.com/watch?v=P5ew0BrRm_I
  https://paperswithcode.com/task/automated-theorem-proving
  https://old.reddit.com/r/math/comments/11mb9lx/future_of_aut...
  https://github.com/RiccardoBiosas/LeanGPT
- Sistemas assim parecem que serão muito mais úteis fora da pesquisa matemática
  Para fazer algo útil, não é necessário provar problemas extremamente difíceis. Muitas vezes basta provar coisas simples. Se você pede a um modelo de linguagem para concluir uma tarefa, organizar itens, coordenar agenda, escrever código que faça X etc., é difícil confiar imediatamente no resultado, mas, se o sistema conseguir traduzir parte do problema para lógica e encontrar uma solução, isso se torna muito mais confiável
- Não. É só parecido com permitir o uso de um mecanismo de busca para encontrar soluções, nada além disso
O ponto principal acaba ficando um pouco escondido: eles estão usando Lean
Isso é importante para além de problemas de matemática. Fazer modelos de aprendizado de máquina brigarem com sistemas de prova é uma boa forma de evitar bobagens genéricas
Espero que, no futuro, mais gente escreva tipos no Lean ou em sistemas parecidos e use isso como uma forma muito melhor de escrever prompts
- O AlphaProof é claramente impressionante, mas a IMO também dá ao computador vantagens que humanos não têm. Ninguém vai montar uma base de Gröbner de cabeça, mas polyrith exige só digitar oito caracteres. Também vi o AlphaProof usando nlinarith
- Impressionante. Eu estava prestes a comentar que seria incrível se simplesmente conectassem isso ao Lean. Acho que a matemática avançada deve seguir por esse caminho daqui para frente, porque as provas importantes ficaram tão complexas que quase ninguém entende todas as partes por completo
  1. https://lean-lang.org/
- Vão mirar a hipótese de Riemann com isso, hehe
Há um bom resumo curto em que Tim Gowers explica e contextualiza as principais ressalvas. Ele é medalhista Fields e também participou deste trabalho: https://x.com/wtgowers/status/1816509803407040909
É verdade, mas entrar na seleção nacional de cada país já é, por si só, um processo muito árduo. Olimpíadas regionais de matemática, olimpíadas nacionais de matemática etc.; em cada etapa há uma filtragem brutal
Depois disso, vem treinamento adicional para esse grupo de elite e, em alguns casos, pode haver também uma seleção adicional
Em resumo, ser escolhido para a equipe da IMO de um país já é um grande feito, e ganhar ouro ou prata dentro dela é simplesmente uma conquista enorme
- Alguns países tiram esses jovens da escola o ano inteiro para se concentrarem no treinamento para a IMO e até garantem a entrada nas melhores universidades do país
  Fonte: um amigo que ganhou medalha de prata na IMO
Tenho muita inveja de quem é pago para fazer esse trabalho. Parece extremamente divertido, e deve ser muito satisfatório empurrar a fronteira do estado da arte desse jeito
- Pode não ser bem assim. Já vi trabalhos que deveriam ser muito satisfatórios se tornarem terrivelmente chatos ou até nocivos, e, por outro lado, trabalhos aparentemente comuns serem realmente interessantes
  Acho que, para satisfação no trabalho, o ambiente de trabalho importa mais do que o tema. Mesmo lidando com um tema que muda o mundo, se a equipe for uma bagunça, você vai passar por maus bocados. Algumas pessoas têm o dom de sugar toda a diversão, e política interna existe em todo lugar, especialmente em temas que mudam o mundo
  Por outro lado, mesmo o assunto mais aparentemente tedioso, como colocar dados de clientes em um banco de dados, pode render momentos ótimos se você tiver uma equipe gentil, uma arquitetura bem projetada e tempo para experimentar e compartilhar conhecimento. Passei a valorizar cada vez mais a beleza de coisas simples que simplesmente funcionam bem. Isso pode ser ainda mais raro do que uma descoberta científica
  Claro, um ótimo ambiente de trabalho e um ótimo tema podem vir juntos, e isso é quase ganhar na loteria, algo de dar inveja
- Trabalho nessa área, especificamente com pré-treinamento de LLMs. Não é tão glamouroso quanto parece de fora. Envolve lidar com YAML gigantesco e usar regex em grande escala. Claro que isso é uma simplificação
  Eu deveria ficar empolgado e grato por poder fazer esse tipo de trabalho, mas ferramentas toscas tiram boa parte do prazer dele
- Talvez a palavra certa seja envious, não jealous
- O melhor que podemos fazer é continuar acompanhando as novidades e apoiando
- Agora não é a hora de reconfigurar aquele YML de 3.292.329 linhas para K8s?
  (/s)
Já faz décadas que máquinas jogam xadrez melhor que humanos
Mesmo assim, ninguém liga. Todo mundo está ocupado assistindo ao Magnus Carlsen
Como somos humanos, nos interessamos pelo que outros humanos fazem. Só nos interessamos por máquinas na medida em que elas nos são úteis
Esse princípio se estende amplamente ao trabalho e à arte. Enquanto existirem humanos, sempre haverá um lugar para humanos nessas áreas
- Por mais que a IA fique melhor em xadrez e arte, humanos continuarão se divertindo com isso. Da mesma forma, provavelmente ainda haverá pessoas estudando matemática como hobby
  Mas tenho muitas dúvidas de que, num futuro próximo, ainda haverá matemáticos publicando novos avanços em matemática que não tenham sido descobertos em sua maior parte, ou totalmente, por IA. Um humano talvez receba crédito por uma prova por ter feito a pergunta inicial, mas quase não há mundo em que se insistiria em que humanos resolvessem problemas matemáticos de forma mais lenta e cara quando computadores conseguem resolver problemas matemáticos significativos com facilidade
- Certo, mas, por exemplo, se uma IA provar a conjectura de Goldbach, isso seria enorme
- Para o consumidor, não faz diferença se uma fábrica de processamento de carne ou um centro logístico da Amazon emprega 5.000 pessoas ou 5
  Esse princípio certamente se aplica à arte, mas ao trabalho se aplica só a algumas partes, ou talvez à maior parte
- Há quem acredite que a matemática, ao contrário do xadrez ou da arte, seja de fato útil. A maioria dos matemáticos não pensaria assim, mas, aceitando por um momento essa ideia maluca, uma prova é apenas uma ferramenta que diz “este pedaço de matemática foi aplicado corretamente”
  Então não é preciso entender a prova, e ninguém se importa se algum matemático em algum lugar entende completamente essa prova. Tudo bem que máquinas sejam melhores que nós em encontrar e verificar provas; na verdade, isso passa a ser esperado
- Acho que esse princípio não se estende bem a provas matemáticas. Verificar uma prova é muito, muito mais fácil do que produzi-la, e uma segunda prova vira apenas uma nota de rodapé
  Muitos matemáticos não vão querer se dedicar a esse tipo de coisa. Ainda assim, há uma grande distância entre a IMO e a fronteira da matemática de pesquisa
Prova de teoremas é um jogo de um jogador com um espaço de busca absurdamente grande, então sempre achei que seria resolvida muito antes da AGI
Pessoalmente, acho que os maiores contribuidores do AlphaProof são as pessoas por trás do Lean e do Mathlib, porque assumiram a tarefa assustadora de formalizar toda a matemática
A falta de formalização nos artigos de matemática sempre matou as tentativas de automação, porque os pesquisadores de IA tinham que lidar com elementos humanos como notação própria dos autores, conhecimento implícito e etapas de prova omitidas
- A frase “prova de teoremas é um jogo de um jogador com um espaço de busca enorme, então será resolvida muito antes da AGI” soa estranha
  Acho que o próprio termo AGI não é definido, mas não entendo por que se esperaria que criar “algo geralmente inteligente”, isto é, uma inteligência no nível mediano humano, fosse muito mais difícil do que “ser melhor em matemática que Terrence Tao”
- Eles não formalizaram toda a matemática. Felizmente, a IMO não precisa de toda a matemática. Mas eles nem formalizaram o suficiente para a IMO. Talvez seja por isso que não conseguiram resolver o problema de combinatória
A melhor discussão está aqui: https://leanprover.zulipchat.com/#narrow/stream/219941-Machi...