Data-driven Optimization of Inductive Generalization

Inductive generalization (IG) is the key to the efficiency of modern Symbolic Model Checkers (SMCs).In this paper, we introduce a data-driven method for inductive generalization, whose performance can be automatically improved through historical runs over similar instances.Our method is inspired by recent advances for the part-of-speech (PoS) tagging problem in natural language processing (NLP).Specifically, we use a hierarchical recurrent neural network augmented with syntactic and semantic information to predict essential parts of a proof obligation that could be generalized, instead of checking each part one by one.We develop a prototype called ROPEY by incorporating our method into SPACER -a state-of-the-art SMC, and perform evaluations on the KIND2's simulation benchmarks.ROPEY is evaluated in two settings: online learning -for a given instance, we run SPACER for a number of iterations and collect its trace on which ROPEY is trained, and then use ROPEY to guide SPACER to finish the remaining solving process; and transfer learning -ROPEY is trained over historical runs of SPACER in advance, and for future instances, ROPEY is used directly to guide SPACER from the very beginning.For non-trivial benchmarks, ROPEY perfectly answers 72% and 77% of the queries in the online and transfer learning settings, respectively.While the speed improvement is not the focus of the paper, our preliminary results are promising: for non-trivial instances, ROPEY's end-toend running time is 25% faster.