Jan, 2024

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

PDF
TL;DR最近的研究描述了神经网络验证中的嵌入间隙存在。在间隙的一侧是高级规范，由领域专家根据可解释的问题空间编写。在另一侧是逻辑上等价的一组可满足性查询，以适合神经网络求解器的不可解释的嵌入空间形式表达。本文描述了一种将前者编译为后者的算法。我们探索并克服了针对神经网络求解器而不是标准 SMT 求解器引发的复杂问题。
embedding gapneural network verificationspecificationsatisfiability queriesneural network solvers
发现论文，激发创造
  • 车辆：弥合神经符号程序验证中的嵌入差距

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

    Jan, 2024

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

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

    Mar, 2024

  • 面向模块化和可编程化的架构搜索

    本文提出一种编码通用计算图上的搜索空间的正式语言，解决了目前基于深度学习架构搜索的特定应用和通用超参数优化系统之间的折衷问题。该语言的结构使我们能够编写模块化、可组合和可重用的搜索空间，并在不同搜索空间和优化算法的组合中自由实验，而不必从头实现每个组合。我们在文中公开了该语言的实现。

    Sep, 2019

  • 潜空间中的数学推理

    通过在固定维度的潜在空间中进行的近似推理的几个步骤，我们证明了神经网络可以对语句进行重写和推理，这对于各种数学学科都是可行的。

    Sep, 2019

  • 构建可逆的语义保留逻辑公式嵌入

    该研究工作探讨了如何使用基于图变分自编码器 (Graph Variational Autoencoder) 的深度架构来训练学习逻辑嵌入，以实现对逻辑嵌入的反向推理，即将嵌入空间中的逻辑公式反向映射回语法空间，进而提高机器学习中学习逻辑规则和性质的能力。

    May, 2023

  • 用于验证深度神经网络的 DPLL (T) 框架

    引入一种新的约束求解方法 NeuralSAT，用作深度神经网络 (DNN) 验证的符号化求解器。

    Jul, 2023

  • 语义解析的瓶颈：自动数学题解决方案的调查

    该研究探讨了自动解决数学问题的挑战，包括语言和逻辑之间的语义鸿沟，综述了将人工智能用于代数和几何问题的主要技术及其性能，并探讨未来的研究方向。

    Aug, 2018

  • 将符号知识嵌入深度网络

    本文提出了一种基于图嵌入网络的符号知识应用方法，该方法将命题公式 (和赋值) 通过增强的 Graph Convolutional Network (GCN) 投射到流形上。通过识别节点异质性和结构约束等技术，我们能够生成语义上忠实的嵌入，提高推理检查和视觉关系预测模型的性能。有趣的是，我们观察到命题理论表示的可处理性与嵌入的易用性之间存在一种联系。

    Sep, 2019

  • 提升神经数学问题求解器的技术

    该研究提出了一种基于编码器 - 解码器的模型，完全利用问题文本并保留逐步的交换律，以产生无论数量的排列方式如何都具有不变性的表达式嵌入，并进一步对问题文本进行编码以指导解码过程，可以提高数学问题自动求解程序的性能。

    Feb, 2023

  • 基于 SMT 求解器的神经网络等价性检查

    本研究通过首次基于 SMT 的编码探讨了神经网络等效性检查的实用性和限制，并提出了未来研究和改进的思路。

    Mar, 2022