A kernel function for Signal Temporal Logic formulae

从深度神经网络中提取多值逻辑公式

Extracting Formulae in Many-Valued Logic from Deep Neural Networks

本文将深度ReLU网络视为Łukasiewicz多值逻辑的电路对应物，提出一种适用于实值权重的MV逻辑公式提取算法，从而可从训练后的深度网络中获取可解释的逻辑公式。

面向逻辑公式的可逆语义保持嵌入

Towards Invertible Semantic-Preserving Embeddings of Logical Formulae

针对现有逻辑公式语义保持嵌入不可逆的问题，本研究基于图变分自编码器框架的深度架构，提出了一种可反转该嵌入的新型模型，经命题逻辑场景实验验证效果良好，推动了逻辑学习中连续优化的应用。

Graph Neural Reasoning May Fail in Certifying Boolean Unsatisfiability

It is feasible and practically-valuable to bridge the characteristics between graph neural networks (GNNs) and logical reasoning. Despite considerable efforts and successes witnessed to solve Boolean satisfiability (SAT), it remains a mystery of GNN-based solvers for more complex predicate logic formulae. In this work, we conjectures with some evidences, that generally-defined GNNs present several limitations to certify the unsatisfiability (UNSAT) in Boolean formulae. It implies that GNNs may probably fail in learning the logical reasoning tasks if they contain proving UNSAT as the sub-proble…

Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes

We introduce a similarity function on formulae of signal temporal logic (STL). It comes in the form of a kernel function, well known in machine learning as a conceptually and computationally efficient tool. The corresponding kernel trick allows us to circumvent the complicated process of feature extraction, i.e. the (typically manual) effort to identify the decisive properties of formulae so that learning can be applied. We demonstrate this consequence and its advantages on the task of predicting (quantitative) satisfaction of STL formulae on stochastic processes: Using our kernel and the kern…

使用 Transformers 和 Mamba 学习估计线性时序逻辑中的系统规约

Learning to Estimate System Specifications in Linear Temporal Logic using Transformers and Mamba

本文提出基于自回归的Transformer和Mamba架构，从系统轨迹生成线性时序逻辑公式以解决规约挖掘问题，并设计了独特性量化指标与语法约束算法，以极低计算成本生成正确且独特的公式。

以星为导：通过时序逻辑语义实现时间序列上的可解释概念学习

Guided by Stars: Interpretable Concept Learning Over Time Series via Temporal Logic Semantics

本文提出神经符号框架STELLE，通过将时间序列嵌入时序逻辑概念空间，在分类的同时提供局部与全局可解释性，并在多个基准上验证了其准确性与解释的忠实性。