By exploiting a number of relatively subtle programming language features, including dynamically-allocated mutable state, first-class functions, and effect handlers, reverse-mode automatic differentiation can be implemented as a library. One outstanding question, however, is: with which logical tools can one specify what this code is expected to compute and verify that it behaves as expected? We answer this question by using a modern variant of Separation Logic to specify and verify a minimalist (but concise and elegant) reverse-mode automatic differentiation library. We view this result as an advanced exercise in program verification, with potential future applications to more realistic automatic differentiation systems.


翻译:通过利用一些相对微妙的编程语言特征,包括动态分布的变异状态、头等功能和效果处理器,可以将反模式自动区分作为图书馆。然而,一个未决问题是:在哪些逻辑工具中可以具体说明该代码预期会如何计算和核实其行为是否如预期?我们用现代的分离逻辑变量来回答这个问题,以具体和核实一个最起码的(但简洁和优雅的)反模式自动区分图库。我们认为这一结果是一种先进的程序核查工作,今后有可能应用到更现实的自动区分系统。

0
下载
关闭预览

相关内容

这个新版本的工具会议系列恢复了从1989年到2012年的50个会议的传统。工具最初是“面向对象语言和系统的技术”,后来发展到包括软件技术的所有创新方面。今天许多最重要的软件概念都是在这里首次引入的。2019年TOOLS 50+1在俄罗斯喀山附近举行,以同样的创新精神、对所有与软件相关的事物的热情、科学稳健性和行业适用性的结合以及欢迎该领域所有趋势和社区的开放态度,延续了该系列。 官网链接:http://tools2019.innopolis.ru/
专知会员服务
28+阅读 · 2021年8月2日
专知会员服务
15+阅读 · 2021年5月21日
机器学习组合优化
专知会员服务
109+阅读 · 2021年2月16日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
152+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【资源】问答阅读理解资源列表
专知
3+阅读 · 2020年7月25日
Transferring Knowledge across Learning Processes
CreateAMind
28+阅读 · 2019年5月18日
已删除
将门创投
6+阅读 · 2019年1月11日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Arxiv
0+阅读 · 2022年2月17日
Arxiv
0+阅读 · 2022年2月15日
Arxiv
3+阅读 · 2021年11月1日
VIP会员
相关资讯
【资源】问答阅读理解资源列表
专知
3+阅读 · 2020年7月25日
Transferring Knowledge across Learning Processes
CreateAMind
28+阅读 · 2019年5月18日
已删除
将门创投
6+阅读 · 2019年1月11日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Top
微信扫码咨询专知VIP会员