ResearchTrend.AI
  • Papers
  • Communities
  • Events
  • Blog
  • Pricing
Papers
Communities
Social Events
Terms and Conditions
Pricing
Parameter LabParameter LabTwitterGitHubLinkedInBlueskyYoutube

© 2025 ResearchTrend.AI, All rights reserved.

  1. Home
  2. Papers
  3. 2207.03880
62
2

Constrained Training of Neural Networks via Theorem Proving

8 July 2022
Mark Chevallier
Matthew Whyte
Jacques D. Fleuriot
ArXiv (abs)PDFHTML
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 (LTLf_ff​) 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 L\mathcal{L}L that we formally prove to be sound, and differentiable to a function dLd\mathcal{L}dL. We subsequently use Isabelle's automatic code generation mechanism to produce OCaml versions of LTLf_ff​, L\mathcal{L}L and dLd\mathcal{L}dL 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.

View on arXiv
Comments on this paper