Verificación formal de redes neuronales

Abstract

La verificación formal de redes neuronales es un área de creciente interés dentro de la inteligencia artificial, motivada por la necesidad de garantizar propiedades críticas como la robustez en modelos de aprendizaje profundo. Este trabajo aborda el problema de la verificación desde una perspectiva teórica, estableciendo su formulación matemática y analizando los desafíos inherentes a su resolución. Se estudian en profundidad dos enfoques principales: alcanzabilidad y optimización, explicando en detalle sus fundamentos, técnicas y algoritmos asociados. Además, se comparan distintos algoritmos dentro de cada enfoque en términos de completitud y complejidad algorítmica, identificando sus similitudes y limitaciones. Finalmente, se presentan herramientas de código abierto relevantes en el área, destacando su utilidad y desempeño.

Formal verification of neural networks is a field of growing interest within artificial intelligence, driven by the need to guarantee critical properties such like robustness in deep learning models. This work approaches the verification problem from a theoretical perspective, establishing its mathematical formulation and analyzing the challenges inherent to its resolution. Two main approaches, reachability and optimization, are studied in depth, explaining in detail their foundations, techniques, and associated algorithms. In addition, different algorithms within each approach are compared in terms of completeness and complexity, identifying their similarities and limitations. Finally, relevant open-source tools in the area are presented, highlighting their usefulness and performance.