Alfagometria: um sistema de IA de nível olímpico para geometria

Nosso sistema de IA supera a abordagem de última geração para problemas de geometria, avançando no raciocínio da IA ​​em matemática

Refletindo o espírito olímpico da Grécia antiga, a Olimpíada Matemática Internacional é uma arena moderna para os matemáticos mais brilhantes do ensino médio do mundo. A competição não apenas mostra os jovens talentos, mas também emergiu como um campo de testes para sistemas avançados de IA em matemática e raciocínio.

Em um artigo publicado hoje em NaturezaIntroduzimos a alfageometria, um sistema de IA que resolve problemas complexos de geometria em um nível que se aproxima de um medalista da Olimpíada Humana – um avanço no desempenho da IA. Em um teste de benchmarking de 30 problemas de geometria da Olimpíada, a alfagometria resolveu 25 dentro do tempo padrão da Olimpíada. Para comparação, o sistema anterior de última geração resolveu 10 desses problemas de geometria e o medalhista médio de ouro humano resolveu 25,9 problemas.

Os sistemas de IA geralmente lutam com problemas complexos em geometria e matemática devido à falta de habilidades de raciocínio e dados de treinamento. O sistema da Alpageometria combina o poder preditivo de um modelo de linguagem neural com um mecanismo de dedução ligado a regras, que trabalha em conjunto para encontrar soluções. E, desenvolvendo um método para gerar um vasto pool de dados de treinamento sintético – 100 milhões de exemplos únicos – podemos treinar alfagometria sem demonstrações humanas, contornando o gargalo de dados.

Com a alfageometria, demonstramos a crescente capacidade de IA de raciocinar logicamente e descobrir e verificar novos conhecimentos. A solução de problemas de geometria no nível da Olimpíada é um marco importante no desenvolvimento de um profundo raciocínio matemático no caminho para sistemas de IA mais avançados e gerais. Estamos de origem aberta do Código de alfagometria e modeloe espero que, juntamente com outras ferramentas e abordagens na geração e treinamento de dados sintéticos, isso ajude a abrir novas possibilidades em matemática, ciência e IA.

A alfagometria adota uma abordagem neuro-simbólica

A alfagometria é um sistema neuro-simbólico composto por um modelo de linguagem neural e um mecanismo de dedução simbólica, que trabalha juntos para encontrar provas para teoremas complexos de geometria. Semelhante à ideia de “Pensando, rápido e lento“, Um sistema fornece idéias rápidas e” intuitivas “e a outra, mais deliberada e racional tomada de decisão.

Como os modelos de idiomas se destacam na identificação de padrões e relacionamentos gerais nos dados, eles podem prever rapidamente construções potencialmente úteis, mas geralmente não têm a capacidade de raciocinar rigorosamente ou explicar suas decisões. Os mecanismos de dedução simbólica, por outro lado, são baseados na lógica formal e usam regras claras para chegar a conclusões. Eles são racionais e explicáveis, mas podem ser “lentos” e inflexíveis – especialmente ao lidar com problemas grandes e complexos por conta própria.

O modelo de linguagem da alfageometria orienta seu mecanismo de dedução simbólica para soluções prováveis ​​para problemas de geometria. Os problemas da geometria da Olympíada são baseados em diagramas que precisam de novas construções geométricas a serem adicionadas antes de serem resolvidas, como pontos, linhas ou círculos. O modelo de linguagem da alfageometria prevê quais novas construções seriam mais úteis para adicionar, de um número infinito de possibilidades. Essas pistas ajudam a preencher as lacunas e permitem que o mecanismo simbólico faça mais deduções sobre o diagrama e feche a solução.

Gerando 100 milhões de exemplos de dados sintéticos

A geometria depende da compreensão do espaço, distância, forma e posições relativas, e é fundamental para a arte, arquitetura, engenharia e muitos outros campos. Os seres humanos podem aprender geometria usando uma caneta e papel, examinando diagramas e usando o conhecimento existente para descobrir novas propriedades e relacionamentos geométricos mais sofisticados. Nossa abordagem de geração de dados sintéticos emula esse processo de construção de conhecimento em escala, permitindo-nos treinar alfagometria do zero, sem nenhuma demonstração humana.

Usando computação altamente paralela, o sistema iniciou gerando um bilhão de diagramas aleatórios de objetos geométricos e derivou exaustivamente todas as relações entre os pontos e as linhas em cada diagrama. A alfagometria encontrou todas as provas contidas em cada diagrama e depois trabalhou para trás para descobrir quais construções adicionais, se houver, eram necessárias para chegar a essas provas. Chamamos esse processo de “dedução simbólica e traceback”.

Esse enorme pool de dados foi filtrado para excluir exemplos semelhantes, resultando em um conjunto de dados de treinamento final de 100 milhões de exemplos únicos de dificuldades variadas, das quais nove milhões apresentavam construções adicionais. Com tantos exemplos de como essas construções levaram a provas, o modelo de linguagem da alfageometria é capaz de fazer boas sugestões para novas construções quando apresentadas com problemas de geometria Olympiad.

Raciocínio matemático pioneiro com IA

A solução para todos os problemas da Olympiad fornecida pela alfageometria foi verificada e verificada pelo computador. Também comparamos seus resultados com os métodos anteriores de IA e com o desempenho humano na Olympiad. Além disso, Evan Chen, treinador de matemática e ex-medalista da Olympiad Gold, avaliou uma seleção das soluções da alfageometria para nós.

Chen disse: “A saída da alfageometria é impressionante porque é verificável e limpa. As soluções anteriores da IA ​​para os problemas de concorrência baseados em prova às vezes foram atingidos ou acertados (as saídas são corretas apenas às vezes e precisam de verificações humanas). A alfagometria não tem essa fraqueza: suas soluções têm estrutura verificável por máquina. No entanto, apesar disso, sua saída ainda é legível por humanos. Pode-se imaginar um programa de computador que resolveu problemas de geometria por sistemas de coordenadas de força bruta: pense em páginas e páginas de cálculo tedioso de álgebra. A alfagometria não é isso. Ele usa regras de geometria clássica com ângulos e triângulos semelhantes, assim como os alunos. ”

Como cada Olympiad apresenta seis problemas, apenas dois dos quais geralmente focados na geometria, a alfagometria só pode ser aplicada a um terço dos problemas em uma determinada Olimpíada. No entanto, sua capacidade de geometria sozinha a torna o primeiro modelo de IA no mundo capaz de aprovar o limiar da medalha de bronze da IMO em 2000 e 2015.

Na geometria, nosso sistema se aproxima do padrão de um medalista de ouro da IMO, mas estamos de olho em um prêmio ainda maior: avançando raciocínio para os sistemas de IA de próxima geração. Dado o potencial mais amplo do treinamento de sistemas de IA do zero com dados sintéticos em larga escala, essa abordagem pode moldar como os sistemas de IA do futuro descobrem novos conhecimentos, em matemática e além.

A alfageometria se baseia no trabalho do Google DeepMind e do Google Research para o raciocínio matemático pioneiro com a IA – de explorar a beleza da matemática pura para Resolvendo problemas matemáticos e científicos com modelos de idiomas. E, mais recentemente, introduzimos o FunSearch, que fez as primeiras descobertas em problemas abertos em ciências matemáticas usando grandes modelos de linguagem.

Nosso objetivo de longo prazo continua a construir sistemas de IA que possam generalizar nos campos matemáticos, desenvolvendo a sofisticada solução de problemas e raciocínio dos quais os sistemas gerais de IA dependerão, o tempo todo, estendendo as fronteiras do conhecimento humano.