SMLP - Symbolic Machine Learning Prover

SMLP is a general purpose tool for verification and optimisation of systems modelled using machine learning.
SMLP uses symbolic reasoning for ML model exploration and optimisation under verification and stability constraints.

Industry adoption: used at Intel in production for optimization of package/board layouts and signal integrity

SMLP applications in Intel and why stability is important

SMLP has been successfully used at Intel to optimize package and board layouts under noisy, real‑world signal‑integrity data collected in the lab. Because this data is inherently noisy—and because ML models are often intentionally approximate to avoid overfitting—robustness is essential when searching for reliable optimal solutions. SMLP addresses this through its notion of stability, ensuring that selected optima remain valid under data and model uncertainty. In most cases the stability radius (*) is actually as large as 10% of the value of the variable in the configuration. This is because the sampling error from analog equipment can be dependent on the intended value itself.

(*) The smallest perturbation (measured by a norm, e.g., Chebyshev) that makes an optimal solution either non-optimal or infeasible.

Combination of robustness and formal assurance of results validity is a distinctive strength of SMLP, not found in other optimization or model‑analysis tools.

SMLP modes:

• optmization
• verification
• synthesis
• exploration
• root cause analysis

Systems analysed by SMLP can be represented as:

• black-box functions: via sampling input -- output behaviour only tabular data is needed
• explicit expressions involving polynomials
• machine learning models:
  • neural networks
  • decision trees
  • random forests
  • polynomial models

SMLP supports:

• symbolic constrains
• stability constraints
• parameter optimization

Papers:

• SMLP: Symbolic Machine Learning Prover, (CAV'24) [pdf] [bib]
• Combining Constraint Solving and Bayesian Techniques for System Optimization, (IJCAI'22) [pdf] [bib]
• Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation, (FMCAD'20), [pdf] [bib]

Installation

pip installation (recommended)

MacOS

• install Python 3.11; for example via Python version management [pyenv]

pyenv install 3.11
pyenv local 3.11

• install smlptech package:

pip install smlptech

Ubuntu 24.04

• cd scripts/venv/

• Follow: [SMLP Installation Guide for Ubuntu-24.04]

Docker

MacOS

docker run -it mdmitry1/python311-dev-mac:latest

Within docker container prepend SMLP Python script with xvfb-run.
For example:

xvfb-run smlp -h

Linux

docker run -it mdmitry1/python311-dev:latest

Within docker container prepend SMLP Python script with xvfb-run.
For example:

xvfb-run smlp -h

Linux with GUI support using VNC

Starting VNC server within container:

./start_vnc

scripts/bin/enter_container

Starting VNC server within container:

./start_vnc

Recommended VNC client:

• Ubuntu: remmina

• Windows: RealVNC®

  Details - see RealVNC® installation instructions

Linux with GUI support using X11

• Entering Docker container with X11 support on native Linux

scripts/bin/enter_container_x11_forwarding

Dependencies: socat

• Entering Docker container with X11 support on wslg

scripts/bin/enter_container_wslg

Dependencies: WSL2 with WSLG enabled

• Installation test:

tests/install/test_container_install mdmitry1/python311-dev

Sources

Installation on a stock Ubuntu-22.04

	sudo apt install \
		python3-pip ninja-build z3 libz3-dev libboost-python-dev texlive \
		pkg-config libgmp-dev libpython3-all-dev python-is-python3
	# get a recent version of the meson configure tool
	pip install --user meson

	# obtain sources
	git clone https://github.com/fbrausse/kay.git
	git clone https://github.com/smlp-systems/smlp.git
	cd smlp/utils/poly

	# workaround <https://bugs.launchpad.net/ubuntu/+source/swig/+bug/1746755>
	echo 'export PYTHONPATH=$HOME/.local/lib/python3/dist-packages:$PYTHONPATH' >> ~/.profile
	# get $HOME/.local/bin into PATH and get PYTHONPATH
	mkdir -p $HOME/.local/bin
	source ~/.profile

	# setup, build & install libsmlp
	meson setup -Dkay-prefix=$HOME/kay --prefix $HOME/.local build
	ninja -C build install

	# tensorflow-2.16 has a change leading to the error:
	# 'The filepath provided must end in .keras (Keras model format).'
	pip install --user \
		pandas tensorflow==2.15.1 scikit-learn pycaret seaborn \
		mrmr-selection jenkspy pysubgroup pyDOE doepy

MacOS

Installation instructions for Ubuntu-22.04 can be followed using `homebrew` in place of `apt`

Tutorial

• Black-box optimization Eggholder Function
• Constrained DORA (Distance to Optimal with Radial Adjustment)
• Binh and Korn (BNH) Multi-Objective Problem
• Intel Signal Integrity domain example

Manual

Comments/Feedback/Discussions: [GitHub] or [Zulip Chat]

Coming soon:

NLP, LLM, Agentic

Current development is in PR #21
See Extended Manual for details.

NLP:

• NLP based text classification. Applicable to spam detection, sentiment analysis, and more.
• NLP based root cause analysis: which words or collections of words are most correlative to classification decision (especially, for the positive class).

LLM:

• LLM training from scratch
• LLM finetuning
• RAG (with HuggingFace and with LangChain)

Agentic:

• SMLP Agent