Bayesian Optimisation with Formal Guarantees

TL;DR

This paper introduces a method combining Bayesian optimization with SMT-based constraint solving to ensure safe, stable, and optimal solutions for complex real-world black-box functions.

Contribution

It presents a novel approach that integrates Bayesian optimization with formal constraint solving to provide validated solutions with correctness guarantees.

Findings

Achieves safe and stable optimization in industrial settings

Provides formal correctness guarantees for solutions

Enhances reliability of black-box function optimization

Abstract

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.