🤖 AI

PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs

El artículo presenta PriorProof, un método automatizado y libre de ontologías para cuantificar la novedad de las técnicas de prueba formal en Lean mediante la medición de la sorpresa de sus huellas de dependencia frente a un conocimiento previo anclado en el tiempo, demostrando una concordancia moderada con expertos humanos y sirviendo como una señal decomponible e interpretable en lugar de un reemplazo para el juicio experto.

Autores originales: Neel Somani

Publicado 2026-07-21

📖 8 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Neel Somani

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que estás caminando a través de una biblioteca masiva y en constante expansión de ideas matemáticas. En esta biblioteca, cada libro nuevo (una demostración) debe citar los libros antiguos que utilizó para construir sus argumentos. Por lo general, cuando un matemático escribe una nueva demostración, intenta usar las herramientas más comunes y trilladas disponibles en ese momento. Pero a veces, toma un camino salvaje e inesperado, utilizando una combinación extraña de herramientas antiguas que nadie pensó en mezclar antes. La gran pregunta es: ¿cómo sabemos, simplemente mirando la lista de libros que utilizó, si su camino fue verdaderamente sorprendente o solo un desvío rutinario? Este es el rompecabezas de la "novedad" en la matemática formal. Mientras que los humanos pueden discutir si una demostración es "elegante" o "original", las computadoras luchan con estos sentimientos difusos. Necesitan una forma dura y mecánica de medir si una demostración tomó una ruta que era improbable que ocurriera dado lo que se sabía en ese momento. Aquí es donde entra la idea de la "sorpresa" (surprisal)—piensa en ello como una medida de cuánto hace la demostración que la biblioteca diga: "¡Espera, no esperaba que usaras esa herramienta específica para este trabajo!".

Entra PriorProof, una nueva herramienta diseñada para actuar como un bibliotecario que viaja en el tiempo. En lugar de preguntar a un humano: "¿Fue esta demostración ingeniosa?", PriorProof hace una pregunta fría y dura: "Si congeláramos la biblioteca en el momento exacto en que esta demostración fue escrita, ¿qué tan sorprendente sería la lista de herramientas utilizadas?". Los investigadores construyeron un sistema que observa una demostración formal (escrita en un lenguaje llamado Lean), elimina el formato elegante y crea una "huella" de la maquinaria matemática específica utilizada. Luego, viaja al pasado para tomar una instantánea de la biblioteca de antes de que existiera esa demostración. Pregunta: "Basándose en otras demostraciones con objetivos similares de ese tiempo anterior, ¿qué tan probable era que alguien usara estas herramientas específicas?". Si la respuesta es "muy improbable", la demostración recibe una "puntuación de novedad" alta. El estudio encontró que este puntaje mecánico a menudo coincide con los expertos humanos sobre qué demostraciones tomaron la ruta más inusual, especialmente cuando la diferencia en las puntuaciones es grande. Sin embargo, los autores tienen cuidado de decir que esto no es una varita mágica que lo resuelve todo; es una señal útil que funciona mejor cuando la brecha entre dos demostraciones es obvia, y no mide la "belleza" o la "importancia" de las matemáticas, solo qué tan inesperado fue el camino.

El Bibliotecario que Viaja en el Tiempo

Imagina que eres un detective tratando de averiguar si un ladrón usó un método secreto y nunca antes visto para abrir una caja fuerte. No puedes preguntar al ladrón qué estaba pensando, pero puedes mirar las herramientas que dejó atrás. PriorProof es ese detective, pero para demostraciones matemáticas. No le importa el motivo del ladrón o qué tan genial pareció el robo; solo le importan las herramientas (las constantes matemáticas y los lemas) utilizadas para resolver el problema y si esas herramientas fueron una elección extraña para el período de tiempo.

Así es como funciona el truco de magia, paso a paso:

La Huella: Cuando un matemático escribe una demostración en Lean (un lenguaje de computadora para las matemáticas), la computadora la convierte en una lista larga y detallada de cada una de las herramientas que utilizó. PriorProof toma esta lista y la limpia, agrupando herramientas similares en "familias" (como agrupar todos los martillos juntos, o todos los destornilladores). Esta es la "huella".
La Máquina del Tiempo: El sistema luego viaja al pasado. Toma una instantánea de toda la biblioteca de matemáticas de antes de que se escribiera la demostración. Observa todas las otras demostraciones escritas alrededor de ese tiempo que intentaban resolver problemas similares.
La Predicción: Usando un modelo de computadora inteligente (un modelo de lenguaje), predice: "Si yo estuviera escribiendo una demostración para este problema en aquel entonces, ¿qué herramientas probablemente usaría?". Construye una expectativa "a priori", como un pronóstico del tiempo para herramientas matemáticas.
La Puntuación de Sorpresa: Finalmente, compara las herramientas reales utilizadas en la nueva demostración contra el pronóstico. Si la demostración utilizó herramientas que el pronóstico dijo que eran muy improbables (baja probabilidad), el sistema le otorga una puntuación de "sorpresa" alta. Una puntuación alta significa: "¡Vaya, ese fue un camino muy extraño de tomar!".

Lo que el Detective Encontró

Los investigadores probaron este sistema en una sección específica de la biblioteca matemática llamada Topología (que trata sobre formas y espacios). No solo adivinaron; establecieron una prueba ciega. Tomaron 100 pares de demostraciones y se las mostraron a tres expertos matemáticos humanos. Los expertos tenían que elegir cuál demostración en cada par tomó la ruta "menos estándar" (más sorprendente). Ellos no vieron las puntuaciones, solo usaron sus cerebros.

Luego, compararon las elecciones de los expertos humanos con lo que predijo PriorProof. Aquí está el resultado:

De 76 pares únicos de demostraciones (algunos fueron mostrados múltiples veces para verificar la consistencia), PriorProof estuvo de acuerdo con la mayoría de los expertos humanos en 53 de ellos. Eso es aproximadamente el 69.7%.
Para los 12 pares que fueron seleccionados específicamente porque eran ejemplos "de libro de texto" obvios de demostraciones sorprendentes frente a las estándar, PriorProof acertó en 11 de ellos (alrededor del 91.7%).
Para los otros 64 pares, que eran un poco más complicados, acertó en 42 (alrededor del 65.6%).

Los autores también observaron la "brecha de puntuación": la diferencia entre la puntuación de sorpresa de las dos demostraciones en un par. Encontraron un patrón interesante: cuando la brecha era enorme (significando que una demostración era mucho más sorprendente que la otra), el sistema era muy confiable, coincidiendo con los humanos el 84.2% de las veces. Pero cuando la brecha era pequeña (las dos demostraciones eran de forma similar sorprendentes), el sistema era menos seguro, coincidiendo solo el 63.2% de las veces. Esto sugiere que la herramienta es excelente para detectar las "grandes sorpresas", pero se vuelve difusa cuando las diferencias son sutiles.

Lo que NO Es (y lo que descarta)

Es crucial entender lo que PriorProof no está afirmando ser. Los autores son muy claros al respecto:

No es una medida de "Originalidad" o "Genio": Una puntuación alta no significa que el matemático fuera un genio. Solo significa que usó una combinación extraña de herramientas. A veces, un camino extraño es solo un desvío torpe, no un insight brillante.
No es una medida de "Importancia": Una demostración puede ser increíblemente importante para el mundo de las matemáticas pero usar herramientas muy estándar y aburridas. PriorProof le daría una puntuación baja, incluso si cambiara la historia.
No es un "Detector de Plagio": Al sistema no le importa si alguien copió una demostración. Solo le importa la probabilidad estadística de las herramientas utilizadas.
No es un Juez "Perfecto": Los autores declaran explícitamente que su método no es un "problema resuelto". De hecho, cuando compararon a PriorProof con un modelo de lenguaje de IA potente (GPT-5-mini), la IA de hecho estuvo de acuerdo con los expertos humanos con un poco más de frecuencia (alrededor del 78.9% frente al 69.7%). Sin embargo, la diferencia no fue lo suficientemente significativa estadísticamente como para decir que uno era definitivamente mejor que el otro. El valor real de PriorProof no es que venza a la IA, sino que es transparente. Puedes mirar la puntuación y ver exactamente qué herramienta causó la sorpresa, mientras que la IA es una "caja negra" que solo da una respuesta.

La Conclusión

PriorProof es una nueva forma mecánica de medir qué tan "no estándar" es una demostración matemática al observar qué tan sorprendentes fueron sus elecciones de herramientas en el momento en que fue escrita. Funciona lo suficientemente bien como para estar de acuerdo con los expertos humanos aproximadamente dos tercios de las veces, y mejora aún más cuando la diferencia entre dos demostraciones es obvia. No nos dice si una demostración es hermosa, importante o brillante, pero sí nos da una señal fiable y con marca de tiempo que dice: "Oye, este camino fue inesperado". Es una herramienta para que los investigadores encuentren casos interesantes para estudiar, no un juez final de la grandeza matemática. Los autores sugieren que en el futuro podríamos usar esto para ayudar a detectar demostraciones generadas por máquinas interesantes o para estudiar cómo evolucionan las bibliotecas matemáticas, pero por ahora, es solo una forma muy inteligente y muy específica de medir la sorpresa.

Resumen Técnico: PriorProof

Planteamiento del Problema

Las bibliotecas de pruebas formales, como Mathlib de Lean, ofrecen un registro único del desarrollo matemático: el término de la prueba elaborado enumera explícitamente las constantes utilizadas, y el control de versiones identifica exactamente qué declaraciones existían en el momento de la escritura. Esto permite una investigación mecánica de la no estandaridad de la ruta de la prueba relativa al tiempo: determinar qué tan "sorprendente" o no estándar fue la ruta de una prueba en relación con las técnicas disponibles cuando fue escrita.

Mientras que las evaluaciones existentes de los probadores de teoremas aprendidos se centran en si un teorema se demuestra, el costo de búsqueda o la transferibilidad, no miden directamente si una prueba exitosa sigue una ruta que la biblioteca anterior habría hecho probable. Filósofos y matemáticos han analizado durante mucho tiempo las virtudes de la prueba como la explicación, la pureza y la elegancia, pero estas son difíciles de operacionalizar mecánicamente. PriorProof aborda un constructo más estrecho: la novedad de la ruta, definida como la desviación de la huella de dependencia de una prueba respecto a la distribución esperada de dependencias para enunciados similares en el estado previo de la biblioteca.

Metodología

PriorProof es una medida trimestral y puntual para las pruebas de Lean 4/Mathlib. El proceso opera sobre una declaración de teorema $D$ escrita en un tiempo $t$ a través de tres etapas principales:

1. Extracción de la Huella de Dependencia

El sistema extrae una "huella de familia de dependencias" ponderada del término de la prueba elaborado $p_D$ :

Extracción: Utiliza getUsedConstants de Lean para identificar las constantes realmente referenciadas por el término de la prueba, excluyendo meras importaciones de archivos.
Filtrado: Un filtro determinista elimina recursores generados, coerciones, la infraestructura de tipos (typeclass plumbing) y el código repetitivo de tácticas (tactic boilerplate).
Recorrido de la Frontera: Las dependencias se reemplazan recursivamente por dependencias más antiguas sobre las que estas reposan hasta que el recorrido alcanza las declaraciones establecidas en la instantánea de la biblioteca anterior a $t$ . La definición de establecimiento se basa en un umbral de recuento de reutilización pre-bin para evitar que las declaraciones co-introducidas aparezcan como establecidas.
Retroceso de Familia: Cada constante superviviente se mapea a la "familia de dependencia" más fina (espacio de nombres, módulo o área de la biblioteca) con al menos cinco ocurrencias pre-bin. Esto reduce la novedad accidental de nombres raros sin requerir una ontología construida a mano.
Resultado: Un conjunto ponderado $\Phi_t(D) = \{(f_i, w_i)\}$ que representa las familias de dependencias observadas.

2. Construcción del Prior Condicionado al Enunciado

Para determinar qué era "esperado", el sistema recupera enunciados de teoremas similares de una instantánea de la biblioteca estrictamente anterior al trimestre del objetivo ( $L_{<b(t)}$ ):

Recuperación: Un codificador de transformador de oraciones (ajustado mediante contraste de pares pre-bin) recupera los $k=32$ vecinos más cercanos basados en la similitud de coseno.
Suavizado: Se construye un prior suavizado jerárquicamente $q_t(f|D)$ $q_{t} (f ∣ D)$ como una mezcla de distribuciones empíricas de familias de:
- Vecinos recuperados ( $q_{r,t}$ )
- Espacio de nombres del objetivo ( $q_{n,t}$ )
- Módulo del objetivo ( $q_{m,t}$ )
- La biblioteca completa pre-bin ( $q_{g,t}$ )
Optimización: Los pesos de la mezcla y los parámetros de suavizado se seleccionan maximizando la verosimilitud logarítmica cronológica de las familias observadas en pruebas anteriores, asegurando que el prior sea predictivo en lugar de estar ajustado al estudio humano.

3. Puntuación

La puntuación PriorProof $S_t(D)$ es la surprisal ponderada de la huella observada bajo el prior construido:
$S_t(D) = \sum_{i=1}^{m_D} w_i [-\log q_t(f_i | D)]$
Una puntuación alta indica que la prueba utiliza familias de dependencias que eran improbables para teoremas anteriores con enunciados similares. Para comparaciones por pares, la métrica selecciona la prueba con la puntuación más alta, utilizando la brecha absoluta de puntuación $\Delta(A, B)$ como una señal de confianza interna.

Contribuciones Clave

Definición Mecánica: Una definición de la no estandaridad de la ruta de la prueba relativa al tiempo como la surprisal de la huella de dependencia, que no requiere una ontología de técnicas construida a mano ni etiquetas humanas.
Disciplina Temporal: Una disciplina de fuga rigurosa donde la recuperación, el soporte de la familia, los recuentos de reutilización y el ajuste del codificador están estrictamente restringidos a los datos pre-bin.
Estudio Empírico: Un estudio cegado sobre la topología de Mathlib que involucra validación mecánica, una comparación de tres evaluadores y un baseline de modelo de lenguaje.
Evidencia de Calibración de Extremo: Evidencia de que la brecha de puntuación absoluta sirve como un indicador de fiabilidad candidato, donde las brechas mayores se correlacionan con una mayor concordancia con los evaluadores humanos, aunque la relación no es una escalera monótona resuelta.

Resultados

El estudio evaluó 100 presentaciones ciegas (que colapsan en 76 pares de pruebas distintos) contra tres evaluadores expertos de dominio y baselines de modelos de lenguaje (gpt-5/gpt-5-mini).

Acuerdo con los Evaluadores: PriorProof estuvo de acuerdo con la mayoría de los tres evaluadores en 53/76 pares (69.7%).
- Pares Canónicos: 11/12 (91.7%) en 12 contrastes canónicos seleccionados a mano.
- Pares Estratificados: 42/64 (65.6%) en el conjunto más amplio.
Baseline de Modelo de Lenguaje: El mejor escenario de modelo de lenguaje estuvo de acuerdo en 60/76 pares (78.9%). Una prueba de McNemar comparando PriorProof y el modelo arrojó $p=0.210$ , lo que indica que la diferencia no está establecida estadísticamente con este tamaño de muestra.
Calibración de la Brecha de Puntuación:
- En el grupo de menor brecha de puntuación, el acuerdo fue de 12/19 (63.2%), estadísticamente compatible con el azar.
- En el grupo de mayor brecha de puntuación, el acuerdo fue de 16/19 (84.2%).
- Los grupos intermedios fueron no monótonos y los intervalos de confianza fueron amplios. El artículo concluye que esto apoya una tendencia de calibración de extremo (las brechas altas son más fiables) en lugar de una curva de calibración universal resuelta.
Validación Mecánica: Las huellas observadas recibieron una probabilidad cronológica significativamente mayor que las alternativas aleatorias. Los estudios de ablación confirmaron que los componentes de recuperación y suavizado contribuyen significativamente a la puntuación, mientras que las comprobaciones de redundancia no encontraron impactos "vivos" en el corpus curado (aunque la ruta anidada estaba inactiva debido a limitaciones del backend).

Significado y Reivindicaciones

El artículo presenta PriorProof no como un reemplazo del juicio experto o de los modelos, ni como una teoría completa de la novedad matemática. En su lugar, se posiciona como una señal decomponible y anclada en el tiempo.

Alcance: La métrica apunta específicamente a si una ruta de prueba utiliza maquinaria previa distribuida de forma inesperada. Es ciega a la novedad de la definición, el valor explicativo, la elegancia o el crédito de autoría.
Indicador de Fiabilidad: La utilidad principal identificada es la brecha de puntuación. Los resultados sugieren que cuando la brecha de puntuación entre dos pruebas es grande, la preferencia de la métrica es más probable que se alinee con el juicio humano. Cuando la brecha es pequeña, la métrica es menos fiable.
Limitaciones: Los autores señalan explícitamente que la métrica puede ser manipulada añadiendo maquinaria rara irrelevante, y que la implementación actual carece de normalización sensible al subtérmino (la detección de redundancia anidada está inactiva). El alcance estadístico está limitado a un dominio matemático (topología) y un tamaño de muestra específico.
Utilidad Futura: La métrica está destinada a ser un instrumento de investigación para analizar pruebas formales verificadas, priorizar casos para revisión experta y estudiar pruebas generadas por máquinas para ver si reproducen patrones esperados o descubren rutas que merecen la atención humana. Es un generador de hipótesis, no un árbitro de la originalidad.