Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 4 results · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Simulation gradient estimation and simultaneous perturbation — Examples

1 · Prerequisites

2 · Summary

Examples

These examples compare pathwise and score gradients in a Gaussian location model, show the missing boundary term for a moving support, compute the covariance benefit of common random numbers, and work through the two simulator calls in one biological-model SPSA step. The numerical outputs in the black-box example verify the estimator arithmetic only; they are not convergence or accuracy certificates for that model.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A moving uniform support contributes a missing score boundary term

Example

For $θ > 0$ , let $X_{θ} \sim Unif (0, θ)$ and use constant payoff $H (x) = 1$ . The objective is $J (θ) = 1$ , so $J^{'} (θ) = 0$ . The pathwise representation $X_{θ} = θ U$ , $U \sim Unif (0, 1)$ , has derivative estimator $0$ . The interior score is $- 1 / θ$ , so $E [H (X_{θ}) S_{θ} (X_{θ})] = - 1 / θ$ ; it misses the moving endpoint contribution $+ 1 / θ$ .

Facts & Assumptions

Given: $θ > 0$ , the density $p_{θ} (x) = θ^{- 1} 1_{(0, θ)} (x)$ with respect to Lebesgue measure, and the constant payoff $H (x) = 1$ .

[A1]

The Axiom of Choice: every family of nonempty sets has a choice function; AC is inherited by the score definition.

[F1]

Score and Fisher information: on the positive-density set the score is $\partial_{θ} \log p_{θ} (x)$ .

[F2]

Pathwise and reparameterized simulation-gradient estimators: in a representation using a fixed random input $U$ , the pathwise estimator is the derivative with $U$ held fixed.

[F3]

Simulation objectives and unbiased payoff oracles: an objective is the expectation of its integrable simulation payoff.

[F4]

Integrating against a density agrees with integrating the product: expectation under density $p_{θ}$ is integration of the payoff times $p_{θ}$ against Lebesgue measure.

[F5]

Expectation of a nonnegative or integrable random variable: the expectation of an integrable constant random variable is that constant.

Verification

1.1givenF2F3F4algebra

The density is normalized because $\int_{0}^{θ} θ^{- 1} d x = 1$ . By [F3] and [F4], the constant payoff has $J (θ) = \int_{0}^{θ} θ^{- 1} d x = 1$ , hence $J^{'} (θ) = 0$ . In the representation $X_{θ} = θ U$ , $H (X_{θ}) = 1$ for every $U$ , so its pathwise derivative is zero by [F2].

2.1A1F1F5step 1.1algebra

On $0 < x < θ$ , $p_{θ} (x) = 1 / θ$ , so [F1] gives $S_{θ} (x) = - 1 / θ$ almost surely under $P_{θ}$ . Since $H = 1$ , the score product is the constant $- 1 / θ$ almost surely, and [F5] gives $E_{θ} [H (X_{θ}) S_{θ} (X_{θ})] = - 1 / θ$ . This differs from $J^{'} (θ) = 0$ , so the fixed-support score identity does not apply.

3.1givenstep 1.1step 2.1algebra∎

The integral is $J (θ) = θ \cdot θ^{- 1}$ . Differentiating this product gives the interior density-derivative contribution $\int_{0}^{θ} H (x) \partial_{θ} (θ^{- 1}) d x = - 1 / θ$ and the moving-endpoint contribution $H (θ) p_{θ} (θ^{-}) = 1 / θ$ , where $p_{θ} (θ^{-})$ is the left limit of the density. Their sum is zero, exactly $J^{'} (θ)$ from step 1.1; the interior score term alone omits this boundary correction.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

One two-call SPSA estimate for an expensive biological simulator

Example

Suppose a costly black-box biological simulator reports a scalar mismatch for three positive kinetic rates. At $θ = (0.20, 0.20, 0.20)$ , take $c = 0.02$ and Rademacher perturbation $Δ = (1, - 1, 1)$ . If the two simulator calls return $13.1$ and $12.7$ , the SPSA estimate is $(10, - 10, 10)$ and uses two calls, compared with six coordinatewise central-difference calls.

Facts & Assumptions

Given: The parameter, step, perturbation, two observed simulator outputs, and the SPSA procedure in the Statement.

[F1]

Two-evaluation simultaneous-perturbation gradient estimator: with two values $Y^{\pm}$ , the coordinate output is $(Y^{+} - Y^{-}) / (2 c Δ_{i})$ .

Verification

1.1givenalgebra

The perturbed parameters are $θ + c Δ = (0.22, 0.18, 0.22)$ and $θ - c Δ = (0.18, 0.22, 0.18)$ , so both remain in the positive-rate domain.

1.2givenF1algebra

The common numerator is $13.1 - 12.7 = 0.4$ and $2 c = 0.04$ . By [F1], the three outputs are $0.4 / 0.04 = 10$ , $0.4 / (- 0.04) = - 10$ , and $0.4 / 0.04 = 10$ .

2.1step 1.2givenalgebra∎

The estimate uses the two simulator values for all coordinates, whereas one central-difference pair per coordinate uses $2 d = 6$ calls at $d = 3$ . The finite calculation verifies the estimator output only; it does not certify its bias, variance, or convergence for the biological model.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Common random numbers can remove finite-difference noise

Example

Assume AC and fix $c > 0$ . Let $Z \sim N (0, 1)$ and let one simulation output be $Y (θ, Z) = θ + Z$ , so $J (θ) = θ$ . Using the same $Z$ at $θ + c$ and $θ - c$ gives a central-difference estimate identically equal to $1$ . Using independent $Z_{+}$ and $Z_{-}$ gives variance $1 / (2 c^{2})$ .

Facts & Assumptions

Given: AC, a radius $c > 0$ , a standard normal noise variable and the simulator $Y (θ, Z) = θ + Z$ .

[F1]

Coupled finite-difference simulation-gradient estimator: the paired estimate is $(Y^{+} - Y^{-}) / (2 c)$ , with the joint law fixed by the coupling.

[F2]

Coupled finite differences have a covariance-controlled variance: the variance is $(Var Y^{+} + Var Y^{-} - 2 Cov (Y^{+}, Y^{-})) / (4 c^{2})$ .

[F3]

Standard normal and normal laws, The Axiom of Choice, AC implies DC implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ ) and A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions: AC implies Countable Choice, and reflection $z \mapsto - z$ preserves Lebesgue measure; since the density $ϕ (z)$ is even, the standard normal law is symmetric.

[F4]

Expectations factor over finite products of independent random variables: independent integrable random variables have factorized product expectation.

[F5]

Gaussian even moments for Brownian increments gives $E Z^{2} = 1$ ; Change of variables for expectation and symmetry in [F3] then give $E Z = 0$ . Linearity, monotonicity, and the modulus bound for expectation gives linearity of expectation.

[F6]

Moments, variance, and covariance on a probability space and Variance and covariance identities for random variables: $Var (Z) = E [Z^{2}] - (E Z)^{2}$ .

Verification

1.1givenF1F3F5F6algebra

By [F5], $2 ∣ Z ∣ \leq 1 + Z^{2}$ gives integrability, and symmetry in [F3] implies $E Z = E [- Z] = - E Z$ , hence $E Z = 0$ . Therefore [F5] gives $J (θ) = E [θ + Z] = θ$ , as stated; [F5] and [F6] also give $Var (Z) = 1$ . With a shared $Z$ , $Y (θ + c, Z) - Y (θ - c, Z) = 2 c$ for every outcome. Thus the coupled estimate is exactly $1$ and has variance zero.

1.2F3F4F5F6algebra

With independent $Z_{+}, Z_{-}$ , the estimate is $1 + (Z_{+} - Z_{-}) / (2 c)$ . Each noise has the same mean zero and variance one just proved; by [F4] their product expectation factors, so their covariance is zero.

2.1F2step 1.1step 1.2algebra∎

Applying [F2] gives variance $(1 + 1) / (4 c^{2}) = 1 / (2 c^{2})$ . The variance contrast is caused by the coupling covariance; common random numbers do not guarantee this benefit for every payoff.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Gaussian reparameterization gives two gradient estimators

Example

Let $Z \sim N (0, 1)$ , set $X_{θ} = θ + Z$ , and use payoff $H (x) = x$ . The objective is $J (θ) = E X_{θ} = θ$ . The pathwise estimator is constant $1$ ; the score estimator is $X_{θ} (X_{θ} - θ)$ , which is unbiased and has variance $θ^{2} + 2$ .

Facts & Assumptions

Given: A standard normal $Z$ , the affine representation $X_{θ} = θ + Z$ , and the identity payoff $H (x) = x$ .

[A1]

The Axiom of Choice: every family of nonempty sets has a choice function; AC is inherited by the normal-law and score interfaces below.

[F1]

Standard normal and normal laws: $Z$ has symmetric density $ϕ (z) = (2 π)^{- 1 / 2} e^{- z^{2} / 2}$ , and $X_{θ}$ is the location-shifted normal law $N (θ, 1)$ . A positive-variance normal law has its location-scale density gives its density $p_{θ} (x) = ϕ (x - θ)$ on $R$ .

[F2]

Gaussian even moments for Brownian increments: $E Z^{2} = 1$ and $E Z^{4} = 3$ .

[F3]

Pathwise and reparameterized simulation-gradient estimators: with the same $Z$ held fixed, the pathwise estimator is $\partial_{θ} H (X_{θ})$ .

[F4]

A dominated pathwise simulation gradient is unbiased: an integrably dominated continuous pathwise derivative is the derivative of the expected payoff and has finite variance under its second-moment hypothesis.

[F5]

Score and Fisher information: on positive density support the score is $\partial_{θ} \log p_{θ}$ .

[F6]

The likelihood-ratio score gradient is unbiased on fixed support: under fixed support, dominated density differentiation, and a finite weighted second moment, $\partial_{θ} E_{θ} H = E_{θ} [H S_{θ}]$ .

[F7]

A positive-variance normal law has its location-scale density: $N (0, 2)$ has density $(4 π)^{- 1 / 2} e^{- z^{2} / 4}$ .

[F8]

Integrating against a density agrees with integrating the product: the integral of a nonnegative measurable function under a law with density $p_{θ}$ is its integral after multiplication by $p_{θ}$ against Lebesgue measure.

[F9]

Change of variables for expectation: if $Z_{2} = \sqrt{2} Z$ with $Z \sim N (0, 1)$ , then $E Z_{2}^{2} = 2 E Z^{2}$ .

[F10]

Moments, variance, and covariance on a probability space and Variance and covariance identities for random variables: variance is the centered second moment and equals the second moment minus squared mean.

[F11]

The Axiom of Choice, AC implies DC implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ ) and A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions: AC implies Countable Choice, and applying change of variables to reflection $z \mapsto - z$ with the even density in [F1] shows that the standard normal law is symmetric.

[F12]

Change of variables for expectation and Linearity, monotonicity, and the modulus bound for expectation: integrable functions of a random variable may be integrated against its law, and expectation is linear.

Verification

1.1givenF1F2F3F4F11F12algebra

From [F2], $2 ∣ Z ∣ \leq 1 + Z^{2}$ makes $Z$ integrable. By [F11], the law is symmetric; [F12] therefore gives $E Z = E [- Z] = - E Z$ , so $E Z = 0$ . Linearity in [F12] gives $E X_{θ} = θ$ . The pathwise payoff derivative is $1$ by [F3], has envelope $M = 1$ and second moment $1$ , so [F4] gives the correct derivative $J^{'} (θ) = 1$ and variance zero.

1.2A1F1F5algebra

Differentiating $\log p_{θ} (x) = - \frac{1}{2} (x - θ)^{2} - \frac{1}{2} \log (2 π)$ gives $S_{θ} (x) = x - θ$ . The support is the fixed set $R$ .

1.3A1F1F2F6F7F8F9F11F12algebra

Fix $θ_{0}$ and restrict $η$ to $∣ η - θ_{0} ∣ < 1$ . With $z = x - θ_{0}$ and $a = η - θ_{0}$ , $(z - a)^{2} \geq z^{2} / 2 - a^{2}$ , while $∣ x ∣ ∣ x - η ∣ \leq (∣ z ∣ + ∣ θ_{0} ∣) (∣ z ∣ + 1)$ . Hence $∣ x \partial_{η} p_{η} (x) ∣ \leq C_{θ_{0}} (1 + z^{2}) e^{- z^{2} / 4}$ for a finite constant $C_{θ_{0}}$ . By [F7]–[F9], the integral of this majorant is a constant times $E [1 + Z_{2}^{2}] < \infty$ for $Z_{2} \sim N (0, 2)$ . Also $2 ∣ Z ∣^{3} \leq Z^{2} + Z^{4}$ makes $Z^{3}$ integrable by [F2]; symmetry in [F11] and [F12] gives $E Z^{3} = 0$ . Therefore $E_{θ} [X_{θ}^{2} S_{θ} (X_{θ})^{2}] = E [(θ Z + Z^{2})^{2}] = θ^{2} + 3 < \infty$ by [F2], so [F6] applies.

2.1A1F2F6F10step 1.1step 1.3algebra∎

By [F6], the score estimator has mean $J^{'} (θ) = 1$ . Its variance is $E [(θ Z + Z^{2})^{2}] - 1 = θ^{2} + 3 - 1 = θ^{2} + 2$ , using [F2] and [F10].