Formal verification of machine learning models has attracted attention recently, and significant progress has been made on proving simple properties like robustness to small perturbations of the input features. In this context, it has also been observed that folding the verification procedure into training makes it easier to train verifiably robust models. In this paper, we extend the applicability of verified training by extending it to (1) recurrent neural network architectures and (2) complex specifications that go beyond simple adversarial robustness, particularly specifications that capture temporal properties like requiring that a robot periodically visits a charging station or that a language model always produces sentences of bounded length. Experiments show that while models trained using standard training often violate desired specifications, our verified training method produces models that both perform well (in terms of test error or reward) and can be shown to be provably consistent with specifications.
Neural Network Verification for Temporal Properties and Sequence Generation Models This paper extends interval bound propagation to recurrent computation and auto-regressive models, introduces and extends Signal Temporal Logic for specifying temporal contraints, and provides proof that STL with bound propagation can ensure neural models conform to temporal specification. A way to train time-series regressors verifiably with respect to a set of rules defined by signal temporal logic, and work in deriving bound propagation rules for the STL language.