Certifying the True Error: Machine Learning in Coq with Verified Generalization Guarantees
Certifying the True Error: Machine Learning in Coq with Verified Generalization Guarantees
复制标题
DOI：
10.1609/aaai.v33i01.33012662
复制
发表时间：
2019-07
期刊：
影响因子：
--
通讯作者：
Alexander Bagnall;Gordon Stewart
中科院分区：
文献类型：
--
作者：
Alexander Bagnall;Gordon Stewart
我们提出了一种用于学习过程的概括的新型系统，以训练或测试误差有限。 COQ的检查器检查。即使没有COQ专业知识的人也可以验证MLCERT，这与诸如Tensorflow之类的外部工具兼容，我们使用它来证明对使用TensorFlow训练的神经网络的概括性界限。
We present MLCERT, a novel system for doing practical mechanized proof of the generalization of learning procedures, bounding expected error in terms of training or test error. MLCERT is mechanized in that we prove generalization bounds inside the theorem prover Coq; thus the bounds are machine checked by Coq’s proof checker. MLCERT is practical in that we extract learning procedures defined in Coq to executable code; thus procedures with proved generalization bounds can be trained and deployed in real systems. MLCERT is well documented and open source; thus we expect it to be usable even by those without Coq expertise. To validate MLCERT, which is compatible with external tools such as TensorFlow, we use it to prove generalization bounds on neural networks trained using TensorFlow on the extended MNIST data set.