Pith. sign in

REVIEW 3 major objections 4 minor 22 references

Identity Testing for Circuits with Exponentiation Gates

T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Pith's one-line read The paper claims that randomized identity testing for arithmetic circuits with exponentiation gates reduces to a single modular query over two finite fields, with perfect completeness and soundness controlled by a sparse-root bound on a…

desk verdict Nice formal framework, but the main soundness theorem rests on a false coefficient-growth estimate; the paper needs a real repair before the headline result can be trusted. read the letter →

arxiv 2506.04529 v1 pith:2TYQKTPS submitted 2025-06-05 cs.CC cs.DS

classification cs.CCcs.DS MSC 68W2068Q2511T0612E05
keywords identitytestingexponentialpolynomialsarithmeticcircuitsfinitefieldsSchwartz-Zippellemmasparsepolynomialrootsneuralnetworkcompilersrandomizedalgorithms
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Identity testing asks whether two arithmetic expressions compute the same function. This paper extends the question to circuits with exponentiation gates, which compute expressions like sums of polynomials times exponentials of rational functions, the shape of softmax and attention blocks in neural networks. The central claim is that a black-box test using one random query over two finite fields is perfectly complete, and rejects every nonzero circuit with probability at least $1 - 8dk^4/q - q^{-1/(k^2-1)}$, where $k$ is the circuit's width, $d$ its degree, and $q$ a prime parameter. The evaluation rules use one prime $p$ for values and a second prime $q$ for exponents, with the test element $a$ drawn from the order-$q$ multiplicative subgroup of $\mathbb{F}_p^*$, so that $a^{x+y}=a^xa^y$ and the finite-field exponential mirrors $e^{x+y}=e^xe^y$. If correct, the result gives optimization compilers a sound, one-sided-error way to detect redundant computations in nonlinear neural-network components without floating-point roundoff errors.

What carries the argument

The load-bearing objects are AExp1 circuits and their associated exponential polynomials $P(\vec x)=\sum_{i=1}^k f_i(\vec x)\exp(g_i(\vec x)/h_i(\vec x))$. A structural lemma rewrites every AExp1 circuit as a fraction $P/P'$ while preserving both real and finite-field evaluations. The two-modulus evaluation rule makes the exponential law hold: because $a$ lies in the order-$q$ subgroup of $\mathbb{F}_p^*$, $a^{x+y \bmod q} = a^xa^y$, so the finite-field gate mirrors the identity $e^{x+y}=e^xe^y$. Soundness rests on a weak Descartes' rule over finite fields: a univariate polynomial with $k$ nonzero terms has at most $q^{1-1/(k-1)}$ roots in the order-$q$ subgroup, proved by rotating exponents to reach a low-degree representative. Condensation, which merges terms whose exponent fractions are equal as rational functions, is what lets the real and algebraic settings line up.

What would settle it

A direct computational check settles the soundness claim: instantiate a small nonzero AExp1 circuit of width $k=3$ and degree $d=1$ with coefficients in $\{-1,0,1\}$, pick primes $q \approx 10^6$ and $p \equiv 1 \pmod q$, sample many triples $(\vec u,\vec v,a)$, and compare the rejection rate with $1 - 8dk^4/q - q^{-1/(k^2-1)}$; a rate far below that bound would refute Theorem 4, while agreement would confirm the bound in the regime the paper targets.

Watch

Extended reading notes

Core claim

Formally, the paper proves Theorem 4. Let $C$ be an AExp1 circuit, an arithmetic circuit with addition, multiplication, division, and exponentiation gates, with at most one exponentiation on any input-to-output path, of width $k$, degree $d$, and weight $w$. For primes $p,q$ with $q \mid p-1$ and $q > 2(kw)^2$, the circuit is evaluated by carrying two values per wire, one in $\mathbb{F}_p$ and one in $\mathbb{F}_q$; addition, multiplication, and division act coordinate-wise, and an exponentiation gate sends $(\tau,\alpha)$ to $(a^\alpha \bmod p, \bot)$ for $a$ in the order-$q$ subgroup $G \subseteq \mathbb{F}_p^*$. The algorithm samples $\vec u \in \mathbb{F}_p^n$, $\vec v \in \mathbb{F}_q^n$, $a \in G$, and accepts when the output lies in $\{0,\bot\}$. Completeness says that if $C$ is identically zero on its real domain, every query returns $\{0,\bot\}$. Soundness says that if $C$ is not identically zero, the query returns a nonzero value with probability at least $1 - 8dk^4 q^{-1} - q^{-1/(k^2-1)}$. The proof converts the circuit into a fraction $P/P'$ of exponential polynomials, condenses terms with equal exponent fractions, and applies a finite-field analogue of Descartes' rule bounding how often a sparse sum $\beta_1 a^{\alpha_1} + \cdots + \beta_k a^{\alpha_k}$ can vanish on the subgroup $G$.

Load-bearing premise

The soundness proof assumes that every coefficient arising after multiplying the two exponential polynomials stays below the primes $p$ and $q$, so that a nonzero real polynomial cannot become the zero polynomial modulo those primes.

Editorial extensions

If this is right

  • For softmax, attention, and similar nonlinear blocks, redundancy detection becomes a single modular evaluation with one-sided error, so a compiler can fuse or eliminate equivalent tensor programs without trusting floating-point arithmetic.
  • Running the test $O(k \log k / \log q)$ times in parallel reduces the error to $1/k^{O(1)}$, which is efficient in the practical regime $dk^3 \le q \le k^{O(1)}$.
  • In the idealized real-query model the same one-query strategy works against any finite sample set $S \subseteq \mathbb{Q}$, with error at most $8dk^2/|S|$, using the Lindemann–Weierstrass theorem in place of the finite-field root bound.
  • If the paper's Strong Descartes' Rule Conjecture over finite fields is true, the soundness error becomes a constant $1-\Omega(1)$ per query, making the algorithm substantially stronger for larger widths.
  • The algebraic query model itself is a reusable abstraction: any future black-box model whose queries can be implemented on tensor-processing hardware with small communication overhead can be plugged into the same testing framework.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The proof's soundness argument goes through only when the integer coefficients produced by multiplying $P$ and $P'$ remain below $p$ in absolute value; spelling out that condition as an explicit bound on degree, rather than only on weight, would make the theorem directly checkable.
  • The two-modulus evaluation trick generalizes: any class of functions expressible as sparse sums of exponentials of rational functions over finite fields could inherit a similar identity test, provided an analogue of the sparse-root bound holds for the chosen subgroup.
  • The Strong Descartes' Rule Conjecture has the flavor of an uncertainty principle for the map $f \mapsto (f(1), f(g), \dots, f(g^{q-1}))$ on $\mathbb{F}_p[x]/(x^q-1)$; proving it would automatically improve the error bounds for this and any analogous subgroup-based tests.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper introduces AExp1 circuits, an arithmetic circuit model with exponentiation gates, and studies black-box identity testing for functions of the form P/P', where P and P' are exponential polynomials. It defines a real query model and an algebraic query model over two finite fields with separate moduli for exponent and coefficient computations. The paper proves a real-query testing bound via Schwartz-Zippel and Lindemann-Weierstrass (Theorem 15), and claims an algebraic-query testing theorem with perfect completeness and a soundness error bound (Theorem 4) using a structural lemma, condensation of exponential polynomials, and a weak Descartes rule over finite fields. It also proposes a Strong Descartes conjecture under which the soundness error would be improved.

Significance. If the algebraic-query theorem can be repaired, this would be a useful contribution: it gives a clean formal model connecting neural-network compiler redundancy detection to identity testing, and the real-query result is an elegant application of Lindemann-Weierstrass. The finite-field query model with two moduli is natural and well motivated, and the paper is appropriately explicit that its conjecture is not needed for the stated theorems. However, the central algebraic soundness proof currently rests on false coefficient-growth assertions, and the simplified Theorem 2 is false as stated. The significance of the paper therefore depends on a corrected statement with explicit coefficient bounds, not merely on the existing proof being patched.

major comments (3)
  1. [Section 1.1, Theorem 2] The simplified soundness theorem is false as stated. Let P(x) = exp(3/10) - exp(-2/11), with k = 2, d = 0, and w = 11. Take q = 53 and any prime p with 53 | p - 1, for example p = 107. Then q > 2w and p, q ≥ 2kw both hold. The exponent fractions 3/10 and -2/11 are distinct over Q, so P is not identically zero over R; but modulo q they are equal because 3·11 - (-2)·10 = 53 ≡ 0 (mod 53). Hence P_a(u,v) = a^{48} - a^{48} = 0 for every query, so the claimed soundness probability bound of roughly q^{-1/(k-1)} is violated. The proof must require q to exceed the integer coefficients of g_i h_j - g_j h_i, or otherwise handle exponent collisions explicitly; q > 2w is not sufficient.
  2. [Section 5.3, proof of Theorem 4] The assertion that R = P·P' has weight w^2, and that after condensation every coefficient of f''_i lies in [-(kw)^2, (kw)^2], is false under the paper's definition of weight as a bound on all integer coefficients. Expanding a product of two degree-d polynomials can produce coefficients as large as binom(n+2d, 2d) w^2, and condensation adds up to k^2 such products. For example, with n = 2, w = 1, k = 2, and P = P' = A·exp(0) + A·exp(1) where A = (1+x_1+x_2)^4, the coefficient of x_1^4 x_2^4 in the condensed exp(1) term of P·P' is 2·binom(8,4) = 140, while the claimed bound is (kw)^2 = 4. Since the theorem assumes only q > 2(kw)^2, such coefficients can vanish modulo p or q, so the proof's conclusion that f''_i and h''_i are nonzero modulo p and q is unjustified. A degree- and dimension-dependent coefficient bound, or a different reduction argument, is needed.
  3. [Section 5.3, Lemma 21] The proof applies the Schwartz-Zippel lemma to g_i h_j - g_j h_i as a nonzero polynomial over F_q, but a nonzero integer polynomial can reduce to the zero polynomial modulo q if all its coefficients are divisible by q. The lemma's hypotheses do not include any bound on q relative to the coefficients of these cross products, and the attempt in Theorem 4 to obtain such a bound from the weight of R is invalid for the reason in the previous comment. Thus the event that all exponent fractions are distinct modulo q is not established, and the subsequent use of Theorem 17 is not justified. This is a load-bearing gap: without distinct exponents modulo q, the weak Descartes bound cannot be applied.
minor comments (4)
  1. [Section 5.1, proof of Lemma 16] The set ζ is defined as the set of indices for which f_i is identically zero, but the subsequent argument and the event E_f require ζ to be the set of indices for which f_i is not identically zero; the definition should be corrected.
  2. [Theorems 17 and 4] The error terms q^{-1/(k-1)} and q^{-1/(k^2-1)} are undefined when k = 1; the statements should either exclude k = 1 or handle this degenerate case separately.
  3. [Section 5.2] The proof of Theorem 17 refers to Lemma 17 where Theorem 17 is meant, and Proposition 18 says the number of roots is 'smaller than' where 'at most' is intended; these should be fixed.
  4. [Abstract and Section 1] There are several typos: 'mathematical simple' in the abstract, 'a-prior' in Section 1, and 'Canettie et al.' in Remark 1 should be 'Canetti et al.'

Circularity Check

0 steps flagged · score 1.0 of 10

No meaningful circularity: main theorems derive from external results; the only self-reference is a non-load-bearing abstract claim about Mirage.

full rationale

The paper's central results (Theorems 15, 17, 4, and Lemma 21) are derived from external mathematical tools: Schwartz-Zippel (Lemma 8), Lindemann-Weierstrass (Theorem 9), and Kelley's root bound (Lemma 19). The circuit-to-exponential-polynomial conversion is proved by induction in Lemma 14, not imported. The algebraic query model is newly defined, not a renamed known result. No parameter is fitted to data, and Conjecture 1 is explicitly nonessential to the theorems. The only self-citation-adjacent passage is the abstract's claim that the algorithm 'has been implemented in the optimization compiler Mirage by Wu et al. (OSDI 2025)'; because Wu is a co-author, this is a self-reference, but it is empirical and non-load-bearing for the mathematical claims. The proof does contain a substantive correctness gap flagged by the skeptic: in Theorem 4's soundness proof, the assertion that the integer weights in f''_i stay within [-(kw)^2,(kw)^2] is false, since products of degree-d polynomials can have coefficient blowup C(n+d,d)w^2, so the conclusion that f''_i is nonzero modulo p is unjustified. This is a mathematical error, not circularity: it does not make the theorem reduce to its assumptions. Honest finding: no significant circularity.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No new physical or conjectural entities are introduced; AExp1 circuits and the algebraic query model are formal definitions rather than testable objects. The free-parameter list is empty because the constants in the algorithm, such as B = 20dk^2 and the primes p, q, are user-chosen parameters rather than values fitted to data.

assumptions (5)
  • standard math Schwartz-Zippel lemma (Lemma 8)
    Used throughout to bound the probability that polynomial evaluations vanish on random points, for example in Lemma 16, Theorem 15, and Lemma 21.
  • standard math Lindemann-Weierstrass theorem (Theorem 9)
    Used in Lemma 16 to conclude that a sum of nonzero algebraic multiples of e raised to distinct algebraic exponents cannot vanish.
  • standard math Kelley's root bound for sparse polynomials (Lemma 19)
    Used in the proof of the weak Descartes rule over finite fields (Theorem 17), which supplies the q^{-1/(k^2-1)} soundness term.
  • domain assumption Two-modulus finite-field evaluation of exponentiation gates: a^alpha with exponents in F_q, values in F_p, and a in the order-q subgroup G
    This is the paper's modeling choice for the algebraic query model. The soundness theorem is about this evaluation rule, not about arbitrary finite-field interpretations of e^x.
  • domain assumption AExp1 restriction: at most one exponentiation gate on each input-to-output path
    Used in Lemma 14's induction, where the subcircuit under an exponentiation gate must contain no exponentiation gates.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Identity Testing for Circuits with Exponentiation Gates." pith.science (2026). https://pith.science/paper/2TYQKTPS

@misc{pith2026250604529,
  author       = {Pith},
  title        = {Pith review of: Identity Testing for Circuits with Exponentiation Gates},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2TYQKTPS}},
  note         = {Machine review of arXiv:2506.04529}
}
abstract

Motivated by practical applications in the design of optimization compilers for neural networks, we initiated the study of identity testing problems for arithmetic circuits augmented with \emph{exponentiation gates} that compute the real function $x\mapsto e^x$. These circuits compute real functions of form $P(\vec x)/P'(\vec x)$, where both $P(\vec x)$ and $P'(\vec x)$ are exponential polynomials \[ \sum_{i=1}^k f_i(\vec x)\cdot \exp\left(\frac{g_i(\vec x)}{h_i(\vec x)}\right), \] for polynomials $f_i(\vec x),g_i(\vec x)$, and $h_i(\vec x)$. We formalize a black-box query model over finite fields for this class of circuits, which is mathematical simple and reflects constraints faced by real-world neural network compilers. We proved that a simple and efficient randomized identity testing algorithm achieves perfect completeness and non-trivial soundness. Concurrent with our work, the algorithm has been implemented in the optimization compiler Mirage by Wu et al.~(OSDI 2025), demonstrating promising empirical performance in both efficiency and soundness error. Finally, we propose a number-theoretic conjecture under which our algorithm is sound with high probability.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

22 extracted references · 15 canonical work pages

  1. [1]

    Primality and identity testing via chinese remaindering

    Manindra Agrawal and Somenath Biswas. Primality and identity testing via chinese remaindering. J. ACM , 50(4):429--443, 2003

  2. [2]

    Computational Complexity - A Modern Approach

    Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach . Cambridge University Press, 2009

  3. [3]

    Probabilistic checking of proofs: A new characterization of NP

    Sanjeev Arora and Shmuel Safra. Probabilistic checking of proofs: A new characterization of NP . J. ACM , 45(1):70--122, 1998

  4. [4]

    Transcendental Number Theory

    Alan Baker. Transcendental Number Theory . Cambridge Mathematical Library. Cambridge University Press, 2022

  5. [5]

    On the statistical properties of diffie-hellman distributions

    Ran Canetti, John Friedlander, Sergei Konyagin, Michael Larsen, Daniel Lieman, and Igor Shparlinski. On the statistical properties of diffie-hellman distributions. Israel Journal of Mathematics , 120:23--46, 2000

  6. [6]

    Maurice Rojas, and Daqing Wan

    Qi Cheng, Shuhong Gao, J. Maurice Rojas, and Daqing Wan. Sparse univariate polynomials with many roots over finite fields. Finite Fields Their Appl. , 46:235--246, 2017

  7. [7]

    Abstract algebra , volume 3

    David Steven Dummit and Richard M Foote. Abstract algebra , volume 3. Wiley Hoboken, 2004

  8. [8]

    DeMillo and Richard J

    Richard A. DeMillo and Richard J. Lipton. A probabilistic remark on algebraic program testing. Inf. Process. Lett. , 7(4):193--195, 1978

Show all 22 references
  1. [9]

    Roots of sparse polynomials over a finite field

    Zander Kelley. Roots of sparse polynomials over a finite field. LMS Journal of Computation and Mathematics , 19(A):196--204, 2016

  2. [10]

    On determinants, matchings, and random algorithms

    L \' a szl \' o Lov \' a sz. On determinants, matchings, and random algorithms. In Lothar Budach, editor, Fundamentals of Computation Theory, FCT 1979, Proceedings of the Conference on Algebraic, Arthmetic, and Categorial Methods in Computation Theory, Berlin/Wendisch-Rietz, G...

  3. [11]

    Analysis of Boolean Functions

    Ryan O'Donnell. Analysis of Boolean Functions . Cambridge University Press, 2014

  4. [12]

    U ber h \

    ystein Ore. \"U ber h \"o here kongruenzen . Gr ndahl, 1921

  5. [13]

    Progress on polynomial identity testing

    Nitin Saxena. Progress on polynomial identity testing. Bull. EATCS , 99:49--79, 2009

  6. [14]

    Progress on polynomial identity testing - II

    Nitin Saxena. Progress on polynomial identity testing - II . CoRR , abs/1401.0976, 2014

  7. [15]

    Schwartz

    Jacob T. Schwartz. Fast probabilistic algorithms for verification of polynomial identities. J. ACM , 27(4):701--717, 1980

  8. [16]

    IP = PSPACE

    Adi Shamir. IP = PSPACE . J. ACM , 39(4):869--877, 1992

  9. [17]

    GLU variants improve transformer

    Noam Shazeer. GLU variants improve transformer. CoRR , abs/2002.05202, 2020

  10. [18]

    The factorization of linear graphs

    William T Tutte. The factorization of linear graphs. Journal of the London Mathematical Society , 1(2):107--111, 1947

  11. [19]

    Attention is all you need

    Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, ukasz Kaiser, and Illia Polosukhin. Attention is all you need. In I. Guyon, U. Von Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett, editors, Advances in Neural In...

  12. [20]

    A multi-level superoptimizer for tensor programs

    Mengdi Wu, Xinhao Cheng, Oded Padon, and Zhihao Jia. A multi-level superoptimizer for tensor programs. CoRR , abs/2405.05751, 2024

  13. [21]

    PET : Optimizing tensor programs with partially equivalent transformations and automated corrections

    Haojie Wang, Jidong Zhai, Mingyu Gao, Zixuan Ma, Shizhi Tang, Liyan Zheng, Yuanzhi Li, Kaiyuan Rong, Yuanyong Chen, and Zhihao Jia. PET : Optimizing tensor programs with partially equivalent transformations and automated corrections. In 15th USENIX Symposium on Operating Syste...

  14. [22]

    Probabilistic algorithms for sparse polynomials

    Richard Zippel. Probabilistic algorithms for sparse polynomials. In Edward W. Ng, editor, Symbolic and Algebraic Computation, EUROSAM '79, An International Symposiumon Symbolic and Algebraic Computation, Marseille, France, June 1979, Proceedings , volume 72 of Lecture Notes in...

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.