SMLP: Symbolic Machine Learning Prover

Franz Brausse; Zurab Khasidashvili; Konstantin Korovin

doi:10.1007/978-3-031-65627-9_11

SMLP: Symbolic Machine Learning Prover

Franz Brausse, Zurab Khasidashvili, Konstantin Korovin

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

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 uses symbolic reasoning for ML model exploration and optimization under verification and stability constraints, based on SMT, constraint, and neural network solvers. In addition, the model exploration is guided by probabilistic and statistical methods in a closed feedback loop with the system’s response. 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 any system that can be sampled and modeled by machine learning models.

Original language	English
Title of host publication	Computer Aided Verification - 36th International Conference, CAV 2024
Publisher	Springer Cham
Pages	219–233
Volume	14681
DOIs	https://doi.org/10.1007/978-3-031-65627-9_11
Publication status	E-pub ahead of print - 26 Jul 2024

Publication series

Name	Lecture Notes in Computer Science

Access to Document

10.1007/978-3-031-65627-9_11Licence: CC BY

Cite this

@inproceedings{1e687becb7da477390787821df444620,

title = "SMLP: Symbolic Machine Learning Prover",

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 uses symbolic reasoning for ML model exploration and optimization under verification and stability constraints, based on SMT, constraint, and neural network solvers. In addition, the model exploration is guided by probabilistic and statistical methods in a closed feedback loop with the system{\textquoteright}s response. 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 any system that can be sampled and modeled by machine learning models.",

author = "Franz Brausse and Zurab Khasidashvili and Konstantin Korovin",

note = "12 pages, 4 figures. (submitted)",

year = "2024",

month = jul,

day = "26",

doi = "10.1007/978-3-031-65627-9_11",

language = "English",

volume = "14681",

series = " Lecture Notes in Computer Science",

publisher = "Springer Cham",

pages = "219–233",

booktitle = "Computer Aided Verification - 36th International Conference, CAV 2024",

address = "Switzerland",

}

TY - GEN

T1 - SMLP: Symbolic Machine Learning Prover

AU - Brausse, Franz

AU - Khasidashvili, Zurab

AU - Korovin, Konstantin

N1 - 12 pages, 4 figures. (submitted)

PY - 2024/7/26

Y1 - 2024/7/26

N2 - 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 uses symbolic reasoning for ML model exploration and optimization under verification and stability constraints, based on SMT, constraint, and neural network solvers. In addition, the model exploration is guided by probabilistic and statistical methods in a closed feedback loop with the system’s response. 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 any system that can be sampled and modeled by machine learning models.

AB - 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 uses symbolic reasoning for ML model exploration and optimization under verification and stability constraints, based on SMT, constraint, and neural network solvers. In addition, the model exploration is guided by probabilistic and statistical methods in a closed feedback loop with the system’s response. 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 any system that can be sampled and modeled by machine learning models.

U2 - 10.1007/978-3-031-65627-9_11

DO - 10.1007/978-3-031-65627-9_11

M3 - Conference contribution

VL - 14681

T3 - Lecture Notes in Computer Science

SP - 219

EP - 233

BT - Computer Aided Verification - 36th International Conference, CAV 2024

PB - Springer Cham

ER -

SMLP: Symbolic Machine Learning Prover

Abstract

Publication series

Access to Document

Fingerprint

Cite this