用门控连续逻辑网络学习非线性回路不变量

106用门控连续逻辑网络学习非线性回路不变量姚嘉楠美国哥伦比亚大学jianan@cs.columbia.edu加布里埃尔·瑞安美国哥伦比亚大学gabe@cs.columbia.eduJustin Wong美国哥伦比亚大学Justin. columbia.edu摘要SumanJanasuman@cs.columbia.edu哥伦比亚大学顾荣辉哥伦比亚大学，CertiK，美国rgu@cs.columbia.edu非线性循环不变量，并显示它解决了27个中的26真实世界的程序通常需要推断具有非线性约束的循环不变量。在执行许多数值运算的程序中尤其如此，例如航空电子设备或工业设备的控制系统最近，数据驱动的循环不变式推理方法已经显示出希望，特别是在线性循环不变式上。然而，将数据驱动的推理应用于非线性回路不变量是具有挑战性的，这是由于高阶项的大量和大幅度、在少量样本上过拟合的可能性以及可能的非线性不等式边界的大空间在本文中，我们介绍了一种新的神经结构一般SMT学习，门控连续逻辑网络（G-CLN），并将其应用于非线性循环不变学习。G-CLN扩展了连续逻辑网络（CLN）架构，具有门控单元和dropout，允许模型在大量项上鲁棒地学习一般不变量。 为了解决有限程序采样产生的过拟合问题，我们引入了分数采样，这是循环语义对连续函数的一种合理放松，它有助于实域上的无界采样。我们还设计了一个新的CLN激活函数，分段偏置二次单元（PBQU），自然学习紧不等式界。我们将这些方法纳入一个非线性回路不变式推理系统，可以学习一般的非线性回路不变式。我们根据以下基准评估我们的系统：平等贡献允许制作本作品的全部或部分数字或硬拷贝供个人或课堂使用，无需付费，前提是复制品不以营利或商业利益为目的制作或分发，并且复制品在第一页上带有此通知和完整的引用必须尊重作者以外的其他人所拥有的本作品组件的版权。允许用信用进行提取 复制，或重新发布，张贴在服务器上或重新分发到列表，需要事先特定的许可和/或费用。 请求权限请发邮件至permissions@acm.org。PLDI© 2020版权归所有者/作者所有 出版权授权给ACM。ACM ISBN 978-1-4503-7613-6/20/06。- 是的- 是的十五块https://doi.org/10.1145/3385412.3385986问题，比以前的工作多3个，平均运行时间为53.3秒。我们通过解决线性Code 2 Inv基准测试中的所有124个问题，进一步证明了G-CLN的通用学习能力。我们还进行了定量稳定-结果表明，G-CLN的收敛速度为97。5%的二次问题，39。比CLN模型提高2%。CCS概念：·软件及其工程→软件验证;·计算方法学→神经网络。关键词：循环不变推理，程序验证，连续逻辑网络ACM参考格式：Jianan Yao，Gabriel Ryan，Justin Wong，Suman Jana，andRonghui Gu.2020.用门控连续逻辑网络学习非线性回路不变量。 在第41届ACM SIGPLAN编程语言设计和实现国际会议（PLDI '20）的会议记录中，2020年6月15日至20日，英国伦敦。ACM ，纽 约 州 纽约市，美国，15页。https://doi.org/10.1145/3385412.33859861介绍形式验证提供了证明程序正确性的技术，从而消除了整个类别的关键错误。 虽然许多操作可以自动验证，但验证具有循环的程序通常需要推断足够强的循环不变量，这通常是不可理解的[5，10，15]。因此，不变推理系统基于对实际中出现的循环很有效的逻辑学数据驱动的循环不变式推理是一种已经显示出显著前景的方法，特别是对于学习线性不变式[30，35，40]。数据驱动推理通过在程序的许多执行中采样程序状态并试图识别所有采样数据点都满足的可满足性模理论（SMT）公式来操作。然而，验证真实世界的程序往往需要循环不变量与非线性约束。在执行许多数值运算的程序中尤其如此，例如航空电子或工业控制系统PLDIJ. Yao，G. Ryan，J. Wong，S.雅纳河顾1073植物[6，20]。数据驱动的非线性不变量推断从根本上是困难的，因为可能的非线性不变量的空间很大，但是必须从有限数量的样本中推断出用于验证的足够的不变量在实践中，这在执行非线性数据驱动的不变推理时导致三个不同的挑战：（i）具有高幅度项的大搜索空间。 学习非线性项会导致可能的不变量空间快速增长（即，项的多项式展开在项的次数上呈指数此外，像x2或x y这样的大型术语在这个过程中占主导地位，并阻止学习有意义的不变量。 ㈡样本有限。整数变量程序中循环迭代次数的界限限制了可能的样本数量，导致学习非线性不变量时的过拟合。(iii) 区分充分不等式。 对于任何给定的有限样本集，数据上可能存在无限个有效的不等式界。然而，验证通常需要尽可能严格地约束循环行为的特定边界。图1a和1b说明了具有许多高阶项以及非线性不等式边界的循环所带来的挑战图1a中的循环计算三次幂，并需要不变量（x=n3）<$（y=3n2+ 3n+ 1）<$（z=6n+ 6）验证其后置条件（x=a）。来推断这个不变量，一个典型的数据驱动推理系统必须考虑35个可能的项，范围从n到x3，其中只有7个包含在不变量中。此外，程序中的高阶项将主导拟合不变量的任何误差测量，因此任何数据驱动的模型都倾向于仅学习约束（x=n3）。图1b显示了一个用于计算整数平方根的循环，其中所需的不变量是（n ≥ a2）以验证其后置条件。然而，数据驱动的模型必须将此不变量与潜在无穷其他有效但松散拟合的不等式不变量。大多数现有的非线性循环不变推断方法通过限制它们可以学习的不变量的结构或它们可以扩展到的不变量的复杂性来解决这些挑战。Numinv和Guess-And-Check等多项式方程求解方法能够学习等式约束，但不能学习非线性不等式不变量[21，33]。相比之下，模板枚举方法（如PIE）可以潜在地学习任意不变量，但很难扩展到具有非线性不变量的循环，因为可能的不变量空间增长得太快[26]。在本文中，我们介绍了一种方法，可以学习一般的非线 性 循 环 不 变 量 。 我 们 的 方 法 基 于 连 续 逻 辑 网 络（CLN），这是一种最近提出的神经架构，可以直接从程序跟踪中学习SMT公式[30]。CLN使用参数化松弛，松弛SMT公式可微功能。这允许CLN学习具有梯度下降的SMT公式，但是必须手动提供定义公式的逻辑结构的模板。我们的方法基于三个发展，解决了非线性循环不变推理中固有的挑战：首先，我们引入了一种新的神经架构，门控连续逻辑网络（G-CLN），一种更强大的CLN架构，不依赖于公式模板。其次，介绍了分数采样，一种用于稠密采样的原理性程序松弛。第三，我们推导出一个新的CLN不等式学习激活函数--分段偏置二次单元（PBQU）.我们在下面提供这些方法的概述。门控连续逻辑网络G-CLN通过使其更健壮和通用来改进CLN架构。与CLN不同，G-CLN不依赖于逻辑结构的公式模板。 我们从深度学习中采用了三种不同的方法，使G-CLN训练更加稳定并对抗过拟合：门控，辍学和批量正常化[2，13，16，37]。为了迫使模型学习不同的约束组合，我们应用了Term Dropout，其操作类似于前馈神经网络中的dropout，通过将每个子句中的随机项子集归零门，ING使CLN架构的鲁棒性，允许它ignore子条款，不能学习满意的系数，为他们的输入，由于穷人的权重初始化或辍学。 为了在存在高幅度非线性项的情况下稳定训练，我们对输入和权重应用归一化，类似于批量归一化。通过将dropout与门控相结合，G-CLN能够学习具有许多高阶项的循环的复杂约束。对于图1a中的循环，G-CLN将在dropout期间将几个子子句中的n2或n3项设置为零， 迫 使 模 型 学习 所 有 三 个 等 式 约 束 的合 取 。由 于dropout而无法学习到令人满意的系数集的子句，即具有门控的模型将忽略仅具有x和n但没有n3项的子句分数采样。 当程序跟踪的样本不足以学习正确的不变量时，由于程序行为的界限，我们执行一个原则性的放松，连续函数的程序语义。 这允许我们执行分数采样，它在整数之间的中间点生成循环行为的样本。为了保持稳健性，我们定义的松弛，使操作保留其离散语义相对于其输入，但操作的真实域，和任何不变量的连续松弛的程序必须是一个不变量的离散程序。这使我们能够采取潜在的无界样本，即使在程序约束阻止足够的采样来学习正确的不变量的情况下。分段偏置二次单位。对于不等式学习，我们设计了一个PBQU激活，它惩罚宽松的拟合，并收敛到严格的数据约束我们证明了这个函数将学习至少一个点上的紧边界，并凭经验证明它学习精确的边界不变量边界，例如图1b中所示的（n≥a2）边界。用G-CLNsPLDI108n += 1;x += y;y += z;z += 6;}返回 x ;18161412t += 2;102ks += t;8}61kreturna;4//使用方法：a^2<= n0//和n < （a+1）^2// 职位： x== a^3051015n(a) 用 于 计 算 立 方 体 的 循 环 ， 需 要 不 变 量 （ x=n3 ）<$（y=3n2+ 3n+ 1）<$（z= 6n+ 6）来推断其后置条件（x=a3）。数据驱动模型必须同时学习立方约束以1000秒为单位变化，线性约束以6为单位递增00 100 200 300n(b) 用于计算平方根的整数近似值的循环。该图显示了三个有效的不等式不变量，但只有紧二次不等式不变量（n ≥ a2）足以证明，a的最终值在10sqrt（n）n和10sqrt（n）n之间。图1. 示例问题展示了非线性循环不变学习的挑战。我们使用G-CLNs与分数采样和PBQUs开发一个统一的方法，一般非线性循环不变的推理。我们评估我们的方法上的一组循环程序与非线性不变，并显示它可以学习27个问题中的26个不变，3比以前的工作，平均运行时间为53.3秒。我们还进行了定量的稳定性评估，并显示G-CLNs的收敛速度为97。5%的二次问题，39。比CLN模型提高2%我们还在线性Code 2 Inv基准测试[35]上测试了G-CLN架构，并表明它可以解决所有124个问题。综上所述，本文做出了以下贡献：• 我们开发了一个新的通用和强大的神经架构，门控连续逻辑网络（G-CLN），学习一般SMT公式，而不依赖于-逻辑结构• 我们介绍了分数采样，这是一种通过应用程序循环语义的原则性放松来简化实域采样的方法，连续函数，同时保持学习的不变量的可靠性• 我们设计了PBQUs，一个新的激活函数学习紧界不等式，并提供收敛性学习有效边界的保证。• 我们将我们的方法集成到一个通用的循环不变推理系统中，并在一个非线性循环不变基准测试中解决了27个问题中的26个，比传统的循环不变推理系统多3个。以 前 的 工 作 。 我 们 的系 统 还可 以 推 断 出线 性Code2Inv基准测试中所有124个问题的循环不变式。本文的其余部分组织如下：在费用2中，我们提供了循环不变推理问题，可微逻辑和用于SMT学习的CLN神经架构的背景。随后，我们在费用3中介绍了我们的方法的高级工作流。接下来，在费用4中，我们正式定义门控CLN构造、分数采样的松弛和不等式学习的PBQU，并为门控和边界学习的收敛保证提供可靠性保证然后，我们在费用5中详细描述了我们使用CLN进行非线性不变学习的方法。最后，我们在费用6中展示评估结果，并在费用7中讨论相关工作，然后在费用8中总结。2背景在本节中，我们简要回顾了循环不变推理问题，然后定义了我们的方法中使用的可微逻辑运算符和连续逻辑网络2.1循环不变推理循环不变量封装了独立于迭代的循环属性，并使验证能够在循环中执行。一个不变量要足够用于验证，它必须同时弱到足以从前提导出，强到足以得出后置条件。形式上，循环不变式推理问题是，给定一个循环，当（LC）C，C，C，一个前提条件P，和一个后置条件Q，我们被要求找到一个满足以下三个条件的归纳不变式IP=I{ILC}C{I}I<$LC=Q其中，归纳条件使用霍尔三元组来定义循环不变量可以在SMT中编码，这有助于使用Z3等求解器有效检查条件[4，7]。因此，我们的工作重点是推断可能的候选人不变量作为验证候选人可以有效地完成数据驱动的方法。数据驱动的循环不变式推断方法使用记录程序中每个变量在循环的每次迭代中的状态的程序跟踪，紧不变样本x y z一// 前：（a>= （0）// 前：（n >=0）n =0; x=0;4kx样品y个样本a =0; s =1; t =1;y =1; z=6;z个样本//computesqrt：2PLDIJ. Yao，G. Ryan，J. Wong，S.雅纳河顾109112引导不变量生成过程。由于不变量必须对任何有效的执行保持，因此收集的跟踪可以用于排除许多潜在的不变量。形式上，给定一组程序轨迹X，数据驱动的不变推理找到SMT公式F，使得：F（x）=True2.2基本模糊逻辑我们的SMT公式学习方法是基于一种称为基本模糊逻辑（BL）的可微逻辑形式BL是一阶逻辑的一个表达式，它对区间[0， 1]上的连续真值而不是布尔值进行操作。BL使用一类称为t-范数（t-norms）的函数，连续真值条件价值观T-范数需要与布尔逻辑一致，在其域上单调，交换和关联[14]。形式上，t-范数定义为：[0， 1]2→[ 0， 1]，使得：• 对于任意t∈ [0， 1]，k是一致的：t1=tt 0= 0• 对于任何t∈ [0，1]，k是交换的和结合的：t1t2=t2t1（t2t3）=（t1t2）t3• 对于任何t∈ [0，1]，k是单调的（非递减的）：1. 它必须保持逻辑的意义，使得有效赋值的连续真值总是大于无效赋值的值（F（x）=True<$F（x′）=False）=S（F）（x）>S（F）（x′）2. 它必须是连续的和平滑的（即，几乎在所有地方都是不同的），以促进培训。3. 它必须严格增加，因为一个不令人满意的项的分配接近满足映射公式，并严格减少，因为一个令人满意的项的分配接近违反公式。S的构造如下以满足这些要求。 逻辑关系{k，k，<$}被映射到它们在BL中的连续等价物：合取：S（F1<$F2）<$S（F1）<$S（F2）析取：S（F1<$F2）<$S（F1）<$S（F2）否定：S（<$F）<$1− S（F）其中任何F都是SMT公式。S定义SMT谓词{=，≤，<>，≥}，其函数映射到连续真值。该映射是使用具有移位参数λ和平滑参数B的S形来针对{>，≥}定义的：大于：S（x1>x2）1+e−B（x−x−）t1≤t2=t1t3≤t2t3大于或等于：S（x11≥x2）BL还要求t-范数是连续的。T-余模（T-conorms）是通过德摩根定律从t-范数中推导出来的，并作为连续真值的析取运算，而否定则定义为<$t：=1−t。在本文中，我们在公式中保持了t-模的抽象性使框架具有通用性。 先前的工作[30]发现乘积t范数x·y=x·y在连续逻辑网络中表现更好。 出于这个原因，我们在最终实现中使用乘积t范数，尽管其他t范数（例如，Godel）也可以使用。2.3连续逻辑网络我们使用连续逻辑网络（CLN）执行SMT公式学习，CLN是[30]中介绍的一种神经架构，能够直接从数据中学习SMT公式。 这些可以用来从程序的观察对象中学习循环不变量。CLN基于SMT公式的参数松弛，该参数松弛从布尔一阶逻辑BL该模型定义了算子S。给定一个无量词的SMT公式F：X→ {True，False}，S将其映射到一个连续函数S（F）：X→ [0， 1]。为了使连续模型既可用于梯度引导在保持布尔逻辑语义的同时，它必须满足三个条件：1+e−B（x1−x2+）其中x1，x2∈R.其他谓词的映射是从它们与{>，≥}的逻辑关系导出的：小于：S（x1x2）=S（<$（x1≥x2））<小于或等于：S（x1≤x2）=S（<$（x1>x2））等式：S（x1=x2）=S（（x1≥x2）<$（x1≤x2））不等式：S（x1<$x2）=S（<$（x1=x2））使用这些定义，对于足够大的B和足够小的ε，参数松弛S满足所有三个条件。基于这种参数松弛S（F），我们建立了一个连续逻辑网络模型M，它是S（F）（x）的一个计算图，具有可学习的参数W。当训练CLN时，应用损失项来惩罚小B，确保当损失接近0时，CLN将学习精确的公式。在这些条件下，对于给定的一组数据点X，在具有系数W的经训练的CLN模型M与其相关联的公式F之间存在以下关系：F（x;W）=True图2显示了单个变量x的公式的CLN示例：F（x）=（x=1）<$（x≥ 5）<$（x≥ 2<$x≤3）用G-CLNsPLDI110.- 是的Σ⊗1д12100 1 2 3 4 5X图2.公式F（x）<$（x= 1）<$（x ≥ 5）<$（x ≥2<$x≤ 3）及其相关的CLNM（x）。枚举程序变量上直到给定次数maxDe的所有单项式，如图4b所示。我们的系统可以配置为考虑其他非线性项，如x，y。然后，我们使用收集的跟踪数据构建和训练G-CLN模型我们使用Expense5.2.1中描述的模型架构，使用Expense5.2.2中的pro-campaign进行边界学习。在训练模型之后，通过递归下降通过模型并提取其门控参数高于0.5的子句来提取用于不变量的SMT公式，如算法1中所概述的。在sqrt程序上，模型将学习不变量a2≤n<$（t=2a+ 1）<$su=（a+ 1）2.最后，如果z3返回一个反例，我们将合并将其转化为训练数据，并使用更多生成的样本对这三个阶段进行我们的系统重复，直到一个有效的不变量被学习或超时。跟踪收集不变量生成不变量检查反例4理论在本节中，我们首先介绍了我们的门控CLN的建设，并证明门控CLN是健全的，就其底层的离散逻辑。然后，我们描述分段偏置图3.由3个阶段组成的方法概述：跟踪从源代码文件生成，G-CLN训练和不变式提取，然后用Z3检查。// 前：（n >=0）二次单位，一个特殊的激活函数构造学习不等式的紧界，并提供理论保证。最后，我们提出了一种技术来放松循环语义，并在需要时生成更多的样本a =0; s =1; t =1;whilee（s=n） {log（a，s，t，n）;a += 1;t += 2;t = t;}int n（n）;(a) 记录样本的程序。1一 个 ... 作为t2st10101111 3 4 9 1212 518 25 451374849112(b) 生成的样本数据点的最大度为2。4.1门控t-模与t-余模在原始的CLN [30]中，需要公式模板来学习不变量。例如，要学习不变量（x+y=0）<$（x−y= 0），我们必须提供模板（w1x+w2y+b1=0）<$（w3x+w4y+b2= 0），可以是构建为CLN模型以学习系数。所以我们必须事先知道正确的不变量是原子子句、合取、析取还是更复杂的逻辑公式。为了解决这个问题，我们引入了门控t-范数和门控t-余模。图4.所示程序的训练数据生成在图1b中。3工作流程图3展示了循环不变式推理的总体工作流程。我们的方法有三个阶段：（i）我们首先执行的程序和执行生成跟踪数据。（ii）然后，我们构建并训练G-CLN模型来拟合跟踪数据。给定一个经典的t-范数T（x，y）=x≠y，我们将其关联的门控t-范数定义为：TG（x，y;<$1，<$2）=（ 1+<$1（x− 1））<$（ 1+<$2（y− 1））这里，<$1，<$2∈ [0，1]是分别指示x和y是否被激活的门参数。下面的等式显示了门控t-范数背后的直观性。(iii)我们从模型中提取一个候选循环不变式，并根据规范对其进行检查。T（x，y;<$，<$）=0x y <$1=1，<$2= 1x <$1=1，<$2= 0给定一个程序循环，我们修改它以记录每次迭代的变量，然后执行程序以生成样本。图4a说明了图1b中sqrt程序的这个过程。 该程序的输入n具有前提条件（n ≥0），因此我们使用值n = 0，1，2，.执行。对于设定范围内的输入。然后，我们将样本扩展到循环不变式的所有候选项。默认情况下，我们G12y <$1=0，<$2= 1=0，0= 0非正式地说，当<$1=1时，输入x被激活并表现为经典的t范数。当<$1=0时，x被停用并丢弃。当0<$1 1时，<$1的值表示我们应该从x中获取多少信息。<<这个模式也适用于<$2和y。F（x）（F）（x）源代码候选不变量执行轨迹Z3真值PLDIJ. Yao，G. Ryan，J. Wong，S.雅纳河顾111G⊕1212我们可以证明，<$1，<$2∈ [0， 1]，门控t-范数是连续的，并且关于x和y单调增加，因此非常适合于训练。像原始的t-范数一样，门控t-范数可以很容易地扩展到两个以上的操作数。在三个操作数的情况下，我们有以下内容：TG（x，y，z;<$1，<$2，<$3）=（ 1+<$1（x−1））<$（ 1+<$2（y− 1））（1+<$3（z− 1））使用德摩根T′（x，y;<$，<$）= 1−（ 1−<$x）<$（ 1−<$y）++-+++图6. 门控CLN的实例。 +SMT公式为（3y− 3z− 2=0）（（x−3z= 0）<$（x+y+z= 0））。与门控t-范数类似，门控t-余范数具有以下性质。算法1公式提取算法。输入：门控CLN模型M，具有输入节点T′（x，y;<$，<$）=零x y <$1=1，<$2= 1x <$1=1，<$2= 0X={x1，x2，...，xn}和输出节点p。输出：SMT公式FG12y<$1= 0，<$2= 1程序浸提配方（M）0<$1= 0，<$2= 0现在，我们用我们的门控替代品替换CLN中的原始t-范数和t-余范数，我们在图5中图示。图6展示了用于表示SMT公式的门控CLN利用门控架构，使得每个门控t范数或门控t约束的门控参数<$1、<$2在模型训练期间是可学习的，使得模型可以决定应该采用哪个输入以及应该从训练数据中丢弃这提高了模型的灵活性，并且不需要指定的模板。现在，我们在算法1中正式陈述从门控CLN模型递归地检索SMT公式的过程。为了简洁起见，滥用符号，第1行中的Mi表示模型Mi的输出节点而不是模型本身，并且这同样适用于第8行和第15行。BuildAtomic公式在第18行中是提取用于没有逻辑连接词的模型的公式的子例程在图6中检索x+y+z=0）。已经学习的线性权重用作等式或不等式中的项的系数，这取决于相关联的激活函数。栅极t模栅极t模栅极1：如果p=T G（M1，...，Mn;<$1，.，n）然后2：F：=真3：对于i：=1到n，4：如果d i>0。5那时5：F：=F提取物配方（Mi）6：否则，如果p=TG′（M1，. . ，Mn;<$1，. . ，<$n）则7：F：=假8：对于i：=1到n，9：如果d i>0。5那时10：F：=F提取物配方（Mi）十一： 否则，如果p=1− M1，则12：F：=<$提取公式（M1）13：其他14：F：=BuildAtomicFormula（M）最后，我们需要将学习的系数舍入为整数。我们首先缩放系数，使最大值为1，然后使用最大可能的分母四舍五入到最近的有理数。我们检查每个四舍五入的不变量是否适合所有的训练数据，并丢弃无效的。在定理4.1中，我们将证明所提取的SMT公式在某些约束下等价于门控CLN模型。我们首先介绍了在原始CLN[ 30 ]中定义的t-范数的性质。财产1. tu，（t>0）在我们的实现中使用的乘积t-范数xy=x·y具有此性质。注意，定理4.1中的超参数c1，c2，σ，σ将在费用4.2中正式引入，在这里并不重要。人们可以简单地看到图5. 由二进制t-范数构造三个操作数的门控t-范数示例。门控T型连接器是Limc1→0，c2→∞σ→0，σ →0M（x;c1，c2，σ，σ）PLDIJ. Yao，G. Ryan，J. Wong，S.雅纳河顾112做类似的。作为模型输出M（x）。用G-CLNsPLDI113（）→S≥[]}（t-u）2+c1G1n1n2定理4.1. 对于具有输入节点的门控CLN模型M，{x1，x2，...， x n}和输出节点p，如果所有选通参数{<$i}CLN映射到SMT的保证C2为0或1，则使用公式提取算法，恢复的SMT公式F等于选通CLN澳门新葡8455= 0while（yk）{y ++;x += y * y * y;}//使用方法：4 x== k^2//** （k） +1）^2(a) 基准测试中的ps4程序Xyy2y3y400000111119248163639278110041664256225525125 625(b) 训练数据在没有分数采样的情况下生成。0 0被认为是不等式学习的误差界虽然可以相应地定义谓词。C2(c) 训练数据使用分数抽样生成。澳门新葡8455<102 t≥u（t-u）2+c1程序将有变量VVI。假设我们可以学习S（t>u）<$S（t≥（u+u））S（tu）<$S（t≤（u−<$））<其中，k是设定的小常数。对于我们的参数松弛，经典逻辑中的一些公理只是近似地而不是严格地成立（例如，t≤u=（t>u））。 当c1→ 0和c2→ ∞时，它们严格成立.我们重新使用高斯函数作为参数松弛-平等的原则[30]。给定一个小常数σ，（t−u）一个新程序的不变谓词I′，即，VIV，VI→然后，令VI=V0，等式（6）将成为V，V0→现在V0是一个常数，I′（V0<$V）满足方程（1）。（5）因此是原始程序的有效不变式。其实如果我们成功地学习谓词I′，那么我们就有了一个更一般的S（t=u）exp（−4.3分数采样2σ2 ）循环不变量，可以应用于任何给定的初始值。图8显示了分数采样如何生成具有不同初始值的更细粒度的样本，在某些情况下，从原始程序生成的样本不足以学习正确的不变量，这是由于某些项（特别是高阶项）的主要增长或有限数量的循环迭代。 为了生成更细粒度但有效的样本，我们执行分数采样，以放松程序语义连续函数，而不违反循环不变式，通过改变程序变量的初始值。直觉如下。任何数值循环不变量I都可以被看作是一个预测变量。对用V0初始化的程序变量V进行赋值，使得V，V0<$→其中V0<$→V 0意味着从初始值V0开始，执行循环0次或多次迭代，以变量的值V现在我们放松初始值X0，并将它们视为输入变量V I，它可以携带任意值。新循环在我们的数据驱动学习系统中，模型拟合变得更加容易。图8a中程序的正确循环不变式是（4x=y+ 2y3+y2）n（y≤k）为了学习等式部分（4x=y4+2y3+y2），如果我们选择maxDeд4并应用正态抽样，则六项{1，y，y，y，y，x}将保留在费用5.1.3中的启发式过滤器之后。 图8b示出了没有分数采样的训练样本的子集（项1的列被省略）。当y变大时，低阶项1、y和y2变得越来越可忽略，因为它们明显小于主导项y4和x。在实践中，我们观察到x4和y的系数可以准确地学习，但不能学习1，y，y2。为了解决这个问题，我们希望在y=1附近生成更多样本，其中所有项都在同一水平上。通过使用Fractional函数在y=1附近输入更多初始值，可以轻松生成此类样本2S（t≤u）图8.分数采样的例子。1x yy2 y3y4 x0 y0y2y3y40-1-0.60.36 -0.22 0.13-1-0.60.36 -0.220.13我们只是在学习时证明了理论保证，-0.90.4 0.160.060.03-1-0.60.36 -0.22 0.13单不等式，我们的不等式1.81.4 1.962.743.84-1-0.60.36 -0.22 0.13可以与其他不等式和等式联系起来，0-1.2 1.44 -1.732.070-1.21.44 -1.73 2.07一个CLN模型下的合取和析取0-0.2 0.04 -0.010.000-1.21.44 -1.73 2.07基于我们对≥的参数松弛，其他不等式0.50.8 0.640.520.410-1.21.44 -1.73 2.07用G-CLNsPLDI116（）p0200=，=取样.表8c示出了来自x0= −1，y0= −0. x0= 0，y0=-1。2.现在我们有更多的样本，条件相同水平，使模型更容易收敛到准确的我们的门控CLN模型可以正确地学习松弛不变量4x−y4− 2y3−y2− 4x0+y4+2y3+y2= 0。最后，我们返回到精确的初始值x00y0 0，原始程序的正确不变量将出现4x−y4− 2y3−y2= 0。注意，为了方便起见，在Eq.（5）（6）（7），我们假设所有变量在原始程序中初始化，所有变量在新程序中松弛。然而，框架可以很容易地扩展到具有未初始化变量的程序，或者我们只是想放松初始化变量的子集。费用5.4中提供了如何将分数采样纳入我们的系统的详细信息。5非线性不变学习在本节中，我们描述了非线性的总体方法，（即，每一行）按比例重新缩放到L2范数10。标准化样品见表1。现在样本占据了一个更规则的范围。请注意，数据规范化并不违反模型正确性。如果原始样本t1，t2，. tk满足等式w1t1+w2t2+. +w k t k= 0（注意t i可以是高阶项），归一化的样本也是如此，反之亦然。同样的道理也适用于不平等。5.1.2权重正则化对于等式不变的w1x1+. +wmxm+b= 0和不等式不变量w1x1+. +w m x m+b≥ 0，w1=. =wm=b=0是真解。 为了避免学习这个微不足道的解决方案，我们需要{w1，.，w m}是非零的。一种更优雅的方法是将权重向量的L范数约束为常数1. 在实践中，我们像在定理4.2中那样选择L2-范数。权重被约束以满足w2+... +w2 =11m耳套不变推理我们首先描述我们的方法在非线性数据上进行稳定的CLN训练然后，我们概述了我们的模型架构，以及我们如何将不等式激活函数用于学习不等式。最后，我们展示了如何扩展我们的方法来学习包含外部函数的不变量。5.1非线性数据上的稳定CLN训练非线性数据会导致CLN训练中的不稳定性，因为它引入了大量的术语和广泛变化的幅度。我们通过修改CLN架构来规范化正向执行的输入和权重来解决这个问题然后，我们描述了如何实现term dropout，这有助于模型学习精确的SMT系数。5.1.1数据标准化。 过大的输入会导致不稳定，并阻止CLN模型收敛到拟合数据的精确SMT公式。因此，我们修改CLN架构，使得其重新缩放其输入，使得L2范数等于设定值l。在我们的实现中，l=10。我们以图1b中的程序为例。归一化前的原始样品如图4b所示。单项项的范围太广，给网络训练带来困难。通过数据归一化，每个样本表1.图1b中的程序归一化后的训练数据，该程序计算整数平方根。1 a t. 作为t2st0.7000.7000.700.700.270.270.811.082.423.230.130.250.632.293.175.710.060.190.453.103.167.235.1.3长期辍学。给定一个有三个变量{x，y，z}且maxDe <$=2的程序，我们将有十个候选项{1，x，y，z，x2，y2，z2，xy，xz，yz}。大量的术语给不变学习带来了困难，在真实世界的程序中，不变量不太可能包含所有这些项。我们使用两种方法来选择术语。首先，采用[33]中基于增长率的启发式算法来过滤掉不必要的术语。其次，我们在训练之前应用随机丢弃丢弃是神经网络中的一种常见做法，以避免过度拟合并提高性能。我们的dropout是在训练之前随机预定的，这是不同的从深度学习中典型的权重下降[37]。在基于增长率的滤波器之后，剩余七项{1，x，y，z，x2，y2，xy}在训练之前，神经元的每个输入项可以以概率p被丢弃。辍