In this work, we present the problem of algorithmic recourse for the setting of binary allocation problems. In this setting, the optimal allocation does not depend only on the prediction model and the individual’s features, but also on the current available resources, utility function used by the decision maker and other individuals currently applying for the resource. We provide a method for generating counterfactual explanations under separable utilities that are monotonically increasing with prediction scores. Here, we assume that we can translate probabilities of “success” together with some other parameters into utility, such that the problem can be phrased as a knapsack problem and solved by known allocation policies: optimal 0–1 knapsack and greedy. We use the two policies respectively in the use cases of loans and college admissions. Moreover, we address the problem of recourse invalidation due to changes in allocation variables, under an unchanged prediction model, by presenting a method for robust recourse under variables’ distributions. Finally, we empirically compare our method with perturbation-robust recourse and show that our method can provide higher validity at a lower cost.

A software product line (SPL) is a family of closely related software systems which capitalizes on the variability and reusability of the software products and can be formalised by a feature model. Feature model evolution plans (FMEP) capture the current SPL as well as the planned evolution of the SPL to ensure successful long-term development. As business requirements often change, FMEPs should support intermediate update. This modification may cause paradoxes in an FMEP, e.g., a node left without a parent, making the plan impossible to realise. Current tools exist to validate FMEPs, but require analysing the entire plan even when a modification affects only small parts of it. Hence, there is a need for a method that detects such paradoxes in a more efficient way. In this paper, we present an interval based feature model (IBFM), a representation for FMEPs, that allows local reasoning to validates only the parts of the plan affected by changes. We define operations for updating the FMEPs and the preconditions under which they preserve soundness, i.e., absence of paradoxes, and show the correctness of the method.

Counterfactual explanation (CE) is a popular post hoc interpretability approach that explains how to obtain an alternative outcome from a machine learning model by specifying minimum changes in the input. In line with this context, when the model’s inputs represent actual individuals, actionable recourse (AR) refers to a personalized CE that prescribes feasible changes according to an individual’s preferences. Hence, the quality of ARs highly depends on the soundness of underlying CEs and the proper incorporation of user preferences. To generate sound CEs, several data-level properties, such as proximity and connectedness, should be taken into account. Meanwhile, personalizing explanations demands fulfilling important user-level requirements, like coherency and actionability. The main obstacles to inclusive consideration of the stated properties are their associated modeling and computational complexity as well as the lack of a systematic approach for making a rigorous trade-off between them based on their importance. This paper introduces CARE, an explanation framework that addresses these challenges by formulating the properties as intuitive and computationally efficient objective functions, organized in a modular hierarchy and optimized using a multi-objective optimization algorithm. The devised modular hierarchy enables the arbitration and aggregation of various properties as well as the generation of CEs and AR by choice. CARE involves individuals through a flexible language for defining preferences, facilitates their choice by recommending multiple ARs, and guides their action steps toward their desired outcome. CARE is a model-agnostic approach for explaining any multi-class classification and regression model in mixed-feature tabular settings. We demonstrate the efficacy of our framework through several validation and benchmark experiments on standard data sets and black box models.

Local surrogate explanation methods are a popular class of post-hoc interpretability approaches that explain the rationale of machine learning models in the locality of every particular instance. Fidelity, which refers to the accuracy of explanation methods in imitating the actual behavior of a model, is highly affected by their strategy for identifying the locality of instances. To find the locality of an instance, we need to calculate the distance between the instance and perturbed data points concerning categorical and numerical features. While the distance of numerical features can be measured precisely, the existing works usually adopt a coarse-grained or imprecise approach for comparing categorical features. This is especially problematic in the categorical data setting, where defining a representative locality demands fine-grained semantic similarity information between categories. In this paper, we propose a locality generation approach for categorical data classifiers that makes no assumption about domain knowledge and infers categorical similarities by relying on the model's explanations. Further, we devise a multi-centered sampling approach based on the derived similarity information that, compared to the conventional instance-centered technique, captures the local behavior of the model more effectively. Moreover, we develop a knowledge-based locality generation approach based on knowledge graphs to benchmark our explanation-based method against a scenario where the similarity information is provided by a domain expert. The experiments conducted on various data sets demonstrate the efficacy of our approach in generating faithful explanations.

The research around developing methods for debugging and refining Machine Learning (ML) models is still in its infancy. We believe employing tailored tools in the development process can help developers in creating more trustworthy and reliable models. This is particularly essential for creating black-box models such as deep neural networks and random forests, as their opaque decision-making and complex structure prevent detailed investigations. Although many explanation techniques provide interpretability in terms of predictive features for a mispredicted instance, it would be beneficial for a developer to find a partition of the training data that significantly influences the anomaly. Such responsible partitions can be subjected to data visualization and data engineering in the development phase to improve the model's accuracy. In this paper, we propose a systematic debugging framework for the development of ML models that guides the data engineering process using the model's decision boundary. Our approach finds the influential neighborhood of anomalous data points using observation-level feature importance and explains them via a novel quasi-global explanation technique. It is also equipped with a robust global explanation approach to reveal general trends and expose potential biases in the neighborhoods. We demonstrate the efficacy of the devised framework through several experiments on standard data sets and black-box models and propose various guidelines on how the framework's components can be practically useful from a developer's perspective.

Recent studies have revealed that Machine Learning (ML) models are vulnerable to adversarial perturbations. Such perturbations can be intentionally or accidentally added to the original inputs, evading the classifier's behavior to misclassify the crafted samples. A widely-used solution is to retrain the model using data points generated by various attack strategies. However, this creates a classifier robust to some particular evasions and can not defend unknown or universal perturbations. Counterfactual explanations are a specific class of post-hoc explanation methods that provide minimal modification to the input features in order to obtain a particular outcome from the model. In addition to the resemblance of counterfactual explanations to the universal perturbations, the possibility of generating instances from specific classes makes such approaches suitable for analyzing and improving the model's robustness. Rather than explaining the model's decisions in the deployment phase, we utilize the distance information obtained from counterfactuals and propose novel metrics to analyze the robustness of tabular classifiers. Further, we introduce a decision boundary modification approach using customized counterfactual data points to improve the robustness of the models without compromising their accuracy. Our framework addresses the robustness of black-box classifiers in the tabular setting, which is considered an under-explored research area. Through several experiments and evaluations, we demonstrate the efficacy of our approach in analyzing and improving the robustness of black-box tabular classifiers.

Defining a representative locality is an urgent challenge in perturbation-based explanation methods, which influences the fidelity and soundness of explanations. We address this issue by proposing a robust and intuitive approach for EXPLaining black-box classifiers using Adaptive Neighborhood generation (EXPLAN). EXPLAN is a module-based algorithm consisted of dense data generation, representative data selection, data balancing, and rule-based interpretable model. It takes into account the adjacency information derived from the black-box decision function and the structure of the data for creating a representative neighborhood for the instance being explained. As a local model-agnostic explanation method, EXPLAN generates explanations in the form of logical rules that are highly interpretable and well-suited for qualitative analysis of the model's behavior. We discuss fidelity-interpretability trade-offs and demonstrate the performance of the proposed algorithm by a comprehensive comparison with state-of-the-art explanation methods LIME, LORE, and Anchor. The conducted experiments on real-world data sets show our method achieves solid empirical results in terms of fidelity, precision, and stability of explanations.

A software product line (SPL) enables large-scale reuse in a family of related software systems through configurable features. SPLs represent a long-term investment so that their ongoing evolution becomes paramount and requires careful planning. While existing approaches enable to create an evolution plan for an SPL on feature-model (FM) level, they assume the plan to be rigid and do not support retroactive changes. In this paper, we present a method that enables to create and retroactively adapt an FM evolution plan while preventing undesired impacts on its structural and logical consistency. This method is founded in structural operational semantics and linear temporal logic. We implement our method using rewriting logic, integrate it within an FM tool suite and perform an evaluation using a collection of existing FM evolution scenarios.

Streams of data are produced today at an unprecedented scale. Efficient and stable processing of these streams requires a careful interplay between the parameters of the streaming application and of the underlying stream processing framework. Today, finding these parameters happens by trial and error on the complex, deployed framework. This paper shows that high-level models can help to determine these parameters by predicting and comparing the performance of streaming applications running on stream processing frameworks with different configurations. To demonstrate this approach, this paper considers Spark Streaming, a widely used framework to leverage data streams on the fly and provide real-time stream processing. Technically, we develop a configurable and executable model to simulate both the streaming applications and the underlying Spark stream processing framework. Furthermore, we model the deployment of Spark Streaming on Apache YARN, which is a popular open-source distributed software framework for big data processing. We show that the developed model provides a satisfactory accuracy for predicting performance by means of empirical validation.

Data sampling has an important role in the majority of local explanation methods. Generating neighborhood samples using either the Gaussian distribution or the distribution of training data is a widely-used procedure in the tabular data case. Generally, this approach has several weaknesses: first, it produces a uniform data which may not represent the actual distribution of samples; second, disregarding the interaction between features tends to create unlikely samples; and third, it may fail to define a compact and diverse locality for the sample being explained. In this paper, we propose a sampling methodology based on observation-level feature importance to derive more meaningful perturbed samples. To evaluate the efficiency of the proposed approach we applied it to the LIME explanation method. The conducted experiments demonstrate considerable improvements in terms of fidelity and explainability.

In the oil and gas industry, during exploration prospect assessment, explorationists rely on ad hoc manual work practices and tools for developing and communicating multiple hypothetical geological scenarios of the prospect. This leaves them with little efficient means to make the fullest use of state of the art digital technologies to communicate and systematically compare and assess different hypothetical geological scenarios before deciding which scenario to pursue. In this paper, we present a formal framework for geological multi-scenario reasoning, a novel tool-based method for geologically oriented subsurface evaluation. The methodology applies formal methods and logic-based techniques to subsurface evaluation and expresses interpretive uncertainty as discrete scenarios with branches of potential alternatives. This framework consists of (i) a proto-scenario generator that takes user observations and geological evidence as input and generates semantically valid initial states based on formalized geological knowledge in first-order logic (ii) geological processes formalized as a rewrite theory that are executable in Maude. By applying geological rewrite rules onto the proto-scenarios, we are able to assist explorationists with multi-scenario generation and reasoning beyond human capacity.

Pay-on-demand resource provisioning is an important driver for cloud computing. Virtualized resources in cloud computing open for resource awareness, such that applications may contain resource management strategies to modify their deployment and reduce resource consumption. The ABS language supports the modelling of deployment decisions and resource management for active objects. In this paper, the semantics of ABS is captured directly as a Coloured Petri Net (CPN) model capable of representing any ABS program by an appropriate initial marking. We define an abstraction relation between the CPN model and the language semantics such that markings of the CPN model become abstract ABS configurations. We use a CPN model checker as an abstract interpreter to investigate resource distribution and starvation problems for deployed active objects in ABS.

It is well-known that the difference between theory and practice seems smaller in theory than in practice. From the perspective of the coordinator, the coordinated components play the role of wild beasts, fortunately imprisoned in boxes. From the perspective of the care-free semanticist, the development of tools is merely a minor step away (possibly hidden in promises of future work). This paper draws parallels between beasts and tool building by describing challenges we have encountered and sharing experiences and lesson learned when going from a compositional semantics to a well-functioning tool interacting with industrial use cases. Concretely, we discuss the development of the simulation backend for Real-Time ABS.

As more and more devices connect to Internet of Things, unbounded streams of data will be generated, which have to be processed "on the fly" in order to trigger automated actions and deliver real-time services. Spark Streaming is a popular realtime stream processing framework. To make efficient use of Spark Streaming and achieve stable stream processing, it requires a careful interplay between different parameter configurations. Mistakes may lead to significant resource overprovisioning and bad performance. To alleviate such issues, this paper develops an executable and configurable model named SSP (stands for Spark Streaming Processing) to model and simulate Spark Streaming. SSP is written in ABS, which is a formal, executable, and object-oriented language for modeling distributed systems by means of concurrent object groups. SSP allows users to rapidly evaluate and compare different parameter configurations without deploying their applications on a cluster/cloud. The simulation results show that SSP is able to mimic Spark Streaming in different scenarios.

This paper proposes a modular proof system based on uninterpreted predicates.The proposed proof system allows modular reasoning about programs with an open-world assumption, which goes beyond behavioral subtyping.The proof system enables modular reasoning about languages with very flexible code reuse mechanisms, such as traits and deltas in the context of object-oriented programming.Whereas related work on incremental proof systems prove soundness in terms of internal consistency, this paper establishes both soundness and relative completeness of the proposed proof system by relating it to a standard proof system for a simple object-oriented language.The applicability of the approach is demonstrated on different code reuse mechanisms: unrestricted class inheritance, delta-oriented programming, and trait-based programming.

Developers use models to design real world distributed applications that often are subject to Service Level Agreements to find a good balance between the quality of the service and its resource usage. Executable models has been used to observe and study such applications using, e.g., the Real Time ABS language, an executable and object-oriented modelling language. For complex models, due to the high number and dependencies between the parameters, it is very difficult to understand the best possible setting that leads the system towards a desired quality of service, while minimising the usage of computing resources. In this work we present POPT, a parameter optimiser tool that starting from Real Time ABS models, by using AI techniques, searches in an automatic way for the best possible setting to satisfy the developer’s expectations.