利用强化学习为基于模板的循环不变式CEGIS学习启发式方法
人工智能
2022-06-16 v3 机器学习
编程语言
摘要
循环不变式合成是程序验证的基础。由于该问题在一般意义上不可判定，不变式合成工具必然使用启发式方法。尽管人们普遍认为启发式的设计对合成器的性能至关重要，但启发式往往由其开发者基于经验和直觉以临时方式设计。在本工作中，我们提出一种利用强化学习为基于模板的反例引导归纳合成（CEGIS）系统性地学习启发式的方法。作为一个具体示例，我们在PCSat之上实现了该方法，PCSat是一个基于模板CEGIS的不变式合成器。实验表明，由我们的框架学习到的启发式引导的PCSat不仅优于现有的最先进的基于CEGIS的求解器（如HoICE和神经求解器Code2Inv），而且在线性约束 Horn 子句（CHC）求解中也相对于非CEGIS求解器（如Eldarica和Spacer）具有轻微优势。
引用
@article{arxiv.2107.09766,
title = {Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning},
author = {Minchao Wu and Takeshi Tsukada and Hiroshi Unno and Taro Sekiyama and Kohei Suenaga},
journal= {arXiv preprint arXiv:2107.09766},
year = {2022}
}