DARE pruning model — masks, rescaling, and coefficient statistics

Definition

DAREx_Model

by Minghui · Sep 29, 2026 · Mathlib c5ea003 (Lean v4.30.0)

delta-parameter-pruningmachine-learningprobability

Fix a natural number $n$ and deterministic real coefficients $c_j$ , indexed by $j\in\{1,\ldots,n\}$ . A Boolean mask $\omega$ records dropped coordinates. For $0\le p\le1$ , it has mass $w_p(\omega)=\prod_j[p\text{ if }\omega_j=1;\;1-p\text{ otherwise}]$ , so the drops are independent Bernoulli variables of parameter $p$ . The bundle defines expectation and event probability as the finite weighted sums and proves nonnegative masses and total mass one.

Write $S=\sum_jc_j$ , $Q=\sum_jc_j^2$ , $\bar c=S/n$ , and $\sigma^2=n^{-1}\sum_j(c_j-\bar c)^2$ . The statistical identities using these last two quantities require $n>0$ . For a positive rescaling denominator $q$ , set $H_q(\omega)=\sum_jc_j(1-(1-\omega_j)/q)$ and $b_q=(1-(1-p)/q)S$ . DARE uses $H=H_{1-p}$ for $0<p<1$ . Define $\Phi(1/2)=1/2$ and $\Phi(p)=(1-2p)/\log((1-p)/p)$ otherwise; concentration theorems restrict $p$ to $(0,1)$ .

Formalization note. Finite-sum encoding of the paper's Bernoulli probability model: true means dropped, the complement of its retention variable. Definitions are total Lean functions; no probability or analytic claim is made outside the stated domains. The model is not an assumption of any concentration conclusion. Primary reference: Deng et al., Section 3.2, PDF p. 5, equation (2); Appendix E.1, PDF pp. 29–31, equations (7)–(8); Appendix E.2, PDF p. 31, initial unnumbered identity. See the linked source.

Definition code

import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real

noncomputable section

open scoped BigOperators

namespace DAREx

/-- A true bit denotes a dropped coordinate. -/
abbrev Mask (n : ℕ) := Fin n → Bool

/-- Product law of independent Bernoulli drop indicators. -/
def maskMass {n : ℕ} (p : ℝ) (ω : Mask n) : ℝ :=
  ∏ j, if ω j then p else 1 - p

def mean {n : ℕ} (p : ℝ) (f : Mask n → ℝ) : ℝ :=
  ∑ ω, maskMass p ω * f ω

def probability {n : ℕ} (p : ℝ) (event : Mask n → Prop) : ℝ := by
  classical
  exact ∑ ω, if event ω then maskMass p ω else 0

def coefficientSum {n : ℕ} (c : Fin n → ℝ) : ℝ := ∑ j, c j

def energy {n : ℕ} (c : Fin n → ℝ) : ℝ := ∑ j, c j ^ 2

def empiricalMean {n : ℕ} (c : Fin n → ℝ) : ℝ := coefficientSum c / n

def empiricalVariance {n : ℕ} (c : Fin n → ℝ) : ℝ :=
  (∑ j, (c j - empiricalMean c) ^ 2) / n

/-- Original output minus pruned output, with surviving weights rescaled by `1/q`. -/
def outputError {n : ℕ} (q : ℝ) (c : Fin n → ℝ) (ω : Mask n) : ℝ :=
  ∑ j, (c j - (if ω j then 0 else c j / q))

def dareError {n : ℕ} (p : ℝ) (c : Fin n → ℝ) : Mask n → ℝ :=
  outputError (1 - p) c

def outputBias {n : ℕ} (p q : ℝ) (c : Fin n → ℝ) : ℝ :=
  (1 - (1 - p) / q) * coefficientSum c

/-- Continuous value at one half; analytic claims use `0 < p < 1`. -/
def phi (p : ℝ) : ℝ :=
  if p = 1 / 2 then 1 / 2 else (1 - 2 * p) / Real.log ((1 - p) / p)

lemma maskMass_nonneg {n : ℕ} {p : ℝ} (hp : 0 ≤ p) (hp' : p ≤ 1) (ω : Mask n) :
    0 ≤ maskMass p ω := by
  apply Finset.prod_nonneg
  intro j _
  split
  · exact hp
  · exact sub_nonneg.mpr hp'

lemma maskMass_sum {n : ℕ} (p : ℝ) : ∑ ω : Mask n, maskMass p ω = 1 := by
  unfold maskMass
  simpa using (Fintype.prod_sum (fun (_ : Fin n) (b : Bool) ↦
    if b then p else 1 - p)).symm

end DAREx

Source

Deng et al., DARE the Extreme: Revisiting Delta-Parameter Pruning For Fine-Tuned Models, ICLR 2025, arXiv:2410.09344v2, https://arxiv.org/pdf/2410.09344v2, Section 3.2, PDF p. 5, equation (2); Appendix E.1, PDF pp. 29–31, equations (7)–(8).

Read-back

What the Lean code literally says, in plain math · inherited model (exact model identifier unavailable)

For every natural number $n$ , let $I_n=\{0,\ldots,n-1\}$ and let $\Omega_n=\{\mathsf{false},\mathsf{true}\}^{I_n}$ be the set of all Boolean masks, with no assumption that $n>0$ . For every real number $p$ and mask $\omega\in\Omega_n$ , the defined mask weight is $w_p(\omega)=\prod_{j\in I_n}a_p(\omega_j)$ , where $a_p(\mathsf{true})=p$ and $a_p(\mathsf{false})=1-p$ . For every function $f:\Omega_n\to\mathbb R$ , its defined mean is $\mathcal M_p(f)=\sum_{\omega\in\Omega_n}w_p(\omega)f(\omega)$ ; for every predicate $A$ on $\Omega_n$ , its defined probability is $\mathcal P_p(A)=\sum_{\omega\in\Omega_n,\ A(\omega)}w_p(\omega)$ . These are finite real sums, with no measurability assumption or supplied decision procedure for $A$ . The definitions themselves permit every real $p$ , so the weights can be signed outside $[0,1]$ ; the names “mean” and “probability” do not impose a probability-measure hypothesis there. The two model lemmas, which have explicit proof bodies, assert that $w_p(\omega)\ge0$ for every natural $n$ , every real $p$ with $0\le p\le1$ , and every mask $\omega$ , and that $\sum_{\omega\in\Omega_n}w_p(\omega)=1$ for every natural $n$ and every real $p$ , including values outside $[0,1]$ . For $0\le p\le1$ , these weights give the finite product distribution in which the Boolean coordinates are independent and each is true with probability $p$ ; at $p=0$ all weight is on the all-false mask, and at $p=1$ all weight is on the all-true mask. For $n=0$ there is exactly one mask, the empty product is $1$ , $\mathcal M_p(f)$ is the value of $f$ on that mask, and $\mathcal P_p(A)$ is $1$ or $0$ according as $A$ holds or fails there, for every real $p$ .

For every natural $n$ and real coefficient family $c:I_n\to\mathbb R$ , define the coefficient sum $C(c)=\sum_{j\in I_n}c_j$ , energy $V(c)=\sum_{j\in I_n}c_j^2$ , empirical mean $\bar c=C(c)/n$ , and empirical variance $s_c^2=\bigl(\sum_{j\in I_n}(c_j-\bar c)^2\bigr)/n$ , where $n$ in a real expression denotes its image in $\mathbb R$ . The variance uses denominator $n$ , with no correction by $n-1$ . These definitions impose no positivity, nonzero, or sign hypothesis on $n$ or the coefficients, and real division is total with $x/0=0$ . In particular, for $n=0$ , the coefficient sum, energy, empirical mean, and empirical variance all equal $0$ ; for $n=1$ , the empirical mean is the sole coefficient and the empirical variance is $0$ .

For every natural $n$ , real $q$ , real coefficient family $c:I_n\to\mathbb R$ , and mask $\omega\in\Omega_n$ , define the output error $E_{q,c}(\omega)=\sum_{j\in I_n}\bigl(c_j-h_{q,c,j}(\omega_j)\bigr)$ , where $h_{q,c,j}(\mathsf{true})=0$ and $h_{q,c,j}(\mathsf{false})=c_j/q$ . Thus a true coordinate contributes $c_j$ to the error and a false coordinate contributes $c_j-c_j/q$ . For every additional real $p$ , the DARE error is defined as $D_{p,c}(\omega)=E_{1-p,c}(\omega)$ , and the output bias is defined as the scalar $b_{p,q,c}=\bigl(1-(1-p)/q\bigr)C(c)$ . Neither definition imposes $p\in[0,1]$ , $q>0$ , or a relation between $p$ and $q$ ; “output bias” is the name of this formula and is not itself an assertion that it equals a mean. With the total convention $x/0=0$ , $E_{0,c}(\omega)=C(c)$ and $b_{p,0,c}=C(c)$ for every mask and every $p$ , and $D_{1,c}(\omega)=C(c)$ . For $n=0$ , all these error and bias quantities are $0$ .

For every real $p$ , define $\phi(p)=\tfrac12$ if $p=\tfrac12$ , and otherwise define $\phi(p)=(1-2p)/\log((1-p)/p)$ . There is no restriction on $p$ in this definition and no separate assertion here that $\phi$ is positive or bounded. The logarithm is Lean's total real logarithm: it has value $0$ at $0$ and takes the logarithm of the absolute value at a negative input; all quotients use total real division with $x/0=0$ . Consequently the formula is defined also at $p=0$ and $p=1$ , where it gives $\phi(0)=\phi(1)=0$ , while the explicitly selected midpoint value is $\phi(\tfrac12)=\tfrac12$ .

Human review

Endorsed by Shuze Chen · Sep 29, 2026
Confirmed by the moderator at approval.
Endorsed by Minghui · Sep 29, 2026
Confirmed by the mission captain (proposal self-audit).

View graph