Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SMLP: Symbolic Machine Learning Prover (User Manual)

Franz Brauße, Zurab Khasidashvili, Konstantin Korovin

TL;DR

SMLP presents a principled framework for symbolic ML-driven design space exploration under verification and stability constraints. It formalizes stability via the Gear framework, linking knob constraints, model behavior, and exploration-mode conditions through a GEAR fragment solved by GearSAT$_\delta$/-BO solvers, while enabling practical ML modeling (NNs, polynomials, trees) and DOE-driven data generation. The system supports certification, querying, verification, synthesis, optimization, and optimized synthesis with robust, region-based guarantees, plus a targeted model refinement loop and root-cause analysis. This combination enables robust design of parameterized systems (notably analog hardware) under environmental and adversarial perturbations, with open-source tooling and integration with standard ML libraries for training, evaluation, and prediction."

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 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.

SMLP: Symbolic Machine Learning Prover (User Manual)

TL;DR

SMLP presents a principled framework for symbolic ML-driven design space exploration under verification and stability constraints. It formalizes stability via the Gear framework, linking knob constraints, model behavior, and exploration-mode conditions through a GEAR fragment solved by GearSAT/-BO solvers, while enabling practical ML modeling (NNs, polynomials, trees) and DOE-driven data generation. The system supports certification, querying, verification, synthesis, optimization, and optimized synthesis with robust, region-based guarantees, plus a targeted model refinement loop and root-cause analysis. This combination enables robust design of parameterized systems (notably analog hardware) under environmental and adversarial perturbations, with open-source tooling and integration with standard ML libraries for training, evaluation, and prediction."

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 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.
Paper Structure (38 sections, 27 equations, 26 figures, 2 tables)

This paper contains 38 sections, 27 equations, 26 figures, 2 tables.

Table of Contents

  1. Introduction
  2. SMLP architecture
  3. How to run SMLP: a quick start
  4. Symbolic representation of the ML model exploration
  5. SMLP problem specification
  6. SMLP input and output
  7. SMLP inputs
  8. SMLP outputs
  9. Data processing options
  10. Data preprocessing options
  11. Selecting features for analysis
  12. Missing values in responses
  13. Constant features
  14. Missing values in features
  15. Boolean typed features
  16. ...and 23 more sections

Figures (26)

  • Figure 1: Parameterized system, with interface constraints
  • Figure 2: Exploration Cube
  • Figure 3: SMLP Tool Architecture
  • Figure 4: Example of SMLP's command in mode $\operatorname{\mathsf{optimize}}$, to build a decision tree model and perform an optimization task.
  • Figure 5: Specification $\operatorname{\mathsf{smlp\_toy\_basic.spec}}$ used by SMLP command in Figure \ref{['fig:command']}.
  • ...and 21 more figures

Theorems & Definitions (5)

  • Definition 1
  • Example 2
  • Example 3
  • Example 4
  • Example 5