ML + FV = $\heartsuit$？机器学习在形式化验证中应用的综述
软件工程
2018-06-13 v2 人工智能
机器学习
摘要
形式化验证（FV）与机器学习（ML）由于其对立的数学基础及在现实问题中的使用方式，似乎互不相容：FV 主要依赖离散数学并旨在确保正确性；ML 常依赖概率模型并从训练数据中学习模式。在本文中，我们假定它们在实践中是互补的，并探讨 ML 如何在其经典方法中帮助 FV：静态分析、模型检测、定理证明与 SAT 求解。我们描绘了当前实践的图景，并编目了 FV 工具中一些最显著的 ML 应用，从而提供关于 FV 技术的新视角，可帮助研究人员与从业者更好地定位可能的协同作用。我们讨论了从工作中获得的经验，指出可能的改进，并依据软件与系统建模科学对领域未来提出展望。
引用
@article{arxiv.1806.03600,
title = {ML + FV = $\heartsuit$? A Survey on the Application of Machine Learning to Formal Verification},
author = {Moussa Amrani and Levi Lúcio and Adrien Bibal},
journal= {arXiv preprint arXiv:1806.03600},
year = {2018}
}
备注
13 pages, no figures, 3 tables