SMiLE: safe machine learning via embedded overapproximation

The 21st century has witnessed the resurgence of Artificial Intelligence, mostly driven by a shift from symbolic methods, dominant in the previous decades, to sub-symbolic techniques, fueled by the rapid growth of data availability and computational power. Neural Networks, in particular, have achieved unprecedented results in a variety of domains, such as computer vision and natural language processing. However, beyond the general excitement, the widespread adoption of AI has also raised concerns on its trustworthiness and reliability, as reflected in the emerging landscape of legal frameworks regulating this technology, pioneered by the EU AI Act. In safety-critical or socially sensitive scenarios, these regulations demand the satisfaction of specific properties, like robustness or fairness, to ensure AI alignment with human values and expectations. Even in non-critical settings, the satisfaction of formal requirements, like monotonicity or physical laws, may be desired to align these systems with the operational domain, hence to foster interpretability and usability. Unfortunately, while highly effective in terms of accuracy, purely data-driven AI remains inherently unable to formally guarantee the satisfaction of additional properties, due to its dependence on data, often scarce and noisy, and to the heuristic nature of the most common training algorithms. This has led, in recent years, to the development of methodologies to train property-aware systems, which however remain limited to specific properties and architectures, given the complexity of the problem. In this thesis, we take a step in this direction by introducing SMiLE (Safe Machine Learning via Embedded Overapproximation), a novel framework to enforce generic properties into arbitrary neural models, built upon the integration of sub-symbolic learning with symbolic reasoning. Across a wide spectrum of properties and learning tasks, we demonstrate the ability of SMiLE to match property-specific baselines in terms of accuracy, while providing advantages in terms of generality and guarantees.