Reliable and Explainable AI in Trieste

Abstract

This paper summarizes the activity in the area of Reliable and Explainable AI carried out at the University of Trieste. The main topics are: monitoring and verification of stochastic systems, embeddings of logical formulae using Graph Neural Networks, formal methods for explainable AI, adversarial robustness, right to interpretability, ethical assessment of data sets and AI auditing. processes and rich specifications given in Signal Temporal Logic (STL). QPM derives prediction intervals that are The research activity in the area of Reliable and Explain- highly eficient to compute and with probabilistic guaranable Artificial Intelligence (AI) at the University of Trieste tees, in that the intervals cover with arbitrary probability is mainly concerned with the following topics: the STL robustness values relative to the stochastic evolution of the system. To do so, we take a machine-learning approach and leverage recent advances in conformal inference for quantile regression, thereby avoiding expensive Monte Carlo simulations at runtime to estimate the intervals. We also show how our monitors can be combined in a compositional manner to handle composite formulas, without retraining the predictors or sacrificing the guarantees.

-

1. Introduction • Monitoring and Verification of Stochastic Systems; • Embeddings of Logical Formulae; using Graph

Neural Networks; • Formal Methods for Explainable AI; • Adversarial Robustness; • Right to interpretability; • Ethical assessment of data sets; • AI auditing.

Parametric Verification. Parametric verification of

linear temporal properties for stochastic models requires In the following, a brief description of each of the afore- to compute the satisfaction probability of a certain mentioned problems is provided. property as a function of the parameters of the model. Smoothed model checking (smMC) [ 2 ] infers the satis2. Research Topics faction function over the entire parameter space from a limited set of observations obtained via simulation. 2.1. Monitoring and Verification of As observations are costly and noisy, smMC leverages Stochastic Systems the power of Bayesian learning providing accurate reconstructions with statistically sound quantification of Monitoring and parametric verification of stochastic sys- the uncertainty. We introduce Stochastic Variational tems are extremely challenging and computationally pro- Smoothed Model Checking (SV-smMC) [ 3 ], which exhibitive. We introduce eficient and reliable approaches ploits stochastic variational inference (SVI) to approxto approximate the two aforementioned problems. imate the posterior distribution of the smMC problem. The strength and flexibility of SVI, a stochastic gradientPredictive Monitoring. Predictive monitoring (PM) based optimization making inference easily parallelizdeals with predicting at runtime the satisfaction of a de- able and enabling GPU acceleration, make SV-smMC sired property from the current system’s state. PM meth- applicable both to Gaussian Processes (GP) and Bayesian ods need to be eficient to enable timely interventions Neural Networks (BNN). SV-smMC extends the smMC against predicted violations, while providing correctness framework by greatly improving scalability to higher guarantees. We introduce quantitative predictive mon- dimensionality of parameter spaces and larger training itoring (QPM) [ 1 ], a PM method to support stochastic datasets, thus overcoming the well-known limits of GP. Additionally, we combine the Bayesian quantification of Ital-IA 2023: 3rd National Conference on Artificial Intelligence, orga- uncertainty of SV-smMC with the Inductive Conformal ∗nCizoerdrebsypoCnINdiIn,Mgaauyt2h9o–r.31, 2023, Pisa, Italy Predictions framework to provide probabilistically ap© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License proximately correct point-specific error estimates, with Attribution 4.0 International (CC BY 4.0).

In an ongoing research endeavour, we are developing a

novel technique to improve adversarial robustness of neural image classifiers, broadly inspired by the process of memory recollection in humans and synergistically complementing the first-line approach of adversarial training. Specifically, we use the representation produced in selected layers of an adversarially-pretrained deep neural network in response to clean and perturbed inputs to condition an adversarial purification generative model, whose output is finally classified conventionally. Preliminary results – to be soon submitted to a major conference in the field – show significant improvement in robustness, as evaluated by [6] on diferent classifier architectures and standardised image classification datasets, with acceptable clean accuracy degradation.

In a further development, such approach is employed to identify the layers of a deep learning model mostly contributing to its adversarial vulnerability, with the goal of producing partially-Bayesian neural networks whose robustness-enhancing efects (as analysed in previous works, e.g. [7]) are focused where they are needed most, bounding the computational burden that follows.

Finally, a flipped perspective will guide the development of a new assessment framework for surrogate deep Bayesian models, exploiting the striking characteristic robustness properties of proper Bayesian neural networks, and how they are mirrored in surrogates.

2.5. Right to interpretability, ethical assessment of data sets, and AI auditing

statistical guarantees over the coverage of the predictive error.

2.2. Formal Methods for Explainable AI

Over the past few years, part of our research has fo

cused on exploring the application of formal methods to enhance the explainability of machine learning components. Cyber-Physical Systems (CPS) are at high risk of cyber-attacks. A possibility to detect anomalies is monitoring CPS sensor and actuator data using Signal Temporal Logic (STL) formulas. In [ 4 ], we propose a one-shot algorithm to learn a set of STL formulas from a data set of only regular behaviors. The algorithm learns an ensemble of STL formulas using a Grammar-Guided Genetic Programming (G3P) algorithm. The ensemble can then be used to detect anomalous behaviors. Testing on real-world datasets shows that the proposed one-shot algorithm provides efective detection performance.

In [ 5 ], we exploit ML for predicting the monitoring result of STL formulas. We introduce a similarity function (as a kernel function) on the semantics space of STL formulae. The approach avoids the need to convert formulae into vectors of numbers explicitly. The proposed method is demonstrated to efectively predict the satisfaction of STL formulae on stochastic processes, with high precision and computational eficiency. Furthermore, the efectiveness of the method is supported by a theoretically sound PAC guarantee.

2.3. Embeddings of Logical Formulae using Graph Neural Networks

Logic is the main formal language to perform automated reasoning, and it is further a human-interpretable lan- We study the legal, ethical and societal issues related guage, at least for small formulae. Learning and opti- to the use of AI system. In particular, taking into acmising logic requirements and rules has always been an count the systematic interpretation of the EU and interimportant problem in Artificial Intelligence. State of the national legal framework surrounding high-risk systems, art Machine Learning (ML) approaches are mostly based we research about the possibility that interpretability, as on gradient descent optimisation in continuous spaces, defined by Rudin, may be used as a standard in in applicawhile learning logic is framed in the discrete syntactic tions that may have a significant impact on citizens’ life space of formulae. Using continuous optimisation to (and even in other sensitive fields) and that black boxes learn logic properties is a challenging problem, requiring should only be used in situations where it is possible to to embed formulae in a continuous space in a meaningful make a decision by evaluating factors other than the AI way, i.e. preserving the semantics. Approaches like [ 5 ] output. The very possibility of expressing informed conare able to construct efective semantic-preserving em- sent and challenging the decision made on the basis of an beddings via kernel methods (for linear temporal logic), automated decision-making system might be excluded but the map they define is not invertible. We address by the opacity and complexity of black boxes. The lack this problem, learning how to invert such an embedding of technical interpretability may prevent the exercise leveraging deep architectures based on the Graph Varia- of many fundamental rights, such as the right to a fair tional Autoencoder framework, proposing a novel model trial, to self-determination, to non-discrimination, and specifically designed for this setting. more. We argue that a “right to technical interpretability” should, therefore, be theorized at the European level, being considered a fundamental right, and embedded in the AI Act proposal [8].

Within the EU AI Act proposal, major attention is signal temporal logic on stochastic processes, in: given to the assessment of data sets, that are required D. Fisman, G. Rosu (Eds.), Tools and Algorithms for to be unbiased. In our research, we are piloting new the Construction and Analysis of Systems - 28th techniques to assess data sets’ fairness and we aim at International Conference, TACAS 2022, Held as providing guidelines to comply with the new AI Act data Part of the European Joint Conferences on Theset compliance framework. ory and Practice of Software, ETAPS 2022, Mu

We are also exploring the field of AI Auditing in light of nich, Germany, April 2-7, 2022, Proceedings, Part the applicable EU and international laws and regulations, I, volume 13243 of Lecture Notes in Computer Scisuch as Convention 108 plus, GDPR, the Data Act, the AI ence, Springer, 2022, pp. 281–300. URL: https:// Act, the AI liability Directive, the Cyber-resilience Act, doi.org/10.1007/978-3-030-99524-9_15. doi:1 0 . 1 0 0 7 / and such. Our aim is to contribute to research on Trust- 9 7 8 - 3 - 0 3 0 - 9 9 5 2 4 - 9 \ _ 1 5 . worthy AI by exploring how to apply abstract principles [6] F. Croce, M. Andriushchenko, V. Sehwag, in practice, embedding them in the whole AI developing E. Debenedetti, N. Flammarion, M. Chiang, lifecycle. P. Mittal, M. Hein, RobustBench: a standardized

Finally, we research about the social issues related adversarial robustness benchmark, in: Thirty-fith to AI systems. Generative models such as Midjourney, Conference on Neural Information Processing Dall-e, Stable Difusion, and Chat GPT have been increas- Systems Datasets and Benchmarks Track, 2021. URL: ingly used to create new content on the basis of a user’s https://openreview.net/forum?id=SSKZPJCt7B. prompt, producing impressive images and texts; however, [7] G. Carbone, M. Wicker, L. Laurenti, A. Patane', when copyrighted materials and personal data are used L. Bortolussi, G. Sanguinetti, Robustness of bayesian to train the model, many ethical and legal issues arise. In neural networks to gradient-based attacks, in: fact, such large data set employed for the AI training are H. Larochelle, M. Ranzato, R. Hadsell, M. Balcan, collected by infringing a number of diferent laws and H. Lin (Eds.), Advances in Neural Information contracts, and, most importantly, without the consent Processing Systems, volume 33, Curran Assoof the interested parties, leading to detrimental efects ciates, Inc., 2020, pp. 15602–15613. URL: https: towards citizens and the society as a whole. //proceedings.neurips.cc/paper_files/paper/2020/ file/b3f61131b6eceeb2b14835fa648a48ff-Paper.pdf. [8] C. Gallese, The AI act proposal: a new right to References technical interpretability?, arXiv preprint (2023).

References

[1] L. Bortolussi , F. Cairoli , N. Paoletti , Conformal quantitative predictive monitoring of stl requirements for stochastic processes , in: 26th ACM International Conference on Hybrid Systems: Computation and Control , 2023 .

[2] L. Bortolussi , D. Milios , G. Sanguinetti, Smoothed model checking for uncertain continuous-time markov chains , Information and Computation 247 ( 2016 ) 235 - 253 .

[3] L. Bortolussi , F. Cairoli , G. Carbone, P. Pulcini , Stochastic variational smoothed model checking , arXiv preprint arXiv:2205.05398 ( 2022 ).

[4] P. Indri , A. Bartoli , E. Medvet , L. Nenzi, Oneshot learning of ensembles of temporal logic formulas for anomaly detection in cyber-physical systems , in: E. Medvet, G. L. Pappa , B. Xue (Eds.), Genetic Programming - 25th European Conference, EuroGP 2022 , Held as Part of EvoStar 2022 , Madrid, Spain, April 20-22 , 2022 , Proceedings, volume 13223 of Lecture Notes in Computer Science, Springer, 2022 , pp. 34 - 50 . URL: https:// doi.org/10.1007/978-3-031 -02056-8_3. doi:1 0 . 1 0 0 7 / 9 7 8 - 3 - 0 3 1 - 0 2 0 5 6 - 8 \ _ 3 .

[5] L. Bortolussi , G. M. Gallo , J. Kretínský , L. Nenzi , Learning model checking and the kernel trick for