Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)

• URL: http://arxiv.org/abs/2003.07959v4
• Date: Thu, 25 Jun 2020 16:43:51 GMT
• Title: Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)
• Abstract summary: We introduce a new neural architecture for general SMT learning, the Gated Continuous Logic Network (G-CLN) G-CLNs extend the Continuous Logic Network (CLN) architecture with gating units and dropout. We show G-CLNs have a convergence rate of $97.5%$ on quadratic problems, a $39.2%$ improvement over CLN models.
• Score: 19.87276407545565
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Verifying real-world programs often requires inferring loop invariants with nonlinear constraints. This is especially true in programs that perform many numerical operations, such as control systems for avionics or industrial plants. Recently, data-driven methods for loop invariant inference have shown promise, especially on linear invariants. However, applying data-driven inference to nonlinear loop invariants is challenging due to the large numbers of and magnitudes of high-order terms, the potential for overfitting on a small number of samples, and the large space of possible inequality bounds. In this paper, we introduce a new neural architecture for general SMT learning, the Gated Continuous Logic Network (G-CLN), and apply it to nonlinear loop invariant learning. G-CLNs extend the Continuous Logic Network (CLN) architecture with gating units and dropout, which allow the model to robustly learn general invariants over large numbers of terms. To address overfitting that arises from finite program sampling, we introduce fractional sampling---a sound relaxation of loop semantics to continuous functions that facilitates unbounded sampling on real domain. We additionally design a new CLN activation function, the Piecewise Biased Quadratic Unit (PBQU), for naturally learning tight inequality bounds. We incorporate these methods into a nonlinear loop invariant inference system that can learn general nonlinear loop invariants. We evaluate our system on a benchmark of nonlinear loop invariants and show it solves 26 out of 27 problems, 3 more than prior work, with an average runtime of 53.3 seconds. We further demonstrate the generic learning ability of G-CLNs by solving all 124 problems in the linear Code2Inv benchmark. We also perform a quantitative stability evaluation and show G-CLNs have a convergence rate of $97.5\%$ on quadratic problems, a $39.2\%$ improvement over CLN models.

Related papers

• LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference [10.534386090450276]
  We propose Incremental ICE, a novel learning framework for incremental synthesis.<n>Our framework integrates the incremental philosophy of IC3 into the general invariant learning framework ICE.<n>Under this framework, we instantiate a loop invariant synthesis tool, LimICE, which leverages LLMs to generate the ordered sequence of lemmas.
  arXiv  Detail & Related papers  (2026-07-30T02:50:09Z)
• Chebyshev-Augmented One-Shot Transfer Learning for PINNs on Nonlinear Differential Equations [0.794957965474334]
  Physics-Informed Neural Networks (PINNs) offer a flexible paradigm for solving differential equations by governing governing laws into the network.<n>A limitation is instance specificity: standard PINNs typically require retraining for each new forcing term, latent/initial condition, or nonlinear problems closed-form adaptation.<n>In this paper we address the class of nonlinearities amenable to one-shot PINN transfer by combining OTL with Chebyshev surrogates.
  arXiv  Detail & Related papers  (2026-05-02T22:49:37Z)
• Simultaneously Solving Infinitely Many LQ Mean Field Games In Hilbert Spaces: The Power of Neural Operators [11.756276506921976]
  Training neural operators (NOs) to learn the rules-to-equilibrium map from the problem data (rules'': dynamics and cost functionals) of LQ MFGs defined on separable Hilbert spaces to the corresponding equilibrium strategy.<n>An NO trained on a small number of randomly sampled rules reliably solves unseen LQ MFG variants, even in infinite-dimensional settings.<n>Our guarantee follows from three results: (i) local-Lipschitz estimates for the highly nonlinear rules-to-equilibrium map; (ii) a universal approximation theorem using NOs with a prespecified Lipschitz regularity;
  arXiv  Detail & Related papers  (2025-10-22T20:40:20Z)
• Quantum algorithms for general nonlinear dynamics based on the Carleman embedding [2.5272147028897476]
  We show that efficient quantum algorithms exist for a much wider class of nonlinear systems than previously known.<n>We also obtain several results related to the Poincar'e-Dulac theorem and diagonalization of the Car matrix.
  arXiv  Detail & Related papers  (2025-09-08T19:09:05Z)
• The Sample Complexity of Online Reinforcement Learning: A Multi-model Perspective [55.15192437680943]
  We study the sample complexity of online reinforcement learning for nonlinear dynamical systems with continuous state and action spaces. Our algorithms are likely to be useful in practice, due to their simplicity, the ability to incorporate prior knowledge, and their benign transient behavior.
  arXiv  Detail & Related papers  (2025-01-27T10:01:28Z)
• Efficient Interpretable Nonlinear Modeling for Multiple Time Series [5.448070998907116]
  This paper proposes an efficient nonlinear modeling approach for multiple time series. It incorporates nonlinear interactions among different time-series variables. Experimental results show that the proposed algorithm improves the identification of the support of the VAR coefficients in a parsimonious manner.
  arXiv  Detail & Related papers  (2023-09-29T11:42:59Z)
• Constrained Optimization via Exact Augmented Lagrangian and Randomized Iterative Sketching [55.28394191394675]
  We develop an adaptive inexact Newton method for equality-constrained nonlinear, nonIBS optimization problems. We demonstrate the superior performance of our method on benchmark nonlinear problems, constrained logistic regression with data from LVM, and a PDE-constrained problem.
  arXiv  Detail & Related papers  (2023-05-28T06:33:37Z)
• Gauss-Newton Temporal Difference Learning with Nonlinear Function Approximation [11.925232472331494]
  A Gauss-Newton Temporal Difference (GNTD) learning method is proposed to solve the Q-learning problem with nonlinear function approximation. In each iteration, our method takes one Gauss-Newton (GN) step to optimize a variant of Mean-Squared Bellman Error (MSBE) We validate our method via extensive experiments in several RL benchmarks, where GNTD exhibits both higher rewards and faster convergence than TD-type methods.
  arXiv  Detail & Related papers  (2023-02-25T14:14:01Z)
• A Fast Scale-Invariant Algorithm for Non-negative Least Squares with Non-negative Data [18.81091632124107]
  We show that the data itself is nonnegative as well, and we show that the nonnegativity in this case makes the problem easier. In particular, while the oracle complexity of unconstrained least squares problems necessarily scales with one of the data matrix constants, we show that nonnegative least squares problems with nonnegative data are solvable to multiplicative error.
  arXiv  Detail & Related papers  (2022-03-08T02:02:32Z)
• Towards Data-driven LQR with KoopmanizingFlows [8.133902705930327]
  We propose a novel framework for learning linear time-invariant (LTI) models for a class of continuous-time non-autonomous nonlinear dynamics. We learn a finite representation of the Koopman operator that is linear in controls while concurrently learning meaningful lifting coordinates.
  arXiv  Detail & Related papers  (2022-01-27T17:02:03Z)
• Training Recurrent Neural Networks by Sequential Least Squares and the Alternating Direction Method of Multipliers [0.20305676256390928]
  We propose the use of convex and twice-differentiable loss and regularization terms for determining optimal hidden network parameters. We combine sequential least squares with alternating direction multipliers. The performance of the algorithm is tested in a nonlinear system identification benchmark.
  arXiv  Detail & Related papers  (2021-12-31T08:43:04Z)
• The SKIM-FA Kernel: High-Dimensional Variable Selection and Nonlinear Interaction Discovery in Linear Time [26.11563787525079]
  We show how a kernel trick can reduce computation with suitable Bayesian models to O(# covariates) time for both variable selection and estimation. Our approach outperforms existing methods used for large, high-dimensional datasets.
  arXiv  Detail & Related papers  (2021-06-23T13:53:36Z)
• Hybrid Trilinear and Bilinear Programming for Aligning Partially Overlapping Point Sets [85.71360365315128]
  In many applications, we need algorithms which can align partially overlapping point sets are invariant to the corresponding corresponding RPM algorithm. We first show that the objective is a cubic bound function. We then utilize the convex envelopes of trilinear and bilinear monomial transformations to derive its lower bound. We next develop a branch-and-bound (BnB) algorithm which only branches over the transformation variables and runs efficiently.
  arXiv  Detail & Related papers  (2021-01-19T04:24:23Z)
• Learning the Linear Quadratic Regulator from Nonlinear Observations [135.66883119468707]
  We introduce a new problem setting for continuous control called the LQR with Rich Observations, or RichLQR. In our setting, the environment is summarized by a low-dimensional continuous latent state with linear dynamics and quadratic costs. Our results constitute the first provable sample complexity guarantee for continuous control with an unknown nonlinearity in the system model and general function approximation.
  arXiv  Detail & Related papers  (2020-10-08T07:02:47Z)
• Hardness of Random Optimization Problems for Boolean Circuits, Low-Degree Polynomials, and Langevin Dynamics [78.46689176407936]
  We show that families of algorithms fail to produce nearly optimal solutions with high probability. For the case of Boolean circuits, our results improve the state-of-the-art bounds known in circuit complexity theory.
  arXiv  Detail & Related papers  (2020-04-25T05:45:59Z)
• Neural Networks are Convex Regularizers: Exact Polynomial-time Convex Optimization Formulations for Two-layer Networks [70.15611146583068]
  We develop exact representations of training two-layer neural networks with rectified linear units (ReLUs) Our theory utilizes semi-infinite duality and minimum norm regularization.
  arXiv  Detail & Related papers  (2020-02-24T21:32:41Z)
• Multiscale Non-stationary Stochastic Bandits [83.48992319018147]
  We propose a novel multiscale changepoint detection method for the non-stationary linear bandit problems, called Multiscale-LinUCB. Experimental results show that our proposed Multiscale-LinUCB algorithm outperforms other state-of-the-art algorithms in non-stationary contextual environments.
  arXiv  Detail & Related papers  (2020-02-13T00:24:17Z)

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.