# Is there a full and precise formulation of Theorem 1 in the Integrated Gradients paper?

Theorem 1 (page 5) in the paper about Integrated Gradients states that

Integrated gradients is the unique path method that is symmetry-preserving.

What I miss is

1. A precise formulation of the theorem: in particular, the exact properties that must be satisfied by the function $$f$$ used in the proof (continuity, differentiability, etc.). Also, should the paths be assumed to be monotonic?

2. A consistent definition of function $$f$$ in the proof - note that $$f$$ is defined inconsistently, e.g. in the region where $$x_i and $$x_j>b$$, where it is not clear whether its value should be $$0$$ or $$(b-a)^2$$.

Point 2 is easy to fix with an appropriate redefinition (e.g. replacing "if $$\text{max}(x_i,x_j)\geq 0$$" with "else if $$\text{max}(x_i,x_j)\geq 0$$"). What it is not clear if whether there is a redefinition that:

1. preserves the properties that have been assumed in the rest of the paper, in particular in Proposition 1 (proving completeness), where the function is assumed to be continuous everywhere, and the set of discontinuous points of each of its partial derivatives along each input dimension has measure zero, and

2. the function is a constant for $$t \notin [t_1,t_2]$$.

Does anybody have a precise formulation and full proof of the theorem?

• Well, I just realized that Proposition 1 in the paper cannot be correct as stated either. In one dimension that proposition is just the (second) Fundamental Theorem of Calculus stated for functions that verify Lebesgue’s integrability criterion, but Cantor's staircase function is a well known counter-example showing that such condition is not enough to ensure the conclusion of the FTC. The premises of the proposition would need to be relaxed somehow, but still keeping them strong enough to be applied to deep networks with functions such as ReLu and max pooling. Mar 10 at 16:51
• Back to Proposition 1, for univariate functions the condition should be "absolutely continuous" (rather than differentiable almost everywhere) - this leads to a suitable generalization of the Fundamental Theorem of Calculus that can be applied to functions occurring in deep networks, but I am still wondering how to generalize the gradient theorem in a similar way so it can be applied to functions implemented by deep networks. That generalization would contain premises to be used in the formulation of Theorem 1. Mar 11 at 1:52

After working on it for a while this is what I got.

Concerning proposition 1 in the paper, a rigorous statement could be the following version of the Gradient Theorem for line integrals:

Proposition 1. (Gradient Theorem for Lipschitz Continuous Functions). Let $$U$$ be an open subset of $$\mathbb{R}^n$$. If $$F : U \to \mathbb{R}$$ is Lipschitz continuous, and $$\gamma : [0,1] \to U$$ is a smooth path such that $$F$$ is differentiable at $$\gamma(t)$$ for almost every $$t\in [0,1]$$, then $$\int_{\gamma} \nabla F(\mathbf{x}) \cdot d\mathbf{x} = F(\gamma(1)) - F(\gamma(0)) \,.$$

I found theorem 1 about symmetry-preserving harder to state rigurously while still fully capturing its intended meaning - this is the best I got:

Theorem 1. Given $$i,j\in \{1,\dots,n\}$$, $$i\neq j$$, real numbers $$a, and a strictly monotonic smooth path $$\gamma : [0,1] \to (a,b)^n$$ such that $$\gamma_i(0)=\gamma_j(0)$$ and $$\gamma_i(1)=\gamma_j(1)$$, then the following statements are equivalent:

(1) For every $$t\in [0,1]$$, $$\gamma_i(t) = \gamma_j(t)$$.

(2) For every function $$F : [a,b]^n \to \mathbb{R}$$ symmetric in $$x_i$$ and $$x_j$$ and verifying the premises of proposition 1 with $$U=(a,b)^n$$ we have $$\int_{\gamma} \frac{\partial F(\mathbf{x})}{\partial x_i} \, dx_i = \int_{\gamma} \frac{\partial F(\mathbf{x})}{\partial x_j} \, dx_j$$.

Further details and proofs: Symmetry-Preserving Paths in Integrated Gradients