AI 中文总结
研究离散概率程序的反向模式自动微分，基于CHAD框架，以有限原子分布单子为例，定义反向模式代码变换并证明其正确性，为离散输出代数效应微分提供可复用模式，是扩展CHAD的基础步骤。
AI 中文摘要
我们分析了离散概率程序的反向模式自动微分（AD）。我们的构建是在组合同态自动微分（CHAD）框架中制定的，将 AD 视为程序的结构保持变换，并由表示语义指导。主要案例研究是有限原子分布单子，其计算具有有限支持和可微权重。关键在于对概率程序求微分时，余切不仅要通过确定性计算反向流动，还要通过概率结构本身。我们定义了相应的反向模式代码变换，并通过范畴逻辑关系论证证明了其对于处理实输出程序的正确性。尽管本文专注于有限离散概率，但该构建为离散输出代数效应的微分提供了可复用模式，包括有限多重集非确定性、异常和写入器式累加等。更广泛地说，我们将此工作视为将 CHAD 扩展到更丰富概率语言和其他带处理程序代数效应的基础步骤。
英文摘要
We analyse reverse-mode automatic differentiation (AD) for discrete probabilistic programs. Our construction is formulated in the framework of Combinatory Homomorphic Automatic Differentiation (CHAD), treating AD as a structure-preserving transformation of programs, guided by a denotational semantics. The main case study is the finite atomic distribution monad, whose computations have finite support and differentiable weights. The key point is that differentiating probabilistic programs requires cotangents to flow backwards not only through deterministic computations, but also through the probabilistic structure itself. We define the corresponding reverse-mode code transformation and prove its correctness, for handled real-output programs, by a categorical logical-relations argument. Although the paper focuses on finite discrete probability, the construction gives a reusable pattern for differentiating discrete-output algebraic effects, including finite multiset non-determinism (e.g., from fork-join parallelism), exceptions, and writer-style accumulation (e.g., for in-place accumulation of high-dimensional vectors). More broadly, we view this work as a foundational step towards extending CHAD to richer probabilistic languages and to other algebraic effects with handlers.
Comments71 pages, submitted to POPL 2027
