一句话：提出用深度强化学习自动学习智能合约不变量，以证明算术安全性并加速验证。
智能合约在现代金融中广泛使用，其正确性与安全性验证备受关注。现有方法多依赖合约不变量（交易边界成立的逻辑公式）来验证算术溢出等漏洞，但不变量获取困难。本文提出基于深度强化学习的合约不变量自动学习技术：离线训练阶段，验证器利用自身验证尝试学习不变量生成策略；验证阶段用学到的神经策略预测有助于证明算术安全的不变量。实现为 Cider 并集成到基于 refinement type checking 的验证器。实验表明，Cider 提升了不变量质量、缩短了推断时间，从而加快验证，并使合约加固后保留更少运行时断言。
Due to the popularity of smart contracts in the modern financial ecosystem, there has been growing interest in formally verifying their correctness and security properties. Most existing techniques in this space focus on common vulnerabilities like arithmetic overflows and perform verification by leveraging contract invariants (i.e., logical formulas hold at transaction boundaries). In this paper, we propose a new technique, based on deep reinforcement learning, for automatically learning contract invariants that are useful for proving arithmetic safety. Our method incorporates an off-line training phase in which the verifier uses its own verification attempts to learn a policy for contract invariant generation. This learned (neural) policy is then used at verification time to predict likely invariants that are also useful for proving arithmetic safety. We implemented this idea in a tool called Cider and incorporated it into an existing verifier (based on refinement type checking) for proving arithmetic safety. Our evaluation shows that Cider improves both the quality of the inferred invariants as well as inference time, leading to faster verification and hardened contracts with fewer run-time assertions.