Vehicle：弥合神经符号程序验证中的嵌入间隙

神经符号程序，即同时包含机器学习组件和传统符号代码的程序，正变得越来越普遍。由于涉及的不同工具数量众多，以及“神经”和“符号”程序组件之间的复杂接口，找到一种通用的方法来验证此类程序具有挑战性。在本文中，我们提出了神经符号验证问题的一般分解，并研究了当试图结合关于神经和符号组件的证明时出现的嵌入间隙问题。为了解决这个问题，我们引入了Vehicle——作为“验证条件语言”的缩写——一个介于机器学习框架、自动定理证明器和神经符号程序的依赖类型形式化之间的中间编程语言接口。Vehicle允许用户一次性指定神经符号程序中神经组件的属性，然后使用定制的类型检查和编译过程安全地将规范编译到每个接口。我们给出了Vehicle整体设计、其接口以及编译和类型检查过程的高级概述，然后通过形式化验证一个由神经网络控制的简单自动驾驶汽车在具有不完美信息的随机环境中的安全性来展示其实用性。