# Bayesian Optimisation with Formal Guarantees

arXiv: https://arxiv.org/abs/2106.06067 · HTML: https://mlsanity.com/paper/2106.06067/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 15 references that are in the map.
- First posted on arXiv 10 Jun 2021.

## Builds on (most cited first, 5 of 5)

- [A Tutorial on Bayesian Optimization](https://mlsanity.com/paper/1807.02811/) (2018)
- [Adversarially Robust Optimization with Gaussian Processes](https://mlsanity.com/paper/1810.10775/) (2018)
- [Robustness Guarantees for Bayesian Inference with Gaussian Processes](https://mlsanity.com/paper/1809.06452/) (2018)
- [A CDCL-style calculus for solving non-linear constraints](https://mlsanity.com/paper/1905.09227/) (2019)
- [The ksmt calculus is a δ-complete decision procedure for non-linear constraints](https://mlsanity.com/paper/2104.13269/) (2021)

## Abstract (arXiv)

Application domains of Bayesian optimization include optimizing black-box functions or very complex functions. The functions we are interested in describe complex real-world systems applied in industrial settings. Even though they do have explicit representations, standard optimization techniques fail to provide validated solutions and correctness guarantees for them. In this paper we present a combination of Bayesian optimisation and SMT-based constraint solving to achieve safe and stable solutions with optimality guarantees.