Search

Random Forests are one of the most popular classifiers in machine learning. The larger they are, the more precise the outcome of their predictions. However, this comes at a cost: it is increasingly difficult to understand why a Random Forest made a specific choice, and its running time for classification grows linearly with the size (number of trees). In this paper, we propose a method to aggregate large Random Forests into a single, semantically equivalent decision diagram which has the following two effects: (1) minimal, sufficient explanations for Random Forest-based classifications can be obtained by means of a simple three step reduction, and (2) the running time is radically improved. In fact, our experiments on various popular datasets show speed-ups of several orders of magnitude, while, at the same time, also significantly reducing the size of the required data structure. [ABSTRACT FROM AUTHOR]

This paper presents a compositional approach to active automata learning of Systems of Procedural Automata (SPAs), an extension of Deterministic Finite Automata (DFAs) to systems of DFAs that can mutually call each other. SPAs are of high practical relevance, as they allow one to efficiently learn intuitive recursive models of recursive programs after an easy instrumentation that makes calls and returns observable. Key to our approach is the simultaneous inference of individual DFAs for each of the involved procedures via expansion and projection: membership queries for the individual DFAs are expanded to membership queries of the entire SPA, and global counterexample traces are transformed into counterexamples for the DFAs of concerned procedures. This reduces the inference of SPAs to a simultaneous inference of the DFAs for the involved procedures for which we can utilize various existing regular learning algorithms. The inferred models are easy to understand and allow for an intuitive display of the procedural system under learning that reveals its recursive structure. We implemented the algorithm within the LearnLib framework in order to provide a ready-to-use tool for practical application which is publicly available on GitHub for experimentation. [ABSTRACT FROM AUTHOR]

In this paper, we present the envisioned style and scope of the new topic "Explanation Paradigms Leveraging Analytic Intuition" (ExPLAIn) with the International Journal on Software Tools for Technology Transfer (STTT). Intention behind this new topic is to (1) explicitly address all aspects and issues that arise when trying to, if possible, reveal and then confirm hidden properties of black-box systems, or (2) to enforce vital properties by embedding them into appropriate system contexts. Machine-learned systems, such as Deep Neural Networks, are particularly challenging black-box systems, and there is a wealth of formal methods for analysis and verification waiting to be adapted and applied. The selection of papers of this first Special Section of ExPLAIn, most of which were co-authored by editorial board members, is an illustrative example of the style and scope envisioned: In addition to methodological papers on verification, explanation, and their scalability, case studies, tool papers, literature reviews, and position papers are also welcome. [ABSTRACT FROM AUTHOR]

In this paper, we present Forest GUMP (for Generalized, Unifying Merge Process) a tool for verification and precise explanation of Random forests. Besides pre/post-condition-based verification and equivalence checking, Forest GUMP also supports three concepts of explanation, the well-known model explanation and outcome explanation, as well as class characterization, i.e., the precise characterization of all samples that are equally classified. Key technology to achieve these results is algebraic aggregation, i.e., the transformation of a Random Forest into a semantically equivalent, concise white-box representation in terms of Algebraic Decision Diagrams (ADDs). The paper sketches the method and demonstrates the use of Forest GUMP along illustrative examples. This way readers should acquire an intuition about the tool, and the way how it should be used to increase the understanding not only of the considered dataset, but also of the character of Random Forests and the ADD technology, here enriched to comprise infeasible path elimination. As Forest GUMP is publicly available all experiments can be reproduced, modified, and complemented using any dataset that is available in the ARFF format. [ABSTRACT FROM AUTHOR]

TADS are a novel, concise white-box representation of neural networks. In this paper, we apply TADS to the problem of neural network verification, using them to generate either proofs or concise error characterizations for desirable neural network properties. In a case study, we consider the robustness of neural networks to adversarial attacks, i.e., small changes to an input that drastically change a neural networks perception, and show that TADS can be used to provide precise diagnostics on how and where robustness errors a occur. We achieve these results by introducing Precondition Projection, a technique that yields a TADS describing network behavior precisely on a given subset of its input space, and combining it with PCA, a traditional, well-understood dimensionality reduction technique. We show that PCA is easily compatible with TADS. All analyses can be implemented in a straightforward fashion using the rich algebraic properties of TADS, demonstrating the utility of the TADS framework for neural network explainability and verification. While TADS do not yet scale as efficiently as state-of-the-art neural network verifiers, we show that, using PCA-based simplifications, they can still scale to medium-sized problems and yield concise explanations for potential errors that can be used for other purposes such as debugging a network or generating new training samples. [ABSTRACT FROM AUTHOR]

In this paper, we present an algebraic approach to the precise and global verification and explanation of Rectifier Neural Networks, a subclass of Piece-wise Linear Neural Networks (PLNNs), i.e., networks that semantically represent piece-wise affine functions. Key to our approach is the symbolic execution of these networks that allows the construction of semantically equivalent Typed Affine Decision Structures (TADS). Due to their deterministic and sequential nature, TADS can, similarly to decision trees, be considered as white-box models and therefore as precise solutions to the model and outcome explanation problem. TADS are linear algebras, which allows one to elegantly compare Rectifier Networks for equivalence or similarity, both with precise diagnostic information in case of failure, and to characterize their classification potential by precisely characterizing the set of inputs that are specifically classified, or the set of inputs where two network-based classifiers differ. All phenomena are illustrated along a detailed discussion of a minimal, illustrative example: the continuous XOR function. [ABSTRACT FROM AUTHOR]

This paper (1) summarizes the history of the RERS challenge for the analysis and verification of reactive systems, its profile and intentions, its relation to other competitions, and, in particular, its evolution due to the feedback of participants, and (2) presents the most recent development concerning the synthesis of hard benchmark problems. In particular, the second part proposes a way to tailor benchmarks according to the depths to which programs have to be investigated in order to find all errors. This gives benchmark designers a method to challenge contributors that try to perform well by excessive guessing. [ABSTRACT FROM AUTHOR]

This paper proposes a simplicity-oriented approach and framework for language-to-language transformation of, in particular, graphical languages. Key to simplicity is the decomposition of the transformation specification into sub-rule systems that separately specify purpose-specific aspects. We illustrate this approach by employing a variation of Plotkin's Structural Operational Semantics (SOS) for pattern-based transformations of typed graphs in order to address the aspect 'computation' in a graph rewriting fashion. Key to our approach are two generalizations of Plotkin's structural rules: the use of graph patterns as the matching concept in the rules, and the introduction of node and edge types. Types do not only allow one to easily distinguish between different kinds of dependencies, like control, data, and priority, but may also be used to define a hierarchical layering structure. The resulting Type-based Structural Operational Semantics (TSOS) supports a well-structured and intuitive specification and realization of semantically involved language-to-language transformations adequate for the generation of purpose-specific views or input formats for certain tools, like, e.g., model checkers. A comparison with the general-purpose transformation frameworks ATL and Groove, illustrates along the educational setting of our graphical WebStory language that TSOS provides quite a flexible format for the definition of a family of purpose-specific transformation languages that are easy to use and come with clear guarantees. [ABSTRACT FROM AUTHOR]

This is the second issue in the new "Competitions and Challenges" (CoCha) theme of the International Journal on Software Tools for Technology Transfer. The new theme was established to support competitions and challenges with an appropriate publication venue. The first issue presented the competition on software testing Test-Comp 2019, which was part of the TOOLympics 2019 event. In this second issue for TOOLympics, we present selected competition reports. The TOOLympics event took place as part of the 25-years celebration of the conference TACAS. The goal of the event was to provide an overview of competitions and challenges in the area of formal methods. [ABSTRACT FROM AUTHOR]