Constrained Training of Neural Networks via Theorem Proving

TL;DR

This paper presents a formal, theorem-proving-based method for training neural networks with temporal logical constraints, ensuring rigor and safety in the specification and enforcement of constraints during training.

Contribution

It formalizes a deep embedding of linear temporal logic in Isabelle, proves the soundness of a corresponding loss function, and integrates it with PyTorch for constrained neural network training.

Findings

Effective training with obstacle avoidance and patrolling constraints

Rigorous formalization reduces risks of ad-hoc implementations

Automated code generation ensures correctness of logical components

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.