Modern AI based on machine learning and deep learning is obtaining amazing results, yet the learned models are highly complex and are used as black boxes. The need of understanding decisions of models that may impact our lives has pushed EU to enforce the right of explanation, boosting research in eXplainable AI (XAI). At the same time, the problem of combining the “fast”, black-box power of deep leaning with more “slow” and traditional reasoning abilities of symbolic AI is getting more and more attention, giving rise to the new field of neuro-symbolic AI.
In the rapidly evolving world of explainable AI, we are particularly interested in robust explanation methods for supervised predictors working on tabular data. We are exploring KPI and metrics to assess trustability, ensembles of explanation techniques, and Bayesian approaches for explainability. As for neuro-symbolic AI, we are interested in exploring how much latent continuous embeddings, which are the main tool in vision and language processing, can be useful in the context of logic, and how they can be combined with classic symbolic reasoning techniques. We are defining embeddings of logical formulae in continuous latent spaces, to perform more effectively downstream learning tasks, leveraging both the old good kernel methods and also Graph Neural Network (GNN). GNN-based variational autoencoders, in particular, provide invertible embeddings that can be used for explainability. We are further exploring neuro-symbolic logics, like Logic Tensor Networks, to constrain generative models. Finally, we are also interested in the use of GNN for reasoning tasks (e.g. model counting for propositional logic).
Keywords: robust explanations, ensembles of explanations, kernel-based encoding of logic formulae, learning temporal logical rules, GNN-based encoding and decoding of logic formulae, GNN for model counting.
In the following, there is a reasoned bibliography, in which each class of contributions is briefly described and the relevant bibliography is cited.
Kernel-based methods for temporal logic
Model checking, which asks to predict the probability that a systems M satisfies a given property, typically requires to know M or the possibility to execute it. In this work model checking is learned with the kernel trick from just a labeled dataset of model checking pairs, drastically reducing information and computational demands. Statistical bounds on the quality of the solution are also provided.
- L. Bortolussi, G. M. Gallo, J. Kretínský, L. Nenzi, Learning model checking and the kernel trick for signal temporal logic on stochastic processes, in: TACAS 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, Springer, 2022, pp. 281–300. Link
Graph Neural Networks for propositional model counting
Graph Neural Networks have been recently leveraged to solve several logical reasoning tasks. Nevertheless, counting problems such as propositional model counting are still mostly approached with traditional solvers. Here we tackle this gap by presenting an architecture which combines GNNs and the Belief Propagation algorithm.
- G. Saveri and L. Bortolussi, Graph Neural Networks for Propositional Model Counting, ESANN 2022. Link
Learning temporal logic properties
Kernel-based methods like the one described above are very effective in computing semantic similarity between temporal formulae in a continuous space, however they cannot be inverted. Finding an invertible embedding of formulae would indeed be crucial to perform requirement mining and optimization in a continuous space, allowing then to go back to discrete temporal formulae.
- G. Saveri and L. Bortolussi, Towards Invertible Semantic-Preserving Embeddings of Logical Formulae, under review.
Neuro-symbolic constrained generative models
Generative models are becoming more powerful and expressive. However, current conditional generation relies either on the specific training of a conditional model or classifier guidance. In this study, we explore efficient and flexible methods for imposing arbitrary logical constraints on generated samples by pre-trained generative models. This approach is applicable across various domains, including tabular data, images, and time series.
- Scassola, Davide, et al. Conditioning Score-Based Generative Models by Neuro-Symbolic Constraints” arXiv preprint arXiv:2308.16534 (2023).
XAI for insurance and asset management
Usage of XAI techniques has been pushed forward by recent EU regulations on the trustability and fairness of black-box models. To be trustworthy, it is necessary to guarantee that a XAI technique is also robust (both to random and adversarial attacks): we propose an ensemble approach to leverage information on the trustability of an explanation, applied to tabular data coming from the insurance and asset management fields.