Resumen Técnico: Mediciones Geométricas del Axioma de la Elección en Incrustaciones de Pruebas Neuronales

Declaración del Problema

El axioma de la elección (AC) ha dividido históricamente los fundamentos matemáticos en campamentos clásicos y constructivos, una distinción que sigue siendo mayoritariamente filosófica y metodológica. Mientras que las pruebas clásicas utilizan atajos no constructivos permitidos por el AC, y las pruebas constructivas requieren testigos explícitos, no estaba claro si estos dos paradigmas difieren estructuralmente de formas detectables más allá de la simple dependencia de axiomas. Este artículo investiga si el axioma de la elección deja una "firma geométrica" medible dentro del espacio de las pruebas formales, específicamente dentro de la biblioteca Mathlib de Lean 4, y si esta firma tiene consecuencias operativas para los demostradores de teoremas neuronales.

Metodología

Partición de Datos y Seguimiento de Dependencias

Los autores utilizan el seguimiento a nivel de núcleo de Lean 4 sobre la dependencia de axiomas para particionar la biblioteca Mathlib, que contiene 471,260 declaraciones certificadas por máquina. Al realizar una búsqueda en anchura en el grafo de dependencias, clasifican las declaraciones en dos conjuntos:

1. Pruebas Clásicas: Aquellas que dependen transitivamente de Classical.choice.
2. Pruebas Constructivas: Aquellas que no lo hacen.

La "distancia" de una prueba clásica se define como la longitud de la cadena de dependencia más corta desde esa prueba hasta Classical.choice. Esto crea un conjunto de datos estratificado donde las pruebas se agrupan por su profundidad desde el axioma. El estudio se centra en una población filtrada de 42,355 teoremas (31,144 clásicos, 11,211 constructivos) con trazas de tácticas entre 2 y 200 pasos.

Aprendizaje de Representación Libre de Etiquetas

Para medir las propiedades geométricas de estas pruebas sin sesgo, los autores entrenan un autoencoder de eliminación de ruido autosupervisado exclusivamente en pruebas constructivas.

• Entrada: Las pruebas se representan como secuencias de cabezales de tácticas (por ejemplo, intro, rw, simp), descartando argumentos específicos para centrarse en la composición de la prueba.
• Arquitectura: Un codificador Transformer de 4 capas emparejado con un decodificador de 2 capas. El modelo está entrenado para reconstruir tokens de tácticas enmascarados (20% de corrupción) a partir de la secuencia de entrada.
• Incrustación (Embedding): La incrustación de la prueba es la media de los estados ocultos del codificador (excluyendo el relleno), normalizada a la esfera unitaria.
• Restricción Libre de Etiquetas: El codificador nunca ve pruebas clásicas durante el entrenamiento, la construcción del vocabulario o la selección de hiperparámetros. Las pruebas clásicas sirven estrictamente como una población de control.

Mediciones Geométricas

Se utilizan tres métricas complementarias para medir la divergencia de las pruebas clásicas respecto a la distribución de entrenamiento constructiva en función de su profundidad de dependencia:

1. Puntuación de Anomalía (k-NN): La distancia euclidiana al $k$-vecino más cercano de tipo constructivo.
2. Pérdida de Reconstrucción: La pérdida de entropía cruzada incurrida cuando el modelo entrenado en constructivas intenta predecir tokens enmascarados en una prueba clásica.
3. Contención de Supernivel de Densidad: La fracción de pruebas clásicas que caen fuera de la región de alta densidad (conjunto de supernivel) definida por la distribución de entrenamiento constructiva.

Evaluación Operativa

El estudio evalúa el impacto de estos hallazgos geométricos en el rendimiento de la demostración de teoremas utilizando dos sistemas:

1. aesop: Un demostrador de búsqueda de mejor primer paso simbólico.
2. Híbrido (ReProver + aesop): Un enfoque guiado neuronal donde un generador de tácticas propone el primer movimiento, seguido de aesop.

Resultados Clave

La Ley de la Profundidad

El hallazgo principal es la existencia de una "ley de profundidad": la distincción geométrica entre las pruebas clásicas y constructivas decae de forma predecible con la distancia de Classical.choice.

• Separación Marcada en Profundidades Superficiales: En la profundidad 2 (pruebas que invocan directamente lemas clásicos), la separación es fuerte. La puntuación de anomalía k-NN logra un AUC de 0.847, la pérdida de reconstrucción es un 34.5% mayor que la línea base constructiva, y el 43% de las pruebas clásicas caen fuera de la región de densidad del 90% de las constructivas.
• Decaimiento hacia la Indistinguibilidad: A medida que la profundidad aumenta, las métricas convergen hacia la línea base constructiva. Para la profundidad 9+, todas las tres métricas se acercan a los niveles del azar (AUC $\approx$ 0.5, pérdida $\approx$ línea base, contención $\approx$ 90%), haciendo que las pruebas clásicas profundas sean geométricamente indistinguibles de las constructivas.
• Ley de Mezcla de un Solo Parámetro: Los autores modelan este gradiente como una mezcla de dos distribuciones: una distribución constructiva $P$ y una distribución directamente clásica $R$. La distribución de profundidad-$d$ $Q_d$ se modela como $Q_d = (1 - \lambda_d)P + \lambda_d R$, donde $\lambda_d$ es un peso de mezcla que disminuye con la profundidad. Las tres mediciones distintas colapsan en una sola curva cuando se normalizan, lo que respalda esta ley de un solo parámetro.

Controles de Robustez

La firma es robusta frente a varios posibles factores de confusión:

• Palabras Clave: Eliminar marcadores de tácticas clásicas explícitos (por ejemplo, classical, by contra) reduce el AUC de la profundidad-2 solo ligeramente (de 0.847 a 0.754), lo que indica que la señal es estructural, no meramente léxica.
• Longitud: La residualización de las incrustaciones por longitud de la prueba no elimina el gradiente.
• Autor/Archivo/Tema: Los modelos de efectos mixtos que controlan al autor, el archivo y el subdominio matemático confirman que la señal persiste dentro de contextos específicos.
• Enunciado vs. Prueba: Los enunciados de los teoremas muestran un gradiente de profundidad mucho más débil (AUC 0.604 agregado) en comparación con las pruebas (AUC 0.675 agregado), confirmando que la señal es principalmente compositiva (estructura de la prueba) y no tópica (contenido del teorema).
• Especificidad del Axioma: Aunque propext y Quot.sound también muestran gradientes de profundidad, Classical.choice produce el gradiente más pronunciado, sugiriendo un acoplamiento operacional único con el razonamiento clásico.

Consecuencias Operativas

La firma geométrica se correlaciona con el rendimiento del demostrador:

• Fallo de aesop: aesop resuelve el 20.0% de los teoremas constructivos pero solo el 1.5% de los clásicos (una brecha de 13$\times$). A diferencia de la señal geométrica, esta brecha operativa no se suaviza con la profundidad; las pruebas clásicas siguen siendo difíciles para aesop independientemente de su distancia al axioma.
• Guía Neuronal: Añadir un generador de tácticas neuronal (ReProver) comprime la brecha a aproximadamente 5$\times$ (22.0% vs 4.5%), pero no la cierra.
• Poder Predictivo: La puntuación de anomalía geométrica predice el fallo de aesop significativamente mejor que la longitud de la prueba por sí sola (el AUC aumenta de 0.766 a 0.841 al añadir la puntuación de anomalía).

Significancia y Reivindicaciones

El artículo afirma proporcionar la primera evidencia empírica de que el axioma de la elección tiene un correlato geométrico medible en el espacio de las pruebas. Los autores argumentan que:

1. Distinción Estructural: La división clásica/constructiva no es solo una postura filosófica, sino una propiedad estructural de la composición de pruebas que es visible en las incrustaciones neuronales.
2. Relevancia Operativa: Esta firma geométrica no es una mera curiosidad abstracta; predice el rendimiento de los demostradores de teoremas automáticos. La "ley de profundidad" sugiere que, a medida que las pruebas se alejan del axioma, se vuelven estructuralmente más similares a las pruebas constructivas, aunque la barrera operativa para los demostores simbólicos como aesop sigue siendo específica para la presencia de Classical.choice.
3. Contribución Metodológica: El trabajo demuestra que el aprendizaje autosupervisado libre de etiquetas en una sola clase (pruebas constructivas) puede revelar los límites estructurales de una clase mantenida aparte (pruebas clásicas) definida por la dependencia lógica, ofreciendo una nueva herramienta para el análisis metamatemático.

Los autores mantienen la modestia sobre los mecanismos causales, señalando que, si bien la firma geométrica y la brecha operativa están fuertemente asociadas, la causa específica de la dificultad del demostrador (barrera estructural vs. configuración del conjunto de reglas) requiere mayor investigación. El trabajo se presenta como una invitación a la comunidad para identificar ejes estructurales similares en las bibliotecas formales.