GradSTL：面向神经符号推理与学习的全方位信号时序逻辑
计算机科学中的逻辑
2025-08-07 v1
摘要
我们提出了 GradSTL——第一个完全全方位的信号时序逻辑（STL）实现，适用于神经符号学习集成。在具体方面，GradSTL 能够成功地对任何信号上的任何 STL 约束进行评估，无论其采样方式如何。我们的采用经过形式验证的 method specifies smooth STL semantics over tensors, 并对其导数函数的 soundness 和 correctness 进行形式证明。我们的实现是从该形式化自动生成的，无需手动编码，确保按构造方式正确。我们通过一个案例研究表明，使用我们的实现，一个神经符号过程能够学习满足预先指定的 STL 约束。我们的 method 为将信号时序逻辑与梯度下降集成提供了高度严谨的基础。
引用
@article{arxiv.2508.04438,
title = {GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning},
author = {Mark Chevallier and Filip Smola and Richard Schmoetten and Jacques D. Fleuriot},
journal= {arXiv preprint arXiv:2508.04438},
year = {2025}
}
备注
Accepted for presentation at TIME 2025