用形式化方法让神经符号模型自动满足逻辑约束。
Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces
- 基于张量的时序逻辑形式化，确保逻辑表达准确
- 设计可微损失函数，使模型自动满足预设逻辑条件
- 自动生成与PyTorch兼容代码，适合安全关键应用
我们提出了线性时序逻辑在有限轨迹（LTLf）上的张量语义新形式化，并在定理证明器Isabelle/HOL中完成正确性证明。通过定义并验证LTLf约束的可微损失函数，将该形式化集成到神经符号学习流程中，自动生成可与PyTorch集成的实现代码。实验表明，该方法能使模型在训练过程中满足预设的逻辑约束。本方法提供了一个完全严谨的约束训练框架，避免了直接在Python等‘不安全’语言中手动实现逻辑带来的诸多风险，同时保持了实现效率。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。