Jan, 2024

车辆：弥合神经符号程序验证中的嵌入差距

PDF
TL;DR通过描述一种名为 Vehicle 的工具，该工具用于模块化地验证神经符号程序，本文确定了 '' 嵌入间隙 '' 作为关键问题之一，Vehicle 提供了方便的语言用于指定神经网络的 '' 问题空间 '' 属性，并声明它们与 '' 嵌入空间 '' 的关系，以及自动化解释这些属性的强大编译器，以验证一个简单的装备有神经网络控制器的自主车辆的安全性。
neuro-symbolic programsembedding gapverificationneural networkssafety
发现论文，激发创造
  • 深度神经网络的神经符号验证

    文章介绍了一种基于神经网络和逻辑规范的神经符号验证框架 Neuro-symbolic Verification，使得现有的神经网络验证基础设施可用于分析复杂的实际特性，从而避免现有神经网络验证技术的严重局限。

    Mar, 2022

  • NLP 验证：向着一种通用的用于证明鲁棒性的方法论

    通过总结现有领域进展，本文试图提炼和评估自然语言处理（NLP）验证流程的一般组成部分并分别给出了两个贡献，首先是针对将句子嵌入连续空间引起的语义一般化技术挑战，提出了一个有效的解决方法作为 NLP 验证流程的标准度量标准之一；其次是针对几何子空间验证和其所代表的句子语义之间的差异提出了一般性的分析方法，并提出了众多实用的 NLP 方法来识别嵌入空间差异的影响，并倡导以语义子空间可伪造性作为 NLP 验证流程的另一个基本度量标准，我们相信这些通用原则共同为这一新领域的更加巩固和有效的发展铺平了道路。

    Mar, 2024

  • 高效编译表达性问题空间规范为神经网络求解器

    最近的研究描述了神经网络验证中的嵌入间隙存在。在间隙的一侧是高级规范，由领域专家根据可解释的问题空间编写。在另一侧是逻辑上等价的一组可满足性查询，以适合神经网络求解器的不可解释的嵌入空间形式表达。本文描述了一种将前者编译为后者的算法。我们探索并克服了针对神经网络求解器而不是标准 SMT 求解器引发的复杂问题。

    Jan, 2024

  • 使用混合马尔可夫逻辑验证嵌入

    我们提出了一种基于概率一阶语言的框架，即混合马尔可夫逻辑网络（HMLNs），用于验证学习得到的表示，并通过编码为混合整数线性规划的方式来进行嵌入的验证。我们使用现有的先进求解器测试了该方法，在图神经网络、深度知识追踪和智能辅导系统中展示了其广泛适用性。

    Dec, 2023

  • 动态神经程序嵌入用于程序修复

    提出了一种基于程序执行轨迹学习的新型语义程序嵌入，相比于基于程序语法的嵌入，可以更准确地捕捉程序语义，并用于预测学生程序提交中的错误类型，并展示了通过该语义嵌入预测进行搜索的效率显著提高的结果。

    Nov, 2017

  • 代码向量：通过嵌入式的抽象符号化痕迹理解程序

    本文介绍了如何使用程序追踪的抽象作为表示学习单词嵌入的一种方法，并展示了使用主要基于语义抽象的学习嵌入提供了接近三倍的准确度。

    Mar, 2018

  • 利用语义嵌入为安全关键应用增强

    本文提出了在神经网络分类器中使用 Semantic Embeddings 来增加自省和错误检测能力，使用从符号领域知识中创建语义嵌入表示，提出了一种简单的错误检测方案，并引入了语义距离概念。通过在交通标志分类器上评估，发现语义距离能够达到接近最先进的性能，计算速度显著快于其他置信度得分。我们的方法不需要对原始网络进行更改，因此适用于任何具有领域知识的任务。

    May, 2019

  • 神经网络验证的高效符号推理

    本文提出一种新的神经网络可验证的符号推理框架，名为符号推理，其利用了符号域和二次关系来解决网络在面临不同情景下的可验证问题。该框架提供了一种新的可验证信号和视角，可为神经网络的验证问题带来新的理论启示和实用工具。

    Mar, 2023

  • 神经符号 VQA: 从视觉和语言理解中分离推理

    该论文介绍了神经符号视觉问答系统，结合深度表示学习和符号程序执行，具有更好的数据和内存效率以及对推理过程的全透明度。

    Oct, 2018

  • 基于能量的神经符号推理知识图谱模型

    本研究提出了一种基于能量的图嵌入算法来描述工业自动化系统，学习多个领域的知识，从而可以进行上下文感知预测和评估异常严重性，该模型可以应用于机器学习和神经形态计算等领域。

    Oct, 2021