Combining Constraint Solving and Bayesian Techniques for System Optimization
Authors: Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
IJCAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We evaluated GEAROPTδ-BO on 6 industrial examples coming from optimization of microprocessor design at Intel where stability is an essential requirement. We conclude in Section 7. |
| Researcher Affiliation | Collaboration | Franz Brauße1 , Zurab Khasidashvili2 , Konstantin Korovin1 1The University of Manchester, UK 2Intel, Israel |
| Pseudocode | Yes | Algorithm 1 Basic optimization algorithm using the BO solver Amax for maximizing f(x). Algorithm 2 (GEARSATδ) General procedure for deciding whether a constant T is a lower or upper bound on the solution y of (2). Algorithm 3 Finding counter-examples: Solving Di(x , y ) with Bayesian optimization and SMT in the i-th iteration of Algorithm 2. Algorithm 4 Finding candidates: Solving Ci(x, y) with Bayesian optimization and SMT in the i-th iteration of Algorithm 2. Ai maximizes. Algorithm 5 (GEAROPTδ-BO) General procedure for optimizing f : Rn R represented by predicate F under stability conditions θ. Arbitrary candidate lower and upper bounds l0, u0 such that l0 < u0. |
| Open Source Code | Yes | GEAROPTδ-BO is implemented in the solver called SMLP (https://github.com/fbrausse/smlp). |
| Open Datasets | No | We evaluated GEAROPTδ-BO on 6 industrial examples coming from the Electrical Validation Lab at Intel. These are neural network models representing signal integrity of transmitters and receivers of a channel to a peripheral device. This application requires solutions to be safe and stable (see, Section 4), moreover the radii of stability regions are required to be proportional to the value of their respective centers. No information about public availability, links, or formal citations for these datasets was provided. |
| Dataset Splits | No | No explicit information about training, validation, or test dataset splits, percentages, or specific counts was found. The paper mentions evaluating on '6 industrial examples' but doesn't detail how the data was partitioned. |
| Hardware Specification | No | No specific hardware details (e.g., GPU/CPU models, memory, or cloud instance types) used for running the experiments were provided. |
| Software Dependencies | No | As Bayesian optimizers Amax, Bmin, we used the SKOPT implementation [Pedregosa et al., 2011] based on Gaussian processes, with acquisition function gp hedge. The SMT part is implemented using the state of the art solver Z3 [de Moura and Bjørner, 2008]. While software components are mentioned, specific version numbers for SKOPT or Z3 are not provided. |
| Experiment Setup | Yes | The accuracy was set to ε = 0.05. These results are shown in Table 1. In the left-most column i refers to the problem instance, c to whether BO search was used for candidates and d to whether BO search was used for counter-examples. |