We present Self-Driven Strategy Learning (sdsl), a lightweight online learning methodology for automated reasoning tasks that involve solving a set of related problems. sdsl automatically gathers information, in form of a dataset, while solving earlier problems. It utilizes the learned data to adjust the solving strategy for later problems by fitting a machine learning model to the obtained data on the fly. We formally define the approach as a set of abstract transition rules. We describe a concrete instance of the sdsl calculus which uses conditional sampling for generating data and random forests as the underlying machine learning model. We implement the approach on top of the Kissat solver and show that the combination of Kissat+sdsl certifies larger bounds and finds more counter-examples than other state-of-the-art bounded model checking approaches on benchmarks obtained from the latest Hardware Model Checking Competition.

翻译：我们提出自驱动策略学习（Self-Driven Strategy Learning, SDSL），这是一种面向涉及求解一组相关问题的自动推理任务的轻量级在线学习方法。SDSL 在求解先前问题的过程中自动收集数据（以数据集形式），并利用所学数据实时调整后续问题的求解策略——通过将机器学习模型拟合至所得数据实现。我们以一组抽象转换规则的形式正式定义该方法，并描述了SDSL演算的一个具体实例：该实例采用条件采样生成数据，以随机森林作为底层机器学习模型。我们在Kissat求解器基础上实现了该方法，实验表明，在最新的硬件模型检验竞赛基准测试中，Kissat+SDSL组合相比其他最先进的边界模型检验方法能够证明更大的边界值并发现更多反例。