Skip to content

SMLP tutorial#49

Draft
mdmitry1 wants to merge 34 commits intomasterfrom
poly_pareto
Draft

SMLP tutorial#49
mdmitry1 wants to merge 34 commits intomasterfrom
poly_pareto

Conversation

@mdmitry1
Copy link
Collaborator

@mdmitry1 mdmitry1 commented Feb 9, 2026

This tutorial has SMLP 3 examples of various complexities:

Example Variables Objectives Constraints Difficulty
Eggholder 2 1 None High (multi-modal)
DORA 2 1 1 (circular) Low (convex)
BNH 2 2 2 (non-linear) Medium

Each example contains:

  1. Reference
  2. Push button script
  3. Vizualization

Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Initial revision - please, review

@mdmitry1 mdmitry1 marked this pull request as draft February 9, 2026 14:25
Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added explicit mention that SMLP supports black-box functions

Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

  1. Added black-box optimization applications reference to README.md
  2. Added reference to black box function definition used in the README.md file
  3. Added SMLP flow stages description
  4. Multiple style improvements

@mdmitry1 mdmitry1 requested review from zurabksmlp and removed request for zurabk February 10, 2026 09:15
Copy link
Collaborator

@zurabksmlp zurabksmlp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The comments below are on README.md

  1. This repository contains  This tutorial contains
  2. Symbolic Machine Learning and Prediction  Symbolic Machine Learning Prover
  3. constraints defining the set Ω is unknown -> what is set Ω here? Definition is missing?
  4. Structure of the objective function of is unknown  the second “of” is redundant? Or it must be “f”?
    1. Regarding this paragraph:
      SMLP optimization flow is comprised of two stages:
  • Model build: input data is converted into the one of 3 types of models:
    1. Polynomial model
    2. Decision tree
    3. Neural network model
  • Optimization: model and constraints are used to find objective function(s) minimum considering input constraints

a. Model build: input data is converted into the one of 3 types of models:  There are more types of tree models supported in SMLP, not just Decision trees.
b. Besides Optimization, there are many more other modes as well like synthesis, verification, certification, querying, subgroup discovery, DOE, …. I thin you can say that this tutorial focuses on optimization (and will be extended in future to cover some other modes as well)
6. Maybe add SMLP results for the three examples? They can be found in thre results files but for the reader it will be more convenient to include in the text (so that one can compare with expected results).
7. Maybe add reference to SMLP tool paper: https://link.springer.com/chapter/10.1007/978-3-031-65627-9_11
Brauße, F., Khasidashvili, Z., Korovin, K. (2024). SMLP: Symbolic Machine Learning Prover. In: Gurfinkel, A., Ganesh, V. (eds) Computer Aided Verification. CAV 2024. Lecture Notes in Computer Science, vol 14681. Springer, Cham. https://doi.org/10.1007/978-3-031-65627-9_11
There is also a free ArXiv report version https://arxiv.org/abs/2402.01415

@mdmitry1 mdmitry1 requested a review from zurabksmlp February 10, 2026 11:36
@konstantin-korovin
Copy link
Collaborator

konstantin-korovin commented Feb 10, 2026 via email

Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Updated README.md after pull request review

Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Merged with main branch and successfully reproduced results for all three tests in tutorial

Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added link to SMLP User Manual

Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added Intel Signal Integrity test

Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Successfully reproduced results for Intel signal integrity test in Docker container

Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added instructions for running Intel test in Docker environment

Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Improved benchmark by replacing Docker Desktop by Docker CLI

Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added plotting

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants