Optimizing over trained graph neural networks: mixed-integer programming, symmetry-breaking, and applications

Optimization over trained machine learning models has applications including verification, minimizing neural acquisition functions, and integrating a trained surrogate into a larger decision-making problem. This thesis formulates and solves optimization problems constrained by trained graph neural networks (GNNs) using mixed-integer programming (MIP). We study the case where the input graph is not fixed, implying that each edge is a decision variable, and develop two mixed-integer optimization formulations. Since different ways of indexing nodes correspond to the same graph but result in different solutions in optimization, we propose two types of symmetry-breaking constraints to remove symmetries, and prove that adding these constraints will not remove all symmetric solutions. As a byproduct, a graph indexing algorithm is constructed to yield an indexing satisfying these constraints. Generally, our symmetry-breaking techniques could be applied in any graph-based decision-making problems with symmetry issue caused by graph isomorphism. The first application is GNN verification, for which we propose two topology-based bounds tightening techniques to efficiently certify the robustness of GNNs. The second application is optimal molecular design, aiming to find molecules with optimal GNN predictive properties. Furthermore, we exploit the ability of MIP in molecular generation and propose Limeade as an end-to-end tool from real-world needs to feasible molecules.