Resumo Técnico: Medições Geométricas do Axioma da Escolha em Embeddings de Provas Neurais

Declaração do Problema

O axioma da escolha (AC) historicamente dividiu os fundamentos matemáticos entre campos clássicos e construtivos, uma distinção que permanece amplamente filosófica e metodológica. Enquanto provas clássicas utilizam atalhos não construtivos permitidos pelo AC, e provas construtivas exigem testemunhas explícitas, não estava claro se esses dois paradigmas diferem estruturalmente de formas detectáveis além da simples dependência de axiomas. Este artigo investiga se o axioma da escolha deixa uma "assinatura geométrica" mensurável no espaço de provas formais, especificamente dentro da biblioteca Mathlib do Lean 4, e se essa assinatura tem consequências operacionais para provadores de teoremas neurais.

Metodologia

Particionamento de Dados e Rastreamento de Dependência

Os autores utilizam o rastreamento de dependência de nível de kernel do Lean 4 para particionar a biblioteca Mathlib, que contém 471.260 declarações certificadas por máquina. Ao realizar uma busca em largura no grafo de dependência, eles classificam as declarações em dois conjuntos:

1. Provas Clássicas: Aquelas que dependem transitivamente de Classical.choice.
2. Provas Construtivas: Aquelas que não dependem.

A "distância" de uma prova clássica é definida como o comprimento da cadeia de dependência mais curta daquela prova até Classical.choice. Isso cria um conjunto de dados estratificado onde as provas são agrupadas por sua profundidade em relação ao axioma. O estudo foca em uma população filtrada de 42.355 teoremas (31.144 clássicos, 11.211 construtivos) com traços de táticas entre 2 e 200 passos.

Aprendizado de Representação Livre de Rótulos

Para medir as propriedades geométricas dessas provas sem viés, os autores treinam um autoencoder de denoising autossupervisionado exclusivamente em provas construtivas.

• Entrada: As provas são representadas como sequências de cabeças de táticas (ex: intro, rw, simp), descartando argumentos específicos para focar na composição da prova.
• Arquitetura: Um codificador Transformer de 4 camadas pareado com um decodificador de 2 camadas. O modelo é treinado para reconstruir tokens de táticas mascarados (2ência de corrupção de 20%) a partir da sequência de entrada.
• Embedding: O embedding da prova é a média dos estados ocultos do codificador (excluindo o preenchimento/padding), normalizada para a esfera unitária.
• Restrição Livre de Rótulos: O codificador nunca vê provas clássicas durante o treinamento, construção de vocabulário ou seleção de hiperparâmetros. As provas clássicas servem estritamente como uma população de controle (held-out).

Medições Geométricas

Três métricas complementares são usadas para medir a divergência das provas clássicas em relação à distribuição de treinamento construtiva como uma função de sua profundidade de dependência:

1. Pontuação de Anomalia (k-NN): A distância euclidiana para os $k$ vizinhos construtivos mais próximos.
2. Perda de Reconstrução: A perda de entropia cruzada incorrida quando o modelo treinado em construtivas tenta prever tokens mascarados em uma prova clássica.
3. Contenção de Supernível de Densidade: A fração de provas clássicas que caem fora da região de alta densidade (conjunto de supernível) definida pela distribuição de treinamento construtiva.

Avaliação Operacional

O estudo avalia o impacto dessas descobertas geométricas no desempenho da prova de teoremas usando dois sistemas:

1. aesop: Um provador de busca de melhor primeiro passo simbólico.
2. Híbrido (ReProver + aesop): Uma abordagem guiada neural onde um gerador de táticas propõe o primeiro movimento, seguido pelo aesop.

Principais Resultados

A Lei da Profundidade

A principal descoberta é a existência de uma "lei da profundidade": a distinção geométrica entre provas clássicas e construtivas decai previsivelmente com a distância de Classical.choice.

• Separação Nítida em Profundidades Rasas: Na profundidade 2 (provas que invocam diretamente lemas clássicos), a separação é forte. A pontuação de anomalia k-NN atinge um AUC de 0,847, a perda de reconstrução é 34,5% maior que a linha de base construtiva, e 43% das provas clássicas caem fora da região de 90% de densidade construtiva.
• Decaimento para Indistinguibilidade: À medida que a profundidade aumenta, as métricas convergem para a linha de base construtiva. Na profundidade 9+, todas as três métricas aproximam-se de níveis de acaso (AUC $\approx$ 0,5, perda $\approx$ linha de base, contenção $\approx$ 90%), tornando as provas clássicas profundas geometricamente indistinguíveis das construtivas.
• Lei de Mistura de Um Parâmetro: Os autores modelam esse gradiente como uma mistura de duas distribuições: uma distribuição construtiva $P$ e uma distribuição diretamente clássica $R$. A distribuição de profundidade-$d$ é modelada como $Q_d = (1 - \lambda_d)P + \lambda_d R$, onde $\lambda_d$ é um peso de mistura que diminui com a profundidade. As três medições distintas colapsam em uma única curva quando normalizadas, apoiando esta lei de um parâmetro.

Controles de Robustez

A assinatura é robusta contra vários potenciais confundidores:

• Palavras-chave: Remover marcadores de táticas explicitamente clássicos (ex: classical, by contra) reduz o AUC da profundidade-2 apenas ligeiramente (de 0,847 para 0,754), indicando que o sinal é estrutural, não meramente lexical.
• Comprimento: A residualização dos embeddings pelo comprimento da prova não elimina o gradiente.
• Autor/Arquivo/Tópico: Modelos de efeitos mistos controlando autor, arquivo e subdomínio matemático confirmam que o sinal persiste dentro de contextos específicos.
• Enunciado vs. Prova: Os enunciados dos teoremas mostram um gradiente de profundidade muito mais fraco (AUC 0,604 agregado) comparado às provas (AUC 0,675 agregado), confirmando que o sinal é primariamente composicional (estrutura da prova) e não topical (conteúdo do teorema).
• Especificidade do Axioma: Embora propext e Quot.sound também mostrem gradientes de profundidade, Classical.choice produz o gradiente mais íngreme, sugerindo um acoplamento operacional único com o raciocínio clássico.

Consequências Operacionais

A assinatura geométrica correlaciona-se com o desempenho do provador:

• Falha do aesop: O aesop resolve 20,0% dos teoremas construtivos, mas apenas 1,5% dos clássicos (uma lacuna de 13$\times$). Diferente do sinal geométrico, essa lacuna operacional não suaviza com a profundidade; as provas clássicas permanecem difíceis para o aesop independentemente de sua distância do axioma.
• Guia Neural: Adicionar um gerador de táticas neural (ReProver) comprime a lacuna para aproximadamente 5$\times$ (22,0% vs. 4,5%), mas não a fecha.
• Poder Preditivo: A pontuação de anomalia geométrica prevê a falha do aesop significativamente melhor do que apenas o comprimento da prova (o AUC aumenta de 0,766 para 0,841 ao adicionar a pontuação de anomalia).

Significância e Alegações

O artigo alega fornecer a primeira evidência empírica de que o axioma da escolha possui um correlato geométrico mensurável no espaço de provas. Os autores argumentam que:

1. Distinção Estrutural: A divisão clássico/construtivo não é apenas uma postura filosófica, mas uma propriedade estrutural da composição de provas que é visível em embeddings neurais.
2. Relevância Operacional: Esta assinatura geométrica não é apenas uma curiosidade abstrata; ela prevê o desempenho de provadores de teoremas automatizados. A "lei da profundidade" sugere que, conforme as provas se afastam do axioma, elas se tornam estruturalmente mais semelhantes às provas construtivas, embora a barreira operacional para provadores simbólicos como o aesop permaneça específica à presença de Classical.choice.
3. Contribuição Metodológica: O trabalho demonstra que o aprendizado autossupervisionado livre de rótulos em uma única classe (provas construtivas) pode revelar os limites estruturais de uma classe mantida (provas clássicas) definida por dependência lógica, oferecendo uma nova ferramenta para análise metamatemática.

Os autores permanecem modestos quanto aos mecanismos causais, observando que, embora a assinatura geométrica e a lacuna operacional estejam fortemente associadas, a causa específica da dificuldade do provador (barreira estrutural vs. configuração do conjunto de regras) requer investigação adicional. O trabalho é apresentado como um convite à comunidade para identificar eixos estruturais semelhantes em bibliotecas formais.