-
Bound Tightening using Rolling-Horizon Decomposition for Neural Network Verification
Authors:
Haoruo Zhao,
Hassan Hijazi,
Haydn Jones,
Juston Moore,
Mathieu Tanneau,
Pascal Van Hentenryck
Abstract:
Neural network verification aims at providing formal guarantees on the output of trained neural networks, to ensure their robustness against adversarial examples and enable their deployment in safety-critical applications. This paper introduces a new approach to neural network verification using a novel mixed-integer programming rolling-horizon decomposition method. The algorithm leverages the lay…
▽ More
Neural network verification aims at providing formal guarantees on the output of trained neural networks, to ensure their robustness against adversarial examples and enable their deployment in safety-critical applications. This paper introduces a new approach to neural network verification using a novel mixed-integer programming rolling-horizon decomposition method. The algorithm leverages the layered structure of neural networks, by employing optimization-based bound-tightening on smaller sub-graphs of the original network in a rolling-horizon fashion. This strategy strikes a balance between achieving tighter bounds and ensuring the tractability of the underlying mixed-integer programs. Extensive numerical experiments, conducted on instances from the VNN-COMP benchmark library, demonstrate that the proposed approach yields significantly improved bounds compared to existing effective bound propagation methods. Notably, the parallelizable nature of the proposed method proves effective in solving open verification problems. Our code is built and released as part of the open-source mathematical modeling tool Gravity (https://github.com/coin-or/Gravity), which is extended to support generic neural network models.
△ Less
Submitted 29 March, 2024; v1 submitted 10 January, 2024;
originally announced January 2024.
-
Benchmarking Large-Scale ACOPF Solutions and Optimality Bounds
Authors:
Smitha Gopinath,
Hassan L. Hijazi
Abstract:
We present the results of a comprehensive benchmarking effort aimed at evaluating and comparing state-of-the-art open-source tools for solving the Alternating-Current Optimal Power Flow (ACOPF) problem. Our numerical experiments include all instances found in the public library PGLIB with network sizes up to 30,000 nodes. The benchmarked tools span a number of programming languages (Python, Julia,…
▽ More
We present the results of a comprehensive benchmarking effort aimed at evaluating and comparing state-of-the-art open-source tools for solving the Alternating-Current Optimal Power Flow (ACOPF) problem. Our numerical experiments include all instances found in the public library PGLIB with network sizes up to 30,000 nodes. The benchmarked tools span a number of programming languages (Python, Julia, Matlab/Octave, and C$++$), nonlinear optimization solvers (Ipopt, MIPS, and INLP) as well as different mathematical modeling tools (JuMP and Gravity). We also present state-of-the-art optimality bounds obtained using sparsity-exploiting semidefinite programming approaches and corresponding computational times.
△ Less
Submitted 21 March, 2022;
originally announced March 2022.
-
Verifying Global Optimality of Candidate Solutions to Polynomial Optimization Problems using a Determinant Relaxation Hierarchy
Authors:
Sikun Xu,
Ruoyi Ma,
Daniel K. Molzahn,
Hassan Hijazi,
Cédric Josz
Abstract:
We propose a method for verifying that a given feasible point for a polynomial optimization problem is globally optimal. The approach relies on the Lasserre hierarchy and the result of Lasserre regarding the importance of the convexity of the feasible set as opposed to that of the individual constraints. By focusing solely on certifying global optimality and relaxing the Lasserre hierarchy using n…
▽ More
We propose a method for verifying that a given feasible point for a polynomial optimization problem is globally optimal. The approach relies on the Lasserre hierarchy and the result of Lasserre regarding the importance of the convexity of the feasible set as opposed to that of the individual constraints. By focusing solely on certifying global optimality and relaxing the Lasserre hierarchy using necessary conditions for positive semidefiniteness based on matrix determinants, the proposed method is implementable as a computationally tractable linear program. We demonstrate this method via application to several instances of polynomial optimization, including the optimal power flow problem used to operate electric power systems.
△ Less
Submitted 3 January, 2021;
originally announced January 2021.
-
Disjunctive linear separation conditions and mixed-integer formulations for aircraft conflict resolution
Authors:
Fernando H. C. Dias,
Hassan Hijazi,
David Rey
Abstract:
We address the aircraft conflict resolution problem in air traffic control. We introduce new mixed-integer programming formulations for aircraft conflict resolution with speed, heading and altitude control which are based on disjunctive linear separation conditions. We first examine the two-dimensional aircraft conflict resolution problem with speed and heading control represented as continuous de…
▽ More
We address the aircraft conflict resolution problem in air traffic control. We introduce new mixed-integer programming formulations for aircraft conflict resolution with speed, heading and altitude control which are based on disjunctive linear separation conditions. We first examine the two-dimensional aircraft conflict resolution problem with speed and heading control represented as continuous decision variables. We show that the proposed disjunctive linear separation conditions are equivalent to the traditional nonlinear conditions for aircraft separation. Further, we characterize conflict-free pairwise aircraft trajectories and propose a simple pre-processing algorithm to identify aircraft pairs which are either always conflict-free, or which cannot be separated using speed and heading control only. We then incorporate altitude control and propose a lexicographic optimization formulation that aims to minimize the number of flight level changes before resolving outstanding conflicts via two-dimensional velocity control. The proposed mixed-integer programming formulations are nonconvex, and we propose convex relaxations, decomposition methods and constraint generation algorithms to solve the two-dimensional and lexicographic optimization formulations to guaranteed optimality. Numerical experiments on four types of conflict resolution benchmarking instances are conducted to test the performance of the proposed mixed-integer formulations. Further, the proposed disjunctive formulations are compared against state-of-the-art formulations based on the so-called shadow separation condition. Our numerical results show that the proposed disjunctive linear separation conditions outperform existing formulations in the literature and can solve significantly more instances to global optimality. For reproducibility purposes, all formulations and instances are made available on a public repository.
△ Less
Submitted 27 August, 2020; v1 submitted 29 November, 2019;
originally announced November 2019.
-
Proving Global Optimality of ACOPF Solutions
Authors:
S. Gopinath,
H. L. Hijazi,
T. Weisser,
H. Nagarajan,
M. Yetkin,
K. Sundar,
R. W. Bent
Abstract:
We present our latest contributions in terms of mathematical modeling and algorithm development for the global optimization of the ACOPF problem. These contributions allow us to close the optimality gap on a number of open instances in the PGLIB and NESTA benchmark libraries. This is achieved by combining valid cut generation with semidefinite programming-based bound tightening. The mathematical f…
▽ More
We present our latest contributions in terms of mathematical modeling and algorithm development for the global optimization of the ACOPF problem. These contributions allow us to close the optimality gap on a number of open instances in the PGLIB and NESTA benchmark libraries. This is achieved by combining valid cut generation with semidefinite programming-based bound tightening. The mathematical formulations along with the solution algorithms are implemented in the modeling framework Gravity (www.gravityopt.com), an open-source platform for reproducible numerical experiments.
△ Less
Submitted 19 February, 2020; v1 submitted 8 October, 2019;
originally announced October 2019.
-
Convex Hull Formulations for Mixed-Integer Multilinear Functions
Authors:
Harsha Nagarajan,
Kaarthik Sundar,
Hassan Hijazi,
Russell Bent
Abstract:
In this paper, we present convex hull formulations for a mixed-integer, multilinear term/function (MIMF) that features products of multiple continuous and binary variables. We develop two equivalent convex relaxations of an MIMF and study their polyhedral properties in their corresponding higher-dimensional spaces. We numerically observe that the proposed formulations consistently perform better t…
▽ More
In this paper, we present convex hull formulations for a mixed-integer, multilinear term/function (MIMF) that features products of multiple continuous and binary variables. We develop two equivalent convex relaxations of an MIMF and study their polyhedral properties in their corresponding higher-dimensional spaces. We numerically observe that the proposed formulations consistently perform better than state-of-the-art relaxation approaches.
△ Less
Submitted 29 July, 2018;
originally announced July 2018.
-
Juniper: An Open-Source Nonlinear Branch-and-Bound Solver in Julia
Authors:
Ole Kröger,
Carleton Coffrin,
Hassan Hijazi,
Harsha Nagarajan
Abstract:
Nonconvex mixed-integer nonlinear programs (MINLPs) represent a challenging class of optimization problems that often arise in engineering and scientific applications. Because of nonconvexities, these programs are typically solved with global optimization algorithms, which have limited scalability. However, nonlinear branch-and-bound has recently been shown to be an effective heuristic for quickly…
▽ More
Nonconvex mixed-integer nonlinear programs (MINLPs) represent a challenging class of optimization problems that often arise in engineering and scientific applications. Because of nonconvexities, these programs are typically solved with global optimization algorithms, which have limited scalability. However, nonlinear branch-and-bound has recently been shown to be an effective heuristic for quickly finding high-quality solutions to large-scale nonconvex MINLPs, such as those arising in infrastructure network optimization. This work proposes Juniper, a Julia-based open-source solver for nonlinear branch-and-bound. Leveraging the high-level Julia programming language makes it easy to modify Juniper's algorithm and explore extensions, such as branching heuristics, feasibility pumps, and parallelization. Detailed numerical experiments demonstrate that the initial release of Juniper is comparable with other nonlinear branch-and-bound solvers, such as Bonmin, Minotaur, and Knitro, illustrating that Juniper provides a strong foundation for further exploration in utilizing nonlinear branch-and-bound algorithms as heuristics for nonconvex MINLPs.
△ Less
Submitted 19 April, 2018;
originally announced April 2018.
-
Exploiting sparsity for the min k-partition problem
Authors:
Guanglei Wang,
Hassan Hijazi
Abstract:
The minimum k-partition problem is a challenging combinatorial problem with a diverse set of applications ranging from telecommunications to sports scheduling. It generalizes the max-cut problem and has been extensively studied since the late sixties. Strong integer formulations proposed in the literature suffer from a prohibitive number of valid inequalities and integer variables. In this work, w…
▽ More
The minimum k-partition problem is a challenging combinatorial problem with a diverse set of applications ranging from telecommunications to sports scheduling. It generalizes the max-cut problem and has been extensively studied since the late sixties. Strong integer formulations proposed in the literature suffer from a prohibitive number of valid inequalities and integer variables. In this work, we introduce two compact integer linear and semidefinite reformulations that exploit the sparsity of the underlying graph and develop fundamental results leveraging the power of chordal decomposition. Numerical experiments show that the new formulations improve upon state-of-the-art.
△ Less
Submitted 16 November, 2017; v1 submitted 1 September, 2017;
originally announced September 2017.
-
Invex Optimization Revisited
Authors:
Ksenia Bestuzheva,
Hassan Hijazi
Abstract:
Given a non-convex optimization problem, we study conditions under which every Karush-Kuhn-Tucker (KKT) point is a global optimizer. This property is known as KT-invexity and allows to identify the subset of problems where an interior point method always converges to a global optimizer. In this work, we provide necessary conditions for KT-invexity in n-dimensions and show that these conditions bec…
▽ More
Given a non-convex optimization problem, we study conditions under which every Karush-Kuhn-Tucker (KKT) point is a global optimizer. This property is known as KT-invexity and allows to identify the subset of problems where an interior point method always converges to a global optimizer. In this work, we provide necessary conditions for KT-invexity in n-dimensions and show that these conditions become sufficient in the two-dimensional case. As an application of our results, we study the Optimal Power Flow problem, showing that under mild assumptions on the variable's bounds, our new necessary and sufficient conditions are met for problems with two degrees of freedom.
△ Less
Submitted 5 July, 2017;
originally announced July 2017.
-
Strengthening the SDP Relaxation of AC Power Flows with Convex Envelopes, Bound Tightening, and Lifted Nonlinear Cuts
Authors:
Carleton Coffrin,
Hassan Hijazi,
Pascal Van Hentenryck
Abstract:
This paper considers state-of-the-art convex relaxations for the AC power flow equations and introduces new valid cuts based on convex envelopes and lifted nonlinear constraints. These valid linear inequalities strengthen existing semidefinite and quadratic programming relaxations and dominate existing cuts proposed in the litterature. Together with model intersections and bound tightening, the ne…
▽ More
This paper considers state-of-the-art convex relaxations for the AC power flow equations and introduces new valid cuts based on convex envelopes and lifted nonlinear constraints. These valid linear inequalities strengthen existing semidefinite and quadratic programming relaxations and dominate existing cuts proposed in the litterature. Together with model intersections and bound tightening, the new linear cuts close 8 of the remaining 16 open test cases in the NESTA archive for the AC Optimal Power Flow problem.
△ Less
Submitted 4 January, 2016; v1 submitted 14 December, 2015;
originally announced December 2015.
-
Efficient Dynamic Compressor Optimization in Natural Gas Transmission Systems
Authors:
Terrence W. K. Mak,
Pascal Van Hentenryck,
Anatoly Zlotnik,
Hassan Hijazi,
Russell Bent
Abstract:
The growing reliance of electric power systems on gas-fired generation to balance intermittent sources of renewable energy has increased the variation and volume of flows through natural gas transmission pipelines. Adapting pipeline operations to maintain efficiency and security under these new conditions requires optimization methods that account for transients and that can quickly compute soluti…
▽ More
The growing reliance of electric power systems on gas-fired generation to balance intermittent sources of renewable energy has increased the variation and volume of flows through natural gas transmission pipelines. Adapting pipeline operations to maintain efficiency and security under these new conditions requires optimization methods that account for transients and that can quickly compute solutions in reaction to generator re-dispatch. This paper presents an efficient scheme to minimize compression costs under dynamic conditions where deliveries to customers are described by time-dependent mass flow. The optimization scheme relies on a compact representation of gas flow physics, a trapezoidal discretization in time and space, and a two-stage approach to minimize energy costs and maximize smoothness. The resulting large-scale nonlinear programs are solved using a modern interior-point method. The proposed optimization scheme is validated against an integration of dynamic equations with adaptive time-stepping, as well as a recently proposed state-of-the-art optimal control method. The comparison shows that the solutions are feasible for the continuous problem and also practical from an operational standpoint. The results also indicate that our scheme provides at least an order of magnitude reduction in computation time relative to the state-of-the-art and scales to large gas transmission networks with more than 6000 kilometers of total pipeline.
△ Less
Submitted 23 November, 2015;
originally announced November 2015.
-
Polynomial SDP Cuts for Optimal Power Flow
Authors:
Hassan Hijazi,
Carleton Coffrin,
Pascal Van Hentenryck
Abstract:
The use of convex relaxations has lately gained considerable interest in Power Systems. These relaxations play a major role in providing global optimality guarantees for non-convex optimization problems. For the Optimal Power Flow (OPF) problem, the Semi-Definite Programming (SDP) relaxation is known to produce tight lower bounds. Unfortunately, SDP solvers still suffer from a lack of scalability.…
▽ More
The use of convex relaxations has lately gained considerable interest in Power Systems. These relaxations play a major role in providing global optimality guarantees for non-convex optimization problems. For the Optimal Power Flow (OPF) problem, the Semi-Definite Programming (SDP) relaxation is known to produce tight lower bounds. Unfortunately, SDP solvers still suffer from a lack of scalability. In this work, we introduce a new set of polynomial SDP-based constraints, strengthening weaker quadratic convex relaxations. The SDP cuts, expressed as polynomial constraints, can be handled by standard Nonlinear Programming solvers, enjoying better stability and computational efficiency. The new cut-generation procedure benefits from recent results on tree-decomposition methods, reducing the dimension of the underlying SDP matrices. As a side result, we present the first formulation of Kirchhoff's Voltage Law in the SDP space and reveal the existing link between these cycle constraints and the original SDP relaxation for three dimensional matrices. Numerical results on state-of-the- art benchmarks show a significant gain both in computational efficiency and optimality bound quality.
△ Less
Submitted 27 October, 2015;
originally announced October 2015.
-
Network Flow and Copper Plate Relaxations for AC Transmission Systems
Authors:
Carleton Coffrin,
Hassan L. Hijazi,
Pascal Van Hentenryck
Abstract:
Nonlinear convex relaxations of the power flow equations and, in particular, the Semi-Definite Programming (SDP), Convex Quadratic (QC), and Second-Order Cone (SOC) relaxations, have attracted significant interest in recent years. Thus far, little attention has been given to simpler linear relaxations of the power flow equations, which may bring significant performance gains at the cost of model a…
▽ More
Nonlinear convex relaxations of the power flow equations and, in particular, the Semi-Definite Programming (SDP), Convex Quadratic (QC), and Second-Order Cone (SOC) relaxations, have attracted significant interest in recent years. Thus far, little attention has been given to simpler linear relaxations of the power flow equations, which may bring significant performance gains at the cost of model accuracy. To fill the gap, this paper develops two intuitive linear relaxations of the power flow equations, one based on classic network flow models (NF) and another inspired by copper plate approximations (CP). Theoretical results show that the proposed NF model is a relaxation of the established nonlinear SOC model and the CP model is a relaxation of the NF model. Consequently, considering the linear NF and CP relaxations alongside the established nonlinear relaxations (SDP, QC, SOC) provides a rich variety of tradeoffs between the relaxation accuracy and performance.
△ Less
Submitted 12 November, 2015; v1 submitted 17 June, 2015;
originally announced June 2015.
-
DistFlow Extensions for AC Transmission Systems
Authors:
Carleton Coffrin,
Hassan L. Hijazi,
Pascal Van Hentenryck
Abstract:
Convex relaxations of the power flow equations and, in particular, the Semi-Definite Programming (SDP), Second-Order Cone (SOC), and Convex DistFlow (CDF) relaxations, have attracted significant interest in recent years. Thus far, studies of the CDF model and its connection to the other relaxations have been limited to power distribution systems, which omit several parameters necessary for modelin…
▽ More
Convex relaxations of the power flow equations and, in particular, the Semi-Definite Programming (SDP), Second-Order Cone (SOC), and Convex DistFlow (CDF) relaxations, have attracted significant interest in recent years. Thus far, studies of the CDF model and its connection to the other relaxations have been limited to power distribution systems, which omit several parameters necessary for modeling transmission systems. To increase the applicability of the CDF relaxation, this paper develops an extended CDF model that is suitable for transmission systems by incorporating bus shunts, line charging, and transformers. Additionally, a theoretical result shows that the established equivalence of the SOC and CDF models for distribution systems also holds in this transmission system extension.
△ Less
Submitted 2 July, 2018; v1 submitted 27 May, 2015;
originally announced June 2015.
-
The QC Relaxation: Theoretical and Computational Results on Optimal Power Flow
Authors:
Carleton Coffrin,
Hassan L. Hijazi,
Pascal Van Hentenryck
Abstract:
Convex relaxations of the power flow equations and, in particular, the Semi-Definite Programming (SDP) and Second-Order Cone (SOC) relaxations, have attracted significant interest in recent years. The Quadratic Convex (QC) relaxation is a departure from these relaxations in the sense that it imposes constraints to preserve stronger links between the voltage variables through convex envelopes of th…
▽ More
Convex relaxations of the power flow equations and, in particular, the Semi-Definite Programming (SDP) and Second-Order Cone (SOC) relaxations, have attracted significant interest in recent years. The Quadratic Convex (QC) relaxation is a departure from these relaxations in the sense that it imposes constraints to preserve stronger links between the voltage variables through convex envelopes of the polar representation. This paper is a systematic study of the QC relaxation for AC Optimal Power Flow with realistic side constraints. The main theoretical result shows that the QC relaxation is stronger than the SOC relaxation and neither dominates nor is dominated by the SDP relaxation. In addition, comprehensive computational results show that the QC relaxation may produce significant improvements in accuracy over the SOC relaxation at a reasonable computational cost, especially for networks with tight bounds on phase angle differences. The QC and SOC relaxations are also shown to be significantly faster and reliable compared to the SDP relaxation given the current state of the respective solvers.
△ Less
Submitted 29 July, 2015; v1 submitted 27 February, 2015;
originally announced February 2015.