Constrained Training of Neural Networks via Theorem Proving

Mark Chevallier, Matthew Whyte, Jacques D. Fleuriot

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 te…