We present semantic correctness proofs of automatic differentiation (AD). We consider a forward-mode AD method on a higher order language with algebraic data types, and we characterise it as the unique structure preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming, based on diffeological spaces. We show that it interprets our language, and we phrase what it means for the AD method to be correct with respect to this semantics. We show that our characterisation of AD gives rise to an elegant semantic proof of its correctness based on a gluing construction on diffeological spaces. We explain how this is, in essence, a logical relations argument. Throughout, we show how the analysis extends to AD methods for computing higher order derivatives using a Taylor approximation.


翻译:我们提出自动区分的语义正确性证明( AD ) 。 我们考虑一种具有代数数据类型的更高顺序语言的前方模式AD方法, 我们把它描述为一种独特的结构, 通过选择基本操作的衍生物来保护宏观。 我们描述一个丰富的基于 difflogist 空间的不同编程语义学。 我们用它来解释我们的语言, 我们用它来表达对于这个语义来说AD方法的正确性的含义。 我们用它来说明我们的AD方法对于这个语义学的正确性。 我们证明我们的AD的特性产生了一个优雅的语义学证明, 证明它是正确的, 其基于在 difflogicutical 空间上加插根的构造。 我们解释这在本质上是一个逻辑关系论证。 我们从总体上讲, 我们展示了分析是如何扩大到使用 Taylor 近似法计算更高顺序衍生物的AD方法。

0
下载
关闭预览

相关内容

专知会员服务
52+阅读 · 2020年9月7日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
商业数据分析,39页ppt
专知会员服务
159+阅读 · 2020年6月2日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
【ICIG2021】Latest News & Announcements of the Tutorial
中国图象图形学学会CSIG
3+阅读 · 2021年12月20日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium6
中国图象图形学学会CSIG
2+阅读 · 2021年11月12日
讲座报名丨 ICML专场
THU数据派
0+阅读 · 2021年9月15日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
vae 相关论文 表示学习 1
CreateAMind
12+阅读 · 2018年9月6日
【推荐】自然语言处理(NLP)指南
机器学习研究会
35+阅读 · 2017年11月17日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
国家自然科学基金
3+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2022年4月19日
Risk and optimal policies in bandit experiments
Arxiv
0+阅读 · 2022年4月18日
Arxiv
23+阅读 · 2022年2月4日
Arxiv
64+阅读 · 2021年6月18日
VIP会员
相关VIP内容
专知会员服务
52+阅读 · 2020年9月7日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
商业数据分析,39页ppt
专知会员服务
159+阅读 · 2020年6月2日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
相关资讯
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
【ICIG2021】Latest News & Announcements of the Tutorial
中国图象图形学学会CSIG
3+阅读 · 2021年12月20日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium6
中国图象图形学学会CSIG
2+阅读 · 2021年11月12日
讲座报名丨 ICML专场
THU数据派
0+阅读 · 2021年9月15日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
vae 相关论文 表示学习 1
CreateAMind
12+阅读 · 2018年9月6日
【推荐】自然语言处理(NLP)指南
机器学习研究会
35+阅读 · 2017年11月17日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
相关基金
国家自然科学基金
3+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员