# Constrained Training of Neural Networks via Theorem Proving

arXiv: https://arxiv.org/abs/2207.03880 · HTML: https://mlsanity.com/paper/2207.03880/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 15 of its 35 references that are in the map.
- First posted on arXiv 8 Jul 2022.

## Builds on (most cited first, 15 of 15)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Soft-DTW: a Differentiable Loss Function for Time-Series](https://mlsanity.com/paper/1703.01541/) (2017)
- [A Semantic Loss Function for Deep Learning with Symbolic Knowledge](https://mlsanity.com/paper/1711.11157/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Supersizing Self-supervision: Learning to Grasp from 50K Tries and 700 Robot Hours](https://mlsanity.com/paper/1509.06825/) (2015)
- [Logic Tensor Networks](https://mlsanity.com/paper/2012.13635/) (2020)
- [Harnessing Deep Neural Networks with Logic Rules](https://mlsanity.com/paper/1603.06318/) (2016)
- [Label-Free Supervision of Neural Networks with Physics and Domain Knowledge](https://mlsanity.com/paper/1609.05566/) (2016)
- [LTL2Action: Generalizing LTL Instructions for Multi-Task RL](https://mlsanity.com/paper/2102.06858/) (2021)
- [Augmenting Neural Networks with First-order Logic](https://mlsanity.com/paper/1906.06298/) (2019)
- [Encoding formulas as deep networks: Reinforcement learning for zero-shot execution of LTL formulas](https://mlsanity.com/paper/2006.01110/) (2020)
- [Elaborating on Learned Demonstrations with Temporal Logic Specifications](https://mlsanity.com/paper/2002.00784/) (2020)

## Abstract (arXiv)

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) 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 that we formally prove to be sound, and differentiable to a function dL. We subsequently use Isabelle's automatic code generation mechanism to produce OCaml versions of LTLf, L and 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.