smlptech 1.1.1

SMLP - The Symbolic Machine Learning Prover

SMLP -- Symbolic Machine Learning Prover

Success story: used at Intel for optimization of package/board layouts and signal integrity

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.

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

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