💻 computer science

Machine-Checked Arithmetic Bit Complexity of the Kannan-Bachem Smith Normal Form in Lean 4

Este artículo presenta una formalización en Lean 4 del algoritmo de la forma normal de Smith de Kannan-Bachem para matrices enteras no singulares, proporcionando pruebas de corrección verificadas por máquina y estableciendo cotas polinómicas fijas tanto para la complejidad de bits aritmética del cálculo como para el tamaño de su salida.

Autores originales: Junye Ji (University of Washington)

Publicado 2026-07-27

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Junye Ji (University of Washington)

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 eres un maestro archivista en una biblioteca donde cada libro es un rompecabezas gigante y complejo hecho de números. A veces, necesitas reorganizar las páginas de estos rompecabezas para encontrar un patrón oculto más simple debajo. Este es el mundo del álgebra lineal, una rama de las matemáticas que trata con cuadrículas de números (llamadas matrices) y cómo estas pueden ser transformadas. Piensa en una matriz como una hoja de cálculo de números enteros. Así como podrías ordenar una lista desordenada de nombres alfabéticamente para encontrar un patrón, los matemáticos intentan ordenar estas cuadrículas de números en una "Forma Normal de Smith": una versión diagonal súper limpia donde los números se vuelven cada vez más grandes a medida que avanzas en la línea, y cada número divide al siguiente perfectamente.

Pero aquí está el truco: aunque describir el orden de los números es fácil, realizar las matemáticas puede ser una pesadilla. A medida que barajas las filas y columnas para limpiarlas, los números dentro de ellas pueden explotar en tamaño, volviéndose tan enormes que bloquean tu computadora o tardan un millón de años en calcularse. Durante décadas, los matemáticos han sabido cómo ordenar estas cuadrículas (un método llamado algoritmo de Kannan–Bachem), pero necesitaban estar absolutamente seguros de que el proceso no se quedaría atrapado en un bucle infinito y que los números no crecerían fuera de control. Este artículo entra en ese vacío, no solo para decir "funciona", sino para construir una prueba digital e inquebrantable de que funciona, y para contar exactamente cuánta "energía computacional" requiere para hacerlo.

La Doble Verificación Digital

En este artículo, Junye Ji, de la Universidad de Washington, toma el algoritmo de Kannan–Bachem —una receta ingeniosa para ordenar matrices de enteros— y construye una prueba verificada por máquina de este utilizando una herramienta llamada Lean 4. Piensa en Lean 4 como un bibliotecario robótico súper estricto que se niega a aceptar una prueba matemática a menos que cada paso sea lógicamente sólido. Si intentas colar un "tal vez" o un "probablemente funcione", el robot cierra la puerta en tu cara. Ji no solo escribió el código; obligó al robot a verificar que el código siempre termina, nunca falla y produce la respuesta exacta en todo momento.

El objetivo era demostrar que, para cualquier cuadrícula cuadrada de enteros no nulos, este algoritmo puede transformarla en su forma diagonal limpia de "Forma Normal de Smith", mientras también realiza un seguimiento de los movimientos exactos realizados para llegar allí. El resultado no es solo una nota de "sí, funciona"; es un paquete completo y verificado que contiene la cuadrícula ordenada final, el mapa "hacia adelante" de cómo llegar allí y el mapa "hacia atrás" para volver al original. Es como tener un mapa del tesoro y un boleto de regreso, ambos verificados por un robot para asegurar que no te pierdas en el bosque de los números gigantes.

La Danza del "Pivote" y el Encogimiento de los Números

El corazón del algoritmo es una danza llamada estabilización. Imagina que estás tratando de organizar una habitación desordenada. Eliges un lugar específico en el suelo (el "pivote") e intentas hacer que todo lo demás en esa fila y columna desaparezca. A veces, las matemáticas se vuelven complicadas y no puedes hacer que todo desaparezca perfectamente. Cuando eso sucede, el algoritmo no se rinde; realiza un movimiento especial que reemplaza el pivote actual con un número más pequeño (un "divisor propio").

El artículo demuestra un hecho crucial: cada vez que este movimiento especial ocurre, el número de bits (el tamaño binario) del pivote se reduce estrictamente. Es como un juego en el que se te permite cambiar una piedra pesada por un guijarro más ligero, y nunca puedes cambiar un guijarro por una piedra más pesada. Debido a que no puedes seguir haciendo las cosas más pequeñas para siempre (eventualmente llegas a cero), el juego debe terminar. Los autores demostraron que esta "descenso" está garantizado, lo que significa que el algoritmo nunca se quedará atrapado en un bucle infinito.

Contando el Costo: El "Rastro"

Una de las partes más emocionantes de este trabajo es cómo contaron el costo. Usualmente, cuando decimos que un algoritmo es "rápido", podemos suponer que toma unos pocos segundos. Pero aquí, los autores querían saber el costo aritmético exacto en términos de operaciones binarias. Crearon un "rastro plano" (flat trace), que es como un recibo que enumera cada una de las diminutas operaciones matemáticas (suma, multiplicación, división) que la computadora realizó.

Demostraron que el costo total de este recibo crece a un ritmo polinómico. En palabras sencicas, esto significa que incluso si tu matriz de entrada se vuelve enorme, el tiempo que toma resolverla no explotará hacia el infinito; crecerá de una manera predecible y manejable. Incluso calcularon el "grado" específico de este crecimiento. El artículo revela que el costo está limitado por un polinomio con un grado de 2,150,687 (para el trabajo realizado) y 98,990 (para el tamaño de la salida).

Ahora, esos números parecen terriblemente grandes, pero los autores son muy cuidadosos al explicar lo que significan. Estos no son exponentes "ajustados" (como decir que toma exactamente $n^2$ pasos); son testigos conservadores. Piensa en ellos como un margen de seguridad. Si estuvieras construyendo un puente, podrías calcular que debe soportar 100 toneladas, pero lo diseñas para que soporte 1,000 toneladas solo para estar seguro. Estos números masivos son las "1,000 toneladas" del mundo de las matemáticas: garantías de que el algoritmo es seguro y eficiente, incluso si el rendimiento en el mundo real es mucho mejor.

¿Qué se dejó Fuera?

Es importante saber qué es lo que este artículo no hizo. Los autores fueron muy específicos sobre los límites de su prueba. Solo contaron las operaciones aritméticas (las matemáticas en sí). No contaron el tiempo que le toma a la computadora cargar los datos en la memoria, el tiempo que toma imprimir los resultados, ni la sobrecarga (overhead) del lenguaje de programación en sí. Tampoco demostraron que esta sea la forma más rápida posible de ordenar matrices; solo demostraron que esta forma específica es segura, está garantizada para terminar y no utiliza más recursos de los límites polinómicos calculados.

El Veredicto Final

Entonces, ¿cuál es la conclusión? Este artículo es un triunfo de la verificación formal. Toma una receta matemática compleja de décadas de antigüedad y la entrega a un robot para que verifique cada paso. El robot confirma que la receta siempre funciona, siempre termina y nunca crea números tan grandes que rompan el sistema. Proporciona un "certificado" de corrección que incluye la matriz ordenada, los mapas de transformación y una garantía matemáticamente probada sobre cuánto trabajo tomó llegar allí.

Para un adolescente curioso, esto es como ver a alguien construir un robot que no solo resuelve un Cubo de Rubik, sino que también escribe un contrato legal demostrando que nunca se quedará trabado, nunca romperá el cubo y lo hará dentro de un número específico de movimientos, sin importar qué tan mezclado comience el cubo. Convierte un "tal vez" en las matemáticas en un "definitivamente", verificado por el juez más estricto imaginable.

Resumen Técnico: Complejidad de Bits Aritmética Verificada por Máquina de la Forma Normal de Smith de Kannan–Bachem en Lean 4

Planteamiento del Problema
El artículo aborda la verificación formal del algoritmo de Kannan–Bachem para computar la Forma Normal de Smith (SNF, por sus siglas en inglés) de matrices enteras cuadradas no singulares. Si bien la existencia de la SNF es un resultado estándar en álgebra, el desafío algorítmico radica en controlar el crecimiento de los coeficientes intermedios. La eliminación gaussiana estándar o los métodos basados en el MCD pueden producir enteros con longitudes de bits exponenciales respecto al tamaño de la entrada. El procedimiento de Kannan–Bachem (1979) ofrece una solución de tiempo polinómico alternando fases de la forma normal de Hermite y reduciendo estrictamente el tamaño binario del pivote activo ante fallos de divisibilidad. El problema específico abordado aquí es la verificación formal de la corrección de este algoritmo, su terminación y su complejidad de bits aritmética dentro del asistente de pruebas Lean 4, incluyendo la generación de certificados explícitos (transformando las matrices y sus inversas) y un modelo de costo verificado.

Metodología
Los autores formalizan el algoritmo en Lean 4 utilizando la biblioteca mathlib. El enfoque distingue entre operaciones estructurales (indexación de matrices, manipulación de listas) y primitivas aritméticas (suma, multiplicación, división sobre enteros de signo-magnitud).

Ejecución Instrumentada: El algoritmo se implementa como una "ejecución instrumentada productora de valores". Cada operación aritmética emite un "rastro plano" (flat trace) de hojas designadas (por ejemplo, MCD, cociente/resto, comparaciones de magnitud). Estos rastros registran los operandos exactos y el costo de la operación, permitiendo que el costo total se pliegue en un único valor.
Códecs Autolimitados: Las matrices de entrada y salida se codifican mediante códecs de prefijo libre verificados. La salida consiste en cinco matrices: la forma de Smith $S$ , los multiplicadores unimodulares $U$ y $V$ , y sus inversas $U^{-1}$ y $V^{-1}$ . La longitud de la codificación se define como el número de bits en una representación de signo-magnitud, incluyendo los bits de enmarcado.
Estructura Recursiva:
- Preparación: Asegura que los menores principales principales sean no nulos utilizando el algoritmo de división sin determinante de Bird.
- Estabilización: Una función recursiva stabilizeFrom que limpia la primera columna y fila. Se basa en un argumento de "descenso del pivote": si una prueba de divisibilidad falla, el algoritmo encuentra un divisor propio, asegurando que el tamaño binario del pivote disminuya estrictamente.
- Recursión Externa: Una vez que la primera fila y columna se han limpiado y el pivote divide al bloque restante, el algoritmo recursa sobre la submatriz de $(n-1) \times (n-1)$ inferior derecha.
Análisis de Costo: El análisis de complejidad se desacopla del tiempo de ejecución de Lean. El teorema acota el "costo aritmético" (suma de los costos de las hojas primitivas) y la "longitud de codificación de la salida" (bits requeridos para serializar las cinco matrices).

Contribuciones Clave

Formalización de Kannan–Bachem: Una formalización completa del algoritmo de 1979, incluyendo la construcción de las matrices de transformación $U, V$ y sus inversas, lo que permite la verificación bidireccional de la equivalencia $UAV = S$.
Costo Aritmético Verificado: El artículo demuestra que el costo aritmético total y el tamaño de la salida están acotados por polinomios fijos del tamaño de la entrada. A diferencia de otras formalizaciones que pueden centrarse en la corrección algebraica o el conteo de operaciones, este trabajo rastrea explícitamente la complejidad de bits mediante un "cálculo de envolvente polinómica".
Testigos Explícitos: La formalización produce constantes concretas verificadas por máquina para los límites polinómicos. El grado del polinomio de costo se verifica como $d_c = 2,150,687$ y el grado de codificación de la salida es $d_o = 98,990$ . Los coeficientes son $C_c = 2^{d_c}$ y $C_o = 2^{d_o}$ . Los autores señalan que estos son testigos conservadores derivados de reglas de clausura genéricas, no exponentes ajustados.
Alineación de Rastros: Una prueba rigurosa de que la ejecución instrumentada (utilizada para el análisis de costo) es definicionalmente igual a la función matemática pura, asegurando que el análisis de costo se aplique directamente al comportamiento lógico del algoritmo.

Resultos
El teorema principal (Teorema 2.1) establece que para cualquier matriz entera no singular $n \times n$ $A$ :

El algoritmo termina y devuelve $S, U, U^{-1}, V, V^{-1}$ .
Las matrices devueltas satisfacen las ecuaciones de transformación directa e inversa ($UAV=S$, $U^{-1}SV^{-1}=A$ ) y las identidades inversas.
$S$ está en forma de Smith y es igual a una matriz de referencia canónica definida en la biblioteca.
El costo aritmético está acotado por $C_c (|encmat(A)| + 1)^{d_c}$ .
La longitud de codificación de la salida está acotada por $C_o (|encmat(A)| + 1)^{d_o}$ .

La terminación se demuestra mediante una relación bien fundada sobre el tamaño binario del pivote activo ($Nat.size(|pivot|)$), que disminuye estrictamente con cada descenso recursivo.

Significancia
El artículo reclama significancia al proporcionar una verificación unificada de un algoritmo de reducción de enteros ejecutable, sus certificados inversos y su costo aritmético dentro de un único marco formal. Mientras que desarrollos en Coq e Isabelle han probado la existencia de la SNF en entornos algebraicos más amplios, este trabajo se centra específicamente en el caso de matrices enteras cuadradas para verificar la eficiencia y corrección de una implementación ejecutable específica (Kannan–Bachem). La metodología se presenta como un precedente para verificar implementaciones de enteros eficientes y el análisis de tiempo polinómico, trazando un paralelo con el algoritmo LLL verificado en Isabelle/HOL. El trabajo demuestra que el análisis de la complejidad de bits verificado por máquina, incluyendo la generación de límites polinómicos explícitos con coeficientes concretos, es factible para algoritmos de álgebra lineal no triviales.

La Doble Verificación Digital

La Danza del "Pivote" y el Encogimiento de los Números

Contando el Costo: El "Rastro"

¿Qué se dejó Fuera?

El Veredicto Final

Más como este