Resumen
El interés que despierta en usuarios expertos y no-expertos la Inteligencia Artificial (IA) y la ciberseguridad han puesto de
manifiesto la necesidad de garantizar que las aplicaciones software que
manejamos diariamente cumplen con ciertos estándares de calidad como la seguridad, eficiencia y corrección, en definitiva
que carecen de fallos y vulnerabilidades. Estos aspectos son fundamentales para
que los humanos confíen en la forma en la que los sistemas software actuales manipulan datos y toman decisiones, con
repercusiones catastróficas cuando no se han diseñado, validado y/o verificado con
garantías suficientes.
El objetivo de este proyecto es el desarrollo de nuevos métodos de análisis y razonamiento basados en datos (fast) y
basados en métodos formales (low), con especial énfasis en la aplicabilidad de las
técnicas desarrolladas para afrontar los retos de corrección, seguridad, confianza, robustez, eficiencia y explicabilidad de
los sistemas software actuales (con mayor o menor grado de integración de técnicas
de IA). Tradicionalmente, estos dos tipos de razonamiento se han considerado ortogonales, es decir independientes. La
hipótesis de partida de este proyecto es que el razonamiento basado en datos y el
razonamiento formal no deben verse como dos paradigmas desconectados sino que ambos deben trabajar de forma
coordinada para poder garantizar que nuestros sistemas poseen las cualidades deseadas. Por ello, el presente proyecto
persigue investigar en diferentes tecnologías y formalismos matemáticos orientados a asegurar la confiabilidad de los
sistemas software y de IA, reuniendo un equipo consolidado con 30 años de trayectoria de investigación en estas áreas y
enfocándose hacia los siguientes objetivos: el desarrollo de aproximaciones basadas en datos, lógica y estadística para
razonar sobre propiedades de los sistemas de IA y sobre su evaluación, y el desarrollo de técnicas y herramientas software
para el análisis, verificación y depuración de sistemas heterogéneos complejos.