一句话：用 Agda 形式化并抽取到 Futhark，使自动微分与 CNN 代码兼具正确性保证和接近 TensorFlow 的性能。
本文提出一种在定理证明器中开发高性能应用并保证正确性的技术。作者用 Agda 形式化一个面向索引安全张量的反向模式自动微分框架，该框架包含张量表达式优化器，并能将表达式翻译为高性能数组语言 Futhark。随后在 Agda 中指定一个典型卷积神经网络，计算训练所需的导数，并抽取生成 Futhark 代码。评估在 GPU 上运行生成的代码，并与 TensorFlow 实现比较；结果显示生成代码的性能接近 TensorFlow，表明形式化规范与抽取可在不牺牲性能的前提下提供强正确性保证。
In this paper we demonstrate a technique for developing high performance applications with strong correctness guarantees. Using a theorem prover, we derive a high-level specification of the application that includes correctness invariants of our choice. After that, within the same theorem prover, we implement an extraction of the specified application into a high-performance language of our choice. Concretely, we are using Agda to specify a framework for automatic differentiation (reverse mode) that is focused on index-safe tensors. This framework comes with an optimiser for tensor expressions and the ability to translate these expressions into Futhark. We specify a canonical convolutional neural network within the proposed framework, compute the derivatives needed for the training phase and then demonstrate that the generated code approaches the performance of TensorFlow code when running on a GPU.
@article{paperbot3035,
title = {Correctness Meets Performance: From Agda to Futhark},
author = {Artjoms Šinkarovs and Troels Henriksen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747524}
}