우리는 이산 확률론적 프로그램에 대한 역모드 자동 미분(reverse-mode automatic differentiation, AD)을 분석합니다. 우리의 구성은 조합자 동형 자동 미분(Combinatory Homomorphic Automatic Differentiation, CHAD) 프레임워크 내에서 공식화되며, AD를 의미론적 해석(denotational semantics)에 의해 안내되는 프로그램의 구조 보존 변환으로 취급합니다. 주요 사례 연구는 유한 원자 분포 모나드(finite atomic distribution monad)이며, 이 계산은 유한 지원(finite support)과 미분 가능한 가중치를 갖습니다. 핵심은 확률론적 프로그램을 미분하려면 코탄젠트(cotangents)가 결정론적 계산뿐만 아니라 확률론적 구조 자체를 통해서도 역방향으로 흐르도록 해야 한다는 것입니다. 우리는 이에 해당하는 역모드 코드 변환을 정의하고, 범주론적 논리 관계(categorical logical-relations argument)를 통해 처리된 실수 출력 프로그램에 대해 그 정확성을 증명합니다. 비록 이 논문이 유한 이산 확률에 초점을 맞추고 있지만, 이 구성은 유한 다중 집합 비결정성(finite multiset non-determinism)(예: fork-join 병렬성에서), 예외 처리(exceptions), 그리고 쓰기 스타일 누적(writer-style accumulation)(예: 고차원 벡터의 제자리 누적을 위해)을 포함하는 이산 출력 대수 효과를 미분하기 위한 재사용 가능한 패턴을 제공합니다. 더 넓게는, 우리는 이 작업을 CHAD를 더 풍부한 확률론적 언어와 핸들러가 있는 다른 대수 효과로 확장하기 위한 기초 단계로 간주합니다.