Constrained Training of Neural Networks via Theorem Proving

• URL: http://arxiv.org/abs/2207.03880v1
• Date: Fri, 8 Jul 2022 13:13:51 GMT
• Title: Constrained Training of Neural Networks via Theorem Proving
• Authors: Mark Chevallier, Matthew Whyte and Jacques D. Fleuriot
• Abstract summary: We formalise a deep embedding of linear temporal logic over finite traces (LTL$_f$) We then formalise a loss function $mathcalL$ that we formally prove to be sound, and differentiable to a function $dmathcalL$. We show that, when used for training in an existing deep learning framework for dynamic movement, our approach produces expected results for common movement specification patterns.
• Score: 0.2578242050187029
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce a theorem proving approach to the specification and generation of temporal logical constraints for training neural networks. We formalise a deep embedding of linear temporal logic over finite traces (LTL$_f$) and an associated evaluation function characterising its semantics within the higher-order logic of the Isabelle theorem prover. We then proceed to formalise a loss function $\mathcal{L}$ that we formally prove to be sound, and differentiable to a function $d\mathcal{L}$. We subsequently use Isabelle's automatic code generation mechanism to produce OCaml versions of LTL$_f$, $\mathcal{L}$ and $d\mathcal{L}$ that we integrate with PyTorch via OCaml bindings for Python. We show that, when used for training in an existing deep learning framework for dynamic movement, our approach produces expected results for common movement specification patterns such as obstacle avoidance and patrolling. The distinctive benefit of our approach is the fully rigorous method for constrained training, eliminating many of the risks inherent to ad-hoc implementations of logical aspects directly in an "unsafe" programming language such as Python.

Related papers

• 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)
• Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces [0.0]
  We present a novel formalisation of tensor semantics for linear temporal logic on finite traces (LTLf) We demonstrate that this formalisation can be integrated into a neurosymbolic learning process by defining and verifying a differentiable loss function for the constraints. We show that, by using this loss, the process learns to satisfy pre-specified logical constraints.
  arXiv  Detail & Related papers  (2025-01-23T14:43:12Z)
• Robust Stochastically-Descending Unrolled Networks [85.6993263983062]
  Deep unrolling is an emerging learning-to-optimize method that unrolls a truncated iterative algorithm in the layers of a trainable neural network. We show that convergence guarantees and generalizability of the unrolled networks are still open theoretical problems. We numerically assess unrolled architectures trained under the proposed constraints in two different applications.
  arXiv  Detail & Related papers  (2023-12-25T18:51:23Z)
• Robust Training and Verification of Implicit Neural Networks: A Non-Euclidean Contractive Approach [64.23331120621118]
  This paper proposes a theoretical and computational framework for training and robustness verification of implicit neural networks. We introduce a related embedded network and show that the embedded network can be used to provide an $ell_infty$-norm box over-approximation of the reachable sets of the original network. We apply our algorithms to train implicit neural networks on the MNIST dataset and compare the robustness of our models with the models trained via existing approaches in the literature.
  arXiv  Detail & Related papers  (2022-08-08T03:13:24Z)
• Learning Finite Linear Temporal Logic Specifications with a Specialized Neural Operator [0.0]
  We address the problem of learning a compact $mathsfLTL_f$ formula from labeled traces of system behavior. Our approach includes a specialized recurrent filter, designed to subsume $mathsfLTL_f$ temporal operators. Experiments on randomly generated $mathsfLTL_f$ formulas show Neural$mathsfLTL_f$ scales to larger formula sizes than existing approaches.
  arXiv  Detail & Related papers  (2021-11-07T18:51:02Z)
• Skew Orthogonal Convolutions [44.053067014796596]
  Training convolutional neural networks with a Lipschitz constraint under the $l_2$ norm is useful for provable adversarial robustness, interpretable gradients, stable training, etc. Methodabv allows us to train provably Lipschitz, large convolutional neural networks significantly faster than prior works.
  arXiv  Detail & Related papers  (2021-05-24T17:11:44Z)
• Reinforcement Learning with External Knowledge by using Logical Neural Networks [67.46162586940905]
  A recent neuro-symbolic framework called the Logical Neural Networks (LNNs) can simultaneously provide key-properties of both neural networks and symbolic logic. We propose an integrated method that enables model-free reinforcement learning from external knowledge sources.
  arXiv  Detail & Related papers  (2021-03-03T12:34:59Z)
• Learning Sign-Constrained Support Vector Machines [0.24466725954625884]
  We develop two optimization algorithms for minimizing the empirical risk under the sign constraints. One of the two algorithms is based on the projected gradient method, in which each iteration of the projected gradient method takes $O(nd)$ computational cost. We empirically demonstrate that the sign constraints are a promising technique when similarities to the training examples compose the feature vector.
  arXiv  Detail & Related papers  (2021-01-05T12:08:17Z)
• On Function Approximation in Reinforcement Learning: Optimism in the Face of Large State Spaces [208.67848059021915]
  We study the exploration-exploitation tradeoff at the core of reinforcement learning. In particular, we prove that the complexity of the function class $mathcalF$ characterizes the complexity of the function. Our regret bounds are independent of the number of episodes.
  arXiv  Detail & Related papers  (2020-11-09T18:32:22Z)
• Deep neural networks for inverse problems with pseudodifferential operators: an application to limited-angle tomography [0.4110409960377149]
  We propose a novel convolutional neural network (CNN) designed for learning pseudodifferential operators ($Psi$DOs) in the context of linear inverse problems. We show that, under rather general assumptions on the forward operator, the unfolded iterations of ISTA can be interpreted as the successive layers of a CNN. In particular, we prove that, in the case of LA-CT, the operations of upscaling, downscaling and convolution, can be exactly determined by combining the convolutional nature of the limited angle X-ray transform and basic properties defining a wavelet system.
  arXiv  Detail & Related papers  (2020-06-02T14:03:41Z)
• Stochastic Flows and Geometric Optimization on the Orthogonal Group [52.50121190744979]
  We present a new class of geometrically-driven optimization algorithms on the orthogonal group $O(d)$. We show that our methods can be applied in various fields of machine learning including deep, convolutional and recurrent neural networks, reinforcement learning, flows and metric learning.
  arXiv  Detail & Related papers  (2020-03-30T15:37:50Z)

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.