一句话：将精确概念学习理论引入不变式推断，提出 fence 条件，首次给出插值式不变式推断的多项式复杂度结果。
本文研究归纳不变式推断的复杂度，并揭示其与精确概念学习的联系。作者提出不变式及其几何性质的“fence 条件”：不变式边界（与不变式 Hamming 距离为 1 的状态）需在少量步骤内从坏状态反向可达。借助该条件，可把概念学习理论结果用于回答不变式推断的开放问题。主要结果包括：首次证明某类基于插值的不变式推断算法具有多项式复杂度，可在以 SAT 求解器为 oracle 的情况下高效推断单调 DNF 不变式；进一步利用 Bshouty 的概念学习结果，将高效推断扩展到比单调 DNF 更大的语法类。最后考察程序变换下推断的鲁棒性，表明简单变换保持 fence 条件，而复杂变换会破坏它。
We study the complexity of invariant inference and its connections to exact concept learning. We define a condition on invariants and their geometry, called the fence condition, which permits applying theoretical results from exact concept learning to answer open problems in invariant inference theory. The condition requires the invariant's boundary---the states whose Hamming distance from the invariant is one---to be backwards reachable from the bad states in a small number of steps. Using this condition, we obtain the first polynomial complexity result for an interpolation-based invariant inference algorithm, efficiently inferring monotone DNF invariants with access to a SAT solver as an oracle. We further harness Bshouty's seminal result in concept learning to efficiently infer invariants of a larger syntactic class of invariants beyond monotone DNF. Lastly, we consider the robustness of inference under program transformations. We show that some simple transformations preserve the fence condition, and that it is sensitive to more complex transformations.
@article{paperbot1194,
title = {Learning the boundary of inductive invariants},
author = {Yotam M. Y. Feldman and Mooly Sagiv and Sharon Shoham and James R. Wilcox},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434296}
}