- O problema da distância unitária é um problema de Erdős de 1946 que pergunta qual é o número máximo de pares de pontos a distância 1 entre n pontos no plano, e uma antiga conjectura central foi refutada
- O modelo de raciocínio de propósito geral da OpenAI criou uma família infinita de exemplos que quebra a crença de que a família da grade quadrada era essencialmente a melhor possível, e apresentou uma melhoria em nível polinomial
- A nova construção produz mais de
n^{1+δ}pares de pontos a distância unitária para infinitos valores de n, e um refinamento de Will Sawin mostra queδ = 0.014é possível - A prova aplica ferramentas de teoria algébrica dos números a um problema geométrico, indo além dos inteiros gaussianos e usando torre infinita de corpos de classes e teoria de Golod–Shafarevich
- O resultado mostra que a IA pode contribuir com descobertas matemáticas originais em problemas abertos antigos, tornando a expertise humana ainda mais importante na escolha e interpretação dos problemas
Avanço no problema da distância unitária
- O problema da distância unitária é um problema de geometria combinatória que pergunta quantos pares de pontos exatamente à distância 1 podem ser formados no máximo entre n pontos colocados no plano
- Foi proposto por Paul Erdős em 1946, e o livro de 2005 de Brass, Moser e Pach, Research Problems in Discrete Geometry, descreve esse problema como “talvez o problema mais conhecido e mais fácil de explicar da geometria combinatória”
- O combinatorista de Princeton Noga Alon o apresentou como um dos problemas de que Erdős mais gostava, e Erdős ofereceu um prêmio por sua solução
- Por muito tempo, acreditou-se que a família de construções em grade quadrada produzia essencialmente o número máximo de pares de pontos a distância unitária
- Um modelo interno da OpenAI criou uma família infinita de exemplos que refuta essa antiga conjectura e oferece uma melhoria em nível polinomial
- A prova foi revisada por um grupo de matemáticos externos, que também escreveram um artigo complementar tratando do argumento, do contexto e do significado do resultado
- O texto original da prova pode ser visto em unit-distance-proof.pdf, o artigo complementar em unit-distance-remarks.pdf, e uma versão resumida da cadeia de raciocínio do modelo em unit-distance-cot.pdf
O método encontrado pela IA
- A prova veio de um sistema treinado para matemática, de um scaffolding para buscar estratégias de prova e de um modelo de raciocínio de propósito geral, e não de um sistema dedicado especificamente ao problema da distância unitária
- A avaliação foi feita como parte de um esforço mais amplo para medir se modelos avançados podem contribuir com pesquisa de ponta, usando uma coletânea de problemas de Erdős, e neste caso foi gerada uma prova que resolve um problema em aberto
- A matemática é um domínio claro para testar capacidade de raciocínio porque os problemas são precisos, provas candidatas podem ser verificadas e argumentos longos precisam manter consistência do início ao fim
- A prova aplica ideias inesperadas e sofisticadas de teoria algébrica dos números a um problema geométrico de aparência elementar
- Tim Gowers descreveu o resultado no artigo complementar como “um marco para a matemática com IA”
- O teórico dos números Arul Shankar avaliou que os modelos atuais de IA já mostram ser capazes de ir além de assistentes de matemáticos humanos, produzindo ideias originais e sofisticadas e levando-as até o fim
O conteúdo matemático do problema da distância unitária
- u(n) é definido como o número máximo possível de pares de pontos a distância unitária entre n pontos no plano
- Uma construção simples pode colocar n pontos em uma reta e produzir n−1 pares, enquanto uma grade quadrada produz cerca de 2n pares
- A melhor construção conhecida anteriormente vinha de uma grade quadrada reescalada e produzia
n^{1 + C / log log(n)}pares de pontos a distância unitária, para alguma constante C - Como
log log(n)cresce à medida que n aumenta, o termo adicional no expoente tende a 0, então o crescimento dessa construção fica apenas um pouco acima do linear - Durante décadas, acreditou-se amplamente que essa taxa era essencialmente a melhor possível, e Erdős conjecturou tecnicamente um limite superior de
n^{1+o(1)} - O novo resultado refuta essa conjectura ao construir, para infinitos valores de n, configurações de n pontos com pelo menos
n^{1+δ}pares de pontos a distância unitária, para algum expoente fixoδ > 0 - A prova original da IA não fornecia um valor explícito para δ, mas um refinamento posterior do professor de matemática de Princeton Will Sawin mostrou que é possível tomar
δ = 0.014
Por que o resultado é surpreendente
- Desde a construção original de Erdős em 1946, o melhor limite inferior conhecido havia permanecido essencialmente inalterado
- O melhor limite superior conhecido,
O(n^{4/3}), veio do trabalho de Spencer, Szemerédi e Trotter em 1984, e permaneceu essencialmente intacto desde então, apesar de refinamentos e estudos de estruturas relacionadas por Székely, Katz e Silier, Pach, Raz, Solymosi e outros - Matoušek e Alon-Bucić-Sauermann estudaram esse problema para distâncias não euclidianas no plano, e apresentaram resultados mostrando que “a maioria” das distâncias não euclidianas segue, em certo sentido, a conjectura de Erdős, o que a reforçava
- É especialmente surpreendente que o ingrediente central da nova construção venha da teoria algébrica dos números, que à primeira vista parece distante de geometria e distância
- A teoria algébrica dos números é a área que trata de conceitos como fatoração dentro de extensões dos inteiros chamadas corpos de números algébricos
Novas técnicas vindas da teoria algébrica dos números
- A nova prova parte de ideias geométricas familiares e se expande em uma direção inesperada
- O limite inferior original de Erdős pode ser entendido por meio dos inteiros gaussianos da forma
a + bi - Aqui, a e b são inteiros, e i é a raiz quadrada de −1
- Os inteiros gaussianos estendem os inteiros usuais e possuem propriedades como fatoração única em primos, assim como os inteiros
- Extensões desse tipo dos inteiros ou dos racionais são chamadas de corpos de números algébricos
- O novo argumento substitui os inteiros gaussianos por generalizações mais complexas da teoria algébrica dos números, cuja simetria mais rica permite criar mais diferenças de comprimento unitário
- O argumento exato usa ferramentas como torre infinita de corpos de classes e teoria de Golod–Shafarevich para mostrar que os corpos numéricos necessários realmente existem
- Essas ideias já eram bem conhecidas pelos teóricos dos números, mas o fato de influenciarem um problema geométrico no plano euclidiano foi recebido como uma grande surpresa
O significado para a matemática
- O fato de um sistema de IA ter resolvido de forma autônoma um antigo problema em aberto no centro de uma área ativa torna este um momento importante na interação entre IA e matemática
- O trabalho complementar dos matemáticos externos oferece um quadro mais rico que não aparece apenas na solução original
- Thomas Bloom escreveu no artigo complementar que, ao avaliar a importância de uma prova gerada por IA, a pergunta é se essa prova ensinou algo novo sobre o problema e se ajudou a entender melhor a geometria discreta
- Bloom avaliou que o resultado mostra que construções de natureza teórica dos números podem dizer muito mais sobre essas questões do que se esperava, e que a teoria dos números necessária pode ser muito profunda
- Bloom acredita que, nos próximos meses, muitos teóricos algébricos dos números vão examinar de perto outros problemas em aberto da geometria discreta
- A conexão inesperada entre teoria algébrica dos números e geometria discreta não serve apenas para resolver uma conjectura específica, mas se torna uma ponte para explorar mais problemas relacionados
- O resultado mostra que a IA pode contribuir não só com respostas, mas também com descobertas matemáticas cujo significado se torna mais claro e mais rico por meio da compreensão humana posterior
Por que isso importa
- Um raciocínio matemático melhor pode tornar a IA uma parceira de pesquisa mais poderosa
- Ela pode manter de forma consistente longas cadeias de pensamento, conectar ideias entre áreas de conhecimento distantes e revelar caminhos promissores que especialistas talvez não priorizassem
- Isso pode ajudar pesquisadores a avançar em problemas complexos demais ou demorados demais para serem tratados com facilidade
- Essa capacidade é útil não só na matemática, mas também em biologia, física, ciência dos materiais, engenharia e medicina
- Se conseguir manter argumentos complexos de forma consistente, conectar áreas distantes do conhecimento e produzir resultados que passem por revisão especializada, isso passa a fazer parte do caminho de longo prazo rumo a sistemas de pesquisa mais automatizados
- Sugere-se que a IA começará a assumir um papel muito sério na parte criativa da pesquisa, especialmente na própria pesquisa em IA
- Esse avanço reforça a urgência de entender o problema do alinhamento de sistemas muito inteligentes, a próxima etapa do desenvolvimento de IA e o futuro da colaboração entre humanos e IA
- Esse futuro ainda depende do julgamento humano
- A expertise não se torna menos importante; ela se torna mais valiosa
- A IA pode ajudar a explorar, propor e verificar, mas cabe às pessoas escolher os problemas importantes, interpretar os resultados e decidir quais questões perseguir em seguida
1 comentários
Comentários do Hacker News
Esse tópico no HN me deixou deprimido, e ainda estou pensando no porquê
Se você tirar os elogios de release da OpenAI, há muitas questões interessantes e sutis sobre o papel dos LLMs na pesquisa matemática
Recomendo muito ler os comentários dos matemáticos que acompanham o resultado, especialmente as falas de Tim Gowers
Mas os comentários viraram um campo de batalha de debates sobre LLMs, refutações e contrarrefutações furiosas que se repetem desde 2023
Fico me perguntando se não é triste repetir a mesma briga em torno das linhas de frente traçadas há 3 anos e se estaremos nisso ainda daqui a 2 anos
Pode melhorar a vida guardar no coração a famosa passagem de Nietzsche: “Não quero travar guerra contra a feiura. Não quero acusar, nem mesmo quero acusar os acusadores. Desviar o olhar deve ser minha única negação”
Quanto mais a IA demonstra capacidade, mais a balança pende numa direção desconfortável para todos que não têm segurança no emprego muito sólida
Vai levar tempo até as pessoas reconhecerem que a IA tem um conjunto de capacidades bem diferente da inteligência humana e a complementa bastante bem
A chance de superar a inteligência humana em larga escala é baixa, e as empresas que apostarem nisso vão ficar para trás
Eu quero ter uma discussão de verdade sobre esses temas, mas como todo mundo acredita que só a própria realidade é real e a realidade oposta é falsa, isso continua escalando
Às vezes percebo que venho ao HN só para ficar com raiva e dou uma longa pausa
Não sei por que fazemos isso conosco mesmos, e no fundo acho que em geral queremos a mesma coisa
Para o pessoal do “LLM só interpola os dados de treino”: Ayer e o Wittgenstein inicial, embora de maneiras diferentes, viam a verdade matemática como algo que não relata novos fatos sobre o mundo
A ideia de que uma prova apenas desdobra o que já está implicitamente contido em axiomas, definições, símbolos e regras é profundamente interessante, e mesmo assim não há problema em dar crédito da descoberta ao matemático
Então, ou a recombinação de material existente não é desqualificante, ou então boa parte das Fields Medals teria de ser devolvida
Nem humanos produzem inovação em nova dimensão em todas as áreas todo ano
Dá para dizer que LLMs “apenas” recombinam, mas ainda duvido que um LLM treinado em toda a literatura de álgebra, geometria e trigonometria anterior a Newton/Leibniz conseguiria inventar o cálculo
Ainda assim, esse tipo de inovação é uma área em que LLMs são bons, e isso não significa que humanos deixem de precisar ser bons em inovação recombinatória
Em termos de sintetizar ideias novas, ainda parece haver muita coisa que humanos conseguem fazer e LLMs não
Se você desenhar a grande envoltória convexa em torno de todos esses pontos, o LLM, por ter aprendido dentro dela, consegue interpolar entre pontos existentes e chegar a pontos novos, mas ainda dentro da envoltória
Se LLMs conseguem chegar a pontos fora da envoltória ainda é discutível
Só chegar a novos pontos dentro dela já é muito útil
Muitas novas descobertas e provas, talvez a maioria das úteis, são desses pontos alcançáveis a partir do que já temos
Há muitas coisas que ainda não foram descobertas apenas porque ninguém dedicou tempo e esforço a isso, e LLMs podem acelerar bastante esse processo
Por outro lado, há pontos fora da envoltória que não são alcançáveis por extrapolação ou interpolação a partir dos pontos existentes, e exigem um salto realmente novo
A passagem da física newtoniana para a relatividade geral me parece um caso candidato
Demis Hassabis já falou em usar como avaliação de AGI um sistema de IA treinado só com conhecimento de física anterior a 1915, mostrar a ele a órbita de Mercúrio e ver se chega independentemente à relatividade geral
Duvido que os LLMs atuais consigam dar esse salto, e a maioria dos humanos também não conseguiria
Chamamos Einstein de gênio porque ele sozinho deu o salto até a relatividade geral; em humanos temos prova de existência de que isso às vezes acontece, mas com IA ainda resta ver
Pessoas como Descartes, Newton, Leibniz, Gauss, Euler, Ramanujan e Galois tratavam a matemática mais como arte do que como ciência
Por exemplo, muitos acham que para resolver a Riemann Hypothesis provavelmente será preciso um novo tipo de matemática, e acho pouco provável que um LLM invente isso do nada
Isso é sem sentido e pouco relevante
Quando o Deep Blue venceu Kasparov, nem tudo mudou, e animais e máquinas sempre foram “melhores” do que humanos em certas dimensões
Para começo de conversa, não existe uma única régua; e, mesmo que existisse, ela não seria unidimensional nem linear, e cada régua e seus extremos mudam com o tempo
Isso também não significa entregar a vitória aos supremacistas de IA
LLMs são ferramentas muito úteis e vão continuar melhorando dramaticamente, mas não vão superar os humanos em todas as dimensões que algumas pessoas consideram centrais
Não haverá um momento em que, só por ultrapassar uma lista de métricas quantificadas, a IA será universalmente reconhecida como superior aos humanos
Porque o próprio “importante” é subjetivo
Para a afirmação de que “já está implicitamente contido” ser verdadeira, a matemática teria de ser um sistema fechado, mas já foi provado que não é
É possível sair da matemática usando a própria matemática, por isso foram necessários vários pinos axiomáticos, incluindo Zermelo-Fraenkel
Na prática, não entendemos bem a vastidão daquilo que poderíamos chamar objetivamente de “matemática”, e é possível que a matemática como a percebemos seja só parte de uma matemática maior, ou esteja gravemente errada
Não sabemos se essa matemática maior teria as mesmas propriedades fechadas e sistêmicas
Para quem usa bastante LLM para programar, isso não é tão surpreendente assim, era só questão de tempo
Matemáticos fazem novas descobertas criando e aplicando ferramentas matemáticas de novas formas
Isso envolve uma quantidade enorme de trabalho iterativo, seguindo intuição e explorando conexões
Como LLMs não têm senso do que significa “descoberta”, é difícil dizer que fazem descoberta de verdade, mas podem tentar todas as ferramentas matemáticas de forma estilo Monte Carlo em direção a um objetivo estreito, achar o que funciona e então empilhar em cima disso ou combinar melhorias
Lendo o texto, essa descoberta parece exatamente desse tipo, e o LLM foi além do resultado esperado usando uma “conexão surpreendente”
Mas sem o objetivo definido por humanos, a compreensão humana do valor do novo caminho usado pela IA e a linguagem matemática criada por humanos que permite explorar os conceitos, o resultado não tem significado
Por que a compreensão só vale quando é humana?
Por que o conhecimento seria só para humanos?
Se outra espécie resolvesse a contradição entre gravidade e mecânica quântica, isso não teria significado até nos explicar e nós entendermos?
O interessante é a forma como essa prova, ou mais precisamente refutação, encontrou um contraexemplo para a conjectura original de Erdős
Como na reação de um matemático no PDF linkado, eu diria que isso é um pouco menos interessante do que provar que a conjectura verdadeira é de fato verdadeira
Provar que uma conjectura é verdadeira exige mais construção teórica
Você precisa explicar por que aquela conjectura está correta com base numa teoria maior; num contraexemplo, basta que o modelo encontre a configuração correta com uma forma mais sofisticada de busca
Claro, essa busca não é simples e é impressionante, e foram necessários muitos passos até provar a conexão com o contraexemplo
Ainda assim, me parece mais uma ligação de ideias já existentes do que o desenvolvimento de matemática nova e profunda
Não é para diminuir esse enorme feito; acho mesmo que estamos chegando a algum lugar
É puro feeling, mas me parece que os modelos não estão longe de conseguir construir teoria o bastante para provar conjecturas mais complexas que exijam desenvolvimento de matemática nova, e que a questão é conseguir trabalhar em horizontes de tempo mais longos
Na maior parte dos casos, você vai roendo as bordas para simplificar o problema
Por exemplo, para provar que algo é impossível, primeiro você mostra que só há 5 famílias de casos possíveis, e consegue provar que 4 delas são impossíveis
Aí 80% do problema está resolvido, e encontrar um contraexemplo também fica com a busca 80% menor
No contraexemplo, você pode fazer conjecturas e dar saltos; se der certo, tudo bem, mas numa prova não pode
Em compensação, quando você encontra o contraexemplo, os becos sem saída que descartou normalmente ficam ocultos
Não importa por quanto tempo você o faça combinar coisas dos dados de treino
Como já disse antes, a IA vai ganhar uma Fields Medal antes de operar um McDonald's
A parte difícil era criar o tabuleiro de xadrez da matemática, ou seja, um ambiente como Lean; agora é reconhecimento de padrões e computação
LLMs são só o começo, e logo teremos IAs matemáticas mais especializadas, parecidas com o Stockfish
Foi feito puramente com entrada e saída em linguagem natural e, em muitos aspectos, eu diria que é até uma demonstração interessante do ponto oposto
A verificação entra quando você quer delegar ao computador também a checagem da prova
No momento, essa prova foi verificada manualmente por um grupo de matemáticos da área
Havia muita automação de “centauro reverso” ali
O Manna tinha uma lista do que precisava ser feito a cada momento e, quando um pedido chegava no caixa, dizia aos funcionários para preparar aquela refeição
Acompanhava centenas de tarefas como limpar banheiro, passar pano no chão, limpar mesas, varrer a calçada, descongelar pão, girar estoque, limpar janelas, e atribuía cada uma aos funcionários uma a uma
No fim do turno, o Manna sempre dizia “acabamos por hoje. Obrigado pela ajuda”, e você tirava o headset e o colocava no carregador
Como por 6 a 8 horas uma voz na sua cabeça dizia em detalhes minuciosos o que fazer, os primeiros minutos depois de tirar o headset eram sempre confusos, e para sair do restaurante você tinha de ligar o cérebro de novo
[0] https://en.wikipedia.org/wiki/Manna_(novel)
A Fields Medal virá bem depois das duas
É preciso validação de especialistas humanos para checar se não é só besteira
O Lean não tem nada de especial aqui, é quase só efeito manada
Além disso, nem sabemos o quanto o treinamento em Lean ajudou esse modelo específico
Essa prova aplica uma ideia inesperada e sofisticada da teoria algébrica dos números a uma questão de geometria elementar
Quanto mais leio sobre resultados assim, mais sinto que boa parte da força do modelo vem de ter conhecimento prévio sobre praticamente todas as áreas possíveis e não ter dificuldade em transferi-lo para um novo domínio
A beleza potencial dessas ferramentas está em poder ajudar a romper a barreira da hiperespecialização excessiva que humanos enfrentam hoje na ciência
A hiperespecialização é importante por um lado, mas por outro limita as ferramentas e inspirações às quais uma pessoa pode ter acesso
Quanto mais hiperespecializados ficamos, mais os LLMs se tornam uma ferramenta valiosa para unir horizontes diferentes
Antes, o custo de acesso a isso era alto, mas agora não é mais
O legal é que, se alguém contribui com algo para a inteligência coletiva, isso pode ser aplicado imediatamente a qualquer problema em que outras pessoas estejam trabalhando
Talvez os LLMs possam ajudar a desenvolver uma compreensão mais horizontal de um campo
Como esse é um modelo geral, ele também tem conhecimento em nível de doutorado ou mais em física, biologia, história etc.
Acho que ainda não entendemos direito quanta coisa uma única “mente” que internalizou conhecimento de tantas áreas pode realizar
Quando a OpenAI disse que o modelo teria “inteligência de nível PhD”, todo mundo riu, e agora é interessante ver o critério mudando para conseguir criar matemática nova
Não se está pedindo nível PhD, e sim nível Leibniz, Euler ou Galois
O resumo do raciocínio desse trabalho, linkado no post do blog, tem 125 páginas
É uma escala de raciocínio absurda, bem parecida com o que a Anthropic insinuava com Mythos
Fico me perguntando por que só ouvimos falar de solução para problemas de Erdős
Deve haver incontáveis problemas em aberto na matemática, mas todas as “descobertas matemáticas” do ChatGPT que vejo em r/singularity e r/accelerate são problemas de Erdős
São famosos o bastante para chamar atenção e, ao mesmo tempo, não são interessantes o suficiente para que muita gente dedique grande esforço a eles
Resolver um problema já formulado por outra pessoa é uma atividade de nicho na pesquisa matemática
Mais comum é estudar algum objeto interessante, enquadrá-lo de um jeito que dê para atacar com as ferramentas disponíveis e então tentar encontrar uma solução
No cenário ideal, tanto a formulação do problema quanto a solução se tornam interessantes por si mesmas
É parecido com os problemas de Hilbert de um século atrás
Sem dúvida é impressionante
Mas, sem saber com o que esse modelo foi treinado, é muito difícil julgar até que ponto ele chegou nisso “por conta própria”
A indústria inteira de IA vem pagando muito dinheiro a especialistas de várias áreas para produzir grandes volumes de novos dados de treino
São dados de treino novos, que não podem ser encontrados em lugar nenhum, e as empresas os mantêm guardados; pode até haver ideias realmente originais ali dentro
É improvável que alguém tenha simplesmente resolvido esse problema e colocado no treino, mas, sendo sincero, também não posso dizer que a OpenAI com certeza não faria isso
O mais interessante é a possibilidade de já terem produzido dados de treino que tocavam a maioria ou até todas as proposições centrais que parecem “originais” nessa prova
Claro, não dá para saber
Mas essa pergunta sempre vai permanecer até que essas coisas sejam feitas de um jeito não secreto