一句话：在 Hoare 查询模型下证明归纳不变式推断需指数查询，并证明 PDR 式丰富查询可较 ICE 学习指数加速。
本文研究基于 SAT 的安全验证中归纳不变式推断的复杂性。作者在 Hoare 查询黑盒模型中分析：算法通过查询 Hoare 三元组有效性获取可达状态信息，该模型可刻画 IC3/PDR 及其变体。主要结果表明，一般 Hoare 查询模型需要指数级查询，下界为信息论下界，即使计算能力不受限也成立。进一步，作者证明利用 PDR 式丰富 Hoare 查询可比仅依赖候选归纳性检查与反例的 ICE 学习指数级更高效：构造的迁移系统类中，单帧 PDR 以多项式查询推断不变式，而任意仅用归纳性检查与反例的算法需指数查询。结果还揭示其与经典精确查询概念学习的联系，表明从归纳反例学习比从标记样本精确学习更难，CEGIS 收敛率取决于反例形式。
This paper addresses the complexity of SAT-based invariant inference, a prominent approach to safety verification. We consider the problem of inferring an inductive invariant of polynomial length given a transition system and a safety property. We analyze the complexity of this problem in a black-box model, called the Hoare-query model, which is general enough to capture algorithms such as IC3/PDR and its variants. An algorithm in this model learns about the system's reachable states by querying the validity of Hoare triples. We show that in general an algorithm in the Hoare-query model requires an exponential number of queries. Our lower bound is information-theoretic and applies even to computationally unrestricted algorithms, showing that no choice of generalization from the partial information obtained in a polynomial number of Hoare queries can lead to an efficient invariant inference procedure in this class. We then show, for the first time, that by utilizing rich Hoare queries, as done in PDR, inference can be exponentially more efficient than approaches such as ICE learning, which only utilize inductiveness checks of candidates. We do so by constructing a class of transition systems for which a simple version of PDR with a single frame infers invariants in a polynomial number of queries, whereas every algorithm using only inductiveness checks and counterexamples requires an exponential number of queries. Our results also shed light on connections and differences with the classical theory of exact concept learning with queries, and imply that learning from counterexamples to induction is harder than classical exact learning from labeled examples. This demonstrates that the convergence rate of Counterexample-Guided Inductive Synthesis depends on the form of counterexamples.
@article{paperbot524,
title = {Complexity and information in invariant inference},
author = {Yotam M. Y. Feldman and Neil Immerman and Mooly Sagiv and Sharon Shoham},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371073}
}