带一点魔法的形式化方法

机器学习与形式化方法具有互补的优势与缺陷。在本文中，我们结合两领域的技朮解决控制器设计问题。深度强化学习（deep RL）中黑盒神经网络的使用给此类结合带来挑战。我们不直接对称为{\em wizard}的deep RL输出进行形式化推理，而是从中提取基于决策树的模型，称之为{\em magic book}。利用提取的模型作为中介，我们能够处理单独使用deep RL或形式化方法均不可行的问题。首先，我们首次提出在综合流程中结合magic book。我们综合出一个独立、正确-by-design的控制器，其享有RL的良好性能。其次，我们将magic book纳入有界模型检验（BMC）流程。BMC使我们能找到在wizard控制下被控对象的众多轨迹，用户可借此增加对wizard的信任并指导进一步训练。