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

AlphaProof e AlphaGeometry 2, do Google DeepMind, conseguiram resolver problemas da Olimpíada Internacional de Matemática
- AlphaProof: sistema de raciocínio matemático baseado em aprendizado por reforço
- AlphaGeometry 2: sistema aprimorado de resolução de problemas de geometria
- Os dois sistemas resolveram 4 das 6 questões da Olimpíada Internacional de Matemática (IMO) deste ano, alcançando um desempenho de nível medalha de prata

Conquistas da IA na resolução de problemas matemáticos complexos

Introdução à IMO
- A mais antiga e prestigiada competição de matemática para jovens, realizada anualmente desde 1959
- Os problemas da competição abrangem álgebra, combinatória, geometria e teoria dos números
- Muitos vencedores da Medalha Fields passaram pela IMO
O desafio da IMO para os sistemas de IA
- AlphaProof e AlphaGeometry 2 resolveram os problemas da IMO deste ano
- As questões foram avaliadas de acordo com as regras oficiais da competição
- O AlphaProof resolveu 2 problemas de álgebra e 1 de teoria dos números
- O AlphaGeometry 2 resolveu 1 problema de geometria
- Os 2 problemas de combinatória não foram resolvidos
- No total, obtiveram 28 de 42 pontos, alcançando um desempenho de nível medalha de prata

AlphaProof: abordagem de raciocínio formal

Como o AlphaProof funciona
- Prova proposições matemáticas na linguagem formal Lean
- Combina um modelo de linguagem pré-treinado com o algoritmo de aprendizado por reforço AlphaZero
- Traduz problemas em linguagem natural para proposições formais, resolvendo questões de diferentes níveis de dificuldade
- Ao receber um problema, o AlphaProof gera candidatos de solução e os prova ou refuta
- Os resultados comprovados reforçam o modelo de linguagem do AlphaProof, melhorando sua capacidade de resolver problemas mais difíceis
Processo de treinamento
- Foi treinado provando ou refutando milhões de problemas
- Mesmo durante o período da competição, aplicou o loop de treinamento para provar variações dos problemas

AlphaGeometry 2 ainda mais competitivo

Melhorias do AlphaGeometry 2
- Modelo de linguagem baseado em Gemini e sistema híbrido neuro-simbólico
- Treinado com 10 vezes mais dados sintéticos do que a versão anterior
- Melhoria na velocidade e na precisão para resolver problemas de geometria
- Usa um mecanismo de compartilhamento de conhecimento ao resolver novos problemas
Resultados na IMO 2024
- Resolveu 83% dos problemas de geometria da IMO dos últimos 25 anos
- Na competição deste ano, resolveu a questão 4 em 19 segundos

Uma nova fronteira para o raciocínio matemático

Experimentos com sistemas de raciocínio em linguagem natural
- Experimentos com um sistema de raciocínio em linguagem natural baseado em Gemini
- Pode resolver problemas sem traduzi-los para uma linguagem formal
- Explora a possibilidade de combinação com outros sistemas de IA
Perspectivas futuras
- Matemáticos poderão colaborar com ferramentas de IA para explorar novas hipóteses, testar abordagens de resolução de problemas e encurtar processos de prova
- Sistemas de IA como o Gemini podem ampliar capacidades em matemática e raciocínio geral

Resumo do GN⁺

AlphaProof e AlphaGeometry 2 mostram o potencial da IA no raciocínio matemático
Ao alcançar desempenho de nível medalha de prata na Olimpíada Internacional de Matemática, comprovam a capacidade da IA de resolver problemas matemáticos
Abrem caminho para que matemáticos explorem novas abordagens de resolução de problemas em colaboração com a IA
Um projeto com funcionalidade semelhante é o uso de modelos de processamento de linguagem natural como o GPT-3, da OpenAI

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

Comentários do Hacker News

Primeiro comentário
- Estou muito empolgado com este projeto, mas não está claro o quanto o computador contribuiu no processo de traduzir problemas de matemática para uma linguagem formal
- Na solução disponível para download, não fica claro o que foi decidido por humanos no processo de tradução e o que foi encontrado pelo computador
Segundo comentário
- Na IMO, medalhas são concedidas a 50% dos participantes, e a proporção entre ouro, prata e bronze é de 1:2:3
- É impressionante que a IA tenha resolvido melhor do que 75% dos estudantes
- No entanto, como o tempo que a IA levou para resolver os problemas é diferente do tempo dado aos estudantes na prova, a comparação direta é inadequada
Terceiro comentário
- O AlphaGeometry resolveu problemas limitados, mas este método deve ter um impacto mais amplo na matemática
- Eles estão implementando um pipeline que converte matemática em linguagem natural para matemática formalizada, e isso também pode aprender a construir teoria básica
- Esse é o santo graal dos assistentes de prova e ajudará os humanos a formalizar matemática de maneira mais natural
Quarto comentário
- Se o sistema levou 3 dias para resolver os problemas, isso não é diferente de simples força bruta
- Isso não é raciocínio de verdade
Quinto comentário
- Está usando Lean
- Isso é importante não apenas para problemas matemáticos, mas também para evitar resultados sem sentido de forma geral
- Espero que mais pessoas passem a escrever tipos em sistemas como o Lean
Sexto comentário
- Tenho inveja das pessoas que participam deste projeto
- Deve ser muito divertido e gratificante avançar o estado da arte
Sétimo comentário
- As melhores discussões acontecem no chat Zulip do LeanProver
Oitavo comentário
- Tim Gowers, medalhista Fields, oferece uma boa visão geral explicando os principais cuidados e fornecendo contexto
Nono comentário
- Prova de teoremas é um jogo solo com um espaço de busca extremamente grande
- Os maiores contribuintes do AlphaProof são os desenvolvedores do Lean e do Mathlib
- A falta de formalização em artigos matemáticos dificultou tentativas de automação
Décimo comentário
- As máquinas superam os humanos no xadrez há décadas
- Ainda assim, as pessoas continuam assistindo a Magnus Carlsen
- Humanos se interessam pelo que outros humanos fazem
- Máquinas só despertam interesse na medida em que são úteis para os humanos