-
SMLP: Symbolic Machine Learning Prover (User Manual)
Authors:
Franz Brauße,
Zurab Khasidashvili,
Konstantin Korovin
Abstract:
SMLP: Symbolic Machine Learning Prover an open source tool for exploration and optimization of systems represented by machine learning models. SMLP uses symbolic reasoning for ML model exploration and optimization under verification and stability constraints, based on SMT, constraint and NN solvers. In addition its exploration methods are guided by probabilistic and statistical methods. SMLP is a…
▽ More
SMLP: Symbolic Machine Learning Prover an open source tool for exploration and optimization of systems represented by machine learning models. SMLP uses symbolic reasoning for ML model exploration and optimization under verification and stability constraints, based on SMT, constraint and NN solvers. In addition its exploration methods are guided by probabilistic and statistical methods. SMLP is a general purpose tool that requires only data suitable for ML modelling in the csv format (usually samples of the system's input/output). SMLP has been applied at Intel for analyzing and optimizing hardware designs at the analog level. Currently SMLP supports NNs, polynomial and tree models, and uses SMT solvers for reasoning and optimization at the backend, integration of specialized NN solvers is in progress.
△ Less
Submitted 16 May, 2024;
originally announced May 2024.
-
SMLP: Symbolic Machine Learning Prover
Authors:
Franz Brauße,
Zurab Khasidashvili,
Konstantin Korovin
Abstract:
Symbolic Machine Learning Prover (SMLP) is a tool and a library for system exploration based on data samples obtained by simulating or executing the system on a number of input vectors. SMLP aims at exploring the system based on this data by taking a grey-box approach: SMLP combines statistical methods of data exploration with building and exploring machine learning models in close feedback loop w…
▽ More
Symbolic Machine Learning Prover (SMLP) is a tool and a library for system exploration based on data samples obtained by simulating or executing the system on a number of input vectors. SMLP aims at exploring the system based on this data by taking a grey-box approach: SMLP combines statistical methods of data exploration with building and exploring machine learning models in close feedback loop with the system's response, and exploring these models by combining probabilistic and formal methods. SMLP has been applied in industrial setting at Intel for analyzing and optimizing hardware designs at the analog level. SMLP is a general purpose tool and can be applied to systems that can be sampled and modeled by machine learning models.
△ Less
Submitted 2 February, 2024;
originally announced February 2024.
-
ESBMC v7.4: Harnessing the Power of Intervals
Authors:
Rafael Menezes,
Mohannad Aldughaim,
Bruno Farias,
Xianzhiyu Li,
Edoardo Manino,
Fedor Shmarov,
Kunjian Song,
Franz Brauße,
Mikhail R. Gadelha,
Norbert Tihanyi,
Konstantin Korovin,
Lucas C. Cordeiro
Abstract:
ESBMC implements many state-of-the-art techniques for model checking. We report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, forward and backw…
▽ More
ESBMC implements many state-of-the-art techniques for model checking. We report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, forward and backward contractors, and particular optimizations related to singleton intervals because of their ubiquity. Other relevant improvements concern the verification of concurrent programs, as well as several operational models, internal ones, and also those of libraries such as pthread and the C mathematics library. An extended memory safety analysis now allows tracking of memory leaks that are considered still reachable.
△ Less
Submitted 22 December, 2023;
originally announced December 2023.
-
ESBMC v7.3: Model Checking C++ Programs using Clang AST
Authors:
Kunjian Song,
Mikhail R. Gadelha,
Franz Brauße,
Rafael S. Menezes,
Lucas C. Cordeiro
Abstract:
This paper introduces ESBMC v7.3, the latest Efficient SMT-Based Context-Bounded Model Checker version, which now incorporates a new clang-based C++ front-end. While the previous CPROVER-based front-end served well for handling C++03 programs, it encountered challenges kee** up with the evolving C++ language. As new language and library features were added in each C++ version, the limitations of…
▽ More
This paper introduces ESBMC v7.3, the latest Efficient SMT-Based Context-Bounded Model Checker version, which now incorporates a new clang-based C++ front-end. While the previous CPROVER-based front-end served well for handling C++03 programs, it encountered challenges kee** up with the evolving C++ language. As new language and library features were added in each C++ version, the limitations of the old front-end became apparent, leading to difficult-to-maintain code. Consequently, modern C++ programs were challenging to verify. To overcome this obstacle, we redeveloped the front-end, opting for a more robust approach using clang. The new front-end efficiently traverses the Abstract Syntax Tree (AST) in-memory using clang APIs and transforms each AST node into ESBMC's Intermediate Representation. Through extensive experimentation, our results demonstrate that ESBMC v7.3 with the new front-end significantly reduces parse and conversion errors, enabling successful verification of a wide range of C++ programs, thereby outperforming previous ESBMC versions.
△ Less
Submitted 10 August, 2023;
originally announced August 2023.
-
Bayesian Optimisation with Formal Guarantees
Authors:
Franz Brauße,
Zurab Khasidashvili,
Konstantin Korovin
Abstract:
Application domains of Bayesian optimization include optimizing black-box
functions or very complex functions. The functions we are interested in describe
complex real-world systems applied in industrial settings. Even though
they do have explicit representations, standard optimization
techniques fail to provide validated solutions and correctness
guarantees for them.
In this paper we…
▽ More
Application domains of Bayesian optimization include optimizing black-box
functions or very complex functions. The functions we are interested in describe
complex real-world systems applied in industrial settings. Even though
they do have explicit representations, standard optimization
techniques fail to provide validated solutions and correctness
guarantees for them.
In this paper we present a combination of Bayesian optimisation and SMT-based constraint solving to achieve safe and stable solutions with optimality guarantees.
△ Less
Submitted 10 June, 2021;
originally announced June 2021.
-
The ksmt calculus is a $δ$-complete decision procedure for non-linear constraints
Authors:
Franz Brauße,
Konstantin Korovin,
Margarita V. Korovina,
Norbert Th. Müller
Abstract:
ksmt is a CDCL-style calculus for solving non-linear constraints over real numbers involving polynomials and transcendental functions.
In this paper we investigate properties of the ksmt calculus and show that it is a $δ$-complete decision procedure for bounded problems.
We also propose an extension with local linearisations, which allow for more efficient treatment of non-linear constraints.
ksmt is a CDCL-style calculus for solving non-linear constraints over real numbers involving polynomials and transcendental functions.
In this paper we investigate properties of the ksmt calculus and show that it is a $δ$-complete decision procedure for bounded problems.
We also propose an extension with local linearisations, which allow for more efficient treatment of non-linear constraints.
△ Less
Submitted 27 April, 2021;
originally announced April 2021.
-
A CDCL-style calculus for solving non-linear constraints
Authors:
Franz Brauße,
Konstantin Korovin,
Margarita Korovina,
Norbert Th. Müller
Abstract:
In this paper we propose a novel approach for checking satisfiability of non-linear constraints over the reals, called ksmt. The procedure is based on conflict resolution in CDCL style calculus, using a composition of symbolical and numerical methods. To deal with the non-linear components in case of conflicts we use numerically constructed restricted linearisations. This approach covers a large n…
▽ More
In this paper we propose a novel approach for checking satisfiability of non-linear constraints over the reals, called ksmt. The procedure is based on conflict resolution in CDCL style calculus, using a composition of symbolical and numerical methods. To deal with the non-linear components in case of conflicts we use numerically constructed restricted linearisations. This approach covers a large number of computable non-linear real functions such as polynomials, rational or trigonometrical functions and beyond. A prototypical implementation has been evaluated on several non-linear SMT-LIB examples and the results have been compared with state-of-the-art SMT solvers.
△ Less
Submitted 5 July, 2019; v1 submitted 22 May, 2019;
originally announced May 2019.
-
A minimal representation for continuous functions
Authors:
Franz Brauße,
Florian Steinberg
Abstract:
Kawamura and Cook specified the least set of information about a continuous function on the unit interval which is needed for fast function evaluation. This paper presents a variation of their result. To make the above statement precise, one has to specify what a "set of information" is and what "fast" should mean. Kawamura and Cook use polynomial-time computability in the sense of second-order co…
▽ More
Kawamura and Cook specified the least set of information about a continuous function on the unit interval which is needed for fast function evaluation. This paper presents a variation of their result. To make the above statement precise, one has to specify what a "set of information" is and what "fast" should mean. Kawamura and Cook use polynomial-time computability in the sense of second-order complexity theory to define what "fast" means but do not use the most general "sets of information" this framework is able to handle. Instead they require codes to be length-monotone. This paper removes the additional premise of length-monotonicity, and instead imposes further conditions on the speed of the evaluation: The operation should now be computable in "hyper-linear" time. This means that the running time can not contain any iterations of the length function and, while an arbitrary polynomial may be applied to its value, on the argument side at most a shift by a constant is allowed. This is a very restrictive notion, but one can check that the Kawamura and Cook representation allows for hyper-linear time evaluation. The paper proves that it is not minimal with this property by providing the minimal set of information necessary for hyper-linear evaluation and proving that it is not polynomial-time equivalent to any encoding using only length-monotone names. Ultimatively, this is due to a failure of polynomial-time computability of an upper bound to a modulus of continuity. Indeed this failure seems to reflect the behavior of software based on the ideas of computable analysis appropriately and was one of the reasons for a closer investigation in the first place.
△ Less
Submitted 26 August, 2018; v1 submitted 29 March, 2017;
originally announced March 2017.
-
Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
Authors:
Sewon Park,
Franz Brauße,
Pieter Collins,
SunYoung Kim,
Michal Konečný,
Gyesik Lee,
Norbert Müller,
Eike Neumann,
Norbert Preining,
Martin Ziegler
Abstract:
We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides a formal programming language-theoretic foundation to the algorithmic processing of real numbers. In order to capture multi-valuedness, which is well-known to be essential to real number computation, we use a Plotkin po…
▽ More
We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides a formal programming language-theoretic foundation to the algorithmic processing of real numbers. In order to capture multi-valuedness, which is well-known to be essential to real number computation, we use a Plotkin powerdomain and make our programming language semantics computable and complete: all and only real functions computable in computable analysis can be realized in ERC. The base programming language supports real arithmetic as well as implicit limits; expansions support additional primitive operations (such as a user-defined exponential function). By restricting integers to Presburger arithmetic and real coercion to the `precision' embedding $\mathbb{Z}\ni p\mapsto 2^p\in\mathbb{R}$, we arrive at a first-order theory which we prove to be decidable and model-complete. Based on said logic as specification language for preconditions and postconditions, we extend Hoare logic to a sound (w.r.t. the denotational semantics) and expressive system for deriving correct total correctness specifications. Various examples demonstrate the practicality and convenience of our language and the extended Hoare logic.
△ Less
Submitted 12 May, 2024; v1 submitted 20 August, 2016;
originally announced August 2016.
