资源介绍
证书
MLCert是用于在Coq证明助手中进行经过验证的机器学习的软件工具和库的集合，其中“在Coq中进行验证的机器学习”是指通过认证的通用保证（例如，学习模型的预期准确性的界限）进行的学习。 即将发布描述MLCert的技术报告。
建造
先决条件
Coq 8.8
Ver
俄亥俄州大学验证工具包，其中包含MLCert中使用的许多引理。
制作说明
第一个构建OUVerT ，通过在克隆库，并按照指示[OUVerT / README.md]。 不要忘记进行make install或sudo make install 。
然后，在MLCert ，执行以下操作：
make
make install
要将在TensorFlow中训练的神经网络传输到Coq，请按照自述文件末尾的说明进行操作。
组织
以下是开发中使用的主要目录和文件：
[NNCert /]：将MLCert应用于在TensorFlo