一句话：用 SyGuS 生成候选、SMT 验证器过滤，并借助逻辑推理剪枝与强化学习排序，高效合成关系不变式。
论文关注关系性质验证所需的关系不变式的自动合成问题，这类不变式可用于验证两个程序或同一程序两次执行之间的函数等价性、非干涉安全性和连续性等性质。作者提出一种组合式方法：先用语法引导合成（SyGuS）生成候选不变式，再交给基于 SMT 求解器的验证器过滤，以确保候选既是归纳不变式又足以证明目标性质。为提升合成效率，论文引入两种学习技术：基于逻辑推理（LR）的技术判断搜索空间中哪些部分可以剪枝，基于强化学习（RL）的技术决定搜索空间中哪些部分应优先探索。在多样化关系验证基准上的实验表明，这些学习技术能大幅缩减搜索空间，从而在远短于当前最先进不变式合成技术的时间内生成更高质量的不变式。
We propose a method for synthesizing invariants that can help verify relational properties over two programs or two different executions of a program. Applications of such invariants include verifying functional equivalence, non-interference security, and continuity properties. Our method generates invariant candidates using syntax guided synthesis (SyGuS) and then filters them using an SMT-solver based verifier, to ensure they are both inductive invariants and sufficient for verifying the property at hand. To improve performance, we propose two learning based techniques: a logical reasoning (LR) technique to determine which part of the search space can be pruned away, and a reinforcement learning (RL) technique to determine which part of the search space to prioritize. Our experiments on a diverse set of relational verification benchmarks show that our learning based techniques can drastically reduce the search space and, as a result, they allow our method to generate invariants of a higher quality in much shorter time than state-of-the-art invariant synthesis techniques.