Revisiting average case complexity of multilevel syllogistic: From the 1995 Courant Technical Report to Lean 4 Formalization

Resumen Técnico: Revisión de la Complejidad del Caso Promedio de la Silogística Multinivel

Planteamiento del Problema
Este trabajo revisa el informe técnico de Courant TR1995-711, "The average case complexity of multilevel syllogistic", de Cox, Ericson y Mishra (1995). El informe original investigó si los sublenguajes decidibles de la teoría de conjuntos —específicamente la Silogística Multinivel (MLS) y la Silogística Multinivel Elemental (EMLS)— son tratables en el caso promedio, a pesar de ser NP-completos en el peor de los casos. El informe afirmó que estos problemas son NP-promedio completos, lo que implica que, bajo distribuciones de probabilidad ordenables simples, no existe un algoritmo eficiente para el caso promedio a menos que las clases de complejidad NEXP y EXP colapsen. Mientras que el informe original proporcionó pruebas matemáticas, carecía de verificación verificada por máquina. Además, el campo de la demostración automática de teoremas posteriormente pivotó hacia los solucionadores SMT y los benchmarks empíricos en lugar del análisis formal del caso promedio de fragmentos de la teoría de conjuntos. Este artículo aborda la brecha entre las afirmaciones teóricas originales y los estándares modernos de verificación formal mediante la reimplementación de la lógica, las definiciones y los teoremas del informe en Lean 4.

Metodología
Los autores emplean una estrategia rigurosa de "programa de prueba", priorizando las definiciones formales sobre los teoremas y evitando el uso de sorry (suposiciones no probadas) en las definiciones finales. El desarrollo se estructura en cinco fases:

1. Infraestructura (Fase 0): Configuración del proyecto Lake y el entorno Lean.
2. Vocabulario de Complejidad del Caso Promedio (AvCom) (Fase 1): Formalización del marco de Reischuk–Schindelhauer (1993) y las definiciones de la complejidad del caso promedio de Levin (1986). Esto incluye la definición de:
   • Distribuciones: Distribuciones de probabilidad de soporte finito sobre cadenas de bits.
   • Funciones de Rango: Conteo de entradas con una probabilidad mayor o igual a una entrada dada.
   • Clases de Complejidad: Definición de AvP (Tiempo Polinomial Promedio), distNP (NP distributivo) y AvDTime (Tiempo Determinista Promedio) utilizando la desigualdad de suma de rangos de RS93.
   • Reducciones: Formalización de reducciones distributivas con la condición de dominación para preservar la tratabilidad del caso promedio.
3. Incrustación de MLS (Fase 2): Incrustación profunda de la sintaxis y semántica de MLS y EMLS.
   • Sintaxis: Definiciones inductivas para términos (variables, unión, intersección, diferencia), relaciones (pertenencia, igualdad) y fórmulas.
   • Semántica: Una semántica de conjuntos ZF (ZFSet) axiomática con funciones de evaluación no computables.
   • Procedimiento de Decisión: Implementación de un procedimiento de decisión parcial basado en Ferro–Omodeo–Schwartz (1980). Los autores demuestran la corrección (soundness) y la completitud parcial para un fragmento libre de pertenencia, reconociendo que la completitud total (que requiere la sustitución del Paso 1 y la búsqueda de modelos del Paso 4 completa) permanece abierta.
4. Serialización y Pertenencia a NP (Fase 3): Definición de codificaciones binarias para fórmulas de MLS y demostración de que el problema de satisfacción (SatMLS) pertenece a NP mediante un verificador basado en certificados.
5. Dureza y Completitud (Fases 4–5):
   • Reducciones: Construcción de una reducción distributiva desde el Problema de Parada Acotado (NBH) hacia SatMLS. Debido a la complejidad de la traducción completa de TM a MLS, el mapa de reducción general se axiomatiza (nbhToMlsMap), mientras que la condición de dominación se verifica para una distribución de soporte específica.
   • Completitud: Demostración de que SatMLS es NP-promedio completo, condicionado al axioma de que todo problema distNP se reduce a NBH.
   • Corolarios de Dureza: Derivación de que SatMLS no está en AvP a menos que NEXP = EXP, utilizando la completitud establecida y la hipótesis del colapso.

Contribuciones Clave

• Formalización de TR1995-711: La primera formalización verificada por máquina de los resultados de complejidad del caso promedio para MLS y EMLS.
• Biblioteca de Lean 4 para AvCom: La creación de una biblioteca personalizada (AvgCaseMls) que implementa las clases de Reischuk–Schindelhauer, reducciones distributivas y distribuciones ordenables, llenando un vacío en el ecosistema Mathlib4 que actualmente se centra en la complejidad del peor de los casos.
• Verificación de Corrección y Completitud Parcial: Pruebas rigurosas de que el procedimiento de decisión implementado es correcto y completo para el fragmento específico de MLS sin literales de pertenencia.
• Transparencia Axiomática: Los autores documentan explícitamente las "bifurcaciones" (decisiones de diseño) y los axiomas (por ejemplo, el mapa de reducción general de TM a MLS, la hipótesis NEXP ≠ EXP) en DEFINITION_FORKS.md, distinguiendo entre teoremas probados y andamiaje necesario.

Resultados
El artículo reporta los siguientes resultados para su plan de fases:

• Fases 1A–1D (Definiciones de AvCom): Todas las definiciones compilan sin sorry. La formalización de entradas, distribuciones, funciones de rango y clases de complejidad coinciden con la literatura.
• Fases 2A–2D (MLS y Decisión): La sintaxis, semántica y el procedimiento de decisión parcial están verificados. La corrección se demuestra; la completitud se demuestra solo para el fragmento libre de pertenencia.
• Fases 3A–3B (Codificación): Se verifican los límites polinómicos en el tamaño de la codificación y la pertenencia a NP del verificador.
• Fases 4A–4C (Reducciones y Completitud): La reducción de NBH a SatMLS se verifica módulo el mapa de traducción general axiomatizado. La completitud de NP-promedio de SatMLS se demuestra módulo el axioma de que todos los problemas distNP se reducen a NBH.
• Fases 5A–5B (Dureza): La dureza condicional de no-AvP para SatMLS se deriva, supeditada al axioma NEXP ≠ EXP.

Significancia y Reivindicaciones
El artículo no pretende haber "resuelto" la complejidad del caso promedio de MLS de una manera que cambie la ingeniería de software práctica. En cambio, su significancia es histórica y metodológica:

1. Supervivencia de la Teoría: Evalúa si las afirmaciones matemáticas del informe de 1995 sobreviven al contacto con un asistente de pruebas moderno. Los resultados indican que la lógica central se mantiene, siempre que se acepten axiomas estructurales específicos (como la existencia de una reducción universal a NBH).
2. Clarificación de Supuestos: Al formalizar el trabajo, los autores exponen las dependencias precisas de la prueba original, como la dependencia de la hipótesis NEXP ≠ EXP para los resultados de dureza y la necesidad de propiedades de reducción distributiva específicas.
3. Fundamento para Trabajos Futuros: El artículo argumenta que, si bien la aplicación específica de AvCom a los procedimientos de decisión de MLS fue ampliamente abandonada en favor de los solucionadores SMT en la década de 1990, el marco formal desarrollado aquí proporciona una infraestructura necesaria para revisar el análisis del caso promedio en otros dominios, como el análisis suavizado o la criptografía post-cuántica, dentro del ecosistema Lean.

Los autores declaran explícitamente que no tratan sorry o los axiomas como un éxito; más bien, sirven como "andamiaje temporal" con tareas pendientes para eliminarlos en trabajos futuros. El artículo concluye que la visión del informe de 1995 de utilizar la complejidad del caso promedio para caracterizar la tratabilidad de los problemas de verificación sigue siendo matemáticamente coherente, incluso si el camino práctico hacia la implementación ha cambiado.