Verificación formal de propiedades de seguridad en clasificador de salud

Recibes un modelo neuronal pequeño (red densa con dos capas ocultas) ya entrenado, junto a los rangos clínicamente válidos de cada signo vital. Aplica técnicas de verificación formal disponibles en herramientas como Marabou o ERAN: certifica o refuta monotonicidad (al aumentar la frecuencia cardiaca con el resto constante, la prioridad no debe disminuir), y robustez local (radio epsilon en norma infinito sobre cada signo vital). Reporta porcentaje de regiones certificadas y contraejemplos cuando los haya. Entrega un dossier interpretable para el comité.