SMiLE: Provably Enforcing Global Relational Properties in Neural Networks

TL;DR

SMiLE: Provably Enforcing Global Relational Properties in Neural Networks extends the Safe ML via Embedded overapproximation framework to enforce global relational properties with guarantees. It reengineers the training pipeline to handle relational predicates by integrating a generator–projector loop with an auxiliary overapproximation and a clipped embedding, enabling provable satisfaction of properties such as monotonicity, robustness, and fairness. Across monotonicity, robustness, and fairness benchmarks, the approach delivers zero-violation guarantees while remaining competitive with property-specific baselines in accuracy and runtime, and it provides a practical defense mechanism for safety-critical settings. By introducing a general, verification-friendly platform for enforcing expressive, globally quantified properties in neural networks, this work lays groundwork for regulatory-compliant and safer AI systems and points to future extensions to functional properties and scalable architectures like Transformers and Graph Neural Networks.

Abstract

Artificial Intelligence systems are increasingly deployed in settings where ensuring robustness, fairness, or domain-specific properties is essential for regulation compliance and alignment with human values. However, especially on Neural Networks, property enforcement is very challenging, and existing methods are limited to specific constraints or local properties (defined around datapoints), or fail to provide full guarantees. We tackle these limitations by extending SMiLE, a recently proposed enforcement framework for NNs, to support global relational properties (defined over the entire input space). The proposed approach scales well with model complexity, accommodates general properties and backbones, and provides full satisfaction guarantees. We evaluate SMiLE on monotonicity, global robustness, and individual fairness, on synthetic and real data, for regression and classification tasks. Our approach is competitive with property-specific baselines in terms of accuracy and runtime, and strictly superior in terms of generality and level of guarantees. Overall, our results emphasize the potential of the SMiLE framework as a platform for future research and applications.

Figures (5)

• Figure 1: A depiction of the SMiLE architecture.
• Figure 2: A SMiLE model $f$ with latent dimension $n=1$ and output function $g = \text{id}$, trained on the task $y = x^3$, and enforced with $|x' - x"| \leq 0.1 \implies |f(x') - f(x")| \leq 0.5\max_{x \in \mathcal{X}, \delta \leq 0.1} |x^3 - (x + \delta')^3|$, i.e., we want the model to be $0.5$ times more robust than the task itself. The subplots show the evolution of the model during its training.
• Figure 3: Accuracy monotonicity (left) and an example of monotonic estimator for the non-monotonic function given by $\alpha = 2$ and $\omega = 0.6$ (right).
• Figure 4: Accuracy and counterfactual variation on fairness.
• Figure 5: Counterfactual variation for different $\epsilon$ on Crime.