基于深度学习和反例制导的循环程序秩函数生成

Ranking Function Synthesis for Loop Programs via Counterexample Guided Deep Learning

程序终止性判定是程序分析与验证领域中的一个研究热点.针对非线性循环程序,提出了一种基于反例制导的神经网络型秩函数的构造方法.该方法采用学习组件和验证组件交互的迭代框架,其中,学习组件利用程序轨迹作为训练集合构造一个候选秩函数;验证组件运用可满足性模理论(satisfiability modulo theories,SMT)确保候选秩函数的有效性;而由SMT返回的反例则进一步用于扩展学习组件中的训练集合,以对候选秩函数进行精化.实验结果表明,所提出的方法比已有的机器学习方法在秩函数的构造效率和构造能力上具有优势.

This study proposes a novel approach for synthesizing ranking functions that are expressed as feed-forward neural networks.The approach employs a counter example-guided synthesis procedure,where a learner and a verifier interact to synthesize ranking function.The learner trains a candidate ranking function that satisfies the ranking function conditions over a set of sampled data,and the verifier either ensures the validity of the candidate ranking function or yields counterexamples,which are passed back to further guide the learner.The procedure leverages efficient supervised learning algorithm,while guaranteeing formal soundness via SMT solver.The tool SyntheRF is implemented,then,its scalability and effectiveness are evaluated over a set of benchmark examples.