Verification and Validation of Convex Optimization Algorithms for Model Predictive Control

• URL: http://arxiv.org/abs/2005.12588v1
• Date: Tue, 26 May 2020 09:18:14 GMT
• Title: Verification and Validation of Convex Optimization Algorithms for Model Predictive Control
• Authors: Rapha\"el Cohen, Eric F\'eron, Pierre-Lo\"ic Garoche (ENAC)
• Abstract summary: This article discusses the formal verification of the Ellipsoid method, a convex optimization algorithm, and its code implementation. The applicability and limitations of those code properties and proofs are presented as well. Modifications to the algorithm are presented which can be used to control its numerical stability.
• Score: 1.5322124183968633
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Advanced embedded algorithms are growing in complexity and they are an essential contributor to the growth of autonomy in many areas. However, the promise held by these algorithms cannot be kept without proper attention to the considerably stronger design constraints that arise when the applications of interest, such as aerospace systems, are safety-critical. Formal verification is the process of proving or disproving the ''correctness'' of an algorithm with respect to a certain mathematical description of it by means of a computer. This article discusses the formal verification of the Ellipsoid method, a convex optimization algorithm, and its code implementation as it applies to receding horizon control. Options for encoding code properties and their proofs are detailed. The applicability and limitations of those code properties and proofs are presented as well. Finally, floating-point errors are taken into account in a numerical analysis of the Ellipsoid algorithm. Modifications to the algorithm are presented which can be used to control its numerical stability.

Related papers

• Accelerated zero-order SGD under high-order smoothness and overparameterized regime [79.85163929026146]
  We present a novel gradient-free algorithm to solve convex optimization problems. Such problems are encountered in medicine, physics, and machine learning. We provide convergence guarantees for the proposed algorithm under both types of noise.
  arXiv  Detail & Related papers  (2024-11-21T10:26:17Z)
• Homomorphically encrypted gradient descent algorithms for quadratic programming [3.185870720907055]
  We numerically analyze the applicability of gradient descent algorithms to solve quadratic programming in a homomorphic encryption setup. The paper shows firsthand the feasibility of homomorphically encrypted gradient descent algorithms.
  arXiv  Detail & Related papers  (2023-09-04T12:25:14Z)
• Interpretable Anomaly Detection via Discrete Optimization [1.7150329136228712]
  We propose a framework for learning inherently interpretable anomaly detectors from sequential data. We show that this problem is computationally hard and develop two learning algorithms based on constraint optimization. Using a prototype implementation, we demonstrate that our approach shows promising results in terms of accuracy and F1 score.
  arXiv  Detail & Related papers  (2023-03-24T16:19:15Z)
• Accelerated First-Order Optimization under Nonlinear Constraints [73.2273449996098]
  We exploit between first-order algorithms for constrained optimization and non-smooth systems to design a new class of accelerated first-order algorithms. An important property of these algorithms is that constraints are expressed in terms of velocities instead of sparse variables.
  arXiv  Detail & Related papers  (2023-02-01T08:50:48Z)
• Fast and Robust Non-Rigid Registration Using Accelerated Majorization-Minimization [35.66014845211251]
  Non-rigid registration, which deforms a source shape in a non-rigid way to align with a target shape, is a classical problem in computer vision. Existing methods typically adopt the $ell_p$ type robust norm to measure the alignment error and regularize the smoothness of deformation. We propose a formulation for robust non-rigid registration based on a globally smooth robust norm for alignment and regularization.
  arXiv  Detail & Related papers  (2022-06-07T16:00:33Z)
• Regret Bounds for Expected Improvement Algorithms in Gaussian Process Bandit Optimization [63.8557841188626]
  The expected improvement (EI) algorithm is one of the most popular strategies for optimization under uncertainty. We propose a variant of EI with a standard incumbent defined via the GP predictive mean. We show that our algorithm converges, and achieves a cumulative regret bound of $mathcal O(gamma_TsqrtT)$.
  arXiv  Detail & Related papers  (2022-03-15T13:17:53Z)
• Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
  This paper addresses learning safe output feedback control laws from partial observations of expert demonstrations. We first propose robust output control barrier functions (ROCBFs) as a means to guarantee safety. We then formulate an optimization problem to learn ROCBFs from expert demonstrations that exhibit safe system behavior.
  arXiv  Detail & Related papers  (2021-11-18T23:21:00Z)
• Finite-Bit Quantization For Distributed Algorithms With Linear Convergence [6.293059137498172]
  We study distributed algorithms for (strongly convex) composite optimization problems over mesh networks subject to quantized communications. A new quantizer coupled with a communication-efficient encoding scheme is proposed, which efficiently implements the Biased Compression (BC-)rule. Numerical results validate our theoretical findings and show that distributed algorithms equipped with the proposed quantizer have more favorable communication complexity than algorithms using existing quantization rules.
  arXiv  Detail & Related papers  (2021-07-23T15:31:31Z)
• Dynamic programming by polymorphic semiring algebraic shortcut fusion [1.9405875431318445]
  Dynamic programming (DP) is an algorithmic design paradigm for the efficient, exact solution of intractable, problems. This paper presents a rigorous algebraic formalism for systematically deriving DP algorithms, based on semiring.
  arXiv  Detail & Related papers  (2021-07-05T00:51:02Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  We investigate the problem of best-policy identification in discounted Markov Decision (MDPs) when the learner has access to a generative model. The advantages of state-of-the-art algorithms are discussed and illustrated.
  arXiv  Detail & Related papers  (2020-09-28T15:22:24Z)
• Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
  A fundamental component of neural network verification is the computation of bounds on the values their outputs can take. We propose a novel approach based on Lagrangian Decomposition. We show that we obtain bounds comparable with off-the-shelf solvers in a fraction of their running time.
  arXiv  Detail & Related papers  (2020-02-24T17:55:10Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.