CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples

We propose CheckDP, the first automated and integrated approach for proving or disproving claims that a mechanism is differentially private. CheckDP can find counterexamples for mechanisms with subtle bugs for which prior counterexample generators have failed. Furthermore, it was able to \emph{automatically} generate proofs for correct mechanisms for which no formal verification was reported before. CheckDP is built on static program analysis, allowing it to be more efficient and more precise in catching infrequent events than existing counterexample generators (which run mechanisms hundreds of thousands of times to estimate their output distribution). Moreover, its sound approach also allows automatic verification of correct mechanisms. When evaluated on standard benchmarks and newer privacy mechanisms, CheckDP generates proofs (for correct mechanisms) and counterexamples (for incorrect mechanisms) within 70 seconds without any false positives or false negatives.

INTRODUCTION
Differential privacy [27] has been adopted in major data sharing initiatives by organizations such as Google [15,29], Apple [48], Microsoft [22], Uber [36] and the U.S. Census Bureau [1,17,35,41]. It allows these organizations to collect and share data with provable bounds on the information that is leaked about any individual.
Crucial to any differentially private system is the correctness of privacy mechanisms, the underlying privacy primitives in larger privacy-preserving algorithms. Manually developing the necessary rigorous proofs that a mechanism correctly protects privacy is a subtle and error-prone process. For example, detailed explanations of significant errors in peer-reviewed papers and systems can be found in [21,40,42]. Such mistakes have led to research in the application of formal verification for proving that mechanisms satisfy differential privacy [3, 5, 7, 9-11, 50, 51]. However, if a mechanism has a bug making its privacy claim incorrect, these techniques cannot disprove the privacy claims -a counterexample detector must be used instead [14,23,34]. Finding a counterexample is typically a two-phase process that (1) first searches an infinitely large space for candidate counterexamples and then (2) uses an exact symbolic probabilistic solver like PSI [33] to verify that the counterexample is indeed valid. The search phase currently presents the most problems (i.e., large runtimes or failure to find counterexamples are most often attributed to the search phase). Earlier search techniques were based on sampling (running a mechanism hundreds of thousands of times), which made them slow and inherently imprecise: even with enormous amounts of samples, they can still fail if a privacy-violating section of code is not executed frequently enough or if the actual privacy cost is slightly higher than the privacy claim. Recently, static program analyses were proposed to accomplish both goals [4,30]. However, they either only analyze a non-trivial but restricted class of programs [4], or rely on heuristic strategies whose effectiveness on many sutble mechanisms is unclear [30].
In this paper, we present CheckDP, an automated and integrated tool for proving or disproving the correctness of a mechanism that claims to be differentially private. Significantly, CheckDP automatically finds counterexamples via static analysis, making it unnecessary to run the mechanism. Like prior work [14], CheckDP still uses PSI [33] at the end. However, replacing sampling-based search with static analysis enables CheckDP to find violations in a few seconds, while previous sampling-based methods [14,23] may fail even after running for hours. Furthermore, sampling-based methods may still require manual setting of some program inputs (e.g., DP-Finder [14] requires additional arguments to be set manually for Sparse Vector Technique in our evaluation) while CheckDP is fully automated. Furthermore, the integrated approach of CheckDP allows it to efficiently analyze a larger class of differentially privacy mechanisms, compared with concurrent work using static analyses [4,30].
Meanwhile, CheckDP still offers state-of-the-art verification capability compared with existing language-based verifiers and is further able to automatically generate proofs for 3 mechanisms for which no formal verification was reported before. CheckDP takes the source code of a mechanism along with its claimed level of privacy and either generates a proof of correctness or a verifiable counterexample (a pair of related inputs and a feasible output). CheckDP is built upon a proof technique called randomness alignment [24,50,51], which recasts the task of proving differential privacy into one of finding alignments between random variables used by two related runs of the mechanism. CheckDP uses a novel verify-invalidate loop that alternatively improves tentative proofs (in the form of alignments), which are then used to improve tentative counterexamples (and vice versa) until either the tentative proof has no counterexample, or the tentative counterexample has no alignment.
We evaluated CheckDP on correct/incorrect versions of existing benchmarks and newly proposed mechanisms. It generated a proof for each correct mechanism within 70 seconds and a counterexample for each incorrect mechanism within 15 seconds.
In summary, this paper makes the following contributions: (1) CheckDP, one of the first automated tools (with concurrent work [4,30]) that generates both proofs for correct mechanisms and counterexamples for incorrect mechanisms (Section 2.4).
(2) A syntax-directed translation from the probabilistic mechanism being checked to non-probabilistic target code with explicit proof obligations (Section 3). (3) An alignment template generation algorithm (Section 3.4).

(4) A novel verify-invalidate loop that incrementally improves tentative proofs and counterexamples (Section 4). (5) Case studies and experimental comparisons between CheckDP
and existing tools using correct/incorrect versions of existing benchmarks and newly proposed mechanisms. For incorrect mechanisms, CheckDP automatically found counterexamples in all cases, even in cases where competing methods [14,23] failed. For correct mechanisms, CheckDP automatically generated proofs of privacy, including proofs for 3 mechanisms for which no formal verification was reported before (Section 5).

PRELIMINARIES AND RUNNING EXAMPLE 2.1 Differential Privacy
Among several popular variants of differential privacy [16,26,27,43], we focus on pure differential privacy [27]. The goal of differential privacy is to hide the effect of any person's record on the output of an algorithm. This is achieved by considering all pairs of datasets D and D ′ that differ on one record. We call such datasets adjacent and denote it by D ∼ D ′ . To offer privacy, a differentially private algorithm injects carefully calibrated random noise during its computation. Given a pair of datasets (D, D ′ ), we call the execution of an algorithm on D the original execution and the execution on (neighboring) D ′ the related execution. Intuitively, we say a randomized algorithm is differentially private if the output distribution of the original execution and its related execution are hard to distinguish for all such dataset pairs: Definition 1 (Pure Differential Privacy [25]). Let ϵ ≥ 0. Often, a differentially private algorithm M interacts with a dataset D through a list of queries f 1 , f 2 , . . .: it iteratively runs a query f i on D to get an exact answer q i , then performs some randomized computation on the set of query answers {q j | j ≤ i}. We call the vector (q 1 , q 2 , . . .) along with other data-independent parameters to M (e.g., privacy parameter ϵ) an input to M. The notion of adjacent datasets translates into the notion of sensitivity on those queries: Definition 2 (Global Sensitivity [28]). The global sensitivity of a query f is We say two inputs inp = {(q 1 , q 2 , . . .), params} and inp ′ = {(q ′ 1 , q ′ 2 , . . .), params} are adjacent with respect to the queries f 1 , f 2 , . . ., and write inp ∼ inp ′ , if the params are the same and there exist two adjacent datasets D and It follows that differential privacy can be proved by showing that for all pair of inputs inp ∼ inp ′ and all outputs o ∈ O, P[M(inp) = o] ≤ e ϵ P[M(inp ′ ) = o]. As standard, we assume that the sensitivity of inputs are either manually specified or computed by sensitivity analysis tools (e.g., [32,44]).
Many mechanisms are built on top of the Laplace Mechanism [27] which adds Laplace noise to query answers: Theorem 1 (Laplace Mechanism [27]). Let ϵ > 0, let D be a dataset, let f be a query with sensitivity ∆ f and let q = f (D).
The Laplace Mechanism which, on input q, outputs q + η (where η is sampled from the Laplace distribution with mean 0 and scale parameter ∆ f /ϵ) satisfies ϵ-differential privacy.
We sometimes abuse notation and refer to the sensitivity ∆ q of a numerical value q -we always take this to mean as the sensitivity of the function that produced q.

Randomness Alignment
Randomness alignment is a simple yet powerful proof technique that underpins the verification tools LightDP [51] and its successor ShadowDP [50]. Precise reasoning using this proof technique was used to improve a variety of algorithms, allowing them to release strictly more information at the same privacy cost [24]. Given two executions of a randomized algorithm M on D and D ′ respectively, a randomness alignment is a mapping between the random variables in the first execution to random variables in the second execution that will cause the second execution to always produce the same output as the first. Upper bounds on privacy parameters depend on how much the random variables change under this mapping [51].
We use the Laplace Mechanism [28] to illustrate the key ideas behind randomness alignment. Let D ∼ D ′ be a pair of neighboring datasets and let f be a query with sensitivity ∆ f . Let q = f (D) and q ′ = f (D ′ ) be the respective query answers. If we use the Laplace Mechanism to answer these queries with privacy, on input q (resp. q ′ ) it will output q + η (resp. q ′ + η ′ ) where η (resp. η ′ ) is a Laplace random variable with scale ∆ f /ϵ. In order for the Laplace Mechanism to produce the same output in both executions, we need q + η = q ′ + η ′ and therefore η ′ = η + q − q ′ . This creates a "mapping" between the values of random noises: if we change the input from q to q ′ , we need to adjust the random noise by an amount of q − q ′ (i.e., this is the distance we need to move η ′ to get to η). Clearly q − q ′ ≤ ∆ f by definition of sensitivity. The privacy proof follows from the fact that if two random samples η and η ′ (from the Laplace distribution with scale ∆ f /ϵ) are at most distance ∆ f apart, the ratio of their probabilities is at most e ϵ . Hence, the privacy cost, the natural log of this ratio, is bounded by ϵ.
Thus randomness alignment can be viewed in terms of distances that we need to move random variables. Let q ∼ q ′ be query answers from neighboring datasets and M be a randomized algorithm which uses a set of random noises H = η . We associate to every random variable η a numeric value η which tracks precisely the amount in value we need to change η in order to obtain the same output when the input to M is changed from q to q ′ . In other words, the output of M with input q and random values η is the same as that of M with input q ′ and random values η + η . Taking M to be the Laplace Mechanism, then the alignment in the previous paragraph is η = q − q ′ . Note that the alignment is a function that depends on M as well as q and q ′ .
If all of the random variables are Laplace, the cost of an alignment is the summation of distance noise scale for each random variable. To find the overall privacy cost (e.g., the ϵ in differential privacy), we then find an upper bound on the alignment cost for all related q and q ′ .

Privacy Proof and Counterexample
Not all randomness alignments serve as proofs of differential privacy. To form a proof, one must show that (1) the alignment forces 2 the two related executions to produce the same output, (2) the privacy cost of an alignment must be bounded by the promised level of privacy, and (3) the alignment is injective. Hence, in this paper, an (alignment-based) privacy proof refers to a randomness alignment that satisfies these requirements.
On the other hand, to show that an algorithm violates differential privacy, it suffices to demonstrate the existence of a counterexample. Formally, if an algorithm M claims to satisfy ϵ-differential privacy, a counterexample to this claim is a triple Challenges. LightDP [51] and ShadowDP [50] can check if a manually generated alignment is an alignment-based privacy proof. On the other hand, an exact symbolic probabilistic solver, such as PSI [33], can check if a counterexample, either generated manually or via a sampling-based generator, witnesses violation of differential privacy. To the best of our knowledge, CheckDP is the first tool that automatically generates alignment-based proofs/counterexamples via static program analysis. 1 To do so, a key challenge is to tackle the infinite search space of proofs (i.e., alignments) and counterexamples. CheckDP uses a novel proof template generation algorithm to reduce the search space of candidate alignments (Section 3) and uses a novel verify-invalidate loop (Section 4) to find tentative proofs, counterexamples showing their privacy cost is too high, improved proofs, improved counterexamples, etc.

Running Examples
To illustrate our approach, we now discuss two variants of the Sparse Vector Technique [28], one correct and one incorrect. Using the two variants, we sketch how CheckDP automatically proves/disproves (as appropriate) their claimed privacy properties.
Sparse Vector Technique (SVT) [28]. A powerful mechanism proven to satisfy differential privacy. It can be used as a building block for many advanced differentially private algorithms. This mechanism is designed to solve the following problem: given a series of queries and a preset public threshold, we want to identify the first N queries whose answers are above the threshold, but in a privacy-preserving manner. To achieve this, it adds independent Laplace noise both to the threshold and each query answer, then it returns the identities of the first N queries whose noisy answers are above the noisy threshold. The standard implementation of SVT outputs true for the above-threshold queries and false for the others (and terminates when there are a total of N outputs equal to true). We use two variants of SVT for an overview of CheckDP.
GapSVT. This is an improved (and correct) variant of SVT which provides numerical information about some queries. When a noisy query exceeds the noisy threshold, it outputs the difference between these noisy values; otherwise it returns false. This provides an estimate for how much higher a query is compared to the threshold. The algorithm was first proposed and verified in [50]; its pseudo code is shown in Figure 1. Here, Lap (2/ϵ) draws one sample from Laplace distribution with mean 0 and scale factor of 2/ϵ. This random value is then added to the public threshold T (stored as noisy 1 Prior work [3] automatically generates coupling proofs, an alternative language-based proof technique for differential privacy. But all existing verifiers using alignment-based proofs [50,51] require manually provided alignments. threshold T η ). For each query answer, another independent Laplace noise η 2 = Lap (4N /ϵ) is added. If the noisy query answer q[i] + η 2 is above the noisy threshold T η , the gap between them (q[i] + η 2 − T η ) is added to the output list out, otherwise 0 is added.
The random variables and θ are inserted as part of the function input.
One key observation from the manual proofs of SVT and its variants [21,24,28,40] is that the privacy cost is only paid for the queries whose noisy answers are above the noisy threshold. In other words, outputting false does not incur any new privacy cost. Correspondingly, the correct alignment for GapSVT [24,50] (that is, the distance that η 1 and η 2 need to be moved to ensure the output is the same when the input changes from q[i] to q ′ [i] ≡ q[i] + q[i], for all i) is: η 1 : 1 and η 2 : Note that η 2 is aligned with non-zero distance only under the true branch; hence, no privacy cost is paid in the other branch. It is easy to verify that if every query has sensitivity 1, the cost of this alignment is bounded by ϵ.
BadGapSVT. We also consider a variant of SVT (and GapSVT) that incorrectly tries to release numerical information. When a noisy query answer is larger than the noisy threshold, the variant releases that noisy query answer (that is, it does not subtract from it the noisy threshold); otherwise it outputs false. This is an incorrect variant of SVT [45] that was reported in [40] and was called iSVT4 in [23]. More precisely, BadGapSVT replaces line 7 of GapSVT with out := (q[i] + η 2 )::out;. This small change makes it not ϵ-differentially private [40]. The reason why is subtle, but the intuition is the following. Suppose BadGapSVT returns a noisy query answer q[i] + η 2 = 3, the attacker is able to deduce that T η ≤ 3. Once this information is leaked, outputting false in the else branch is no longer "free"; every output incurs a privacy cost.

Approach Overview
We use GapSVT and BadGapSVT to illustrate how CheckDP generates proofs and counterexamples.
Code Transformation (Section 3). CheckDP first takes the probabilistic algorithm being checked, written in the CheckDP language (Section 3.1), and generates the non-probabilistic target code with assertions and alignment templates (i.e. templates for possible alignments). The bottom of Figure 1 shows the transformed code of GapSVT with alignment templates. The transformed code is distinguished from the source code in a few important ways: (1) The probabilistic sampling commands (at lines 1 and 5) are replaced by non-probabilistic counterparts that read samples from the instrumented function input sample. (2) An alignment template (e.g., A 1 , A 2 ) is generated for each sampling command; each template contains a few holes, i.e., θ , which is also instrumented as function input. (3) A distinguished variable v ϵ is added to track the overall privacy cost and lines 14 and 20 update the cost variable in a sound way. (4) Assertions are inserted in the transformed code (lines 22,23,27,30) to ensure the following soundness property: if M(inp) is transformed to M ′ (inp, inp, sample, θ ), then ∃θ . ∀inp, inp, sample. all assertions in M ′ pass =⇒ M is differentially private We note that the transformed code forms the basis for both proof and counterexample generation in CheckDP.
Proof/Counterexample Generation (Section 4). Inspired by the Counterexample Guided Inductive Synthesis (CEGIS) [46] technique, originally proposed for program synthesis, CheckDP uses a verify-invalidate loop to simultaneously generate proofs and counterexamples. Unlike CEGIS, however, the verify-invalidate loop is bidirectional, in the sense that it internally records all previous counterexamples (resp. proofs) to generate one proof (resp. counterexample) as the algorithm output. On the other hand, the CEGIS loop is unidirectional: it only collects and uses a set of inputs to guide synthesis internally. At a high level, the verify-invalidate loop of CheckDP includes two integrated sub-loops, one for proof generation and the other for counterexample generation.
Verify Sub-loop. Its goal is to generate a proof (i.e., an instantiation of θ ) such that ∀inp, inp, sample. all assertions in M ′ pass This is done by two iterative phases: (1) Generating invalidating inputs: Given a proof candidate (i.e., an instantiation of θ ), it is incorrect if ∃inp, inp, sample. some assertion in M ′ fails We use I to denote a triple of inp, inp, sample. Hence, given any instantiation of θ , we use an off-the-shelf symbolic execution tool such as KLEE [18] to find invalidating inputs when possible. (2) Generating proof candidates: with a set of invalidating inputs found so far I 1 , · · · , I i , we can try to generate a new proof candidate to satisfy Starting from a default instantiation (e.g., one that sets ∀i. θ [i] = 0), CheckDP iteratively repeats Phases 1 and 2. Since CheckDP uses all invalidating inputs found so far in Phase 2, the proof candidate after each iteration is improving. When Phase 1 gets stuck, CheckDP obtains a proof candidate θ which is a privacy proof if due to the soundness property above. Hence, a proof (alignment) can be validated by program verification tools such as CPAChecker [13]. For GapSVT, CheckDP generates and verifies (via CPAChecker) that θ = {1, 1, 0, −1, 0, 0, 0} results in a proof that GapSVT satisfies ϵdifferential privacy.
Invalidate Sub-loop. While the verify sub-loop is conceptually similar to a CEGIS loop [46], CheckDP also employs an invalidate sub-loop (integrated with the verify sub-loop); its goal is to generate one invalidating input I such that ∀θ . some assertion in M ′ fail. This is done by two iterative phases: 2 (1) Generating proof candidates: Given an invalidating input I , it is incorrect if ∃θ . M ′ (I, θ ). Hence, given any I , we can use KLEE [18] to find an alignment when possible. (2) Generating counterexamples: with a set of previously found alignments θ 1 , · · · , θ i , we try to find a new invalidating input to satisfy To integrate with the verify sub-loop, Phase 1 of the invalidate sub-loop starts when Phase 2 of the verify sub-loop gets stuck with a set of invalidating inputs I 1 , · · · , I i ; it uses I i to proceed since it is the most promising one. When Phase 1 of invalidate sub-loop gets stuck, CheckDP obtains a counterexample candidate, which can be validated by PSI [33] (this is necessary since a mechanism might be differentially private even if no alignment-based proof exists). For example, the counterexample found for BadGapSVT sets the threshold T = 0, N = 1 (max number of outputs equal to true before termination), neighboring inputs q = [0, 0, 0, 0, 0] and q ′ = [1, 1, 1, 1, −1], and the following output to examine [0, 0, 0, 0, 1]. PSI confirms that the probability of this output when q is an input is ≥ e ϵ times the probability of this output when q ′ is the input. When Phase 1 of the invalidate sub-loop generates a new alignment θ , which happens in our empirical study (Section 5), Phase 2 follows to generate an "improved" invalidating input, which is then used to start Phase 2 of the validate sub-loop.

PROGRAM TRANSFORMATION
CheckDP takes a probablistic program along with an adjacency specification (i.e., how much two adjacent inputs can differ) and the claimed level of differential privacy as inputs. It translates the source code into a non-probabilistic program with assertions to ensure differential privacy. The transformed code forms the basis of finding a proof or a counterexample (Section 4).

Syntax
The syntax of CheckDP source code is listed in Figure 2. Most of the syntax is standard with the following features: • Real numbers, booleans and their standard operations; • Ternary expressions b ? n 1 : n 2 , it returns n 1 when b evaluates to true or n 2 otherwise; • List operations: e 1 :: e 2 appends element e 1 to list e 2 , and e 1 [e 2 ] gets the e th 2 element of list e 1 ; • Loop with keyword while and branch with keyword if; • A final return command return e. We now introduce other interesting parts that are needed for developing differentially private algorithms.
Random Expressions. Differential privacy relies heavily on probabilistic computations: many mechanisms achieve differential privacy by adding appropriate random noise to variables. To model this behavior, we embed a sampling command η := Lap r in CheckDP, which draws a sample from the Laplace distribution with mean 0 and scale of r . In this paper, we only focus on the most interesting sampling command Lap r (which is used in Laplace Mechanism and GapSVT in Section 2). However, we note that it is fairly easy to add new sampling distributions to CheckDP.
For clarity, we distinguish variables holding random values, denoted by η ∈ H, from other ones, denoted by x ∈ V.
Types with Distances. To enable alignment-based proof, one important aspect of the type system in CheckDP is the ability to compute and track the distances for each program variable. Motivated by verification tools using alignments (e.g., LightDP [51] and ShadowDP [50]), types in the source language of CheckDP have the form of B 0 or B * , where B is the base type such as numerics (num), booleans (bool) and lists (list τ ). The subscript of each type is the key to alignment-based proofs: it explicitly tracks the exact difference between the value of a variable in two related runs.
In the source language of CheckDP, the distances can either be 0 or * : the former indicates the variables stay the same in the related runs; the latter means that the variable might hold different values in two related runs and the value difference is stored in a distinguished variable x added by the program transformation (i.e., a syntactic sugar for dependent sum type ( x : num 0 ) B x ). For example, inputs T,N,size are annotated with distance 0 in Figure 1, meaning that they are public parameters to the algorithm; query answers q are annotated with distance * , meaning that each q[i] differ by exactly q[i] in two related runs. The type system distinguishes zero-distance variables as an optimization: as we show shortly, it helps to reduce the code size for later stages (Section 3.3) as well as aids proof template generation (Section 3.4).
Note that boolean types (bool) and list types (list τ ) cannot be associated with numeric distances, hence omitted in the syntax. However, nested cases such as list num * still accurately track the distances of the elements inside the list.
The semantics of CheckDP follows the standard definitions of probabilistic programs [37]; the formal semantics can be found in the Appendix. Finally, CheckDP also supports shadow execution, a technique that underpins ShadowDP [50] and is crucial to the verification of challenging mechanisms such as Report Noisy Max [25]. However, in order to focus on the most interesting parts of CheckDP, we first present the transformation without shadow execution, and later discuss how to support it.

Program Transformation
CheckDP is equipped with a flow-sensitive type system whose typing rules are shown in Figure 3. At command level, each rule has the following format: ⊢ Γ {c ⇀ c ′ } Γ ′ where a typing environment Γ tracks for each program variable its type with distance, c and c ′ are the source and target programs respectively, and the flow-sensitive type system also updates typing environment to Γ ′ after command c. At a high-level, the type system transforms the probabilistic source code c into the non-probabilistic target code c ′ in a way that if all assertions in c ′ holds, then c is differentially private.
CheckDP's program transformation is motivated by those of LightDP and ShadowDP [50,51], all built on randomness alignment proof. However, there are a few important differences: • CheckDP generates an alignment template for each sampling instruction, rather than requiring manually provided alignments. • CheckDP defers all privacy-related checks to assertions. This is crucial since information needed for proof and counterexample generation is unavailable in a lightweight static type system. 5 Transformation rules for expressions with form Γ ⊢ e : B n (T-Laplace) Transformation rules for merging environments • CheckDP only tracks if a variable has the same value in two related runs (with distance 0) or not (with distance * ). This design aids alignment template generation and reduces the size of transformed code.
Checking Expressions. Each typing rule for expression e computes the correct distance for its resulting value: Γ ⊢ e : B n | C, which reads as: expression e has type B and distance n under the typing environment Γ if the constraints C are satisfied. The reason to collect constraints C instead of statically checking them, is to defer all privacy-related checks to later stages.
Most of the expression rules are straightforward: they check the base types (just like a traditional type system) and compute the distance of e's value in two related runs. For example, all constants must be identical (Rules (T-Num,T-Boolean)) and the distance of a variable is retrieved from the environment (T-VarZero,T-VarStar) (note that rule (T-VarStar) just desugers the * notation). For linear operation (⊕), the distance of the result is computed in a precise way (Rule (T-OPlus)), while the other operations are treated in a more conservative way: constraints are generated to ensure that the result is identical in Rules (T-OTimes, T-ODot). For example, (T-ODot) ensures boolean value of e 1 ⊙ e 2 will be the same in two related runs by adding a constraint (e 1 ⊙ e 2 ) ⇔ (e 1 + n 1 ) ⊙ (e 2 + n 2 ) (T-Cons) restricts constructed list elements to have 0-distance (note that the restriction does not apply to input lists), while (T-Index) requires the index to have zero-distance. Rule (T-Select) restricts e 1 and e 2 to have the same distance. The constraints gathered in the 6 expression rules will later be explicitly instrumented as assertions in the translated programs, which we will explain shortly.

Checking Commands
For each program statement, the type system updates the typing environment and if necessary, instruments code to update x variables to the correct distances. Moreover, it ensures that the two related runs take the same branch in if-statement and while-statement.
Flow-Sensitivity. Each typing rule updates the typing environment to track if a variable has zero-distance. When a variable has non-zero distance, it instruments the source code to properly maintain the corresponding x variables. The most interesting rules are: rule (T-Asgn) properly promotes the type of x to be B * (tracked by distance variables) in Γ ′ if the distance of e is not 0. Meanwhile it optimizes away updates to x and properly downgrades type to B 0 if e has a zero-distance. For example, line 16 in GapSVT (Figure 1) is instrumented to update distance of T η , according to the distance of T + η 1 . Moreover, variable count in GapSVT always has the type num 0 ; therefore its distance variable never appears in the translated program due to the optimization in (T-Asgn).
Rule (T-If) and (T-While) are more complicated since they both need to merge environments. In rule (T-If), as c 1 and c 2 might update Γ to Γ 1 and Γ 2 respectively, we need to merge them in a natural way: the distance of a type form a two-level lattice with 0 ⊏ * . Thus we define a union operator ⊔ for distances d as: therefore the union operator for two environments are defined as follows: Moreover, we use an auxiliary function Γ 1 , Γ 2 ⇛ c to "promote" a variable to star type. Similarly, the typing environments are merged in rule (T-While), except that it requires a fixed point Γ f such that ⊢ Γ ⊔ Γ f {c} Γ f . We follow the construction in [50] to compute a fixed point, noting that the computation always terminates since all of the translation rules are monotonic and the lattice only has two levels.
Assertion Generation. To ensure differential privacy, the type system inserts assertion in various rules: • To ensure that two related runs take the same control flow, (T-If) and (T-While) asserts that the value of the branch condition stays the same across two related executions. A helper function e, Γ • is used to compute the value of e in the aligned execution; its full definition can be found in the Appendix.
• To ensure that the final output value is differentially private, rule (T-Return) asserts that its distance is zero (i.e., identical in two related runs). • To ensure all constraints collected in the expression rules are satisfied, assignment rules (T-Asgn) and (T-AsgnStar) also insert corresponding assertions.

Checking Sampling Commands
Rule (T-Laplace) performs a few important tasks: Replacing Sampling Command. Rule (T-Laplace) removes the sampling instruction and assign to η the next (unknown) sample value sample[idx], where sample is a parameter of type list num added to the transformed code. The typing rule also increments idx so that the next sampling command will read out the next value.
Checking Injectivity. T-Laplace adds an assertion c a to check the injectivity of the generated alignment (a fundamental requirement of alignment-based proofs): the same aligned value of η implies the same value of η in the original execution.
Tracking Privacy Cost. A distinguished privacy cost variable v ϵ is also instrumented to track the cost for aligning the random variables in the program. Due to the properties of Laplace distribution, for a sampling command η := Lap r with alignment template A, we have P(η)/P(η +A) ≤ e | A |/r . Hence, the privacy cost for aligning η by A is|A| /r . Note that the symbols in gray, including A, are placeholders when the rule is applied, since function GenerateTemplate takes all assertions in the transformed code as inputs. Once translation is complete, the placeholders are filled in by the algorithm that we discuss in Section 4.
Alignment Template Generation. For each sampling command η := Lap r , an alignment of η is needed in a randomness alignment proof. In its most flexible form, the alignment can be written as any numerical expression n, which is prohibitive for our goal of automatic proof generation. On the other hand, using simple heuristics such as only considering constant alignment does not work: for example, the correct alignment for η 2 in GapSVT is written as "(q[i] + η 2 ≥ T η ) ? (1 − q[i]) : 0", where the alignment actually depends on which branch is taken during the execution.
To tackle the challenges, CheckDP generates an alignment template for each sampling instruction; a template is a numerical expression with "holes" whose values are to be searched for in later stages. For example, the template generated for η 2 in GapSVT is where θ [0] − θ [5] are symbolic coefficients to be found later.
In general, for each sampling command η = Lap r , CheckDP first uses static program analysis to find a set of relevant program expressions, denoted by E, and a set of relevant program variables, denoted by V (as described shortly). Second, it generates an alignment template as follows: where θ denotes coefficients ("holes") to be filled out out by later stages and each of them is generated fresh. To find proper E and V, our insight is that the alignments serve to "cancel out" the differences between two related runs (i.e., to make all assertions pass). Algorithm 1 follows the insight to compute E and V for each sampling instruction: it takes Γ s , the typing environment right before the sampling instruction and A, all assertions in the transformed code, as inputs. It also assumes an oracle Depends(e, x) which returns true whenever the expression e depends on the variable x. We note that the oracle can be implemented as standard program dependency analysis [2,31] or information flow analysis [12]; hence, we omit the details in this paper. The algorithm first checks (at line 4) if aligning η has a chance to make an assertion pass. If so, it will increment E and V as follows. For E, we notice that only for the assertions generated by rule (T-If), depending on the branch condition allows the alignment to have different values under different branches. Hence, we add the branch condition to E in this case. For V, our goal is to use the alignment to "cancel" the differences caused by other variables and array elements such as q[i] used in e. Hence, we only need to consider v if (1) v is different between two related runs (i.e., Γ s ̸ ⊢ v : B 0 ) and (2) v contributes the assertion (i.e., e depends on v).
Finally, the algorithm performs a "scope check": if any element in E or V contains out-of-scope variables, then the element is excluded; for example, η 1 should not depend on q[i] in GapSVT since q[i], essentially an iterator of q, is not in scope at that point.
Consider η 1 and η 2 in GapSVT. The assertions in the translated programs are (we only list the assertion in the true branch since the constraint in false branch is symmetric) : For η 1 , we have Γ s = {q : * } (we omit the base types and the variables that have 0 distance for brevity) and both assertions depend on η 1 . Since both assertions depend on η 1 and q[i], Algorithm 1 adds q[i] into V. Moreover, assertion (1) is generated by rule (T-If). Thus,the algorithm adds q[i] + η 2 ≥ T η into E. Finally, since q[i] is out of scope at the sampling instruction, expression using q[i] and variable q[i] are excluded, resulting V ={ } and E ={ }.

Function Signature Rewrite
Finally, CheckDP rewrites the function signature to reflect the extra parameters and holes introduced in the transformed code. In general, M(inp) is transformed to a new function signature M ′ (inp, inp, sample, θ ) where inp are the distance variables associated with inputs whose distance is not zero (e.g., q is associated with q in GapSVT), sample is a list of random values used in M, and θ are the missing holes in alignment templates.

Shadow Execution
To tackle challenging mechanisms such as Report Noisy Max [25], CheckDP uses shadow execution [50]. Intuitively, the shadow execution tracks another program execution where the injected noises are always the same as those in the original execution. Therefore, values computed in the shadow execution incur no privacy cost. The aligned execution can then switch to shadow execution when certain conditions are met, allowing extra permissiveness [50].
Supporting shadow execution only requires a few modifications: (1) Expressions will have a pair of distances (⟨d • , d † ⟩), where the extra distance d † tracks the distance in the shadow execution; (2) Since the branches and loop conditions in shadow execution are not aligned, they might diverge from the original execution. Hence, a separate shadow branch/loop is generated to correctly update the shadow distances for the variables. Since the extended transformation rules largely follow the corresponding typing rules of ShadowDP, we present the complete set of rules with detailed explanations in the Appendix.

Soundness
CheckDP enforces a fundamental property: suppose M(inp) is transformed to M ′ (inp, inp, sample, θ ), then M(inp) is differentially private if there is a list of values of θ , such that all assertions in M ′ hold for all inp, inp, sample. Recall that an alignment template A is a function of θ . Hence, we have a concrete alignment A(θ ) (i.e., a proof) when such values of θ exist.
We build the soundness of CheckDP based on that of Shad-owDP [50]. The main difference is that ShadowDP requires every sampling command η := Lap r to be manually annotated. Thus, we can easily rewrite a program M in CheckDP to a programM in ShadowDP by adding the following annotations: where A η is the alignment template for η. We formalize the main soundness results next; the full proof can be found in the Appendix.
Theorem 2 (Soundness). Let M be a mechanism written in CheckDP. With a list of concrete values of θ , letM be the corresponding mechanism in ShadowDP by rule (CheckDP to ShadowDP). If (1) M type checks, i.e., ⊢ Γ {M ⇀ M ′ } Γ ′ and (2) the assertions in M ′ hold for all inputs. ThenM type checks in ShadowDP, and the assertions inM ′ (transformed fromM by ShadowDP) pass.
Theorem 3 (Privacy). With exactly the same notation and assumption as Theorem 2, M satisfies ϵ-differential privacy.

PROOF AND COUNTEREXAMPLE GENERATION
Recall that the transformed source code has the form of the following: M ′ (inp, inp, sample, θ ). For brevity, Let I denote a triple of (inp, inp, sample), and C denote a counterexample in the form of C = (inp, inp ′ , o) as defined in Section 2.3. Proof/counterexample generation is divided into two tasks: • Proof Generation: find an instantiation of θ such that assertions in M ′ never fail for any input I , or • Counterexample Generation: find an instantiation of I , such that no θ exists to make all assertions in M ′ pass, and then construct a counterexample C based on I .
The key challenge here is the infinite search space of both θ and I . Our insight is to use a verify-invalidate loop, as depicted in Figure 4, to improve θ and I after each iteration. At a high-level, the iterative process involves two sub-loops: the (green) verify sub-loop generates proofs, and the (blue) invalidate sub-loop generates counterexamples. Moreover, the two sub-loops are integrated: starting from a default θ 0 where θ 0 [i] = 0. ∀i, the procedure generates sequences of proofs and invalidating inputs in the form of θ 0 , I 0 , θ 1 , I 1 , · · · . The final θ k or I k is used to construct proof or counterexamples correspondingly.

Verify Sub-Loop
The verify sub-loop that involves Invalidating Input Generation and Proof Generation components is responsible of generating a sequence of improving alignments θ 0 , θ 1 , · · · , θ i such that, if the mechanism is correct, θ i is a privacy proof (i.e, ∀I . M ′ (I, θ i )).
Invalidating Input Generation. This component takes a proof candidate θ i and then tries to find an input I i such that ¬M ′ (I i , θ i ) (meaning that at least one assertion in M ′ fails).
Intuitively, θ i is the currently "best" proof candidate (initially, a default null proof θ 0 = [0, · · · ] is used to bootstrap the process) that is able to validate all previously found inputs (I 0 , · · · , I i−1 ). An input I i , if any, shows that θ i is in fact not a valid proof (recall that a proof needs to ensure M ′ (I, θ i ) ∀I ). Hence, we call such I i an invaliding input of θ i and feed it with all previously identified invalidating inputs to the Proof Generation component following the "Verify Sub-loop" edge.
Take GapSVT (Figure 1) for example. Since the initial null proof θ 0 = [0, · · · ] does not align any random variable, any input, say I 0 , that diverges on the branch q[i] + η 2 ≥ T will trigger an assertion  Proof Generation. This component takes in a series of invalidating inputs I 0 , · · · , I i seen so far, and tries to find an proof candidate θ i such that: M ′ (I 0 , θ i ) ∧ · · · ∧ M ′ (I i , θ i ). Intuitively, the goal is to find a proof candidate θ i that successfully "covers" all invalidating inputs seen so far. Most likely, an improved proof candidate θ i that is able to align randomness for more inputs is generated by the component. Then θ i is fed back to the Invalidating Input Generation component, closing the loop.
Consider the GapSVT example again. In order to align randomness for the invalidating input I 0 , one possible θ 1 is to align the random variable η 2 by − q[i] to cancel out the difference introduced by q[i]. Note that this tentative proof θ 1 does not work for all possible inputs: it only serves as the "best" proof given I 0 . With the Verify Sub-loop, such imperfect proof candidates enable the generation of more invalidating inputs, such as an invalidating input I 1 where the query answers are mostly below the threshold T (I 1 invalidates θ 1 since a privacy cost incurs whenever any branch is taken, which eventually exhausts the given privacy budget). Therefore, a more general proof that leverages the conditional expression q[i] + η 2 ≥ T ? • : • in the alignment template can be discovered by Proof Generation. For GapSVT, the Verify sub-loop eventually terminates with a correct proof (Section 5).
Exit Edges. The verify loop has two exit edges. First, when no invalidating input is generated, θ i is likely a valid proof. Hence, θ i is passed to a verifier with the following condition: ∀I . M ′ (I , θ i ). Due to the soundness result (Theorem 3), we have a proof of differential privacy when the verifier passes (the "Exit" edge from Verifier component). Otherwise, CheckDP uses the counterexample returned by the verifier to construct I i (the "Verify Sub-loop" edge). We note that the verification step is required since KLEE, the symbolic executor that we use to find invalidating inputs, is unsound (i.e., it might miss an invalidating input) in theory; however, we did not experience any such unsound case of KLEE in our experience.
Second, the Proof Generation component might fail to find an alignment for I 0 , · · · , I i , a case that will eventually occur for incorrect mechanisms. This exit edge leads to the invalidate sub-loop that we discuss next.

Invalidate Sub-Loop
The invalidate sub-loop involves Counterexample Generation and Restart; it is responsible of generating one single invalidating input I such that, if the mechanism is incorrect, I cannot be aligned (i.e, θ . M ′ (I, θ )). At first glance, it could be attempting to directly use I i from the Verify Sub-Loop. However, this is problematic both in theory and in practice: no alignment for I 0 , · · · , I i does not imply no alignment of I i alone. In practice, we found such a naive approach fails for BadSmartSum and BadGapSVT in Section 5.
Counterexample Generation. This component takes an invalidating input I i and then tries to find an alignment θ i such that M ′ (I i , θ i ) (meaning that I i is not a counterexample since it can be aligned by θ i ). For example, consider a corner case in Figure 5a, where Proof Generation fails to find a common proof of both I 0 and I 1 , but each of I 0 and I 1 has a proof (illustrated by the two solid circles around them). Mostly likely, this occurs when the program being analyzed is incorrect (hence, no common proof) but neither I 1 nor I 2 is a good candidate for counterexample of differential privacy, since each of them can be aligned in isolation.
Restart. This component is symmetric to the Invalidating Input Generation component in the verify sub-loop: it takes all previously found proof candidates θ 1 , · · · , θ i and tries to find an invalidating input I i+1 such that: If found, I i+1 will intuitively be out of scope of all found proofs and serve as a "better" invalidating input. In theory, we can close the invalidate sub-loop by feeding I i+1 back to Counterexample Generation. However, doing so will make proof and counterexample generation isolated tasks. Instead, we take an integrated approach, which we discuss shortly, where the verify and invalidate sub-loops communicate to generate proofs and counterexamples in a more efficient and simultaneous way.
Exit Edges. If no θ is found to prove I i = (inp, inp, sample), a counterexample C = (inp, inp + inp, M ′ (inp, inp, sample, θ 0 )) can be formed and sent to an external exact probabilistic solver PSI [33] for validation. In theory, the Restart component might fail to find a new invalidating input given θ 1 , · · · , θ i . However, this "unknown" state never showed up in our experience.

Integrating Verify and Invalidate Sub-Loops
We integrate the verify and invalidate sub-loops as follows: following the "Invalidate Sub-loop" edge of the Proof Generation component, the latest invalidating input I i (i.e., the "best" invalidating input so far) is passed to the Counterexample Generation component to start the invalidate sub-loop. Moreover, the newly generated invalidating input I i from the Restart component is fed back to the Proof Generation component to start the verify sub-loop.
We note that by the design of the verify-invalidate loop, it alternatively runs Invalidating Input Generation and Proof Generation components. By doing so, the proof keeps improving while the invalidating inputs are getting closer to a true counterexample (since the most recent one violates a "better" proof). More intuitively, consider an invalidating input I 0 as a point in the entire input space, illustrated in Figure 5b. A proof candidate θ 1 is able to prove the algorithm for a subset of inputs including I 0 (indicated by the circle around I 0 ). The Invalidating Input Generation component then tries to find another invalidating I 1 that violates θ 1 (falls outside of the θ 1 circle). Next, the Proof Generation component finds better proof candidate θ 2 which proves ("covers") both I 0 and I 1 .
We also note that it is crucial to consider all invalidating inputs so far rather than the last input I i in the Proof Generation component: the efficiency of our approach crucially relies on "improving" the proofs quantified by validating more invalidating inputs. Without the improving proofs, the iterative procedure might fail to terminate in case shown in Figure 5a: the procedure might repeat I 0 , θ 1 , I 1 , θ 2 , I 0 , θ 1 , · · · . This is confirmed in our empirical study.
Unknown State. Due to the soundness result (Theorem 3), the program being analyzed is verified whenever CheckDP returns with a proof. Moreover, a validated counterexample by PSI disproves an incorrect mechanism. However, two reasons might lead to the "unknown" state in the Figure 4: the generated counterexample is invalid or the Restart component fails to find a new invalidating input. However, for all the correct and incorrect examples we explored, the unknown state never showed up.

IMPLEMENTATION AND EVALUATION
We implemented CheckDP in Python 3 . The Program Transformation phase is implemented as a trans-compiler from CheckDP code ( Figure 2) to C code. Following the transformation rules in Figure 3, the trans-compiler tracks the typing environment, gathers the needed constraints for the expressions, and more importantly, instruments corresponding statements when appropriate. Moreover, it adds a final assertion assert(v ϵ ≤ ϵ b ) before each return command, where ϵ b is the annotated privacy bound to be checked. Once all assertions are generated, the trans-compiler generates one alignment template for each sampling instruction as described in Algorithm 1. For the Proof and Counterexample Generation phase (i.e., verify-invalidate loop in Section 4), we used an efficient symbolic executor KLEE [18] for most tasks. Due to limited support of unbounded lists in KLEE, we fix the length of lists to be 5 in our evaluation. Also, to speed up the search, KLEE is configured to exit once an assertion is hit. We note that the use of KLEE is to discover alignments and counterexamples, where alignments are eventually verified by our sound Verifier component with arbitrary array length; counterexamples are confirmed by PSI. Moreover, CheckDP automatically extends the array length until either a verified proof or verified counterexample is produced.
Finally, we deploy a verification tool CPAChecker [13] for the Verifier component in CheckDP, which is capable of automatically verifying C programs with given configuration (predicateAnalysis is used). Note that CPAChecker is able to generate counterexamples for a failed verification. If the verification fails (which did not happen in our evaluation), CheckDP can feed the counterexample back to the Proof and Counterexample Generation component.

Case Studies
Aside from GapSVT, we also evaluate CheckDP on the standard benchmark used in previous mechanism verifiers [3,50,51] and counterexample generators [14,23], 4 including correct ones such as NumSVT, PartialSum, and SmartSum, as well as the incorrect variants of SVT reported in [40] and BadPartialSum. To show the power    of CheckDP and expressiveness of our template generation algorithm, we also evaluate on a couple of correct/incorrect mechanisms that, to the best of our knowledge, have not been proved/disproved by existing verifiers and counterexample generators. This set of mechanisms include: Sparse Vector with monotonic queries [40], AdaptiveSVT (called Adaptive Sparse Vector with Gap in [24]) as well as new incorrect variants of SVT, AdaptiveSVT and SmartSum. For all mechanisms we explore, CheckDP is able to: (1) provide a proof if it satisfies differential privacy, or (2) provide a counterexample if it violates the claimed level of privacy. Neither false positives nor false negatives were observed. In this section, we discuss the new cases; detailed explanations can be found in the Appendix.
Sparse Vector with Monotonic Queries. The queries in some usages of SVT are monotonic. In such cases, a Lap 2N /ϵ noise (instead of Lap 4N /ϵ in SVT) is sufficient for ϵ-privacy [40].
AdaptiveSVT, BadAdaptiveSVT and BadSmartSum. Ding et al. [24] recently proposed a new variant of SVT which adaptively allocates privacy budget, saving privacy cost when noisy query answers are much larger than the noisy threshold. The difference from standard (correct) SVT is that it first draws a η 2 := Lap 8N /ϵ noise (instead of Lap 4N /ϵ in SVT) and checks if the gap between noisy query and noisy threshold T η is larger than a preset hyper-parameter σ (if q[i] + η 2 -T η ≥ σ ). If the test succeeds, the gap is directly returned, hence costing only ϵ/(8N ) (instead of ϵ/(4N )) privacy budget. Otherwise, it draws η 3 := Lap 4N /ϵ and follows the same procedure as SVT. We also create an incorrect variant called BadAdaptiveSVT. It directly releases the noisy query answer instead of the gap after the first test. Sampling-based methods can have difficulty detecting the privacy leakage because the privacy-violating branch of the BadAdaptiveSVT code is not executed frequently. We also create an incorrect variant of SmartSum by releasing a noise-less sum of queries in an infrequent branch. Details of SmartSum and this variant can be found in the Appendix.
SVT with Wrong Privacy Claims (Imprecise SVT). We also study another interesting yet quite challenging violation of differential privacy: suppose a mechanism satisfies 1.1-differential privacy but claims to be 1-differentially private. This slight violation requires precise reasoning about the privacy cost and poses challenges for prior sampling-based approaches. We thus evaluate a variant of SVT, referred to as Imprecise SVT, which is ϵ = 1.1-differentially private but with an incorrect claim of ϵ = 1 (check(1) in the signature).

Experiments
We evaluate CheckDP on a Intel ® Xeon ® E5-2620 v4 CPU machine with 64 GB memory. To compare CheckDP with the state-of-the-art tools, we either directly run tools on the benchmark when they are publicly available (including ShadowDP [50], StatDP [23] and DP-Finder [14]), or cite the reported results from the corresponding papers (including Coupling [3] and DiPC [4]). 5 For the latter case, we note that the numbers are for reference only, due to different settings, including hardware, used in the experiments.
Counterexample Generation. Table 1 lists the counterexamples (i.e., a pair of related inputs and a feasible output that witness the violation of claimed level of privacy) automatically generated by CheckDP for the incorrect algorithms. For all incorrect algorithms, CheckDP is able to provide a counterexample (validated by PSI [33]) in 15 seconds and 8 iterations. 6 Notably, both StatDP and DP-Finder fail to find the privacy violations in BadSmartSum and BadAdaptiveSVT, as well as the violation of ϵ = 1-privacy in Imprecise SVT after hours of searching. 7 This is due to the limitations of sampling-based approaches. In certain cases, we can help these sampling-based algorithms by manually providing proper values for the extra arguments that some of the mechanisms require (4 t h column of Table 1). This extra advantage (labeled Semi-Manual in the table) sometimes allows the samplingbased methods to find counterexamples. We note that CheckDP, in contrast, generates all inputs automatically.
Verification. Table 2 lists the automatically generated proofs (i.e., alignments) for each random variable in the correct algorithms. Due to the soundness of CheckDP, all returned proofs are valid. We note that correct algorithms on average take more iterations (and hence, time) to verify; still all of them are verified within 70 seconds. . Report Noisy Max is the only example that uses shadow execution; the selector generated is S = q[i] +η 2 ≥ bq ∨i = 0 ? † : •, the same as the manually generated one in [50].
Performance. We note that all examples finish within 10 iterations. We contribute the efficiency to the reduced search space of Algorithm 1 (e.g., the alignment template for GapSVT only contains 7 "holes") as well as our novel verify-invalidate loop that allows verification and counterexample generation components to communicate in meaningful ways. Compared with StatDP and DP-Finder, CheckDP is more efficient on the cases where they do find counterexamples. Compared with static tools [3,4], we note that CheckDP is much faster on BadSVT3, SmartSum and SVT. In summary, CheckDP is mostly more efficient compared to counterexample detectors and automated provers.

RELATED WORK
Proving and Disproving Differential Privacy. Concurrent works [4,30] also target both proving and disproving differential privacy. Barthe et al. [4] identify a non-trivial class of programs where checking differential privacy is decidable. Their work also supports approximate differential privacy. However, the decidable programs only allow finite inputs and outputs, while CheckDP is applicable to a larger class of programs. Moreover, CheckDP is more scalable, as observed in our evaluation. Farina [30] builds a relational symbolic execution framework, which when combined with probabilistic couplings, is able to prove differential privacy or generate failing traces for SVT and its two incorrect variants. However, it is unclear if the employed heuristic strategies work on other mechanisms, such as Report Noisy Max. Moreover, CheckDP is likely to be more scalable since their approach treats both program inputs and proofs in a symbolic way, whereas in the novel verify-invalidate loop of CheckDP, either program inputs or proofs are concrete.
Formal Verification of Differential Privacy. From the verification perspective, CheckDP is mostly related to LightDP [51] and Shad-owDP [50] -all use randomness alignment. The type system of CheckDP is directly inspired by that of [50,51]. However, the most important difference is that CheckDP is the first that automatically generates alignment-based proofs; both LightDP and Shad-owDP assume manually-provided proofs. As discussed in Section 3, CheckDP also simplifies the previous type systems and defers all 7 For StatDP, we use 1000X of the default number of samples to confirm the failure. privacy-related checks to later stages. Both changes are important for automatically generating proofs and counterexamples.
Besides alignment-based proofs, probabilistic couplings and liftings [3,7,9] have also been used in language-based verification of differential privacy. Most notably, Albarghouthi and Hsu [3] proposed the first automated tool capable of generating coupling proofs for complex mechanisms. Coupling proofs are known to be more general than alignment-based proofs, while alignment-based proofs are more light-weight. Since CheckDP and [3] are built on different proof techniques, the proof generation algorithm in [3] is not directly applicable in our context. Moreover, [3] does not generate counterexamples and we do not see an obvious way to extend the Synthesize-Verify loop of [3] to do so .
With verified privacy mechanisms, such as SVT and Report Noisy Max, we still need to verify that the larger program built on top of them is differentially private. An early line of work [8,10,11,32,44] uses (variations of) relational Hoare logic and linear indexed types to derive differential privacy guarantees. For example, Fuzz [44] and its successor DFuzz [32] combine linear indexed types and lightweight dependent types to allow rich sensitivity analysis and then use the composition theorem to prove overall system privacy. We note that CheckDP and those systems are largely orthogonal: those systems rely on trusted mechanisms (e.g., SVT and Report Noisy Max) without verifying them, while CheckDP is likely less scalable; they can be combined for sophisticated verification tasks.
Counterexample Generation. Ding et al. [23] and Bichsel et al. [14] proposed counterexample generators that rely on samplingrunning an algorithm hundreds of thousands of times to estimate the output distribution of mechanisms (this information is then used to find counterexamples). The strength of these methods is that they do not rely on external solvers, and more importantly, they are not tied to (the limitation of) any particular proof technique (e.g., randomness alignment and coupling). However, sampling also make the counterexample detectors imprecise and more likely to fail in some cases, as confirmed in the evaluation.

CONCLUSIONS AND FUTURE WORK
We proposed CheckDP, an integrated tool based on static analysis for automatically proving or disproving that a mechanism satisfies differential privacy. Evaluation shows that CheckDP is able to provide proofs for a number of algorithms, as well as counterexamples for their incorrect variants within 2 to 70 seconds. Moreover, all generated proofs and counterexamples are validated.
For future work, CheckDP relies on the underlying randomness alignment technique; hence it is subject to its limitations, including lack of support for (ϵ, δ )-differential privacy and renyi differential privacy [43]. We plan to extend the underlying proof technique for other variants of differential privacy.
Moreover, subtle mechanisms such as PrivTree [52] and private selection [39], where the costs of intermediate results are dependent on the data but the cost of sum is data-independent, is still out of reach for formal verification (including CheckDP).
Finally, CheckDP is designed for DP mechanisms, rather than larger programs built on top of them. An interesting area of future work is integrating CheckDP with tools like DFuzz [32], which are 12 more efficient on programs built on top of DP mechanisms (but don't verify the mechanisms themselves).

A CHECKDP SEMANTICS
Let A be a discrete set. The set of sub-distributions over A, written Dist(A), to be the set of functions µ : A → [0, 1] such that a ∈A µ(a) ≤ 1. The reason to use sub-distributions instead of distributions (those µ such that a ∈A µ(a) = 1) is that sub-distributions give rise to an elegant semantics for programs that do not necessarily terminate [37]. We use 1 a to represent the degenerate distribution µ that µ(a) = 1 and µ(a ′ ) = 0 if a ′ a. Moreover, we define monadic functions unit and bind functions to formalize the semantics for commands: That is, unit takes an element in A and returns the Dirac distribution where all mass is assigned to a; bind takes µ, a distribution on A, and f , a mapping from A to distributions on B (e.g., a conditional distribution of B given A), and returns the corresponding marginal distribution on B. This monadic view avoids cluttered definitions and proofs when probabilistic programs are involved.

B SHADOW EXECUTION
We show how to extend the program transformation in Figure 3 to support shadow execution. At a high level, the extension encodes the selectors (which requires manual annotations in Shad-owDP [50]) and integrates them with the generated templates. With the extra "holes" in the templates, the verify-invalidate loop will automatically find alignments (including selectors)/counterexamples. The complete set of transformation rules with shadow execution is shown in Figure 7, where the extensions are highlighted in gray.
Syntax and Expressions. Since a new shadow execution is tracked, types for each variable would be expanded to include a pair of distances ⟨d • , d † ⟩. More specifically, the types should now be defined as: τ ::= num ⟨d • ,d † ⟩ | bool | list τ .
With the modified types, corresponding modifications to the transformation rules for expressions are straightforward and minimal: the handling of shadow distances are essentially the same as that of aligned distances.
Normal Commands. Following the type system of ShadowDP, a program counter pc ∈ {⊤, ⊥} is introduced to each transformation rule for commands to capture potential divergence of shadow execution. Specifically, pc ⊢ c ⇀ c ′ . pc = ⊤ (resp. ⊥) means that the branch / loop command might diverge in the shadow execution (resp. must stay the same). The value of pc is used to guide how each rule should handle the shadow distances (e.g., (T-Asgn)), which we will explain shortly. Therefore, another auxiliary function updatePC is added to track the value of pc.
Compared with the type system of ShadowDP, the first major difference is in (T-Asgn). If pc = ⊥, shadow distances are handled as the aligned distances. However, when pc = ⊤ (shadow execution diverges), it updates the shadow distance of the variable to make sure the value in shadow execution (i.e., x + x † ) remains the same after the assignment. For example, Line 20 in Figure 8 is instrumented to maintain the value of bq in the shadow execution (bq + bq † ), so that the branch at Line 26 is not affected by the new assignment of bq.
, else e 1 :: e 2 , Γ ⋆ = e 1 , Γ ⋆ :: As previously explained, a separate shadow branch / loop has to be generated to correctly track the shadow distances of the variables. More specifically, Rules (T-If) and (T-While) is extended to include an extra shadow execution command c † when pc transits from ⊥ to ⊤. The shadow execution is constructed by an auxiliary function c, Γ † , as defined in Figure 6, which is the same as the ones in ShadowDP [50]. It essentially replaces each variable with its correspondence (e.g., variable x to x + x † ), as is standard in selfcomposition [6,49]. Note that the value of an expression e in an aligned execution (i.e., e, Γ • used in Rules (T-If) and (T-While)) are defined in a similar way.
Sampling Commands. The most interesting rule is (T-Laplace). In order to enable the automatic discovery of the selectors, our GenerateTemplate algorithm needs to be extended to return a selector template S. Intuitively, a selector expression S with the following syntax decides if the aligned or shadow execution is picked: The definition of the selector template is then similar to the alignment template, where the value can depend on the branch conditions: S E ::= e 0 ? S E\{e 0 } : S E\{e 0 } , when E = {e 0 , · · · } θ with fresh θ , otherwise

D EXTRA CASE STUDIES
In this section we list the pseudo-code of the algorithms we evaluated in the paper for completeness. The incorrect part for the incorrect algorithms is marked with a box.

D.1 Report Noisy Max
Report Noisy Max [25]. This is an important building block for developing differentially private algorithms. It generates differentially private synthetic data by finding the identity with the maximum (noisy) score in the database. Here we present this mechanism in a simplified manner: for a series of query answers q, where each of them can differ at most one in the adjacent underlying database, its goal is to return the index of the maximum query answer in a privacy-preserving way. To achieve differential privacy, the mechanism first adds η = Lap 2/ϵ noise to each of the query answer, then returns the index of the maximum noisy query answers q[i] + η, instead of the true query answers q[i]. The pseudo code of this mechanism is shown in Figure 8.
To prove its correctness using randomness alignment technique, we need to align the only random variable η in the mechanism (Line 3). Therefore, a corresponding privacy cost of aligning η would be incurred for each iteration of the loop. However, manual proof [25] suggests that we only need to align the random variable added to the actual maximum query answer. In other words, we need an ability to "reset" the privacy cost upon seeing a new current maximum noisy query answer.
Bad Noisy Max. We also created an incorrect variant of Report Noisy Max. This variant directly returns the maximum noisy query answer, instead of the index.
More specifically, it can be obtained by changing Line 5 in Figure 8 from max := i to max := q[i] + η. CheckDP is then able to find a counterexample for this incorrect variant.

D.2 Variants of Sparse Vector Technique
SVT. We first show a correctly-implemented standard version of SVT [40]. This standard implementation is less powerful than running example GapSVT, as it outputs true instead of the gap between noisy query answer and noisy threshold. This can be obtained by changing Line 7 in Figure 1 from out := (q[i] + η 2 )::out; to out := true::out;.
SVT with Monotonic Queries. There exist use cases with SVT where the queries are monotonic. More formally, queries are monotonic if for related queries q ∼ q ′ , ∀i. q i ≤ q ′ i or ∀i. q i ≥ q ′ i . As shown in [40]. When the queries are monotonic, it suffices to add η 2 := Lap 2N /ϵ to each queries (Line 5 in Figure 1) and the algorithm still satisfies ϵ-DP.
Thanks to the flexibility of CheckDP, it only requires one change in the function specification in order to verify this variant: modify the constraint on q[i] in the precondition. Specifically, the new precondition for SVT with monotonic queries becomes ∀ i. 0 ≤ q[i] ≤ 1 for the ∀i. q i ≤ q ′ i and ∀ i. −1 ≤ q[i] ≤ 0 for the other case. The final found alignment by CheckDP is the same as the ones reported in the manual randomness alignment based proofs [24]: NumSVT. Numerical Sparse Vector (NumSVT) [28] is another interesting correct variant of SVT which outputs a numerical answer when the input query is larger than the noisy threshold. It follows the same procedure as Sparse Vector Technique, the difference is that it draws a fresh noise η 3 in the true branch, and outputs q[i] + η 3 instead of true. Note that this is very similar to our running example GapSVT and BadGapSVT, the key difference is that the freshly-drawn random noise hides the information about T η , unlike the BadGapSVT. This variant can be obtained by making the following changes in Figure 1  finds the same alignment as shown in [51] with which CPAChecker is able to verify the algorithm with this generated alignment.
Adaptive SVT. As mentioned in Section 5, we list the pseudo code of Adaptive SVT in Figure 11. BadSVT1 -3. We now study other three incorrect variants of SVT collected from [40]. All three variants are based on the classic SVT algorithm we have seen (i.e., Line 7 in Figure 1 is out := true::out;).
BadSVT1 [47] adds no noise to the query answers and has no bounds on the number of true's it can output. This variant is obtained by changing Line 4 from while (count<N∧i<size) to while (i<size) and Line 5 from Lap 4N /ϵ to 0. Another variant BadSVT2 [20] has no bounds on the number of true's it can output as well. It keeps outputting true even if the given privacy budget has been exhausted. Moreover, the noise added to the queries does not scale with parameter N. Specifically, based on BadSVT1, Line 5 is changed to Lap 2/ϵ. BadSVT3 [38] is an interesting case since it tries to spend its privacy budget in a different allocation strategy between the threshold T and the query answers q[i] (1 : 3 instead of 1 : 1). However, the noise added to η 2 does not scale with parameter N. The 3/4 privacy budget is allocated to each of the queries where it should be shared among them. To get this variant, based on SVT algorithm, the noise generation commands (Line 1 and Line 5) are changed to η 1 := Lap 4/ϵ and η 2 := Lap 4/(3 × ϵ) , respectively.


extfieldsofstudy:
Computer Science
Mathematics

text:
Newtonian Monte Carlo: single-site MCMC meets second-order gradient methods

Single-site Markov Chain Monte Carlo (MCMC) is a variant of MCMC in which a single coordinate in the state space is modified in each step. Structured relational models are a good candidate for this style of inference. In the single-site context, second order methods become feasible because the typical cubic costs associated with these methods is now restricted to the dimension of each coordinate. Our work, which we call Newtonian Monte Carlo (NMC), is a method to improve MCMC convergence by analyzing the first and second order gradients of the target density to determine a suitable proposal density at each point. Existing first order gradient-based methods suffer from the problem of determining an appropriate step size. Too small a step size and it will take a large number of steps to converge, while a very large step size will cause it to overshoot the high density region. NMC is similar to the Newton-Raphson update in optimization where the second order gradient is used to automatically scale the step size in each dimension. However, our objective is to find a parameterized proposal density rather than the maxima. As a further improvement on existing first and second order methods, we show that random variables with constrained supports don't need to be transformed before taking a gradient step. We demonstrate the efficiency of NMC on a number of different domains. For statistical models where the prior is conjugate to the likelihood, our method recovers the posterior quite trivially in one step. However, we also show results on fairly large non-conjugate models, where NMC performs better than adaptive first order methods such as NUTS or other inexact scalable inference methods such as Stochastic Variational Inference or bootstrapping.

Introduction
Markov Chain Monte Carlo (MCMC) methods are often used to generate samples from an unnormalized probability density π(θ) that is easy to evaluate but hard to directly sample. Such densities arise quite often in Bayesian inference as the posterior of a generative model p(θ, Y ) conditioned on some observations Y = y, where π(θ) = p(θ, y). The typical setup is to select a proposal distribution q(.|θ) that proposes a move of the Markov chain to a new state θ * ∼ q(.|θ). The Metropolis-Hastings acceptance rule is then used to ac-Copyright c 2019, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. cept or reject this move with probability: min 1, π(θ * )q(θ|θ * ) π(θ)q(θ * |θ) .
When θ ∈ R k , a common proposal density is the Gaussian distribution N (θ, 2 I k ) centered at θ with covariance 2 I k , where is the step size and I k is the identity matrix defined over R k,k . This proposal forms the basis of the so-called Random Walk MCMC (RWM) first proposed in Metropolis et al. (1953).
In cases where the target density π(θ) is differentiable, an improvement over the basic RWM method is to propose a new value in the direction of the gradient, as follows: This method is known as Metropolis Adjusted Langevin Algorithm (MALA), and arises from an Euler approximation of a Langevin diffusion process (Robert and Tweedie, 1996). MALA has been shown to reduce the number of steps required for convergence to O(n 1/3 ) from O(n) for RWM (Roberts and Rosenthal, 1998). An alternate approach, which also uses the gradient, is to do an L-step Euler approximation of Hamiltonian dynamics known as Hamiltonian Monte Carlo (Neal, 1993), although it was originally published under the name Hybrid Monte Carlo (Duane et al., 1987).
In HMC the number of steps, L, can be learned dynamically by the No-U-Turn Sampler (NUTS) algorithm (Hoffman and Gelman, 2014). However, in all three of the above algorithms -RWM, MALA, and HMC -there is an open problem of selecting the optimal step size. Normally, the step size is adaptively learned by targeting a desired acceptance rate. This has the unfortunate effect of picking the same step size for all the dimensions of θ, which forces the step size to accomodate the dimension with the smallest variance as pointed out in Girolami and Calderhead (2011). The same paper introduces alternate approaches, using Riemann manifold versions of MALA (MMALA) and HMC (RMHMC). They propose a Riemann manifold using the expected Fisher information matrix plus the negative Hessian of the log-prior as a metric tensor, −E y|θ ∂ 2 ∂θ 2 log{p(y, θ)} , and proceed to derive the Langevin diffusion equation and Hamiltonian dynamics in this manifold. The use of the above metric tensor does address the issue of differential scaling in each dimension. However, the method as presented requires analytic knowledge of the Fisher information matrix. This makes it difficult to design inference techniques in a generic way, and requires derivation on a per-model basis. A more practical approach involves using the negative Hessian of the log-probability as the metric tensor, − ∂ 2 ∂θ 2 log{p(y, θ)}. However, this encounters the problem that this is not necessarily positive definite throughout the state space. An alternate approach for scaling the moves in each dimension is to use a preconditioning matrix M (Roberts and Stramer, 2002) in MALA, q(.|θ) = N θ + 2 M ∇ log π(θ), 2 M , also known as the mass matrix in HMC and NUTS, but it's unclear how to compute this.
Another approach is to approximately compute the Hessian (Zhang and Sutton, 2011) using ideas from quasi-Newton optimization methods such as L-BFGS (Nocedal and Wright, 2006). This approach and its stochastic variant (Simsekli et al., 2016) use a fixed window of previous samples of size M to approximate the Hessian. However, this makes the chain an order M Markov chain, which introduces considerable complexity in designing the transition kernel in addition to introducing a new parameter M . The key observation in our work is that for single-site methods we only need to compute the Hessian of one coordinate at a time, and this is usually tractable. The other key observation is that we don't need to always make a Gaussian proposer using the Hessian. In cases when the coordinate under consideration is a constrained random variable then we can propose from any parameterized density in the same constrained space by matching its curvature. This approach of curvature-matching to an approximating density allows us to deal with constrained random variables without introducing a transformation such as in Stan (Carpenter et al., 2017).
In the rest of the paper, we will describe our approach to exploit the curvature of the target density, and show some results on multiple data sets.

Overview
This paper introduces the Newtonian Monte Carlo (NMC) technique for sampling from a target distribution via a proposal distribution that incorporates curvature around the current sample location. We wish to choose a proposal distribution that uses second order gradient information in order to closely match the target density. Whereas related MCMC techniques discussed in Section 1 may utilize second order gradient information, those techniques typically use it only to adjust the step size when simulating steps along the general direction of the target density's gradient.
Our proposed method involves matching the target density to a parameteric density that best explains the current state. We have a library of 2-parameter target densities F i , and simple inference rules such that, given the first and sec-ond order gradients, we can solve the following two equations: to determine α i and β i . For example, in the case of θ ∈ R k , we use either the multivariate Gaussian or the multivariate Cauchy. For the former, the update equation leads to the natural proposal, The update term in the mean of this multivariate Gaussian is precisely the update term of the Newton-Raphson Method (Whittaker and Robinson, 1967), which is where NMC gets its name from. However, if the negative Hessian inverse matrix is not positive definite, then the multivariate normal is not defined. In this case, we can instead use the Cauchy proposer as shown by Minka (2000). The full list of estimation methods are enumerated in Section 3. For example, for positive real values we use a Gamma proposer with parameters, and we don't need a log-transform to an unconstrained space. We rely on generic Tensor libraries such as PyTorch (Paszke et al., 2017) that make it easy to write statistical models and also automatically compute the gradients. This makes our approach easy to apply to models generically.
In the case of conjugate models, our estimation methods automatically recover the appropriate conditional posterior distribution, such as the ones used in BUGS (Spiegelhalter et al., 1996). However, even in cases of non-conjugacy, our proposal distributions pick out reasonable approximations to the conditional posterior of each variable.

Single Site Inference
An important observation related to our method is that we don't need to compute the joint Hessian of all the parameters in the latent space. Most statistical models with relational structure can be decomposed into multiple latent variables. This decomposition allows for single site MCMC methods that change the value of one variable at a time. In this case, we only need to compute the gradient and Hessian of the target density w.r.t. the variable being modified. Consider a model with N variables each drawn from R K . The full Hessian is of size (N K) 2 and has a cost of (N K) 3 to invert. On the other hand, a single site approach computes N Hessians each of size K 2 with a total cost of N K 3 to invert.

Estimation Rules
The estimation rules presented here are based on the work of Minka (2000).

Unconstrained spaces
We first consider distributions with the support R k .

Normal Distribution
The multivariate Normal distribution has the log-density: This leads to the natural estimation rule: In case the estimated Σ has a negative eigenvalue we set those negative eigenvalues to a very small positive number, and reconstruct Σ.

Cauchy Distribution
The multivariate Cauchy distribution has the log-density: , and Noting that the second term above is the outer product of the first gradient leads to the following estimation rules:

Constrained Spaces
Half-Space We use the Gamma distribution for proposing values for variables which lie on any half-space constrained distribution, i.e. R + . The Gamma distribution has the logdensity: Which leads to the estimation rules: α = 1 − x 2 ∇ 2 log π(x), β = −x∇ 2 log π(x) − ∇ log π(x), Simplexes The K-simplexes refers to the set {x ∈ We use the Dirichlet distribution to propose random variables with this support. The log-density of the Dirichlet is given by, We consider the modified density, which includes the simplex constraint, Thus, Which leads to the following estimation rule,

Models
Neal's Funnel We first consider a toy model, which is considered difficult for MCMC methods. The model was first proposed in Neal and others (2003) and has been since called Neal's Funnel. The following equations define the joint density of the model, which is deceptively simple.
z ∼ N (0, 3) x ∼ N (0, e z 2 ) The difficulty for inference arises when we try to sample values of (x, z) for increasingly negative z. Since the scale of x varies exponentially with z it is hard to learn a good scale. Indeed Figure 1 shows that Stan, which uses NUTS, has a hard time sampling from this distribution as highlighted by the posterior marginal of z. On the other hand NMC, which effectively computes the scale dynamically at each point has no difficulty in generating good samples, as shown in Figure 2.
Bayesian Logistic Regression Next we consider the Bayesian Logistic Regression model that is commonly used in machine learning. The model is defined as follows: α ∼ N (0, 10, size = 1), β ∼ N (0, 2.5, size = K), X i ∼ N (0, 10, size = K) ∀i ∈ 1..N From this model we generate samples of α, β, X i and Y i for some given N and K. Half of the X, Y samples are given to the inference method to produce posterior samples of α and β. The held out values of X, Y are used to evaluate the predictive log-likelihood, which is averaged over the posterior samples. In this and the rest of the models, we draw exactly 1 000 samples using each method. For single-site methods a sample includes an update to each coordinate. Figure 3 shows results for N = 20 000 using a variety of methods. Table 1 shows the run times to produce 1 000 samples, plus the number of samples required to achieve convergence. We have defined samples to convergence to be the number of samples it takes for the predictive log-likelihood to stabilize to within 1% of the final value for the method. Figure 4 shows results for N = 2 000 000, where we only compare two of the methods since the other methods were too slow for such a large data set.
This model has a nice log concave posterior which is quite easy for MCMC inference and hence both JAGS and NMC converge in 1 sample. Stan, which uses NUTS, does take a bit longer to converge because it has to learn the optimum scale in each of the K dimensions of β. Bootstrappingbased approaches are often used for this model, but they do appear to incur additional cost of re-training the model for each bootstrap sample. Finally, we also used Stochastic Variational Inference as implemented in Pyro (Bingham et al., 2019), but it doesn't appear from this example that the loss of accuracy of using variational inference is worthwhile. In this model, NMC seems to be the fastest both in terms of time per samples and samples to convergence. Robust Regression Robust regression is a regression model in which an error distribution with a much wider tail than Gaussian such as the Student's t distribution is used to model data with outliers. We use the following model: As before we generate samples from the model of all the variables including N values of X i and Y i . Half of the generated samples are given to the inference algorithm and the other half are used for evaluating the posterior. This model is not log-concave because of the Student's t distribution, and as a result JAGS takes much longer to converge as shown in Figure 5 and and Table 2. We also ran an experiment for much larger N , Figure 6, where we left out JAGS because it was too slow. On this model, NMC converges much faster than Stan using merely 3 samples to converge for the larger data set, and with much faster runtimes as well. Annotation Model Our final model has a lot more relational structure than the regression models above. This is a slightly modified version of the model presented in Passonneau and Carpenter (2014) and Dawid and Skene (1979), and is designed to compute the true labels of items given noisy crowd-sourced labels. There are N items, K labelers, and each item could be one of C categories. Each item i is labeled by a set J i of labelers. Such that the size of J i is sampled randomly, and each labeler in J i is drawn uniformly without replacement from the set of all labelers. z i is the true label for item i and y ij is the label provided to item  i by labeler j. Each labeler l has a confusion matrix θ l such that θ lmn is the probability that an item with true class m is labeled n by l.
Here α m ∈ R + C . We set α mn = γ · ρ if m = n and α mn = γ · (1 − ρ) · 1 C−1 if m = n. Where γ is the concentration and ρ is the a-priori correctness of the labelers. In this model, Y il and J i are observed.
In our experiments, we fixed K = 100, C = 3, J loc = 2.5, γ = 10, and ρ = 0.5. As before we generated data for different sizes of N and used a random partition of the data for inference and evaluation. Since Stan doesn't support discrete variables such as z i above, we had to analytically integrate 1 the z's out of the model. For the purpose of evaluation, since Stan doesn't give us samples of z, we integrate over these variables to compute the predictive likelihood, which gives a disadvantage to methods such as JAGS and NMC where the samples depend on a specific value of z.
In this model each random variable has a conjugate conditional posterior, and since JAGS is designed to exploit conjugacy it really shines here. Unfortunately, the version of JAGS that we used kept crashing on larger data sets. The results for N = 10 000 are shown in Figure 7 and run times are in Table 3. NMC exploits the relational structure in this model to use single-site inference on each of the random variables such as θ lm individually rather than the entire θ jointly as in Stan. As such NMC is easily able to keep up with JAGS in terms of number of samples and is only a factor of 2,5 slower on the small data set. On the larger data set, Figure 8 and 9, NMC is nearly 7 times faster than Stan.

Conclusion
We have presented a new MCMC method that uses the first and second gradients of the target density for each coordinate in the latent state space to determine an appropriate proposal distribution. The method is shown to perform better than the existing state of the art NUTS implementation without requiring an adaptive phase or tuning of inference hyper-parameters.