Um modelo da OpenAI refutou uma conjectura central da geometria discreta

Durante quase 80 anos, os matemáticos estudaram uma questão enganosamente simples: se colocarmos $n$ pontos no plano, quantos pares de pontos podem estar exatamente à distância $1$ um do outro?

Este é o problema das distâncias unitárias no plano, formulado pela primeira vez por Paul Erdős em 1946. É uma das questões mais conhecidas da geometria combinatória, fácil de enunciar e notavelmente difícil de resolver. O livro de 2005 Research Problems in Discrete Geometry, de Brass, Moser e Pach, chama-lhe «possivelmente o problema mais conhecido (e mais simples de explicar) da geometria combinatória». Noga Alon, um combinatorialista de referência em Princeton, descreve-o como «um dos problemas favoritos de Erdős». Erdős chegou mesmo a oferecer um prémio monetário para a resolução deste problema.

Hoje, partilhamos um avanço no problema da distância unitária. Desde o trabalho original de Erdős, a crença predominante tem sido a de que as construções em «grelha quadrada» apresentadas mais abaixo eram essencialmente ótimas para maximizar o número de pares à distância unitária. Um modelo interno da OpenAI refutou esta conjectura de longa data, fornecendo uma família infinita de exemplos que produz uma melhoria polinomial. A prova foi verificada por um grupo de matemáticos externos. Também escreveram um artigo complementar que explica o argumento e fornece mais antecedentes e contexto sobre a importância do resultado.

O resultado também é notável pela forma como foi encontrado. A prova veio de um novo modelo de raciocínio de uso geral, e não de um sistema treinado especificamente para matemática, estruturado para procurar estratégias de prova ou direcionado em particular para o problema da distância unitária. Como parte de um esforço mais amplo para testar se modelos avançados podem contribuir para investigação de fronteira, avaliámo-lo numa coleção de problemas de Erdős. Neste caso, produziu uma prova que resolve o problema em aberto.

Esta prova é um marco importante para as comunidades da matemática e da IA. Marca a primeira vez que um problema em aberto de destaque, central para um subcampo da matemática, foi resolvido autonomamente por IA. Também demonstra a profundidade de raciocínio que estes sistemas agora suportam. A matemática oferece um terreno de teste particularmente claro para o raciocínio: os problemas são precisos, as provas potenciais podem ser verificadas, e um argumento longo só funciona se o raciocínio se mantiver coeso do princípio ao fim. O método pelo qual o problema foi resolvido também é notável. A prova aplica ideias inesperadas e sofisticadas da teoria algébrica dos números a uma questão geométrica elementar.

O medalhado Fields Tim Gowers, escrevendo no artigo complementar, chama ao resultado «um marco na matemática da IA». Segundo o destacado teórico dos números Arul Shankar, «Na minha opinião, este artigo demonstra que os atuais modelos de IA vão além de meros auxiliares dos matemáticos humanos – são capazes de ter ideias originais e engenhosas, e depois levá-las até à sua concretização».

A prova está disponível aqui⁠(abre numa nova janela). O artigo complementar de matemáticos externos de referência está disponível aqui⁠(abre numa nova janela). Pode encontrar uma versão abreviada da cadeia de pensamento do modelo aqui⁠(abre numa nova janela).

Seja $u(n)$ o maior número possível de pares à distância unitária entre $n$ pontos no plano. É fácil construir exemplos que atinjam uma taxa de crescimento linear: colocar $n$ pontos numa linha dá $n-1$ pares, enquanto uma grelha quadrada dá cerca de $2n$ pares. A melhor construção anteriormente conhecida, proveniente de uma grelha quadrada reescalada, acaba por dar ainda mais: $n^{1 + C / \log \log(n)}$ para uma constante $C$. Como $\log \log(n)$ tende para infinito com $n$, o termo adicional no expoente tende para $0$, o que significa que estas construções atingem um crescimento apenas ligeiramente mais rápido do que linear. Durante décadas, acreditou-se amplamente que esta taxa era essencialmente a melhor possível, e que nenhuma construção poderia melhorar significativamente a grelha quadrada. Em termos técnicos, Erdős conjeturou um limite superior de $n^{1+o(1)}$, em que o $o(1)$ adicional indica um termo que tende para $0$ com $n$.

O nosso novo resultado refuta esta conjetura. Mais precisamente, para infinitos valores de $n$, a prova constrói configurações de $n$ pontos com pelo menos $n^{1+\delta}$ pares à distância unitária, para algum expoente fixo $\delta > 0$. (A prova original da IA não dá um $\delta$ explícito, mas um refinamento futuro devido ao professor de matemática de Princeton Will Sawin mostrou que é possível tomar $\delta=0.014$.)

A história do problema ajuda a perceber por que motivo o resultado é surpreendente. O melhor limite inferior conhecido mantinha-se essencialmente inalterado desde a construção original de Erdős em 1946. O melhor limite superior, $O(n^{4/3})$, remonta ao trabalho de Spencer, Szemerédi e Trotter em 1984 e, apesar de refinamentos posteriores e de trabalho estrutural relacionado de Székely, Katz e Silier, Pach, Raz e Solymosi, entre outros, o limite superior permaneceu essencialmente inalterado. Como evidência a favor da conjetura, Matoušek e Alon-Bucić-Sauermann estudaram o problema com distâncias não euclidianas no plano e provaram que a «maioria» destas distâncias não euclidianas obedece à conjetura em algum sentido.

Surpreendentemente, os ingredientes-chave da construção vêm de uma parte muito diferente da matemática, conhecida como teoria algébrica dos números, que estuda conceitos como a fatorização em extensões dos inteiros conhecidas como corpos de números algébricos.

A um nível elevado, a prova começa com uma ideia geométrica familiar e leva-a numa direção inesperada.

O limite inferior original de Erdős pode ser compreendido através dos inteiros gaussianos: números da forma $a+bi$, em que $a$ e $b$ são inteiros e $i$ é a raiz quadrada de $-1$. Os inteiros gaussianos estendem os inteiros comuns e, tal como eles, gozam de propriedades como a fatorização única em primos. Tais extensões dos inteiros comuns ou dos racionais são conhecidas como corpos algébricos de números. O novo argumento substitui os inteiros gaussianos por generalizações mais complicadas da teoria algébrica dos números, com simetrias mais ricas que podem criar muito mais diferenças de comprimento unitário.

O argumento preciso usa ferramentas como torres infinitas de corpos de classes e a teoria de Golod–Shafarevich para mostrar que os corpos numéricos necessários para o argumento realmente existem. Estas ideias eram bem conhecidas dos teóricos algébricos dos números, mas foi uma grande surpresa que estes conceitos tenham implicações para questões geométricas no plano euclidiano.

Este resultado marca um momento importante na interação entre a IA e a matemática: um sistema de IA resolveu autonomamente um problema em aberto de longa data no centro de uma área ativa. Também oferece um primeiro vislumbre de um novo tipo de colaboração entre a IA e os matemáticos humanos. Neste caso, o trabalho complementar de matemáticos externos traça um quadro substancialmente mais rico do que a solução original por si só.

Como Thomas Bloom escreve na nota complementar:

«Ao avaliar a importância e a influência de uma prova gerada por IA, uma pergunta que faço a mim próprio é: isto ensinou-nos algo de novo sobre o problema? Compreendemos melhor a geometria discreta agora? Penso que a resposta é um sim moderado: isto mostra que as construções da teoria dos números têm muito mais a dizer sobre este tipo de questões do que suspeitávamos; além disso, que a teoria dos números necessária pode ser muito profunda. Sem dúvida, muitos teóricos algébricos dos números irão olhar atentamente para outros problemas em aberto da geometria discreta nos próximos meses.»

A ligação inesperada entre a teoria algébrica dos números e a geometria discreta revelada pela solução é parte do que torna o resultado notável. Não se limita a resolver uma conjectura específica, podendo antes fornecer aos matemáticos uma ponte para começar a explorar outros problemas relacionados.

Bloom aponta também para uma possibilidade mais ampla:

«As fronteiras do conhecimento são muito irregulares e, sem dúvida, os próximos meses e anos verão sucessos semelhantes em muitas outras áreas da matemática, em que problemas em aberto de longa data são resolvidos por uma IA ao revelar ligações inesperadas e ao levar a maquinaria técnica existente ao seu limite. A IA está a ajudar-nos a explorar mais plenamente a catedral da matemática que construímos ao longo dos séculos; que outras maravilhas ainda invisíveis estarão à espera nos bastidores?»

Este resultado oferece um exemplo promissor: a IA contribui não só com uma solução, mas com uma descoberta matemática cujo significado se torna mais claro e mais rico através da compreensão humana subsequente.

A principal conclusão é maior do que este resultado em particular. Um melhor raciocínio matemático pode tornar a IA num parceiro de investigação mais forte: algo que consegue manter linhas de pensamento difíceis coesas, ligar ideias entre áreas distantes do conhecimento, revelar caminhos promissores que os especialistas podem não ter priorizado e ajudar os investigadores a progredir em problemas que, de outra forma, seriam demasiado complexos ou exigentes em tempo para abordar.

Essas capacidades importam para além da matemática. Se um modelo consegue manter coerente um argumento complicado, ligar ideias entre áreas distantes do conhecimento e produzir trabalho que resiste ao escrutínio de especialistas, então essas também são capacidades úteis na biologia, física, ciência dos materiais, engenharia e medicina, e fazem parte do nosso caminho de mais longo prazo para uma investigação mais automatizada: sistemas que podem ajudar cientistas e engenheiros a explorar mais ideias e a perseguir questões técnicas mais difíceis.

A IA está prestes a começar a assumir um papel muito sério nas partes criativas da investigação e, mais importante ainda, da própria investigação em IA. Embora este progresso não seja inesperado, reforça a urgência que sentimos em compreender esta próxima fase do desenvolvimento da IA, os desafios de alinhar sistemas muito inteligentes e o futuro da colaboração entre humanos e IA.

Esse futuro continua a depender do juízo humano. A especialização torna-se mais valiosa, não menos. A IA pode ajudar a procurar, sugerir e verificar. As pessoas escolhem os problemas que importam, interpretam os resultados e decidem que questões seguir a seguir.