论文标题
带有魔术的正式方法
Formal Methods with a Touch of Magic
论文作者
论文摘要
机器学习和正式方法具有免费的好处和缺点。在这项工作中，我们通过两个领域的技术组合解决了控制器设计问题。黑盒神经网络在深度增强学习中的使用（DEEP RL）对这种组合构成了挑战。我们从中提取了基于决策树的模型，而不是正式推理深RL的输出，我们称之为{\ em魔术书}。使用提取的模型作为中介，我们能够自己处理对深RL或正式方法不可行的问题。首先，我们首次将魔术书结合在合成过程中。我们合成了一个独立的逐个设计控制器，该控制器享有RL的良好性能。其次，我们将魔术书纳入有界模型检查（BMC）过程中。 BMC允许我们在巫师的控制下找到许多植物的痕迹，用户可以用来提高向导的信任度并直接进行进一步的培训。
Machine learning and formal methods have complimentary benefits and drawbacks. In this work, we address the controller-design problem with a combination of techniques from both fields. The use of black-box neural networks in deep reinforcement learning (deep RL) poses a challenge for such a combination. Instead of reasoning formally about the output of deep RL, which we call the {\em wizard}, we extract from it a decision-tree based model, which we refer to as the {\em magic book}. Using the extracted model as an intermediary, we are able to handle problems that are infeasible for either deep RL or formal methods by themselves. First, we suggest, for the first time, combining a magic book in a synthesis procedure. We synthesize a stand-alone correct-by-design controller that enjoys the favorable performance of RL. Second, we incorporate a magic book in a bounded model checking (BMC) procedure. BMC allows us to find numerous traces of the plant under the control of the wizard, which a user can use to increase the trustworthiness of the wizard and direct further training.
