Embedding Formal Worst-Case Latency Proofs and Memory-Safety Certificates into the snn-mlir MLIR Lowering Pipeline for IEC 62304-Compliant Edge Deployment of Spiking Neural Networks

Resumen Técnico: Incorporación de Pruebas de Latencia de Peor Caso Formales y Certificados de Seguridad de Memoria en el Pipeline de Reducción de snn-mlir MLIR

1. Declaración del Problema

Las Redes Neuronales de Picos Neuromórficas (SNN, por sus siglas en inglés) ofrecen una computación temporal eficiente energéticamente, adecuada para dispositivos médicos de borde, como los neuroestimuladores de bucle cerrado para la epilepsia. Sin embargo, su despliegue en entornos de seguridad crítica está actualmente bloqueado por una "brecha de herramientas". Aunque los marcos de trabajo existentes como snnTorch y los compiladores como snn-mlir pueden generar código C11 válido a partir de modelos entrenados, no logran producir evidencia verificable por máquina de que las funciones de inferencia compiladas satisfagan los límites de Tiempo de Ejecución de Peor Caso (WCET) o los requisitos de documentación de la certificación IEC 62304 Clase B.

Los compiladores de SNN actuales no integran métodos de verificación formal (como la Técnica de Enumeración de Caminos Implícitos, o IPET) para demostrar que el código cumple con las estrictas restricciones de latencia requeridas para el hardware implantable. Sin estas pruebas, las SNN no pueden certificarse para uso médico bajo estándares como el IEC 62304, que exige la trazabilidad desde los requisitos hasta la implementación verificada.

2. Metodología

Los autores proponen un paso de análisis de post-procesamiento que opera sobre la Representación Intermedia Multinivel (MLIR) emitida por el compilador snn-mlir. El pipeline consta de las siguientes etapas:

• Entrenamiento y Exportación del Modelo: Se entrenó una SNN de tres capas de alimentación hacia adelante de tipo Leaky Integrate-and-Fire (LIF) utilizando snnTorch con el conjunto de datos de EEG de la escala CHB-MIT (pacientes chb01 y chb02) para la detección de convulsiones. El modelo se exportó al formato de Representación Intermedia Neuromórfica (NIR).
• Compilación: El grafo NIR fue reducido a código C11 utilizando snn-mlir (commit 89b65e0). El código se compiló con GCC al nivel de optimización -O0 para asegurar una correspondencia estable y no optimizada entre la estructura de la fuente y las instrucciones emitidas, lo cual es necesario para una extracción precisa del Grafo de Flujo de Control (CFG).
• Análisis de WCET Formal (IPET): Un paso de post-procesamiento en Python (certify.py) extrae el CFG de cada capa LIF compilada. Formula un Programa Lineal Entero (ILP) de la Técnica de Enumeración de Caminos Implícitos (IPET) parametrizado por el tiempo de instrucción del microcontrolador ARM Cortex-M4F. El ILP maximiza el flujo de ciclos sujeto a restricciones de conservación de flujo y límites de retroalimentación de bucle.
• Anotación y Certificación: El paso anota el código C11 resultante con comentarios @wcet_bound y genera estuches de obligación de prueba de Lean4. Estos estuches declaran formalmente los límites de WCET como obligaciones de prueba, vinculando la salida del compilador con un asistente de pruebas.
• Mapeo de IEC 62304: Los artefactos generados (documentación del CFG, código fuente anotado, registros de prueba) se mapean a cláusulas específicas de la norma IEC 62304 Clase B (Proceso de Desarrollo de Software) para demostrar el cumplimiento con los requisitos de documentación y trazabilidad.

3. Contribuciones Clave

El artículo reclama cuatro contribuciones primarias:

1. Formulación de WCET para SNN: Los autores formulan el análisis de WCET para las funciones de inferencia LIF compiladas con snn-mlir como un ILP de IPET parametrizado por el tiempo de instrucción de ARM Cortex-M4F.
2. Paso de Post-procesamiento Automatizado: Implementación de un paso en Python que automatiza la extracción de CFG, la resolución de ILP, la anotación de WCET y la generación de estuches de Lean4 sin requerir modificaciones al código base del compilador en C++.
3. Validación de Extremo a Extremo: Validación del pipeline en una tarea de detección de convulsiones clínicamente relevante, demostrando que la inferencia C11 compilada coincide con el modelo de referencia en Python mientras se adhiere a las restricciones de análisis estático.
4. Paquete de Artefactos de IEC 62304: Provisión de un paquete de artefactos mapeados que cubren categorías de documentación del proceso de desarrollo IEC 62304 Clase B, representando una vía desde un modelo entrenado hasta la documentación reglamentaria.

4. Resultados

• Rendimiento del Modelo: La SNN entrenada logró una precisión balanceada del 78.8% (IC 95%: 74.5–83.2%) en el conjunto de prueba no visto, superando el umbral de credibilidad del 75%. La sensibilidad fue del 68.6% y la especificidad del 89.1%.
• Corrección de la Compilación: La función de inferencia C11 compilada mostró una divergencia insignificante respecto a la referencia en Python de snnTorch (divergencia máxima $\approx 1 \times 10^{-5}$), atribuida a diferencias de precisión de punto flotante en lugar de un sesgo sistemático.
• Límites de WCET:
  • El análisis IPET produjo un límite uniforme por capa de 5,634 ciclos.
  • El límite de la red certificada para la red de tres capas es de 16,902 ciclos (100.6 µs a 168 MHz).
  • Este límite proporciona un margen de 497× por debajo del plazo de tiempo real estricto de 50 ms para la neuroestimulación.
  • El tiempo de ejecución medido fue de 8,627 ciclos (51.4 µs), muy dentro del límite certificado.
• Cobertura de Artefactos: El paquete generado cubre totalmente cinco de las ocho categorías de proceso de desarrollo de software de IEC 62304 §5.x y cubre parcialmente otras dos, resultando en una puntuación de 6.0/8.0 para el proceso de desarrollo. Cubre totalmente la gestión de configuración (§8.0) pero señala la falta de un análisis formal de gestión de riesgos de software (§7.1).

5. Significado y Reivindicaciones

Los autores posicionan este trabajo como la primera vía documentada públicamente desde un modelo snnTorch entrenado hasta un paquete de documentación IEC 62304 Clase B para una función de inferencia de SNN.

• Novedad: El trabajo cierra la brecha entre las salidas de compiladores neuromórficos y los estándares de verificación formal, aplicando específicamente IPET a las SNN y generando obligaciones de prueba de Lean4.
• Modestia y Limitaciones: Los autores declaran explícitamente que los estuches de Lean4 son especificaciones, no pruebas verificadas; la descarga de estas pruebas se deja para futuros colaboradores. Los límites de WCET se derivan de compilaciones no optimizadas (-O0) y se aplican como una aproximación de arquitectura cruzada (host x86_64 con modelos de tiempo ARM) en lugar de realizar una compilación cruzada nativa de ARM. El análisis de gestión de riesgos (§7.1) no se realizó, y el estudio está limitado a dos pacientes del conjunto de datos CHB-MIT.
• Conclusión: El pipeline establece una base reproducible para trabajos futuros hacia el despliegue de borde neuromórfico totalmente verificado, demostrando que las SNN pueden compilarse en código C11 con límites de latencia verificables por máquina, adecuados para la certificación de dispositivos médicos de seguridad crítica.