Gradients intégrés renforcés
In Explain’AI - EGC workshop
Abstract
Les visualisations fournies par les techniques d’Intelligence Artificielle Explicable xAI) pour expliquer les réseaux de neurones convolutionnels (CNN’s) sont parfois difficile á interpréter. La richesse des motifs d’une image qui sont fournis en entrées (les pix l d’une image) entraîne des corrélations complexes entre les classes. Les techniques basées sur les gradients, telles que les gradients intégrés, mettent en évidence l’import nce de ces caractéristiques. Cependant, lorsqu’on les visualise sous forme d’images, on peut e retrouver avec un bruit excessif et donc une difficulté á interpréter les explic tions fournies. Nous proposons la méthode intitulée Gradients Intégrés Renforcés (RI ), une variation des gradients intégrés, qui vise á mettre en évidence les régions nfluentes des images dans la décision des réseaux. Cette méthode vise á réduire la sur ace des zones á analyser lors de la visualisation des résultats, générant ainsi moins e bruit apparent. Des expériences á base d’occlusions démontrent que les régions chois es par notre méthode jouent effectivement un rôle important en terme de classification.
Learning diversity attributes in multi-session recommendations
In 2022 IEEE international conference on big data (big data)
Abstract
Diversity in recommendation has been studied extensively. It has been shown that maximizing diversity subject to constrained relevance yields high user engagement over time. Existing work largely relies on setting some attributes that are used to craft an item similarity function and diversify results. In this paper, we examine the question of learning diversity attributes. That is particularly important when users receive recommendations over multiple sessions. We devise two main approaches to look for the best diversity attribute in each session: the first is a generalization of traditional diversity algorithms and the second is based on reinforcement learning. We implement both approaches and run extensive experiments on a semi-synthetic dataset. Our results demonstrate that learning diversity attributes yields a higher overall diversity than traditional diversity algorithms. We also find that training policies using reinforcement learning is more efficient in terms of response time, in particular for high dimensional data.
Trie-based output itemset sampling
In Proceedings of the 2022 IEEE international conference on big data (BigData’22)
Abstract
Pattern sampling algorithms produce interesting patterns with a probability proportional to a given utility measure. Utility changes need quick re-preprocessing when sampling patterns from large databases. In this context, existing sampling techniques require storing all data in memory, which is costly. To tackle these issues, this work enriches D. Knuth’s trie structure, avoiding 1) the need to access the database to sample since patterns are drawn directly from the enriched trie and 2) the necessity to reprocess the whole dataset when the utility changes. We define the trie of occurrences that our first algorithm TPSpace (Trie-based Pattern Space) uses to materialize all of the database patterns. Factorizing transaction prefixes compresses the transactional database. TPSampling (Trie-based Pattern Sampling), our second algorithm, draws patterns from a trie of occurrences under a length-based utility measure. Experiments show that TPSampling produces thousands of patterns in seconds.
Methods for explaining top-N recommendations through subgroup discovery
In Data Mining and Knowledge Discovery
Abstract
Explainable Artificial Intelligence (XAI) has received a lot of attention over the past decade, with the proposal of many methods explaining black box classifiers such as neural networks. Despite the ubiquity of recommender systems in the digital world, only few researchers have attempted to explain their functioning, whereas one major obstacle to their use is the problem of societal acceptability and trustworthiness. Indeed, recommender systems direct user choices to a large extent and their impact is important as they give access to only a small part of the range of items (e.g., products and/or services), as the submerged part of the iceberg. Consequently, they limit access to other resources. The potentially negative effects of these systems have been pointed out as phenomena like echo chambers and winner-take-all effects, because the internal logic of these systems is to likely enclose the consumer in a deja vu loop. Therefore, it is crucial to provide explanations of such recommender systems and to identify the user data that led the respective system to make the individual recommendations. This then makes it possible to evaluate recommender systems not only regarding their effectiveness (i.e., their capability to recommend an item that was actually chosen by the user), but also with respect to the diversity, relevance and timeliness of the active data used for the recommendation. In this paper, we propose a deep analysis of two state-of-the-art models learnt on four datasets based on the identification of the items or the sequences of items actively used by the models. Our proposed methods are based on subgroup discovery with different pattern languages (i.e., itemsets and sequences). Specifically, we provide interpretable explanations of the recommendations of the Top-N items, which are useful to compare different models. Ultimately, these can then be used to present simple and understandable patterns to explain the reasons behind a generated recommendation to the user.
Go2Pins: A framework for the LTL verification of Go programs (extended version)
In International Journal on Software Tools for Technology Transfer (STTT)
Abstract
We introduce Go2Pins, a tool that takes a program written in Go and links it with two model-checkers: LTSMin and Spot. Go2Pins is an effort to promote the integration of both formal verification and testing inside industrial-size projects. With this goal in mind, we introduce black-box transitions, an efficient and scalable technique for handling the Go runtime. This approach, inspired by hardware verification techniques, allows easy, automatic and efficient abstractions. Go2Pins also handles basic concurrent programs through the use of a dedicated scheduler. Moreover, in order to efficiently handle recursive programs, we introduce PSLRec, a formalism that augments PSL without changing the complexity of the underlying verification process.
Towards better heuristics for solving bounded model checking problems
In Constraints
Abstract
This paper presents a new way to improve the performance of the SAT-based bounded model checking problem on sequential and parallel procedures by exploiting relevant information identified through the characteristics of the original problem. This led us to design a new way of building interesting heuristics based on the structure of the underlying problem. The proposed methodology is generic and can be applied for any SAT problem. This paper compares the state-of-the-art approaches with two new heuristics for sequential procedures: Structure-based and Linear Programming heuristics. We extend these study and applied the above methodology on parallel approaches, especially to refine the sharing measure which shows promising results.
Tuning SAT solvers for LTL model checking
In Proceedings of the 29th asia-pacific software engineering conference (APSEC’22)
Abstract
Bounded model checking (BMC) aims at checking whether a model satisfies a property. Most of the existing SAT-based BMC approaches rely on generic strategies, which are supposed to work for any SAT problem. The key idea defended in this paper is to tune SAT solvers algorithm using: (1) a static classification based on the variables used to encode the BMC into a Boolean formula; (2) and use the hierarchy of Manna&Pnueli that classifies any property expressed through Linear-time Temporal Logic (LTL). By combining these two information with the classical Literal Block Distance (LBD) measure, we designed a new heuristic, well suited for solving BMC problems. In particular, our work identifies and exploits a new set of relevant (learnt) clauses. We experiment with these ideas by developing a tool dedicated for SAT-based LTL BMC solvers, called BSaLTic. Our experiments over a large database of BMC problems, show promising results. In particular, BSaLTic provides good performance on UNSAT problems. This work highlights the importance of considering the structure of the underlying problem in SAT procedures.
CosySEL: Improving SAT solving using local symmetries
In 24th international conference on verification, model checking, and abstract interpretation
Abstract
Many satisfiability problems exhibit symmetry properties. Thus, the development of symmetry exploitation techniques seems a natural way to try to improve the efficiency of solvers by preventing them from exploring isomorphic parts of the search space. These techniques can be classified into two categories: dynamic and static symmetry breaking. Static approaches have often appeared to be more effective than dynamic ones. But although these approaches can be considered as complementary, very few works have tried to combine them. In this paper, we present a new tool, CosySEL, that implements a composition of the static Effective Symmetry Breaking Predicates (esbp) technique with the dynamic Symmetric Explanation Learning (sel). esbp exploits symmetries to prune the search tree and sel uses symmetries to speed up the tree traversal. These two accelerations are complementary and their combination was made possible by the introduction of Local symmetries. We conduct our experiments on instances issued from the last ten sat competitions and the results show that our tool outperforms the existing tools on highly symmetrical problems.
Diversifying a parallel SAT solver with bayesian moment matching
In Symposium on dependable software engineering theories, tools and applications
Abstract
In this paper, we present a Bayesian Moment Matching (BMM) in-processing technique for Conflict-Driven Clause-Learning (CDCL) SAT solvers. BMM is a probabilistic algorithm which takes as input a Boolean formula in conjunctive normal form and a prior on a possible satisfying assignment, and outputs a posterior for a new assignment most likely to maximize the number of satisfied clauses. We invoke this BMM method, as an in-processing technique, with the goal of updating the polarity and branching activity scores. The key insight underpinning our method is that Bayesian reasoning is a powerful way to guide the CDCL search procedure away from fruitless parts of the search space of a satisfiable Boolean formula, and towards those regions that are likely to contain satisfying assignments.