-
Language-Driven Engineering An Interdisciplinary Software Development Paradigm
Authors:
Bernhard Steffen,
Tiziana Margaria,
Alexander Bainczyk,
Steve Boßelmann,
Daniel Busch,
Marc Driessen,
Markus Frohme,
Falk Howar,
Sven Jörges,
Marvin Krause,
Marco Krumrey,
Anna-Lena Lamprecht,
Michael Lybecait,
Alnis Murtovi,
Stefan Naujokat,
Johannes Neubauer,
Alexander Schieweck,
Jonas Schürmann,
Steven Smyth,
Barbara Steffen,
Fabian Storek,
Tim Tegeler,
Sebastian Teumert,
Dominic Wirkner,
Philip Zweihoff
Abstract:
We illustrate how purpose-specific, graphical modeling enables application experts with different levels of expertise to collaboratively design and then produce complex applications using their individual, purpose-specific modeling language. Our illustration includes seven graphical Integrated Modeling Environments (IMEs) that support full code generation, as well as four browser-based application…
▽ More
We illustrate how purpose-specific, graphical modeling enables application experts with different levels of expertise to collaboratively design and then produce complex applications using their individual, purpose-specific modeling language. Our illustration includes seven graphical Integrated Modeling Environments (IMEs) that support full code generation, as well as four browser-based applications that were modeled and then fully automatically generated and produced using DIME, our most complex graphical IME. While the seven IMEs were chosen to illustrate the types of languages we support with our Language-Driven Engineering (LDE) approach, the four DIME products were chosen to give an impression of the power of our LDE-generated IMEs. In fact, Equinocs, Springer Nature's future editorial system for proceedings, is also being fully automatically generated and then deployed at their Dordrecht site using a deployment pipeline generated with Rig, one of the IMEs presented. Our technology is open source and the products presented are currently in use.
△ Less
Submitted 16 February, 2024;
originally announced February 2024.
-
The Power of Typed Affine Decision Structures: A Case Study
Authors:
Gerrit Nolte,
Maximilian Schlüter,
Alnis Murtovi,
Bernhard Steffen
Abstract:
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 chan…
▽ More
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 mediumsized 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.
△ Less
Submitted 28 April, 2023;
originally announced April 2023.
-
Towards Rigorous Understanding of Neural Networks via Semantics-preserving Transformations
Authors:
Maximilian Schlüter,
Gerrit Nolte,
Alnis Murtovi,
Bernhard Steffen
Abstract:
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 Decisi…
▽ More
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.
△ Less
Submitted 28 April, 2023; v1 submitted 19 January, 2023;
originally announced January 2023.
-
ADD-Lib: Decision Diagrams in Practice
Authors:
Frederik Gossen,
Alnis Murtovi,
Philip Zweihoff,
Bernhard Steffen
Abstract:
In the paper, we present the ADD-Lib, our efficient and easy to use framework for Algebraic Decision Diagrams (ADDs). The focus of the ADD-Lib is not so much on its efficient implementation of individual operations, which are taken by other established ADD frameworks, but its ease and flexibility, which arise at two levels: the level of individual ADD-tools, which come with a dedicated user-friend…
▽ More
In the paper, we present the ADD-Lib, our efficient and easy to use framework for Algebraic Decision Diagrams (ADDs). The focus of the ADD-Lib is not so much on its efficient implementation of individual operations, which are taken by other established ADD frameworks, but its ease and flexibility, which arise at two levels: the level of individual ADD-tools, which come with a dedicated user-friendly web-based graphical user interface, and at the meta level, where such tools are specified. Both levels are described in the paper: the meta level by explaining how we can construct an ADD-tool tailored for Random Forest refinement and evaluation, and the accordingly generated Web-based domain-specific tool, which we also provide as an artifact for cooperative experimentation. In particular, the artifact allows readers to combine a given Random Forest with their own ADDs regarded as expert knowledge and to experience the corresponding effect.
△ Less
Submitted 24 December, 2019;
originally announced December 2019.
-
Aggressive Aggregation: a New Paradigm for Program Optimization
Authors:
Frederik Gossen,
Marc Jasper,
Alnis Murtovi,
Bernhard Steffen
Abstract:
In this paper, we propose a new paradigm for program optimization which is based on aggressive aggregation, i.e., on a partial evaluation-based decomposition of acyclic program fragments into a pair of computationally optimal structures: an Algebraic Decision Diagram (ADD) to capture conditional branching and a parallel assignment that refers to an Expression DAG (ED) which realizes redundancy-fre…
▽ More
In this paper, we propose a new paradigm for program optimization which is based on aggressive aggregation, i.e., on a partial evaluation-based decomposition of acyclic program fragments into a pair of computationally optimal structures: an Algebraic Decision Diagram (ADD) to capture conditional branching and a parallel assignment that refers to an Expression DAG (ED) which realizes redundancy-free computation. The point of this decomposition into, in fact, side-effect-free component structures allows for powerful optimization that semantically comprise effects traditionally aimed at by SSA form transformation, code specialization, common subexpression elimination, and (partial) redundancy elimination. We illustrate our approach along an optimization of the well-known iterative Fibonacci program, which, typically, is considered to lack any optimization potential. The point here is that our technique supports loop unrolling as a first class optimization technique and is tailored to optimally aggregate large program fragments, especially those resulting from multiple loop unrollings. For the Fibonacci program, this results in a performance improvement beyond an order of magnitude.
△ Less
Submitted 24 December, 2019;
originally announced December 2019.
