AlphaGeometry, o sistema de IA de geometria em nível de Olimpíada

 (deepmind.google)
1 pontos por GN⁺ 2024-01-18 | 1 comentários | Compartilhar no WhatsApp
  • Enquanto a Olimpíada Internacional de Matemática se tornou um campo de prova para o raciocínio matemático de IA, o AlphaGeometry resolveu 25 de 30 problemas de geometria dentro do tempo limite, chegando perto da média de 25,9 dos medalhistas de ouro humanos
  • O ponto central é a combinação de um modelo de linguagem neural com um motor de raciocínio simbólico baseado em regras, tratando em um mesmo loop tanto sugestões intuitivas de construções quanto a verificação por lógica formal
  • 100 milhões de exemplos sintéticos únicos criados sem demonstrações humanas reduziram o gargalo de treinamento, e 9 milhões deles incluem construções auxiliares necessárias para as provas
  • Todas as soluções de Olimpíada foram verificadas por computador, e Evan Chen avaliou que a saída é verificável por máquina, mas também legível por humanos e segue regras clássicas de geometria usadas por estudantes
  • Como em uma edição da IMO normalmente apenas 2 das 6 questões são de geometria, o escopo de aplicação é limitado, mas ainda assim ele se tornou o primeiro modelo de IA capaz de superar, só com desempenho em geometria, o patamar de medalha de bronze da IMO de 2000 e 2015

Desempenho no benchmark de geometria da IMO

  • O AlphaGeometry, apresentado na Nature, resolve problemas complexos de geometria em um nível próximo ao de medalhistas de ouro humanos da Olimpíada
  • O benchmark é composto por 30 problemas de geometria IMO-AG-30 selecionados das Olimpíadas de 2000 a 2022
    • AlphaGeometry: 25 resolvidos dentro do tempo limite
    • Wu’s method, a melhor abordagem anterior: 10 resolvidos
    • Média dos medalhistas de ouro humanos: 25,9 resolvidos
  • O Google DeepMind publicou em código aberto o código e os modelos do AlphaGeometry

Arquitetura do sistema neuro-simbólico

  • O AlphaGeometry é um sistema neuro-simbólico, no qual um modelo de linguagem neural e um motor de raciocínio simbólico trabalham juntos para encontrar provas de teoremas geométricos complexos
  • O modelo de linguagem identifica rapidamente padrões e relações gerais nos dados para prever construções com potencial de utilidade
    • No entanto, pode ter limitações em raciocínio rigoroso ou na capacidade de explicar suas decisões
  • O motor de raciocínio simbólico chega a conclusões seguindo lógica formal e regras claras
    • É explicável e racional, mas pode ser lento e menos flexível ao lidar sozinho com problemas grandes
  • Quando os dois componentes são usados juntos, o modelo de linguagem propõe elementos auxiliares de construção como novos pontos, retas e círculos, e o motor de raciocínio extrai conclusões adicionais sobre a figura a partir disso

Loop de resolução para encontrar construções auxiliares

  • Problemas de geometria de Olimpíada nem sempre podem ser resolvidos diretamente com a figura dada, e às vezes exigem a adição de novos elementos geométricos necessários para a solução
  • O processo de resolução do AlphaGeometry funciona com raciocínio simbólico e sugestões do modelo de linguagem se alternando
    • A partir da figura dada e das premissas do teorema, o motor de raciocínio simbólico deriva novas proposições
    • Se não encontrar a resposta ou não puder mais gerar novas proposições, o modelo de linguagem adiciona um elemento auxiliar de construção com potencial de utilidade
    • O elemento adicionado abre novos caminhos para o motor de raciocínio, e esse processo se repete até encontrar a solução
  • Na questão 3 da Olimpíada Internacional de Matemática de 2015, a solução do AlphaGeometry é composta por 109 etapas lógicas

Geração de 100 milhões de dados sintéticos

  • A geometria se baseia na compreensão de espaço, distância, forma e posição relativa, e é fundamento para várias áreas como arte, arquitetura e engenharia
  • O método de geração de dados sintéticos do AlphaGeometry imita em larga escala o processo pelo qual humanos observam figuras e descobrem novas propriedades e relações geométricas com base em conhecimento prévio
  • O sistema gera 1 bilhão de figuras aleatórias com computação altamente paralelizada
    • Em cada figura, deriva de forma exaustiva todas as relações entre pontos e retas
    • Encontra todas as provas contidas em cada figura
    • Rastreia de volta quais elementos adicionais de construção seriam necessários para chegar a essas provas
  • Esse processo é chamado de dedução simbólica e rastreamento reverso (symbolic deduction and traceback)
  • O enorme conjunto de dados é filtrado para remover exemplos semelhantes, resultando ao final em 100 milhões de exemplos únicos de treinamento com diferentes níveis de dificuldade
    • Destes, 9 milhões são casos com elementos auxiliares de construção adicionados
    • Como o modelo de linguagem aprende muitos exemplos em que a construção auxiliar leva à prova, ele pode propor novas construções também em problemas de Olimpíada

Verificabilidade e limites de aplicação

  • Todas as soluções fornecidas pelo AlphaGeometry para problemas de Olimpíada foram confirmadas e verificadas por computador
  • Os resultados foram comparados com métodos anteriores de IA e com o desempenho humano em Olimpíadas
  • Evan Chen, treinador de matemática e ex-medalhista de ouro de Olimpíada, avaliou algumas soluções
    • A saída do AlphaGeometry é verificável e limpa
    • Em problemas de competição baseados em provas, respostas de IA no passado às vezes estavam certas e às vezes erradas, o que podia exigir verificação humana
    • As soluções do AlphaGeometry têm uma estrutura verificável por máquina e, ao mesmo tempo, legível por humanos
    • Em vez de forçar enormes cálculos algébricos via coordenadas, ele usa regras clássicas de geometria como ângulos e triângulos semelhantes, da mesma forma que estudantes
  • Uma edição da IMO é composta por 6 problemas, e normalmente apenas 2 deles focam em geometria
    • Portanto, o AlphaGeometry se aplica a apenas cerca de um terço das questões de uma edição
    • Mesmo assim, ele se tornou o primeiro modelo de IA capaz de atingir, apenas com habilidade em geometria, o patamar de medalha de bronze da IMO de 2000 e 2015

Expansão para IA de raciocínio matemático

  • O AlphaGeometry mostra que a capacidade da IA de raciocinar logicamente e descobrir e verificar novo conhecimento está crescendo
  • Resolver problemas de geometria em nível de Olimpíada é um marco importante rumo a um raciocínio matemático mais profundo e a sistemas de IA geral mais avançados
  • A abordagem de treinar IA do zero com grandes volumes de dados sintéticos pode influenciar a forma como novo conhecimento é descoberto na ciência e na IA para além da matemática
  • O AlphaGeometry se apoia na linha de trabalho de IA para raciocínio matemático do Google DeepMind e do Google Research
  • O objetivo de longo prazo é generalizar para várias áreas da matemática, desenvolver a resolução sofisticada de problemas e o raciocínio necessários para sistemas de IA geral e criar sistemas de IA que expandam as fronteiras do conhecimento humano

Leituras relacionadas

1 comentários

 
GN⁺ 2024-01-18
Opiniões no Hacker News

  • Como alguém que já foi autor de problemas em competições como a IMO, li este artigo com muito interesse. Ao mesmo tempo, acho que o primeiro tema a cair diante da IA — isto é, de índices inteligentes de conhecimento e de métodos de raciocínio — só podia ser geometria
    Entre os temas da Olimpíada de Matemática, os problemas de geometria em geral são os mais “mecânicos”. Se for possível expressar um problema em coordenadas, por exemplo coordenadas XY ou no plano complexo, surge um conjunto finito de etapas que um computador pode usar para encontrar a solução. É claro que, no ambiente da IMO, o limite de tempo e os erros humanos impedem que isso seja prático. Antigamente, eu costumava usar o WolframAlpha para verificar provas de problemas de geometria e conjecturas que eu criava dessa forma
    Álgebra, especialmente desigualdades, é parecida: muitas vezes, forçar uma computação poderosa leva à resposta
    As áreas em que eu gostaria de ver sistemas inteligentes realmente avançarem são teoria dos números e combinatória. O espaço de busca é muito mais complexo, e muitas vezes é preciso provar que algo é impossível. Esses problemas são difíceis de resolver por computação de força bruta

    • Falando como alguém que resolve esses problemas, antes de tudo, obrigado. Mesmo décadas depois de terminar o ensino médio, ainda os resolvo de vez em quando por diversão
      Concordo que geometria seria a primeira. Pelo que vi aqui, não é “força bruta” no sentido de depender de geometria algébrica, vetores ou soluções com números complexos, mas chega perto de uma busca exaustiva no sentido de vasculhar construções auxiliares “interessantes”
      Geometria sempre foi minha pior matéria, mas eu sentia que, quando a construção correta era dada, o problema ficava muito mais fácil. Só que nunca adquiri a intuição para pensar rapidamente nessas construções. Esta IA também não parece ter essa intuição, mas consegue despejá-las muito mais rapidamente. No fim, as candidatas que se pode construir — como retas perpendiculares, paralelas e bissetrizes — são limitadas, e dá para avaliá-las de modo bastante mecânico, abrindo todos os ângulos e proporções ou tentando usar a potência de um ponto
      É muito impressionante, mas, no sentido de “motor versus IA”, parece algo como DeepMind:Kasparov::AlphaGeo:Terry Tao
      Concordo que álgebra provavelmente vem em seguida. Como na geometria, em geral basta encontrar uma, duas ou três substituições inteligentes, e as opções são limitadas
      Alguns problemas de combinatória também podem se encaixar nessa estratégia de busca. Por exemplo, problemas que contam o mesmo objeto de duas maneiras. Mas essa é uma ponte mais distante e só cobriria parte do conjunto total de problemas
      Acho que teoria dos números será a última fronteira antes de chegar aos 42 pontos perfeitos
    • Gosto dessa atitude positiva em relação a esse avanço. Fico curioso se você sente alguma perda diante da possibilidade de que a capacidade de ser muito bom em matemática em breve possa ser alcançada por máquinas. Ou você acha que isso não deve acontecer tão cedo?
    • Fiquei curioso sobre como se entra nessa posição de autor de problemas. Existe algum tipo de processo de candidatura?
      Depois de verificar se os problemas são solucionáveis, também queria saber como escolhem quais problemas específicos entram no conjunto final. É por votação ou por algum outro método de avaliação?
    • No começo, achei que desigualdades de três variáveis cairiam primeiro. Porque há menos ambiguidade sobre o que conta como prova. Mas eu não sabia que o problema de trás já tinha sido resolvido em 2000 (http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf)
      Alguém deveria transformar geometria sintética em um jogo de aventura. Poderia usar uma linguagem de escrita de provas mais simples que Lean, e também poderia ficar visualmente bonito

  • Se eu li o artigo corretamente, isso parece um trabalho de verdade. É muito mais legítimo do que aquele artigo de matemática com IA que a DeepMind divulgou erroneamente no mês passado como se tivesse resolvido um problema aberto de pesquisa matemática. Ainda assim, chama bastante atenção o quanto essa estrutura é diferente do que normalmente se imagina como raciocínio/inteligência automatizados
    Entendi que eles treinam um Transformer com milhões de teoremas de geometria elementar e o usam para fazer busca por força bruta de provas. Por causa do contexto de geometria elementar, a estrutura é necessariamente elementar, e é fácil determinar simbolicamente se algo é verdadeiro ou falso. Se a busca por força bruta falha, pelo que entendi, eles adicionam aleatoriamente construções geométricas auxiliares, como acrescentar um ponto médio, e verificam se a busca passa a funcionar com esse material adicional
    Edit: como corrigiu Imnimo, eu tinha entendido ao contrário. A busca por força bruta é uma busca puramente por força bruta, e o Transformer é usado para prever quais construções auxiliares adicionar
    Além disso, embora isso não esteja no post do blog, os enunciados reais dos problemas também tiveram de ser modificados/adaptados. Por exemplo, um enunciado original como “sejam AH1, BH2, CH3 as alturas do triângulo ABC...” foi transformado em uma lista de definições muito mais explícita, como “seja ABC um triângulo. A IA define o ponto I de modo que seja a bissetriz do ângulo BAC e CI seja a bissetriz do ângulo ACB...”, e no final vira algo como “prove que T1I=IZ”

    • Acho que essa explicação não está muito correta. A busca por força bruta é realizada pelo solucionador simbólico, não pelo Transformer. Quando não surgem novas inferências, o Transformer é chamado para sugerir possíveis construções auxiliares; elas não são adicionadas aleatoriamente
    • Não entendo por que você vê isso como distante da ideia comum de raciocínio/inteligência automatizados. Raciocínio é, fundamentalmente, um problema de busca
      O processo descrito é exatamente igual ao que humanos fazem. Você chuta algo que parece útil e resolve os detalhes mecanicamente. Se empacar, faz outro palpite. No fim, é parecido com explorar uma árvore
      As pessoas já tinham entendido esse processo em 1955 e até criado um protótipo funcional capaz de provar teoremas: https://en.wikipedia.org/wiki/Logic_Theorist O ponto central está em usar boas heurísticas. Redes neurais conseguem extrair heurísticas dos dados, então fazem sentido aqui
      Fico curioso sobre o que você considera a ideia comum de “raciocínio automatizado”. Um dispositivo mágico que resolve qualquer problema em uma única passada linear?
    • O método de “se a busca por força bruta falha, adicionar construções geométricas auxiliares, como um ponto médio, e ver se a busca funciona com esse material adicional” era exatamente igual à geometria que aprendi na escola, e eu realmente odiava aquilo
      Só depois de entrar no curso de matemática na universidade aprendi a fazer direito e passei a gostar
    • Usar um LLM para o papel de traçar linhas auxiliares é ineficiente demais. É difícil imaginar colocar inúmeras máquinas para resolver um problema simples da IMO
      Essa área ainda está em estágio inicial, e parece haver muito trabalho inacabado. A parte de busca deveria ser substituída por uma rede neural pequena, e a parte de raciocínio não é difícil nem parece precisar de grandes melhorias
      Agora é hora de aumentar o desempenho com auto-jogo. Em problemas de geometria plana, pode-se ver a conclusão a ser provada como um ponto da figura, as condições como outro ponto, e fazer dois jogadores se moverem o máximo possível um em direção ao outro, compartilhando dados. Nesse processo, a contribuição de cada jogador poderia ser usada para melhorar o desempenho por analogia ao cálculo de vitória/derrota no Go

  • Este modelo específico não parece generalizável, mas a abordagem neuro-simbólica parece muito promissora
    É uma forma de conectar ferramentas de “Sistema 1” cada vez mais poderosas, que são a maior parte do aprendizado de máquina atual, a ferramentas estruturadas de “Sistema 2”, como a geração de provas lógicas. O Sistema 2 pode elaborar planos e verificar a veracidade ou o valor da saída
    O Sistema 2 avança até ficar travado; quando trava, o Sistema 1 oferece um palpite intuitivo sobre qual parte do espaço de estados verificar em seguida
    Aqui, eles aproveitaram o fato de que provas podem ser geradas por computador para criar um conjunto de dados com 100 milhões de provas, possibilitando aprendizado autossupervisionado escalável. Domínios simbólicos parecem ter uma forma que permite bem esse tipo de geração de dados. Embora o valor de cada instância individual seja baixo, em conjunto elas podem permitir um pré-treinamento útil
    Combinando esses elementos, essa é uma abordagem que pode ir bastante longe
    O marco essencial é deixar de depender de um domínio formal/simbólico específico e criar um sistema de pré-treinamento capaz de generalizar as habilidades aprendidas nesse domínio

    • Não é preciso resolver tudo de uma vez. Essa abordagem tem potencial para transformar tanto matemática quanto programação, porque pode levar a verificação formal de uma ferramenta de nicho, usada apenas parcialmente, para uma parte do kit geral de ferramentas de todos os profissionais
      Além disso, dentro dos domínios aplicáveis, ela resolve completamente um dos problemas fundamentais que a onda atual de IA chama de “alucinação”. Só que essa solução é possível porque existe um sistema não-IA que prova a correção
      Em linhas gerais, essa abordagem não é tão nova. Em bioquímica, já se usa IA para encontrar moléculas candidatas e experimentos físicos para validá-las
      IAs de jogos combinatórios também vêm usando IA há bastante tempo como entrada para a busca Monte Carlo à moda antiga
    • Isto parece ser a possibilidade mais próxima de chegar a alguma forma de inteligência artificial geral

  • Agradeço por terem publicado o código e os pesos junto com o artigo. Até onde me lembro, esta é a primeira vez que um artigo famoso da DeepMind publica código de inferência executável e checkpoints. Se houver exemplos anteriores, aceito correções
    Ainda não vejo um conjunto de treinamento público nem código de treinamento de exemplo, mas mesmo assim é um bom avanço por oferecer algo sobre o qual outros pesquisadores podem construir. No fim das contas, esse também é o objetivo de um artigo acadêmico

    • É uma pena que o dataset também esteja ausente. Eles dizem ter criado 100 milhões de exemplos sintéticos; esses exemplos foram gerados com o AlphaGeometry? Onde estão o código de filtragem e as entradas iniciais para criar esses dados sintéticos?
      Se eu não estiver enganado, eles usam um modelo t5? Pelo menos parecem usar o vocabulário SentencePiece do t5
      Também fico curioso para saber quanto tempo de GPU foi usado para treinar esse modelo e quais parâmetros de treinamento foram utilizados
      Não me entendam mal. Este sistema é fascinante e mostra como a engenharia aplicada deveria ser. Só gostaria de saber mais detalhes de treinamento, os dados iniciais e o método de geração dos dados sintéticos

  • Fico muito curioso para saber com que frequência o modelo de linguagem gera construções auxiliares úteis. Certamente deve ser melhor do que aleatório, mas não sei se ele lança milhares de construções até encontrar uma boa, ou se faz sugestões úteis em uma proporção parecida com a de um especialista humano
    O artigo diz: “Como o processo de decodificação do modelo de linguagem retorna k sequências diferentes que descrevem k construções auxiliares alternativas, usamos a pontuação de cada beam como função de valor para fazer busca em feixe sobre essas k opções. Essa configuração é muito fácil de paralelizar entre beams, o que acelera bastante quando há recursos de computação paralela. Nos experimentos, usamos tamanho de beam k=512, número máximo de iterações 16 e fator de ramificação em cada nó, isto é, tamanho do lote de decodificação 32”
    Mas não entendo completamente como 512 e 16 se traduzem no número total de construções propostas. Também dizem que, mesmo removendo o tamanho de beam e o máximo de iterações, o desempenho cai só até certo ponto. Isso quer dizer que o modelo, de fato, ranqueia bem no topo construções úteis, e que milhares só são necessários nos problemas mais difíceis?

    • Meu palpite pessoal é que esta parte esbarra com força nos limites da analogia entre linguagem e humano-máquina
      Ainda assim, tentando resumir, o número é 262.144, mas não se deve levar isso ao pé da letra
      A saída da função de decodificação são tokens, que são mais ou menos 3/4 de uma palavra, mas vamos tratar como 1 palavra
      O número de tokens considerados por token de saída é beam_size * branching_factor * max_iterations = 512 * 32 * 16 = 262.144
      Basta contar o número de palavras da solução de exemplo: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
      O número total de tokens da solução é 2289, e o total de tokens considerados é 262.144 * 2289 = 600.047.616
      Numa conta forçada, se definirmos “número de soluções consideradas” como total de tokens considerados / total de tokens da solução, dá 262.144. É o mesmo valor do número de tokens vistos em cada etapa de iteração, então faz algum sentido

  • É interessante que o Transformer usado seja pequeno. Segundo o artigo, ele foi treinado com a configuração padrão da biblioteca Meliad, com 12 camadas, dimensão de embedding 1.024, 8 cabeças de atenção e camadas densas entre atenções de dimensão 4.096 usando ativação ReLU
    Excluindo as camadas de embedding da entrada e da cabeça de saída, o Transformer inteiro tem 151 milhões de parâmetros. O tokenizador personalizado foi treinado no modo ‘word’ do SentencePiece, com tamanho de vocabulário 757. O comprimento máximo de contexto foi limitado a 1.024 tokens, e foram usados embeddings de posição relativa no estilo T5. Como mais de 90% das sequências têm menos de 200 tokens, também foi usado empacotamento de sequências

    • Não é fácil chamar isso de pequeno. Fora do campo dos LLMs, é um tamanho bem comum. Por exemplo, equivale a modelos de linguagem, modelos de tradução ou modelos acústicos de tamanho normal. Algumas pessoas até chamariam isso de grande
    • Esse resultado sugere que, se conseguirmos formalizar corretamente, talvez ainda existam mais frutas baixas fáceis para Transformers colherem nas ciências duras. Parece que, neste caso, não era uma questão de escala

  • O que foi realmente novo para mim foi saber que o melhor sistema anterior já conseguia resolver 10 desses problemas. Eu tinha ouvido falar que existiam algoritmos de decisão para problemas de geometria plana, mas não sabia que eram algoritmos práticos. Procurando, encontrei como referência http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf

    • Sim. E a parte não neural do AlphaGeometry, isto é, os componentes de processamento simbólico e álgebra linear, sozinha já consegue superar o melhor desempenho anterior. Uma quantidade considerável de trabalho também entrou nos componentes que não são a rede neural
    • É interessante, mas acho que, se você simplesmente for até o fim com cálculos de coordenadas baricêntricas usando as fórmulas do livro de Evan Chen, conseguiria resolver cerca de 30% da IMO até em um laptop moderno. Considerando que a maioria são problemas sobre triângulos, parece plausível

  • Eu estava pronto para desconfiar desse tipo de resultado, que em geral vem com algo como “não parece uma prova humana”, mas mudei de ideia ao ver Evan Chen dizer que as provas são de fato limpas e legíveis por humanos
    Evan Chen é uma figura conhecida na comunidade de matemática de olimpíadas e também autor de um livro famoso sobre geometria de olimpíadas[1], então desta vez é preciso admitir que a máquina realmente conquistou parte dos problemas da IMO
    [1]: https://web.evanchen.cc/geombook.html

    • Porém, na prova completa do material suplementar[1], achei que havia um erro na prova da IMO P3, Fig1.f e Step 26. Ela diz ∠GMD = ∠GO2D, mas isso está errado; acho que deveria ser ∠GMD + ∠GO2D = π. Tentei acompanhar a lógica, mas não consegui interpretar o Step 25. Fiquei pensando se essa etapa era uma alucinação
      Ainda assim, a ideia de que O2 está sobre o círculo dos nove pontos está correta
      Edit: retiro o que disse. Parece que estão usando ângulos orientados[2], e nesse caso a afirmação está correta
      [1]: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
      [2]: https://web.evanchen.cc/handouts/Directed-Angles/Directed-An...

  • Relacionado a isso, https://www.nytimes.com/2024/01/17/science/ai-computers-math... também vale a leitura
    Veio por meio de https://news.ycombinator.com/item?id=39030186, e essa thread deve ser mesclada aqui

  • Relacionado: https://aimoprize.com/
    É um prêmio de US$ 10 milhões para modelos que tenham bom desempenho na IMO