Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces

要約

我々は、定理証明器 Isabelle/HOL で実行される正しさの形式的証明とともに、有限トレース上の線形時相論理 (LTLf) のためのテンソル セマンティクスの新しい形式化を提示します。
LTLf 制約の微分可能な損失関数を定義して検証し、PyTorch と統合する実装を自動的に生成することで、この形式化を神経記号学習プロセスに統合できることを示します。
この損失を利用することで、プロセスが事前に指定された論理制約を満たすことを学習することを示します。
私たちのアプローチは、制約付きトレーニングのための完全に厳密なフレームワークを提供し、実装の効率を維持しながら、Python などの「安全でない」プログラミング言語で論理的側面をアドホックに手動で直接実装することに固有のリスクの多くを排除します。

要約(オリジナル)

We present a novel formalisation of tensor semantics for linear temporal logic on finite traces (LTLf), with formal proofs of correctness carried out in the theorem prover Isabelle/HOL. We demonstrate that this formalisation can be integrated into a neurosymbolic learning process by defining and verifying a differentiable loss function for the LTLf constraints, and automatically generating an implementation that integrates with PyTorch. We show that, by using this loss, the process learns to satisfy pre-specified logical constraints. Our approach offers a fully rigorous framework for constrained training, eliminating many of the inherent risks of ad-hoc, manual implementations of logical aspects directly in an ‘unsafe’ programming language such as Python, while retaining efficiency in implementation.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google