LeanBET: Formally-verified surface area calculations in Lean

Este artículo presenta LeanBET, un pipeline de análisis de área superficial Brunauer–Emmett–Teller (BET) totalmente ejecutable y verificado formalmente, implementado en Lean 4, que garantiza la corrección matemática mientras logra un acuerdo numérico casi perfecto con la implementación de referencia BETSI establecida.

Lo esencial

Imagina que estás intentando medir el área superficial de una esponja, pero la esponja está hecha de agujeros invisibles y microscópicos. Los científicos utilizan un método llamado BET (nombrado en honor a tres científicos) para estimar esta área observando cómo se adhiere un gas a la esponja. Es una herramienta estándar en química, pero es un poco como intentar resolver un rompecabezas cuya imagen en la caja está borrosa.

Aquí está el problema: Para obtener la respuesta, los científicos deben seleccionar un rango específico de puntos de datos de su experimento y trazar una línea recta a través de ellos. El problema es que diferentes personas (o diferentes programas informáticos) podrían seleccionar rangos ligeramente distintos. Una persona podría decir: "Usemos los 10 puntos centrales", mientras que otra dice: "No, usa los 12 centrales". Esto conduce a respuestas diferentes para la misma esponja, causando confusión y una falta de confianza en los resultados.

Para solucionar esto, un equipo creó un programa informático llamado BETSI que verifica automáticamente cada rango posible de datos para encontrar el "mejor". Es como tener un robot que prueba cada combinación posible de piezas de rompecabezas para encontrar la que encaja perfectamente. Sin embargo, incluso los robots pueden tener errores o suposiciones ocultas que los hacen incorrectos de maneras sutiles.

Presentamos "LeanBET": El Robot Demostrado Matemáticamente

Los autores de este artículo construyeron una nueva versión de este robot utilizando una herramienta informática especial llamada Lean 4. Piensa en Lean 4 no solo como un lenguaje de programación, sino como un profesor de matemáticas súper estricto que nunca te permite cometer un error sin una demostración.

Así es como lo hicieron, utilizando algunas analogías simples:

1. El sistema de "Dos Cerebros" (Polimorfismo)

Por lo general, cuando escribes un programa informático, utilizas "números de punto flotante" (como los números en una calculadora). Estos son rápidos pero ligeramente desordenados porque las computadoras no pueden mantener una precisión infinita. Cuando realizas demostraciones matemáticas, utilizas "números reales" (precisión perfecta e infinita), pero no puedes ejecutarlos en una computadora.

Los autores resolvieron esto construyendo un robot cambiante.

• Cerebro A (La Demostración): Cuando necesitan demostrar que las matemáticas son correctas, el robot viste un traje de "Número Real". Realiza matemáticas perfectas y teóricas para demostrar que la lógica es impecable.
• Cerebro B (La Ejecución): Cuando necesitan ejecutar el programa con datos reales, el robot cambia a un traje de "Punto Flotante". Se ejecuta rápidamente en computadoras reales.
• La Magia: Dado que el robot está construido de la misma manera en ambos trajes, si el "Cerebro de Demostración" dice que la lógica es perfecta, el "Cerebro de Ejecución" está garantizado para seguir esas mismas reglas. Es como demostrar que el diseño de un puente es seguro con matemáticas perfectas y luego construir el puente real con acero real, sabiendo que el diseño se mantiene.

2. La "Receta vs. La Cocción" (Derivación como Especificación)

En la ciencia normal, escribes una receta (la teoría matemática) en papel, y luego un chef (el programador) intenta cocinarla en la cocina (el software). A veces el chef añade una pizca de sal aquí o allá, o malinterpreta un paso, y el plato sabe diferente a la receta.

En LeanBET, la receta y la cocción ocurren en la misma habitación. La "derivación matemática" (la receta) se escribe directamente en el código. La computadora verifica que el código es la receta. Si el código dice "añadir sal", la demostración matemática verifica que "añadir sal" es exactamente lo que la teoría exige. No hay brecha entre la teoría y la práctica.

3. El "Inspector Estricto" (Verificación Formal)

El artículo afirma que su programa no solo adivina la respuesta; lleva consigo un certificado de corrección.

• Software Estándar: Ejecutas el programa, te da un número y esperas que sea correcto.
• LeanBET: Ejecutas el programa, te da un número y, además, te entrega un documento matemáticamente probado que dice: "Verifiqué cada paso, seguí cada regla y este número es la única respuesta correcta basada en los datos que me diste".

¿Qué Encontraron?

Probaron su nuevo "Robot Demostrado Matemáticamente" contra el antiguo "Robot Estándar" (BETSI) utilizando 19 conjuntos de datos diferentes (como 19 esponjas diferentes).

• El Resultado: Para 18 de las 19 esponjas, los dos robots dieron exactamente la misma respuesta hasta el decimal más pequeño.
• El Único Fallo: Para una esponja (llamada UiO-66), hubo una diferencia diminuta (0,03%). Los autores admiten que aún no están seguros de por qué, pero es un error muy pequeño en comparación con el ruido habitual en los experimentos.

La Conclusión

Este artículo no trata sobre inventar una nueva forma de medir esponjas. Se trata de construir una versión confiable del método existente. Tomaron una herramienta científica estándar, la reconstruyeron dentro de un entorno de "demostración matemática" y mostraron que funciona tan bien como las herramientas antiguas, pero con la garantía de que no ha cometido ningún error lógico.

Es como actualizar de un mapa normal a un GPS que no solo te indica la ruta, sino que también demuestra, paso a paso, que la ruta es la más corta y segura posible, sin desvíos ocultos.

Resumen técnico

Resumen Técnico de "LeanBET: Cálculos de área superficial formalmente verificados en Lean"

Enunciado del Problema
El método Brunauer–Emmett–Teller (BET) es el marco estándar para estimar el área superficial específica a partir de isotermas de adsorción de gases. Sin embargo, la implementación práctica implica una subjetividad significativa, particularmente en la selección del rango de presión relativa para la regresión lineal. Aunque existen criterios de consistencia (criterios de Rouquerol) para filtrar regiones válidas, a menudo múltiples intervalos de presión satisfacen estas reglas, lo que conduce a variabilidad en los valores de área superficial reportados entre diferentes laboratorios e implementaciones de software. Esfuerzos previos para estandarizar este proceso, como el algoritmo de Identificación de Superficie BET (BETSI), dependen de software numérico de propósito general (Python). Aunque BETSI reduce la subjetividad mediante enumeración exhaustiva, sigue siendo un algoritmo numérico donde no se pueden descartar formalmente suposiciones ocultas de implementación o errores sutiles, dejando las garantías científicas del resultado sin verificar.

Metodología
Los autores presentan LeanBET, una tubería de análisis BET totalmente ejecutable y formalmente verificada implementada en el probador de teoremas Lean 4. El enfoque integra código ejecutable con pruebas matemáticas dentro de un único entorno, utilizando un diseño numérico polimórfico para cerrar la brecha entre la computación y la verificación:

• Polimorfismo: El algoritmo se escribe utilizando un tipo genérico α restringido por una clase de tipos BETLike. Esto permite que la misma estructura de código se instancie sobre números de punto flotante (Float) para una ejecución eficiente en datos experimentales reales y sobre números reales (Real) para pruebas matemáticas no computables.
• Derivación como Especificación: La derivación algebraica de la ecuación linealizada de BET no es meramente una motivación, sino que sirve como especificación formal. El código se construye para reflejar esta derivación, asegurando que la transformación ejecutable coincida con el modelo teórico.
• Flujo de Trabajo: La tubería realiza los siguientes pasos, cada uno acompañado de una prueba formal:
  1. Enumeración de Ventanas: Genera sistemáticamente todas las sublistas contiguas de la isoterma que contienen al menos dos puntos de datos.
  2. Linealización: Transforma los puntos de datos $(p, n)$ en la forma linealizada de BET $p/[n(1-p)]$.
  3. Regresión Lineal: Realiza una regresión de mínimos cuadrados en cada ventana para extraer la pendiente, la intersección y $R^2$.
  4. Verificaciones de Admisibilidad: Filtra candidatos basándose en los criterios de Rouquerol (monotonía de $n(1-p)$, positividad de los parámetros $C$ y $n_m$, y consistencia de la presión de monocapa).
  5. Selección de Rodilla: Resuelve empates entre ventanas válidas seleccionando aquella con el índice final más grande, rompiendo empates adicionales con el menor porcentaje de error.

Contribuciones Clave

1. Verificación Formal de la Tubería BETSI: El artículo proporciona la primera implementación verificada por máquina de todo el flujo de trabajo BETSI. Demuestra que el código ejecutable satisface las definiciones matemáticas de la teoría BET y los criterios de selección específicos.
2. Pruebas de Solidez y Completitud: Los autores prueban formalmente:
   • Teorema A.1 y A.2: La ecuación de la isoterma de BET se deriva de las suposiciones del modelo de capas, y el paso de linealización es algebraicamente correcto.
   • Teorema A.3: La enumeración de ventanas es sólida (solo se generan ventanas válidas) y completa (no se omite ninguna ventana contigua válida).
   • Teorema A.4 y A.5: El paso de regresión devuelve un minimizador verdadero de mínimos cuadrados, y los parámetros físicos extraídos ($n_m$, $C$) coinciden con sus definiciones teóricas.
   • Teorema A.6 y A.7: Las verificaciones de admisibilidad y la estrategia de selección basada en la rodilla satisfacen estrictamente sus especificaciones formales.
3. Implementación Polimórfica: El trabajo demuestra un patrón práctico para la computación científica en Lean, donde la corrección se prueba sobre números reales idealizados mientras la ejecución ocurre sobre aritmética de punto flotante, evitando la necesidad de lenguajes de verificación separados.

Resultados
La implementación de LeanBET se evaluó contra la implementación de referencia basada en Python de BETSI utilizando un conjunto de referencia de 19 isotermas de adsorción.

• Acuerdo Numérico: LeanBET coincide con la referencia BETSI hasta la precisión de máquina para 18 de las 19 isotermas.
• Discrepancia: Para el conjunto de datos UiO-66, se observó una desviación de aproximadamente 0.03% (0.36 m²/g). Los autores señalan que la causa de esta desviación específica permanece indeterminada, pero enfatizan que es significativamente menor que las incertidumbres experimentales típicas.
• Estado de Verificación: Todas las pruebas se compilaron con éxito, proporcionando garantías verificadas por máquina de que la salida del algoritmo se adhiere a las restricciones matemáticas especificadas.

Significado
El artículo afirma que LeanBET demuestra que se puede construir un flujo de trabajo práctico de computación científica en un probador de teoremas sin sacrificar el acuerdo numérico con las implementaciones de referencia establecidas. La contribución principal no es un nuevo algoritmo, sino una garantía formalmente verificada de corrección. Al vincular la tubería ejecutable con enunciados matemáticos verificados por máquina, el trabajo aborda la crisis de reproducibilidad en el análisis BET al eliminar la ambigüedad sobre la adherencia de la implementación a la teoría subyacente y a los criterios de selección. Los autores posicionan esto como un paso hacia la reducción de la brecha entre las derivaciones teóricas y las implementaciones de software en la ciencia de materiales.