Mar, 2020

使用门控连续逻辑网络学习非线性循环不变量 (扩展版本)

HTML
PDF
TL;DR本文提出了一种新的神经架构，G-CLN，用于非线性循环不变量的学习，通过引入门控单元和dropout，允许模型在大量项上强大地学习常规不变量，并通过分数采样解决有限程序采样引起的过拟合问题，此外还提出了新的CLN激活函数-分段偏置二次单元（PBQU），用于自然地学习紧凑的不等式边界。实验证明，该方法可以解决一系列非线性循环不变量问题。
发现论文，激发创造
  • 分段线性神经网络验证的统一视角

    本文介绍了一种统一的深度学习模型形式验证的框架，利用分段线性结构和形式方法，结合现有方法的优势以实现两个数量级的加速。并提出了一组新的基准数据集，通过实验比较现有算法并确定影响验证问题难度的因素。

    Nov, 2017

  • 分支定界用于分段线性神经网络验证

    研究了深度学习的形式验证以及提出了一种基于分支定界的族算法，并提出了新型的组合方法，以及新的有效的分支策略，将之用于高维输入上的问题，并提出包含以前发布的测试案例的全面测试数据集和基准测试。

    Sep, 2019

  • 使用连续逻辑网络学习循环不变量

    本文提出了一种新的神经网络体系结构 Continuous Logic Network (CLN)，可以从程序执行路径中直接自动学习循环不变量，使用新的SMT公式嵌入方法，实现了完整且精确的自动化推理，并展示了其在各自领域中的性能优势。

    Sep, 2019

  • 神经网络验证的神经网络分支

    通过训练图神经网络来设计一个有效的分支策略，能够在形式化验证神经网络的过程中减少验证时间并获得更好的验证结果。

    Dec, 2019

  • 神经网络训练和验证的可微逻辑

    该论文讨论如何使用可微逻辑（Differentiable logics）来训练神经网络以满足逻辑条件，并以此保证其正确性。

    Jul, 2022

  • LogicMP：一种编码一阶逻辑约束的神经符号化方法

    该论文提出了一种新颖的神经层，LogicMP，它的层对一个MLN执行均场变分推理，可以插入到任何现有的神经网络中以编码FOLCs，同时保持模块化和高效性。利用MLNs中的结构和对称性，我们理论上证明了我们设计良好的高效均场迭代有效地缓解了MLN推断的困难，将推断从顺序计算减少为一系列并行张量操作。在图形、图像和文本的三种任务中的实证结果表明，LogicMP在性能和效率上胜过其他先进的竞争对手。

    Sep, 2023

  • 为程序验证评级LLM生成的循环不变量

    利用大型语言模型合成归纳循环不变量是自动化程序验证的基础。本研究观察到，大型语言模型（如gpt-3.5或gpt-4）能够在0-shot设置下为一类程序合成循环不变量，但需要多个样本来生成正确的不变量，这可能导致大量调用程序验证器以建立不变量。为解决这个问题，我们提出了一种对生成结果进行重新排名的方法，设计了一个能够根据问题定义区分正确的归纳不变量和错误尝试的排名器，该排名器被优化为对比排名器。实验结果表明，这种重新排名机制显著提高了正确不变量在生成的候选项中的排名，从而显著减少了对验证器的调用次数。

    Oct, 2023

  • 利用大型语言模型发现归纳循环不变量

    本文通过使用大语言模型，探索了在自动程序验证中找到归纳循环不变量的新方法，并证明了其可以改进目前的技术水平。

    Nov, 2023

  • 具有实数和浮点数的循环图神经网络的逻辑特征

    对于具有浮点数和实数的循环图神经网络，我们给出了两种情况下的精确逻辑特征，对于浮点数，与循环GNN匹配的形式是一种具有计数的基于规则的模态逻辑，而对于实数，我们使用适当的无限模态逻辑，也带有计数。此外，相对于在单调二阶逻辑（MSO）中定义的图属性，我们的无限和基于规则的逻辑的表达力是相等的，这意味着具有实数和浮点数的循环GNN在MSO可定义的属性上具有相同的表达力，并且说明对于这样的属性，实数循环GNN也是由（有限的！）基于规则的模态逻辑来特征化的。

    May, 2024

  • 用于学习逻辑程序的变量赋值不变神经网络

    本研究解决了传统符号算法在处理噪声和未观察转换时的局限性。我们提出了一种利用符号领域内在的变量排列不变性的技术，确保变量的排列和命名不会影响结果。实验表明该方法具有良好的效果和可扩展性，能够提高逻辑程序的学习能力。

    Aug, 2024