一句话：提出 RL 剪枝与 SMT 求解协同的框架，在一般非线性假设空间中高效推断循环不变式。
循环不变式推断是程序验证中最困难的问题之一，人们希望引入机器学习来提升推断能力。本文提出一个强化学习（RL）剪枝框架，用于在一般的非线性假设空间上推断循环不变式。其核心思想是让基于 RL 的剪枝与 SMT 求解协同工作，从而高效地生成候选不变式：RL 负责在庞大的假设空间中进行启发式剪枝，SMT 求解器负责判定候选的有效性。针对学习中奖励稀疏的问题，作者设计了一种新颖的二维奖励机制，使 RL 剪枝器能够识别 SMT 求解器的能力边界，并在很少的轮次内学到剪枝启发式。作者基于 Z3 实现了工具 LIPuS，并在线性与非线性基准上进行了大量实验。结果表明，与 Code2Inv、ICE-DT、GSpacer、SymInfer、ImplCheck 和 Eldarica 等当前最先进的循环不变式推断工具相比，LIPuS 能求解最多数目的实例，尤其非线性基准上优势显著。
Inferring loop invariants is one of the most challenging problems in program verification. It is highly desired to incorporate machine learning when inferring. This paper presents a Reinforcement Learning (RL) pruning framework to infer loop invariants over a general nonlinear hypothesis space. The key idea is to synergize the RL-based pruning and SMT solving to generate candidate invariants efficiently. To address the sparse reward problem in learning, we design a novel two-dimensional reward mechanism that enables the RL pruner to recognize the capability boundary of SMT solvers and learn the pruning heuristics in a few rounds. We have implemented our approach with Z3 SMT solver in the tool called LIPuS and conducted extensive experiments over the linear and nonlinear benchmarks. Experiment results show that LIPuS can solve the most cases compared to the state-of-the-art loop invariant inference tools such as Code2Inv, ICE-DT, GSpacer, SymInfer, ImplCheck, and Eldarica. Especially, LIPuS outperforms them significantly on nonlinear benchmarks.