notícias

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Novo Relatório de Sabedoria

Editor: Departamento Editorial

[Introdução à Nova Sabedoria] Agora mesmo, o modelo matemático mais recente do Google DeepMind ganhou a medalha de prata da Olimpíada de Matemática da IMO! Não só resolveu 4 das 6 questões com pontuação perfeita, a apenas 1 ponto da medalha de ouro, mas também levou apenas 19 segundos para resolver a 4ª questão. A qualidade e rapidez na resolução do problema surpreenderam os juízes humanos que pontuaram. .

AI ganhou a medalha de prata da Olimpíada de Matemática da IMO!

Agora mesmo, o Google DeepMind anunciou que as verdadeiras questões da Olimpíada Internacional de Matemática deste ano foram produzidas por seu próprio sistema de IA.

Entre eles, a IA não apenas completou com êxito 4 das 6 questões, mas também recebeu nota máxima em cada questão, o que equivale à pontuação mais alta de uma medalha de prata - 28 pontos.

Este resultado está a apenas 1 ponto da medalha de ouro!

Entre 609 competidores, apenas 58 ganharam medalhas de ouro

Na competição oficial, os competidores humanos enviarão suas respostas em duas sessões, com tempo limite de 4,5 horas cada vez.

Curiosamente, a IA levou apenas alguns minutos para responder a uma das perguntas, mas as perguntas restantes levaram três dias inteiros, o que pode ser considerado um sério tempo limite.

O que fez grandes contribuições desta vez foram dois sistemas de IA – AlphaProof e AlphaGeometry 2.

Ponto importante: 2024 IMO não está nos dados de treinamento dessas duas IAs.

Scott Wu, um dos fundadores do engenheiro de IA Devin (três vezes medalhista de ouro do IOI), lamentou: “Quando eu era criança, as Olimpíadas eram tudo que eu tinha. Nunca pensei que, apenas 10 anos depois, elas seriam substituídas pela IA. . resolvido".

Na competição IMO deste ano, há seis questões de competição envolvendo álgebra, combinatória, geometria e teoria dos números. Seis caminhos são quatro, vamos sentir o nível da IA——

A capacidade de raciocínio matemático da IA ​​choca o professor

Todos sabemos que a IA anterior era limitada na resolução de problemas matemáticos devido a limitações nas capacidades de raciocínio e nos dados de treino.

Os dois jogadores de IA que apareceram juntos hoje quebraram essa limitação. eles são, respectivamente -

- AlphaProof, um novo sistema de raciocínio matemático formal baseado em aprendizagem por reforço

- AlphaGeometry 2, o sistema de resolução de problemas geométricos de segunda geração

As respostas dadas pelas duas IAs foram pontuadas de acordo com as regras dos famosos matemáticos Professor Timothy Gowers (medalhista de ouro IMO e medalhista Fields) e Dr. Joseph Myers (duas vezes medalhista de ouro IMO e presidente do Comitê de Seleção de Perguntas IMO 2024) .

No final, AlphaProof resolveu corretamente duas questões algébricas e uma questão de teoria dos números. Uma das questões mais difíceis foi resolvida por apenas 5 competidores humanos no AlphaGeometry 2 deste ano;

Existem apenas dois problemas matemáticos combinatórios que não foram resolvidos.

O professor Timothy Gowers também ficou profundamente chocado durante o processo de classificação——

Que um programa possa apresentar uma solução tão pouco óbvia é realmente impressionante e muito além do que eu esperava, dado o estado da arte atual.

Prova Alfa

AlphaProof é um sistema capaz de provar proposições matemáticas na linguagem formal Lean.

Ele combina um grande modelo de linguagem pré-treinado com o algoritmo de aprendizagem por reforço AlphaZero, que aprendeu sozinho a dominar xadrez, shogi e Go.

Uma vantagem importante das linguagens formais é que elas podem ser verificadas formalmente para provas que envolvem raciocínio matemático. No entanto, a sua aplicação na aprendizagem automática tem sido limitada devido à quantidade muito limitada de dados relevantes escritos por humanos.

Em contraste, as abordagens baseadas em linguagem natural, apesar de terem acesso a grandes quantidades de dados, podem produzir passos e soluções de raciocínio intermediários plausíveis, mas incorretos.

Para superar isso, os pesquisadores do Google DeepMind aperfeiçoaram o modelo Gemini para traduzir automaticamente declarações de problemas em linguagem natural em declarações formais, construindo uma grande biblioteca contendo problemas formais de dificuldade variada, construindo assim uma ponte entre os dois campos complementares.

Ao resolver um problema, o AlphaProof gera soluções candidatas e as prova ou refuta, buscando possíveis etapas de prova no Lean.

Cada prova encontrada e verificada é usada para fortalecer o modelo de linguagem do AlphaProof para que ele possa resolver problemas mais difíceis no futuro.

Para treinar o AlphaProof, os pesquisadores provaram ou refutaram milhões de questões cobrindo uma ampla gama de dificuldades e áreas de tópicos matemáticos desde as semanas que antecederam e durante a competição.

Durante a competição, eles também aplicaram um ciclo de treinamento reforçando as provas em variações autogeradas do problema da competição até que uma solução completa fosse encontrada.

Infográfico do fluxo do ciclo de treinamento de aprendizagem por reforço AlphaProof: aproximadamente um milhão de problemas matemáticos informais são traduzidos pela rede formal em uma linguagem matemática formal e, em seguida, treina-se gradualmente usando o algoritmo AlphaZero, buscando provas ou refutações desses problemas; , para resolver problemas mais desafiadores

AlfaGeometria 2

AlphaGeometry 2, a versão atualizada do AlphaGeometry, é um sistema híbrido neural-simbólico treinado do zero com base no modelo de linguagem do Gemini.

Com base em uma ordem de grandeza maior de dados sintéticos do que a geração anterior, ele pode resolver problemas geométricos mais difíceis, incluindo equações envolvendo movimento de objetos, ângulos, proporções, distâncias, etc.

Além disso, possui um mecanismo simbólico duas ordens de grandeza mais rápido que seu antecessor. Quando novos problemas são encontrados, utiliza um novo mecanismo de partilha de conhecimento que permite combinações avançadas de diferentes árvores de pesquisa para resolver problemas mais complexos.

Antes de participar da IMO este ano, o AlphaGeometry 2 já havia alcançado muito sucesso: poderia resolver 83% dos problemas de geometria da IMO nos últimos 25 anos, enquanto a primeira geração só poderia resolver 53%.

Neste IMO, a velocidade do AlphaGeometry 2 chocou a todos - 19 segundos após receber a pergunta formal, ele resolveu a questão 4!

A questão 4 exige prova de que a soma de ∠KIL e ∠XPY é igual a 180°. AlphaGeometry 2 recomenda construir um ponto E na linha BI tal que ∠AEB=90°.O ponto E ajuda a determinar o ponto médio L de AB, formando muitos pares semelhantes de triângulos, como ABE ~ YBI e ALE ~ IPC, comprovando assim a conclusão

Processo de resolução de problemas de IA

Vale ressaltar que essas questões serão primeiro traduzidas manualmente para uma linguagem matemática formal antes de serem submetidas à IA.
P1

De modo geral, a primeira questão (P1) em cada teste IMO é relativamente fácil.

Os internautas disseram: “P1 requer apenas conhecimento de matemática do ensino médio, e os jogadores humanos geralmente o completam em 60 minutos”.

A primeira questão da IMO 2024 examina principalmente as propriedades do número real α e exige encontrar um número real α que satisfaça certas condições.

AI deu a resposta correta - α é um número inteiro par. Então, como exatamente isso é respondido?

Na primeira etapa da resolução do problema, a IA primeiro apresentou um teorema de que os conjuntos esquerdo e direito são iguais.

O conjunto da esquerda representa que todos os números reais α que atendem às condições, para qualquer inteiro positivo n, n pode dividir ⌊i*α⌋ de 1 a n; um número par, e o número real α é igual a k.

A prova a seguir está dividida em duas direções.

Primeiro prove que o conjunto da direita é um subconjunto (direção simples) do conjunto da esquerda.

Então, prove que o conjunto da esquerda é um subconjunto do conjunto da direita (direção difícil).

Até o final do código, a IA surgiu com uma equação chave ⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋), usando a equação para provar que α deve ser um numero par.

Finalmente, DeepMind resumiu os três axiomas nos quais a IA depende no processo de resolução de problemas: propext, Classical.choice e Quot.sound.

A seguir está o processo completo de resolução de problemas de P1: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html

P2

A segunda questão examina a relação entre o par de inteiros positivos (a, b), que envolve a propriedade do máximo divisor comum.

A resposta resolvida pela IA é:

O teorema é que para um par de inteiros positivos (a, b) que satisfaça certas condições, seu conjunto só pode conter (1,1).

No seguinte processo de resolução de problemas, a estratégia de prova adotada pela IA é primeiro provar que (1,1) satisfaz as condições dadas e depois provar que esta é a única solução.

Prove que (1,1) é a solução final, usando g=2, N=3.

Mostre que se (a,b) é a solução, então ab+1 deve dividir g.

Neste processo, a IA utilizou o teorema de Euler e as propriedades das operações modulares para o raciocínio.

Finalmente, prove que a=b=1 é a única solução possível.

A seguir está o processo completo de resolução de problemas do P2: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html

P4

P4 é uma questão de prova geométrica que requer a prova de uma relação angular geométrica específica.

Conforme mencionado acima, isso foi concluído pelo AlphaGeometry 2 em 19 segundos, estabelecendo um novo recorde.

Dependendo da solução dada, assim como no AlphaGeometry de primeira geração, pontos auxiliares em todas as soluções são gerados automaticamente pelo modelo da linguagem.

Na prova, todo rastreamento de ângulo usa eliminação gaussiana, e d(AB)−d(CD) é igual ao ângulo direcional de AB para CD (módulo π).

Durante o processo de resolução de problemas, a IA marcará manualmente pares de triângulos semelhantes e triângulos congruentes (marcados em vermelho).

A seguir, seguem os passos para resolver o problema de AlphaGeometria, que é completado utilizando o “método de recontradição”.

Primeiro utilize o Lean para formalizar as proposições que precisam ser provadas e visualizar a construção geométrica.

As principais etapas da prova são as seguintes.

Veja a imagem abaixo para o processo completo de resolução de problemas: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html

P6

A sexta questão da IMO é o "chefe final", que explora as propriedades das funções e exige a comprovação de conclusões específicas sobre números racionais.

AI resolve, c=2.

Vejamos primeiro a declaração do teorema, que define as propriedades da "função Aquaesuliana" e declara que para todas essas funções, o conjunto de valores de f(r)+f(-r) tem no máximo 2 elementos.

A estratégia de prova é primeiro provar que para qualquer função Aquaesuliana, o conjunto de valores de f(r)+f(-r) tem no máximo 2 elementos. Em seguida, construa uma função Aquaesuliana específica para que f(r)+f(-r) tenha exatamente 2 valores diferentes.

Prove que quando f(0)=0, f(x)+f(-x) assume no máximo dois valores diferentes, e prove que não existe função Aquaesuliana f(0)≠0.

Construa a função f(x)=-x+2⌈x⌉ e prove que é uma função Aquaesuliana.

Finalmente, prove que para esta função, f(-1)+f(1) =0 e f(1/2)+f(-1/2)=2 são dois valores diferentes.

A seguir está o processo completo de resolução de problemas: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html

Você pode responder às questões de matemática das Olimpíadas, mas consegue dizer qual é maior, 9,11 ou 9,9?

Andrew Gao, pesquisador da Universidade de Stanford e Sequoia, afirmou a importância deste avanço da IA——

O principal é que as últimas questões do teste IMO não estão incluídas no conjunto de treinamento. Isto é importante porque mostra que a IA pode lidar com problemas novos e invisíveis.

Além disso, os problemas geométricos resolvidos com sucesso pela IA sempre foram considerados extremamente desafiadores devido à natureza do espaço envolvido (exigindo pensamento intuitivo e imaginação espacial).

Jim Fan, um cientista sênior da Nvidia, postou um longo artigo dizendo que grandes modelos são existências misteriosas——

Eles podem ganhar medalhas de prata em Olimpíadas de matemática e frequentemente cometem erros em perguntas como "Qual número é maior, 9,11 ou 9,9?"

Não apenas Gemini, mas também GPT-4o, Claude-3.5 e Llama-3 não conseguem responder 100% corretamente.

Ao treinar modelos de IA, estamos explorando vastas áreas além da nossa própria inteligência.No processo, descobrimos uma área muito estranha – um exoplaneta que se parece com a Terra, mas está cheio de vales estranhos

Isso parece irracional, mas podemos explicar usando a distribuição dos dados de treinamento:

AlphaProof e AlphaGeometry 2 são treinados em provas formais e mecanismos simbólicos específicos de domínio. Até certo ponto, eles são melhores na resolução de problemas especializados de Olimpíadas, embora sejam baseados em um LLM de uso geral. O conjunto de treinamento do GPT-4o é misturado com uma grande quantidade de dados de código GitHub, que pode exceder em muito os dados matemáticos. Entre as versões de software, "v9.11 > v9.9" pode distorcer seriamente a distribuição de dados. Portanto, esse erro é compreensível até certo ponto.

O chefe dos desenvolvedores do Google disse que modelos que podem resolver problemas matemáticos e físicos difíceis são o caminho principal para AGI, e hoje demos mais um passo nesse caminho.

Outros internautas disseram que houve muita informação esta semana.

Referências:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

https://x.com/DrJimFan/status/1816521330298356181