Learning Invariants using Decision Trees and Implication Counterexamples
Learning Invariants using Decision Trees and Implication Counterexamples
复制标题
DOI：
10.1145/2914770.2837664
复制
发表时间：
2016-01-01
影响因子：
--
通讯作者：
Roth, Dan
中科院分区：
文献类型：
--
作者：
Garg, Pranav;Neider, Daniel;Roth, Dan
归纳不变量可以鲁棒地合成使用的学习模型，其中教师是一个程序验证谁指导学习者通过具体的程序配置，分类为积极的，消极的，和影响。我们提出了第一个学习算法在这个模型中的含义反例是基于机器学习技术。特别是，我们扩展了机器学习中的经典决策树学习算法来处理隐含样本，建立了新的可扩展的方法来构建小决策树使用统计措施。我们还开发了一个决策树学习算法在这个模型中，保证收敛到正确的概念（不变），如果存在的。我们实现了学习者和适当的教师，并表明由此产生的不变合成对于大型程序来说是高效且收敛的。
Inductive invariants can be robustly synthesized using a learning model where the teacher is a program verifier who instructs the learner through concrete program configurations, classified as positive, negative, and implications. We propose the first learning algorithms in this model with implication counter-examples that are based on machine learning techniques. In particular, we extend classical decision-tree learning algorithms in machine learning to handle implication samples, building new scalable ways to construct small decision trees using statistical measures. We also develop a decision-tree learning algorithm in this model that is guaranteed to converge to the right concept (invariant) if one exists. We implement the learners and an appropriate teacher, and show that the resulting invariant synthesis is efficient and convergent for a large suite of programs.