875
Certigrad——随机计算图优化系统
更多深度文章，请关注：https://yq.aliyun.com/cloud
Certigrad是一种概念证明，它是用于开发机器学习系统的一个新途径。其中包含以下组件：
- 应用本身
- 基础数据库
- 应用在数学上所需求的形式化描述
- 应用满足其形式化描述的机器可测证明
具体来说，Certigrad是一个优化的随机计算图形系统，我们使用Lean Theorem Prover调试系统，最终证明了在基础数学上是正确的。
优化验证
Certigrad项目的性能验证
- 我们对数学基础进行了理论化，而不是从最初的原理来构造它。
- 尽管我们的正确性定理只适用于无限精度实数，但我们必须用浮点数执行。
- Eigen的调用来替换原始的张量操作。
-
Certigrad
1.下载我们的Lean项目从https://github.com/dselsam/lean/tree/certigrad并且根据在https://github.com/leanprover/lean中的说明构建/安装。
2.下载Eigen并安装。
3.下载这个库，并在主目录执行leanpkg --建立。
我们已经正式证明Certigrad是正确的(在上面提到的问题)，但这并不意味着Certigrad是你所期望的那样。它的意思是，根据假设，与上面相关的定理是正确的。
Certigrad的设计是一个概念证明，不是一个生产系统。有许多功能需要添加，使之成为一个有用的工件。在发展的过程中，我们遇到了很多需要解决的问题来使我们的方法论经济化，并且我们在解决这些挑战比扩展和维护Certigrad作为目的本身更感兴趣。
一篇描述了Certigrad背后的理念的文章可以在 https://arxiv.org/abs/1706.08605 看，并将在2017年的ICML中出现。
- Daniel Selsam，斯坦福大学
- Percy Liang，斯坦福大学
本文由北邮@爱可可-爱生活老师推荐，阿里云云栖社区组织翻译。
最后更新：2017-07-13 15:32:44