我们演示了学习信号时间逻辑公式的第一个复发性神经网络体系结构,并介绍了公式推理方法的第一个系统比较。传统系统嵌入了许多未明确形式化的专业知识。有很大的兴趣学习表征此类系统理想行为的形式规格 - 即时逻辑中的公式,这些公式被系统的输出信号所满足。此类规格可用于更好地理解系统的行为并改善其下一次迭代的设计。以前的推断方法假设某些公式模板,或者对所有可能的模板进行了启发式枚举。这项工作提出了一种神经网络体系结构,该结构通过梯度下降来渗透公式结构,从而消除了施加任何特定模板的需求。它将公式结构和参数的学习结合在一个优化中。通过系统的比较,我们证明了该方法与列举和晶格方法相比,该方法达到相似或更好的错误分类率(MCR)。我们还观察到,不同的公式可以实现相似的MCR,从经验上证明了时间逻辑推断问题的不确定性。
translated by 谷歌翻译
本文介绍了一个名为STLCG的技术,使用计算图计算信号时间逻辑(STL)公式的定量语义。 STLCG提供了一个平台,它可以将逻辑规范纳入从基于梯度的解决方案中受益的机器人问题。具体而言,STL是一种强大且表现力的正式语言,可以指定连续和混合系统产生的信号的空间和时间特性。 STL的定量语义提供了鲁棒性度量,即,信号满足或违反STL规范的量。在这项工作中,我们设计了一种系统方法,用于将STL鲁棒性公式转化为计算图形。通过这种表示,通过利用现成的自动差异化工具,我们能够通过STL稳健性公式有效地反向,因此可以实现具有许多基于梯度的方法的STL规范的自然且易于使用的STL规范集成。通过各种机器人应用的许多示例,我们证明STLCG是多功能的,计算效率,并且能够将人域知识纳入问题制定中。
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 谷歌翻译
网络物理系统中的实时和人为可解释的决策是一个重要但具有挑战性的任务,通常需要预测来自有限数据的未来可能的事件。在本文中,我们介绍了一个时间增量学习框架:给定具有共同时间范围的标记信号迹线的数据集,我们提出了一种方法来预测随时间递增地接收的信号的标签,称为前缀信号。前缀信号是当生成时被观察的信号,并且它们的时间长度短于信号的公共范围。我们介绍了一种基于决策树的决策树方法来生成来自给定数据集的有限数量的信号时间逻辑(STL)规范,并基于它们构造预测器。作为时间序列数据的二进制分类器,每个STL规范都会随着时间的推移捕获数据集的时间特性。通过将时间变量权重分配给STL公式来构建预测器。通过使用神经网络来学习权重,目的是最小化在给定数据集上定义的前缀信号的错误分类率。通过计算前缀信号的鲁棒性相对于每个STL公式的鲁棒性的加权之和来预测前缀信号的标签来预测前缀信号的标签。我们的算法的有效性和分类性能在城市驾驶和海军监测案例研究中进行了评估。
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 谷歌翻译
我们概述了在其知识表示和声明问题解决的应用中的视角下的时间逻辑编程。这些程序是将通常规则与时间模态运算符组合的结果,如线性时间时间逻辑(LTL)。我们专注于最近的非单调形式主义的结果​​称为时间平衡逻辑(电话),该逻辑(电话)为LTL的全语法定义,但是基于平衡逻辑执行模型选择标准,答案集编程的众所周知的逻辑表征(ASP )。我们获得了稳定模型语义的适当延伸,以进行任意时间公式的一般情况。我们记得电话和单调基础的基本定义,这里的时间逻辑 - 和那里(THT),并研究无限和有限迹线之间的差异。我们还提供其他有用的结果,例如将转换成其他形式主义,如量化的平衡逻辑或二阶LTL,以及用于基于自动机计算的时间稳定模型的一些技术。在第二部分中,我们专注于实际方面,定义称为较近ASP的时间逻辑程序的句法片段,并解释如何在求解器Telingo的构建中被利用。
translated by 谷歌翻译
人工智能代理必须从周围环境中学到学习,并了解所学习的知识,以便做出决定。虽然从数据的最先进的学习通常使用子符号分布式表示,但是使用用于知识表示的一阶逻辑语言,推理通常在更高的抽象级别中有用。结果,将符号AI和神经计算结合成神经符号系统的尝试已经增加。在本文中,我们呈现了逻辑张量网络(LTN),一种神经组织形式和计算模型,通过引入许多值的端到端可分别的一阶逻辑来支持学习和推理,称为真实逻辑作为表示语言深入学习。我们表明LTN为规范提供了统一的语言,以及多个AI任务的计算,如数据聚类,多标签分类,关系学习,查询应答,半监督学习,回归和嵌入学习。我们使用TensorFlow2的许多简单的解释例实施和说明上述每个任务。关键词:神经组音恐怖症,深度学习和推理,许多值逻辑。
translated by 谷歌翻译
这是一门专门针对STEM学生开发的介绍性机器学习课程。我们的目标是为有兴趣的读者提供基础知识,以在自己的项目中使用机器学习,并将自己熟悉术语作为进一步阅读相关文献的基础。在这些讲义中,我们讨论受监督,无监督和强化学习。注释从没有神经网络的机器学习方法的说明开始,例如原理分析,T-SNE,聚类以及线性回归和线性分类器。我们继续介绍基本和先进的神经网络结构,例如密集的进料和常规神经网络,经常性的神经网络,受限的玻尔兹曼机器,(变性)自动编码器,生成的对抗性网络。讨论了潜在空间表示的解释性问题,并使用梦和对抗性攻击的例子。最后一部分致力于加强学习,我们在其中介绍了价值功能和政策学习的基本概念。
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 谷歌翻译
从数据中提取空间时间知识在许多应用中都很有用。重要的是,所获得的知识是人类解释的和适用于正式分析。在本文中,我们提出了一种方法,该方法列举神经网络以学习基于加权图的信号时间逻辑(WGSTL)公式的形式的空间时间特性。对于学习WGSTL公式,我们介绍了一种灵活的WGSTL公式结构,其中用户的偏好可以应用于推断的WGSTL公式中。在所提出的框架中,神经网络的每个神经元对应于柔性WGSTL公式结构中的子核。我们初始训练一个神经网络来学习WGSTL运营商,然后训练第二个神经网络以在灵活的WGSTL公式结构中学习参数。我们使用Covid-19数据集和雨量预测数据集来评估所提出的框架和算法的性能。我们将建议框架的性能与三个基线分类方法进行比较,包括K-Collest邻居,决策树,支持向量机和人工神经网络。所提出的框架获得的分类准确性与基线分类方法相当。
translated by 谷歌翻译
背景信息:在过去几年中,机器学习(ML)一直是许多创新的核心。然而,包括在所谓的“安全关键”系统中,例如汽车或航空的系统已经被证明是非常具有挑战性的,因为ML的范式转变为ML带来完全改变传统认证方法。目的:本文旨在阐明与ML为基础的安全关键系统认证有关的挑战,以及文献中提出的解决方案,以解决它们,回答问题的问题如何证明基于机器学习的安全关键系统?'方法:我们开展2015年至2020年至2020年之间发布的研究论文的系统文献综述(SLR),涵盖了与ML系统认证有关的主题。总共确定了217篇论文涵盖了主题,被认为是ML认证的主要支柱:鲁棒性,不确定性,解释性,验证,安全强化学习和直接认证。我们分析了每个子场的主要趋势和问题,并提取了提取的论文的总结。结果:单反结果突出了社区对该主题的热情,以及在数据集和模型类型方面缺乏多样性。它还强调需要进一步发展学术界和行业之间的联系,以加深域名研究。最后,它还说明了必须在上面提到的主要支柱之间建立连接的必要性,这些主要柱主要主要研究。结论:我们强调了目前部署的努力,以实现ML基于ML的软件系统,并讨论了一些未来的研究方向。
translated by 谷歌翻译
时间序列数据分类对于自治系统(例如机器人和自动驾驶汽车)的分析和控制至关重要。最近已经提出了基于时间逻辑的学习算法作为此类数据的分类器。但是,当前的框架要么不准确,例如自动驾驶等现实应用程序,要么产生缺乏可解释性的漫长而复杂的公式。为了解决这些局限性,我们引入了一种新颖的学习方法,称为“增强简洁决策树(BCDTS)”,以生成表示为信号时间逻辑(STL)公式的二进制分类器。我们的算法利用简洁决策树(CDT)的合奏来改善分类性能,其中每个CDT都是由一组技术赋予的决策树,以生成更简单的公式并提高可解释性。我们的算法的有效性和分类性能在海军监视和城市驾驶案例研究中评估。
translated by 谷歌翻译
实际上,所有验证和综合技术都假定正式规格很容易获得,在功能上正确并完全匹配工程师对给定系统的理解。但是,在实践中,这种假设通常是不现实的:正式化系统要求非常困难,容易出错,并且需要大量的培训。为了减轻这一严重的障碍,我们提出了一种从根本上新颖的编写形式规范的方法,称为线性时间逻辑(LTL)的规范草图。关键的想法是,工程师可以提供部分LTL公式,称为LTL草图,在该公式中很难形式化。给定一组描述规范应该或不应允许的系统行为的示例,然后将所谓的草图算法的任务完成给定的草图,以使所得的LTL公式与示例一致。我们表明,决定是否可以完成草图属于复杂性NP,并呈现两个基于SAT的草图算法。我们还证明,素描是使用原型实现编写形式规格的实用方法。
translated by 谷歌翻译
在安全关键方案中利用自主系统需要在存在影响系统动态的不确定性和黑匣子组件存在下验证其行为。在本文中,我们开发了一个框架,用于验证部分可观察到的离散时间动态系统,从给定的输入输出数据集中具有针对时间逻辑规范的未暗模式可分散的动态系统。验证框架采用高斯进程(GP)回归,以了解数据集中的未知动态,并将连续空间系统抽象为有限状态,不确定的马尔可夫决策过程(MDP)。这种抽象依赖于通过使用可重复的内核Hilbert空间分析以及通过离散化引起的不确定性来捕获由于GP回归中的错误而捕获不确定性的过渡概率间隔。该框架利用现有的模型检查工具来验证对给定时间逻辑规范的不确定MDP抽象。我们建立将验证结果扩展到潜在部分可观察系统的抽象结果的正确性。我们表明框架的计算复杂性在数据集和离散抽象的大小中是多项式。复杂性分析说明了验证结果质量与处理较大数据集和更精细抽象的计算负担之间的权衡。最后,我们展示了我们的学习和验证框架在具有线性,非线性和切换动力系统的几种案例研究中的功效。
translated by 谷歌翻译
深度学习使用由其重量进行参数化的神经网络。通常通过调谐重量来直接最小化给定损耗功能来训练神经网络。在本文中,我们建议将权重重新参数转化为网络中各个节点的触发强度的目标。给定一组目标,可以计算使得发射强度最佳地满足这些目标的权重。有人认为,通过我们称之为级联解压缩的过程,使用培训的目标解决爆炸梯度的问题,并使损失功能表面更加光滑,因此导致更容易,培训更快,以及潜在的概括,神经网络。它还允许更容易地学习更深层次和经常性的网络结构。目标对重量的必要转换有额外的计算费用,这是在许多情况下可管理的。在目标空间中学习可以与现有的神经网络优化器相结合,以额外收益。实验结果表明了使用目标空间的速度,以及改进的泛化的示例,用于全连接的网络和卷积网络,以及调用和处理长时间序列的能力,并使用经常性网络进行自然语言处理。
translated by 谷歌翻译
这本数字本书包含在物理模拟的背景下与深度学习相关的一切实际和全面的一切。尽可能多,所有主题都带有Jupyter笔记本的形式的动手代码示例,以便快速入门。除了标准的受监督学习的数据中,我们将看看物理丢失约束,更紧密耦合的学习算法,具有可微分的模拟,以及加强学习和不确定性建模。我们生活在令人兴奋的时期:这些方法具有从根本上改变计算机模拟可以实现的巨大潜力。
translated by 谷歌翻译
大多数现有的时间序列分类(TSC)模型缺乏可解释性,难以检查。可解释的机器学习模型可以帮助发现数据中的模式,并为域专家提供易于理解的见解。在这项研究中,我们提出了神经符号时间序列分类(NSTSC),这是一种利用信号时间逻辑(STL)和神经网络(NN)的神经符号模型,使用多视图数据表示并将模型表示为TSC任务人类可读,可解释的公式。在NSTSC中,每个神经元与符号表达相关,即STL(sub)公式。因此,NSTSC的输出可以解释为类似于自然语言的STL公式,描述了隐藏在数据中的时间和逻辑关系。我们提出了一个基于NSTSC的分类器,该分类器采用决策树方法来学习公式结构并完成多类TSC任务。 WSTL提出的平滑激活功能允许以端到端的方式学习模型。我们在来自UCR时间序列存储库中的小鼠和基准数据集的现实伤口愈合数据集上测试NSTSC,这表明NSTSC与最先进的模型实现了可比的性能。此外,NSTSC可以生成与域知识匹配的可解释公式。
translated by 谷歌翻译
This paper surveys the eld of reinforcement learning from a computer-science perspective. It is written to be accessible to researchers familiar with machine learning. Both the historical basis of the eld and a broad selection of current work are summarized. Reinforcement learning is the problem faced by an agent that learns behavior through trial-and-error interactions with a dynamic environment. The work described here has a resemblance to work in psychology, but di ers considerably in the details and in the use of the word \reinforcement." The paper discusses central issues of reinforcement learning, including trading o exploration and exploitation, establishing the foundations of the eld via Markov decision theory, learning from delayed reinforcement, constructing empirical models to accelerate learning, making use of generalization and hierarchy, and coping with hidden state. It concludes with a survey of some implemented systems and an assessment of the practical utility of current methods for reinforcement learning.
translated by 谷歌翻译
Multilayer Neural Networks trained with the backpropagation algorithm constitute the best example of a successful Gradient-Based Learning technique. Given an appropriate network architecture, Gradient-Based Learning algorithms can be used to synthesize a complex decision surface that can classify high-dimensional patterns such as handwritten characters, with minimal preprocessing. This paper reviews various methods applied to handwritten character recognition and compares them on a standard handwritten digit recognition task. Convolutional Neural Networks, that are specifically designed to deal with the variability of 2D shapes, are shown to outperform all other techniques.Real-life document recognition systems are composed of multiple modules including eld extraction, segmentation, recognition, and language modeling. A new learning paradigm, called Graph Transformer Networks (GTN), allows such multi-module systems to be trained globally using Gradient-Based methods so as to minimize an overall performance measure.Two systems for on-line handwriting recognition are described. Experiments demonstrate the advantage of global training, and the exibility of Graph Transformer Networks.A Graph Transformer Network for reading bank check is also described. It uses Convolutional Neural Network character recognizers combined with global training techniques to provides record accuracy on business and personal checks. It is deployed commercially and reads several million checks per day.
translated by 谷歌翻译
自然语言是人类将任务传达给机器人的直觉方式。尽管自然语言(NL)是模棱两可的,但现实世界的任务及其安全要求需要明确传达。信号时间逻辑(STL)是一种形式的逻辑,可以用作描述机器人任务的多功能,表达和明确的形式语言。一方面,使用STL用于机器人域的现有工作通常要求最终用户在STL中表达任务规格,这是非专家用户的挑战。另一方面,从NL转换为STL规范的转换限制为特定片段。在这项工作中,我们提出了Dialoguestl,这是一种从(通常)模棱两可的NL描述中学习正确和简洁的STL公式的交互方法。我们结合了语义解析,基于预训练的变压器的语言模型以及少数用户演示的用户澄清,以预测编码NL任务描述的最佳STL公式。将NL映射到STL的一个优点是,在使用增强学习(RL)以识别机器人的控制策略方面,最近有很多工作。我们表明,我们可以使用深层学习技术来从学习的STL规范中学习最佳策略。我们证明DialogUestl具有高效,可扩展性和健壮性,并且在预测正确的STL公式方面具有很高的精度,并与Oracle用户进行了一些演示和一些交互。
translated by 谷歌翻译