Orateur : Joao Marques-Silva (website, scholar), IRIT ANITI
Titre : Logic-Based Explainability in Machine Learning
Résumé : The forecast applications of machine learning (ML) in high-risk and safety-critical applications hinge on systems that are robust in their operation and that can be trusted. This talk gives a broad overview of ongoing efforts in applying logic-enabled automated reasoning tools for explaining black-box ML models. The talk details the computation of rigorous explanations for the predictions black-box models, and illustrates how these serve to assess the quality of widely used heuristic explanation approaches. The talk also overviews properties relating different kinds of rigorous explanations. Finally, the talk briefly overviews a number of emerging topics of research in formal explainability.
Orateur : Stéphane Grandcolas, LIS
Titre : WRM: a metaheuristic algorithm for ship weather routing
Résumé : In recent years ship weather routing has attracted a lot of interest, resulting of the significant increase of transport by sea. The primary objective is to limit the costs, but other parameters, such as time, safety or preservation of the environment, can also be considered. These aspects and the fact that the domains of the variables are continuous make the problem difficult to solve. We propose a metaheuristic algorithm called WRM (for Weather Routing Metaheuristic) that aims at finding routes of minimal cost within a given time period. The cost can be the fuel oil consumption, the amount of greenhouse gas emissions or any other measure. It depends on the weather conditions that are expected and on the speed of the vessel, which can vary all along the route. Constraints forbidding or penalizing the navigation in specific conditions or in some given areas can be easily enforced. The method is simple and general. It converges progressively towards the most promising regions, generating new potential way points which are not derived from a predefined mesh. Simulating the fuel oil consumption of the vessel according to the expected wind and waves conditions, we have performed experimentations that show the efficiency of the approach.
Orateur : Matthieu Py, LIS
Titre : Production de certificats pour le problème Max-SAT
Résumé : Dans cet exposé, on s’intéresse à la production de certificats pour le problème de satisfiabilité maximum. Le problème de satisfiabilité maximum, ou problème Max-SAT, consiste, étant donnée une formule propositionnelle sous forme normale conjonctive, à trouver comment affecter à chaque variable de la formule une valeur booléenne afin de satisfaire le plus de clauses possible, ou, de manière équivalente, de falsifier le moins de clauses possible. Les travaux présentés portent sur la génération de certificats d’optimalité pour le problème Max-SAT, c’est à dire, non seulement être en capacité de donner le nombre minimum de clauses devant être falsifiées, mais produire en plus une preuve d’optimalité de la valeur trouvée.
Pour produire de tels certificats, on s’intéresse d’abord à une première problématique qui est l’adaptation des réfutations par résolution en max-réfutations. Une réfutation par résolution est un certificat d’insatisfiabilité d’une formule, autrement dit c’est une preuve qu’un ensemble de clauses ne peut être satisfait. Ces réfutations par résolution sont très utiles dans le cadre du problème SAT, mais sont inutilisables dans le cadre du problème Max-SAT. En effet, si exhiber une réfutation par résolution d’une formule permet bien de démontrer qu’il est toujours nécessaire de falsifier au moins une clause de la formule, exhiber dix réfutations par résolution d’une même formule ne permet pas de démontrer qu’il est toujours nécessaire de falsifier au moins dix clauses. Il est donc nécessaire d’adapter ces réfutations par résolution pour qu’elles soient utilisables dans le cadre de Max-SAT. Ces réfutations par résolution, adaptées pour Max-SAT et appelées max-réfutations, formeront un maillon essentiel des certificats pour le problème Max-SAT.
Grâce aux travaux portant sur l’adaptation des réfutations par résolution en max-réfutation, on montrera comment générer des certificats pour le problème Max-SAT. Pour cela, on fait itérativement appel à un oracle SAT pour calculer une réfutation par résolution de la formule courante, puis on transforme cette réfutation en max-réfutation et l’applique sur la formule courante. Ce processus est répété jusqu’à ce que la formule courante devienne satisfiable, et l’ensemble des max-réfutations calculées plus l’interprétation permettant de satisfaire la dernière formule calculée forment un certificat pour le problème Max-SAT. Ainsi, pour démontrer que l’optimum Max-SAT d’une formule est de satisfaire 40 clauses d’une formule possédant 50 clauses, on pourra calculer et exhiber 10 max-réfutations (afin de démontrer qu’il est nécessaire de falsifier au moins 10 clauses) et exhiber une interprétation satisfaisant la formule obtenue après application des 10 max-réfutations (afin de démontrer qu’il est possible de falsifier exactement 10 clauses).