A Formally Verified Generic Branching Algorithm for Global Optimization

This paper presents a formalization in higher-order logic of a generic algorithm that is used in automated strategies for solving global optimization problems. It is a generalization of numerical branch and bound algorithms that compute the minimum of a function on a given domain by recursively dividing the domain and computing estimates for the range of the function on each sub-domain. The correctness statement of the algorithm has been proved in the Prototype Verification System PVS theorem prover. This algorithm can be instantiated with specific functions for performing particular global optimization methods. The correctness of the instantiated algorithms is guaranteed by simple properties that need to be verified on the specific input functions. The use of the generic algorithm is illustrated with an instantiation that yields an automated strategy in PVS for estimating the maximum and minimum values of real-valued functions.