Program verification offers a framework for ensuring program correctness and
therefore systematically eliminating different classes of bugs. Inferring loop invariants is one of the main challenges behind automated verification of real-world
programs which often contain many loops. In this paper, we present Continuous Logic Network (CLN), a novel neural architecture for automatically learning
loop invariants directly from program execution traces. Unlike existing neural networks, CLNs can learn precise and explicit representations of formulas in Satisfiability Modulo Theories (SMT) for loop invariants from program execution traces.
We develop a new sound and complete semantic mapping for assigning SMT formulas to continuous truth values that allows CLNs to be trained efficiently. We use
CLNs to implement a new inference system for loop invariants, CLN2INV, that
significantly outperforms existing approaches on the popular Code2Inv dataset.
CLN2INV is the first tool to solve all 124 theoretically solvable problems in the
Code2Inv dataset. Moreover, CLN2INV takes only 1.1 seconds on average for
each problem, which is 40× faster than existing approaches. We further demonstrate that CLN2INV can even learn 12 significantly more complex loop invariants
than the ones required for the Code2Inv dataset.
more »
« less
Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks
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 loop invariants. However, applying data-driven inference to nonlinear loop invariants is challenging due to the large numbers of and large magnitudes of high-order terms, the potential for overfitting on a small number of samples, and the large space of possible nonlinear 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 the 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.
more »
« less
- Award ID(s):
- 1918400
- NSF-PAR ID:
- 10164831
- Date Published:
- Journal Name:
- Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation
- ISSN:
- 1531-7102
- Page Range / eLocation ID:
- 106-120
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
We introduce Flux, which shows how logical refinements can work hand in glove with Rust's ownership mechanisms to yield ergonomic type-based verification of low-level pointer manipulating programs. First, we design a novel refined type system for Rust that indexes mutable locations, with pure (immutable) values that can appear in refinements, and then exploits Rust's ownership mechanisms to abstract sub-structural reasoning about locations within Rust's polymorphic type constructors, while supporting strong updates. We formalize the crucial dependency upon Rust's strong aliasing guarantees by exploiting the Stacked Borrows aliasing model to prove that "well-borrowed evaluations of well-typed programs do not get stuck". Second, we implement our type system in Flux, a plug-in to the Rust compiler that exploits the factoring of complex invariants into types and refinements to efficiently synthesize loop annotations-including complex quantified invariants describing the contents of containers-via liquid inference. Third, we evaluate Flux with a benchmark suite of vector manipulating programs and parts of a previously verified secure sandboxing library to demonstrate the advantages of refinement types over program logics as implemented in the state-of-the-art Prusti verifier. While Prusti's more expressive program logic can, in general, verify deep functional correctness specifications, for the lightweight but ubiquitous and important verification use-cases covered by our benchmarks, liquid typing makes verification ergonomic by slashing specification lines by a factor of two, verification time by an order of magnitude, and annotation overhead from up to 24% of code size (average 14%), to nothing at all.more » « less
-
Shoham, Sharon ; Vizel, Yakir (Ed.)Morgan and McIver’s weakest pre-expectation framework is one of the most well-established methods for deductive verification of probabilistic programs. Roughly, the idea is to generalize binary state assertions to real-valued expectations, which can measure expected values of probabilistic program quantities. While loop-free programs can be analyzed by mechanically transforming expectations, verifying loops usually requires finding an invariant expectation, a difficult task. We propose a new view of invariant expectation synthesis as a regression problem: given an input state, predict the average value of the post-expectation in the output distribution. Guided by this perspective, we develop the first data-driven invariant synthesis method for probabilistic programs. Unlike prior work on probabilistic invariant inference, our approach can learn piecewise continuous invariants without relying on template expectations. We also develop a data-driven approach to learn sub-invariants from data, which can be used to upper- or lower-bound expected values. We implement our approaches and demonstrate their effectiveness on a variety of benchmarks from the probabilistic programming literature.more » « less
-
We use deep neural networks to machine learn correlations betweenknot invariants in various dimensions. The three-dimensional invariantof interest is the Jones polynomial J(q) J ( q ) ,and the four-dimensional invariants are the Khovanov polynomial \text{Kh}(q,t) Kh ( q , t ) ,smooth slice genus g g ,and Rasmussen’s s s -invariant.We find that a two-layer feed-forward neural network can predict s s from \text{Kh}(q,-q^{-4}) Kh ( q , − q − 4 ) with greater than 99% 99 % accuracy. A theoretical explanation for this performance exists in knottheory via the now disproven knight move conjecture, which is obeyed byall knots in our dataset. More surprisingly, we find similar performancefor the prediction of s s from \text{Kh}(q,-q^{-2}) Kh ( q , − q − 2 ) ,which suggests a novel relationship between the Khovanov and Leehomology theories of a knot. The network predicts g g from \text{Kh}(q,t) Kh ( q , t ) with similarly high accuracy, and we discuss the extent to which themachine is learning s s as opposed to g g ,since there is a general inequality |s| ≤2g | s | ≤ 2 g .The Jones polynomial, as a three-dimensional invariant, is not obviouslyrelated to s s or g g ,but the network achieves greater than 95% 95 % accuracy in predicting either from J(q) J ( q ) .Moreover, similar accuracy can be achieved by evaluating J(q) J ( q ) at roots of unity. This suggests a relationship with SU(2) S U ( 2 ) Chern—Simons theory, and we review the gauge theory construction ofKhovanov homology which may be relevant for explaining the network’sperformance.more » « less
-
Traditional linear subspace-based reduced order models (LS-ROMs) can be used to significantly accelerate simulations in which the solution space of the discretized system has a small dimension (with a fast decaying Kolmogorov 𝑛-width). However, LS-ROMs struggle to achieve speed-ups in problems whose solution space has a large dimension, such as highly nonlinear problems whose solutions have large gradients. Such an issue can be alleviated by combining nonlinear model reduction with operator learning. Over the past decade, many nonlinear manifold-based reduced order models (NM-ROM) have been proposed. In particular, NM-ROMs based on deep neural networks (DNN) have received increasing interest. This work takes inspiration from adaptive basis methods and specifically focuses on developing an NM-ROM based on Convolutional Neural Network-based autoencoders (CNNAE) with iteration-dependent trainable kernels. Additionally, we investigate DNN-based and quadratic operator inference strategies between latent spaces. A strategy to perform vectorized implicit time integration is also proposed. We demonstrate that the proposed CNN-based NM-ROM, combined with DNN- based operator inference, generally performs better than commonly employed strategies (in terms of prediction accuracy) on a benchmark advection-dominated problem. The method also presents substantial gain in terms of training speed per epoch, with a training time about one order of magnitude smaller than the one associated with a state-of-the-art technique performing with the same level of accuracy.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1145/3385412.3385986
