English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We introduce a theorem proving approach to the specification and generationof temporal logical constraints for training neural networks. We formalise adeep embedding of linear temporal logic over finite traces (LTL$_f$) and anassociated evaluation function characterising its semantics within thehigher-order logic of the Isabelle theorem prover. We then proceed to formalisea loss function $\mathcal{L}$ that we formally prove to be sound, anddifferentiable to a function $d\mathcal{L}$. We subsequently use Isabelle'sautomatic code generation mechanism to produce OCaml versions of LTL$_f$,$\mathcal{L}$ and $d\mathcal{L}$ that we integrate with PyTorch via OCamlbindings for Python. We show that, when used for training in an existing deeplearning framework for dynamic movement, our approach produces expected resultsfor common movement specification patterns such as obstacle avoidance andpatrolling. The distinctive benefit of our approach is the fully rigorousmethod for constrained training, eliminating many of the risks inherent toad-hoc implementations of logical aspects directly in an "unsafe" programminglanguage such as Python.

Constrained Training of Neural Networks via Theorem Proving