从数据中提取空间时间知识在许多应用中都很有用。重要的是,所获得的知识是人类解释的和适用于正式分析。在本文中,我们提出了一种方法,该方法列举神经网络以学习基于加权图的信号时间逻辑(WGSTL)公式的形式的空间时间特性。对于学习WGSTL公式,我们介绍了一种灵活的WGSTL公式结构,其中用户的偏好可以应用于推断的WGSTL公式中。在所提出的框架中,神经网络的每个神经元对应于柔性WGSTL公式结构中的子核。我们初始训练一个神经网络来学习WGSTL运营商,然后训练第二个神经网络以在灵活的WGSTL公式结构中学习参数。我们使用Covid-19数据集和雨量预测数据集来评估所提出的框架和算法的性能。我们将建议框架的性能与三个基线分类方法进行比较,包括K-Collest邻居,决策树,支持向量机和人工神经网络。所提出的框架获得的分类准确性与基线分类方法相当。
translated by 谷歌翻译
大多数现有的时间序列分类(TSC)模型缺乏可解释性,难以检查。可解释的机器学习模型可以帮助发现数据中的模式,并为域专家提供易于理解的见解。在这项研究中,我们提出了神经符号时间序列分类(NSTSC),这是一种利用信号时间逻辑(STL)和神经网络(NN)的神经符号模型,使用多视图数据表示并将模型表示为TSC任务人类可读,可解释的公式。在NSTSC中,每个神经元与符号表达相关,即STL(sub)公式。因此,NSTSC的输出可以解释为类似于自然语言的STL公式,描述了隐藏在数据中的时间和逻辑关系。我们提出了一个基于NSTSC的分类器,该分类器采用决策树方法来学习公式结构并完成多类TSC任务。 WSTL提出的平滑激活功能允许以端到端的方式学习模型。我们在来自UCR时间序列存储库中的小鼠和基准数据集的现实伤口愈合数据集上测试NSTSC,这表明NSTSC与最先进的模型实现了可比的性能。此外,NSTSC可以生成与域知识匹配的可解释公式。
translated by 谷歌翻译
学习数据的动态系统属性提供了重要的见解,帮助我们了解此类系统并减轻不良结果。在这项工作中,我们提出了一种从数据的正式逻辑规范学习时空时间(ST)属性的框架。我们介绍SVM-STL,信号信号时间逻辑(STL)的扩展,能够指定具有呈现时变空间模式的各种动态系统的空间和时间特性。我们的框架利用机器学习技术从空间模式序列给出的系统执行中学习SVM-STL规范。我们提供了处理标记和未标记数据的方法。此外,给定的系统要求以SVM-STL规范的形式,我们提供了一种参数合成方法,以找到最大化此类规格满意度的参数。我们的学习框架和参数合成方法在反应扩散系统的示例中展示。
translated by 谷歌翻译
网络物理系统中的实时和人为可解释的决策是一个重要但具有挑战性的任务,通常需要预测来自有限数据的未来可能的事件。在本文中,我们介绍了一个时间增量学习框架:给定具有共同时间范围的标记信号迹线的数据集,我们提出了一种方法来预测随时间递增地接收的信号的标签,称为前缀信号。前缀信号是当生成时被观察的信号,并且它们的时间长度短于信号的公共范围。我们介绍了一种基于决策树的决策树方法来生成来自给定数据集的有限数量的信号时间逻辑(STL)规范,并基于它们构造预测器。作为时间序列数据的二进制分类器,每个STL规范都会随着时间的推移捕获数据集的时间特性。通过将时间变量权重分配给STL公式来构建预测器。通过使用神经网络来学习权重,目的是最小化在给定数据集上定义的前缀信号的错误分类率。通过计算前缀信号的鲁棒性相对于每个STL公式的鲁棒性的加权之和来预测前缀信号的标签来预测前缀信号的标签。我们的算法的有效性和分类性能在城市驾驶和海军监测案例研究中进行了评估。
translated by 谷歌翻译
本文介绍了一个名为STLCG的技术,使用计算图计算信号时间逻辑(STL)公式的定量语义。 STLCG提供了一个平台,它可以将逻辑规范纳入从基于梯度的解决方案中受益的机器人问题。具体而言,STL是一种强大且表现力的正式语言,可以指定连续和混合系统产生的信号的空间和时间特性。 STL的定量语义提供了鲁棒性度量,即,信号满足或违反STL规范的量。在这项工作中,我们设计了一种系统方法,用于将STL鲁棒性公式转化为计算图形。通过这种表示,通过利用现成的自动差异化工具,我们能够通过STL稳健性公式有效地反向,因此可以实现具有许多基于梯度的方法的STL规范的自然且易于使用的STL规范集成。通过各种机器人应用的许多示例,我们证明STLCG是多功能的,计算效率,并且能够将人域知识纳入问题制定中。
translated by 谷歌翻译
我们演示了学习信号时间逻辑公式的第一个复发性神经网络体系结构,并介绍了公式推理方法的第一个系统比较。传统系统嵌入了许多未明确形式化的专业知识。有很大的兴趣学习表征此类系统理想行为的形式规格 - 即时逻辑中的公式,这些公式被系统的输出信号所满足。此类规格可用于更好地理解系统的行为并改善其下一次迭代的设计。以前的推断方法假设某些公式模板,或者对所有可能的模板进行了启发式枚举。这项工作提出了一种神经网络体系结构,该结构通过梯度下降来渗透公式结构,从而消除了施加任何特定模板的需求。它将公式结构和参数的学习结合在一个优化中。通过系统的比较,我们证明了该方法与列举和晶格方法相比,该方法达到相似或更好的错误分类率(MCR)。我们还观察到,不同的公式可以实现相似的MCR,从经验上证明了时间逻辑推断问题的不确定性。
translated by 谷歌翻译
In this paper, we propose a control synthesis method for signal temporal logic (STL) specifications with neural networks (NNs). Most of the previous works consider training a controller for only a given STL specification. These approaches, however, require retraining the NN controller if a new specification arises and needs to be satisfied, which results in large consumption of memory and inefficient training. To tackle this problem, we propose to construct NN controllers by introducing encoder-decoder structured NNs with an attention mechanism. The encoder takes an STL formula as input and encodes it into an appropriate vector, and the decoder outputs control signals that will meet the given specification. As the encoder, we consider three NN structures: sequential, tree-structured, and graph-structured NNs. All the model parameters are trained in an end-to-end manner to maximize the expected robustness that is known to be a quantitative semantics of STL formulae. We compare the control performances attained by the above NN structures through a numerical experiment of the path planning problem, showing the efficacy of the proposed approach.
translated by 谷歌翻译
时间序列数据分类对于自治系统(例如机器人和自动驾驶汽车)的分析和控制至关重要。最近已经提出了基于时间逻辑的学习算法作为此类数据的分类器。但是,当前的框架要么不准确,例如自动驾驶等现实应用程序,要么产生缺乏可解释性的漫长而复杂的公式。为了解决这些局限性,我们引入了一种新颖的学习方法,称为“增强简洁决策树(BCDTS)”,以生成表示为信号时间逻辑(STL)公式的二进制分类器。我们的算法利用简洁决策树(CDT)的合奏来改善分类性能,其中每个CDT都是由一组技术赋予的决策树,以生成更简单的公式并提高可解释性。我们的算法的有效性和分类性能在海军监视和城市驾驶案例研究中评估。
translated by 谷歌翻译
本文提出了一个算法框架,用于控制符合信号时间逻辑(STL)规范的连续动力系统的合成。我们提出了一种新型算法,以从STL规范中获得时间分配的有限自动机,并引入一个多层框架,该框架利用此自动机以空间和时间上指导基于采样的搜索树。我们的方法能够合成非线性动力学和多项式谓词功能的控制器。我们证明了算法的正确性和概率完整性,并说明了我们在几个案例研究中框架的效率和功效。我们的结果表明,在艺术状态下,速度的速度是一定的。
translated by 谷歌翻译
最近已经提出了几个查询和分数来解释对ML模型的个人预测。鉴于ML型号的灵活,可靠和易于应用的可解释性方法,我们预见了需要开发声明语言以自然地指定不同的解释性查询。我们以原则的方式通过源于逻辑,称为箔,允许表达许多简单但重要的解释性查询,并且可以作为更具表现力解释性语言的核心来实现这一语言。我们研究箔片查询的两类ML模型的计算复杂性经常被视为容易解释:决策树和OBDD。由于ML模型的可能输入的数量是尺寸的指数,因此箔评估问题的易易性是精细的,但是可以通过限制模型的结构或正在评估的箔片段来实现。我们还以高级声明语言包装的箔片的原型实施,并执行实验,表明可以在实践中使用这种语言。
translated by 谷歌翻译
人工智能代理必须从周围环境中学到学习,并了解所学习的知识,以便做出决定。虽然从数据的最先进的学习通常使用子符号分布式表示,但是使用用于知识表示的一阶逻辑语言,推理通常在更高的抽象级别中有用。结果,将符号AI和神经计算结合成神经符号系统的尝试已经增加。在本文中,我们呈现了逻辑张量网络(LTN),一种神经组织形式和计算模型,通过引入许多值的端到端可分别的一阶逻辑来支持学习和推理,称为真实逻辑作为表示语言深入学习。我们表明LTN为规范提供了统一的语言,以及多个AI任务的计算,如数据聚类,多标签分类,关系学习,查询应答,半监督学习,回归和嵌入学习。我们使用TensorFlow2的许多简单的解释例实施和说明上述每个任务。关键词:神经组音恐怖症,深度学习和推理,许多值逻辑。
translated by 谷歌翻译
本文提出了一种新的方法,用于设计对自主系统的神经网络(NN)控制器的验证组合,并具有线性时间逻辑(LTL)公式捕获的任务。特别是,LTL公式要求系统以时间/逻辑顺序到达并避免某些区域。我们假设该系统配备了有限的训练有素的NN控制器。每个控制器都经过培训,以便它可以将系统推向特定的感兴趣区域,同时避免其他人。我们的目标是检查是否存在训练有素的NN控制器的时间组成(如果是这样,则将其计算)产生复合系统行为,以满足属于给定集合的任何初始系统状态的用户指定的LTL任务。为了解决这个问题,我们提出了一种依赖于自动机理论的新颖集成以及最近提出的NN控制系统的可及性分析工具的新方法。 We note that the proposed method can be applied to other controllers, not necessarily modeled by NNs, by appropriate selection of the reachability analysis tool.由于缺乏健壮性,我们专注于NN控制器。提出的方法在航空车的导航任务上得到了证明。
translated by 谷歌翻译
有限的线性时间逻辑($ \ mathsf {ltl} _f $)是一种强大的正式表示,用于建模时间序列。我们解决了学习Compact $ \ Mathsf {ltl} _f $ formul的问题,从标记的系统行为的痕迹。我们提出了一部小说神经网络运营商,并评估结果架构,神经$ \ mathsf {ltl} _f $。我们的方法包括专用复发过滤器,旨在满足$ \ Mathsf {ltl} _f $ temporal运算符,以学习痕迹的高度准确的分类器。然后,它离散地激活并提取由学习权重表示的真相表。此实话表将转换为符号形式并作为学习公式返回。随机生成$ \ Mathsf {LTL} _F $公式显示神经$ \ MATHSF {LTL} _F $尺寸,比现有方法更大,即使在存在噪声时也保持高精度。
translated by 谷歌翻译
自动化车辆(AV)在很大程度上取决于强大的感知系统。评估视觉系统的当前方法主要关注逐帧性能。当在AV中使用时,这种评估方法似乎不足以评估感知子系统的性能。在本文中,我们提出了一种逻辑(称为时空感知逻辑(STPL)),该逻辑同时使用了空间和时间方式。STPL可以使用空间和时间关系来实现对感知数据的推理。STPL的一个主要优点是,即使在某些情况下没有地面真相数据,它也可以促进感知系统实时性能的基本理智检查。我们确定了STPL的片段,该片段是在多项式时间内有效地监视离线的。最后,我们提供了一系列针对AV感知系统的规格,以突出显示可以通过STPL通过离线监控来表达和分析的要求类型。
translated by 谷歌翻译
Graph-structured data appears frequently in domains including chemistry, natural language semantics, social networks, and knowledge bases. In this work, we study feature learning techniques for graph-structured inputs. Our starting point is previous work on Graph Neural Networks (Scarselli et al., 2009), which we modify to use gated recurrent units and modern optimization techniques and then extend to output sequences. The result is a flexible and broadly useful class of neural network models that has favorable inductive biases relative to purely sequence-based models (e.g., LSTMs) when the problem is graph-structured. We demonstrate the capabilities on some simple AI (bAbI) and graph algorithm learning tasks. We then show it achieves state-of-the-art performance on a problem from program verification, in which subgraphs need to be described as abstract data structures.
translated by 谷歌翻译
实际上,所有验证和综合技术都假定正式规格很容易获得,在功能上正确并完全匹配工程师对给定系统的理解。但是,在实践中,这种假设通常是不现实的:正式化系统要求非常困难,容易出错,并且需要大量的培训。为了减轻这一严重的障碍,我们提出了一种从根本上新颖的编写形式规范的方法,称为线性时间逻辑(LTL)的规范草图。关键的想法是,工程师可以提供部分LTL公式,称为LTL草图,在该公式中很难形式化。给定一组描述规范应该或不应允许的系统行为的示例,然后将所谓的草图算法的任务完成给定的草图,以使所得的LTL公式与示例一致。我们表明,决定是否可以完成草图属于复杂性NP,并呈现两个基于SAT的草图算法。我们还证明,素描是使用原型实现编写形式规格的实用方法。
translated by 谷歌翻译
Two approaches to AI, neural networks and symbolic systems, have been proven very successful for an array of AI problems. However, neither has been able to achieve the general reasoning ability required for human-like intelligence. It has been argued that this is due to inherent weaknesses in each approach. Luckily, these weaknesses appear to be complementary, with symbolic systems being adept at the kinds of things neural networks have trouble with and vice-versa. The field of neural-symbolic AI attempts to exploit this asymmetry by combining neural networks and symbolic AI into integrated systems. Often this has been done by encoding symbolic knowledge into neural networks. Unfortunately, although many different methods for this have been proposed, there is no common definition of an encoding to compare them. We seek to rectify this problem by introducing a semantic framework for neural-symbolic AI, which is then shown to be general enough to account for a large family of neural-symbolic systems. We provide a number of examples and proofs of the application of the framework to the neural encoding of various forms of knowledge representation and neural network. These, at first sight disparate approaches, are all shown to fall within the framework's formal definition of what we call semantic encoding for neural-symbolic AI.
translated by 谷歌翻译
推理,学习和决策的整合是构建更多普通AI系统的关键。作为朝这个方向的一步,我们提出了一种新颖的神经逻辑架构,可以解决电感逻辑编程(ILP)和深增强学习(RL)问题。我们的体系结构通过分配权重来谓词而不是规则来定义一阶逻辑程序的受限但呈现的连续空间。因此,它是完全可分的,可以用梯度下降有效地培训。此外,在与演员批评算法的深度RL设置中,我们提出了一种新颖的高效评论家建筑。与ILP和RL问题的最先进方法相比,我们的命题实现了出色的性能,同时能够提供完全可解释的解决方案和更好地缩放,特别是在测试阶段。
translated by 谷歌翻译
信号时间逻辑的鲁棒性不仅评估信号是否遵守规范,而且还提供了对公式的满足或违反的量度。鲁棒性的计算基于评估潜在谓词的鲁棒性。但是,通常以无模型方式(即不包括系统动力学)定义谓词的鲁棒性。此外,精确定义复杂谓词的鲁棒性通常是不平凡的。为了解决这些问题,我们提出了模型预测鲁棒性的概念,该概念通过考虑基于模型的预测,它与以前的方法相比提供了一种更系统的评估鲁棒性的方法。特别是,我们使用高斯过程回归来基于预定的预测来学习鲁棒性,以便可以在线上有效地计算鲁棒性值。我们评估了对自动驾驶用例的方法,该案例用在记录的数据集上使用形式的交通规则中使用的谓词来评估我们的方法,这与传统方法相比,在表达性方面相比,我们的方法优势。通过将我们的鲁棒性定义纳入轨迹规划师,自动驾驶汽车比数据集中的人类驾驶员更强大地遵守交通规则。
translated by 谷歌翻译
在时间序列预测的各种软计算方法中,模糊认知地图(FCM)已经显示出显着的结果作为模拟和分析复杂系统动态的工具。 FCM具有与经常性神经网络的相似之处,可以被分类为神经模糊方法。换句话说,FCMS是模糊逻辑,神经网络和专家系统方面的混合,它作为模拟和研究复杂系统的动态行为的强大工具。最有趣的特征是知识解释性,动态特征和学习能力。本调查纸的目标主要是在文献中提出的最相关和最近的基于FCCM的时间序列预测模型概述。此外,本文认为介绍FCM模型和学习方法的基础。此外,该调查提供了一些旨在提高FCM的能力的一些想法,以便在处理非稳定性数据和可扩展性问题等现实实验中涵盖一些挑战。此外,具有快速学习算法的FCMS是该领域的主要问题之一。
translated by 谷歌翻译