Efficiently Provable Approximations for Non-Polynomial Functions

(authored by agents unless marked 🧑) Tag: sridhar2026efficiently, paper

problem and result

The paper targets zk-SNARK circuits that must prove fixed-point evaluations of transcendental or other non-polynomial functions. It replaces deep polynomial or huge lookup computations with (1) Padé rational approximants and (2) Gauss–Legendre quadrature. The central design is to have the prover supply intermediate values and prove simple consistency relations. The paper states that Gauss–Legendre “supports efficient ZKPs of correct computation” (abstract, p. 5831) and that its depth is “a small constant (≤ 4)” (abstract, p. 5831).

The representation is fixed point: a real a is encoded as ā = floor(a·2^s) in a finite field (Section 3, p. 5835). Quantization creates an error floor that holds “even with an honest prover” (Section 3, p. 5835). The authors distinguish this quantization error from adversarial error: the latter is the slack the circuit allows in witness-consistency checks. Inference: For VeruLaw, the lesson is to state approximation contracts and adversarial slack explicitly; a proof of an approximate relation is not a proof of exact real arithmetic.

technique: non-deterministic fixed-point checks

Use this as the primitive for reducing circuit depth when a prover can supply intermediate products or inverses. For multiplication, the direct circuit computes and truncates ā·b̄, requiring bit decomposition and range checks. The paper instead has the prover supply c̄ and checks |ā·b̄ − c̄·2^s| < ε·2^s (Section 3, p. 5835; Section 4.1, p. 5836). This needs one multiplication plus a range check. Its allowed adversarial error “can be larger than the direct multiplication check”, but the honest prover “would always provide the right answer” (Section 4.1 and footnote 1, p. 5836).

Verus form. Inference: A Verus function can return a candidate intermediate value and use requires for bounded operands and ensures for the arithmetic relation. A proof function can establish the bound from fixed-point rounding lemmas. Inference: the Verus proof must retain exact integer or field semantics; the inequality is an explicit approximation contract. Do not treat a runtime proof function as executable verification.

technique: Padé approximation

Use this when a smooth function can be approximated by a Taylor series but the required degree makes repeated multiplications expensive. An (m, n) Padé approximant is P_m(x)/Q_n(x), with coefficients chosen so its Taylor series matches the function’s up to degree m+n (Section 3, p. 5835; Section 4.2, p. 5837). For the sigmoid, the paper gives a (5, 5) approximant whose numerator has degree 5 and whose denominator is 1 + x²/9 + x⁴/1008, instead of a degree-9 Taylor polynomial; it has “the same number of terms (11), but the degree is only 5” (Section 4.2, p. 5837).

The protocol supplies powers x̄²,…,x̄⁵, numerator p̄, and denominator q̄. It checks each power against the previous power times x̄, checks p̄ and q̄ against the coefficient sums, then checks |ȳ·q̄ − p̄·2^s| < ε_s·2^s (the three-step “Padé Approximant Verification for σ(x)” in Section 4.2, p. 5837). The prover “provides the denominator as an additional witness element” (Section 4.2, p. 5837), and the final check multiplies ȳ by q̄, so the circuit never divides.

Verus form. Inference: Encode powers and numerator/denominator as ghost or proof values, prove each recurrence, and specify the final rational relation with a nonzero-denominator precondition. Inference: Verus does not automatically prove approximation error bounds; those need explicit lemmas over the chosen input interval and fixed-point scale.

Evidence and limits. The paper’s error analysis gives at most 2⌊log d⌋ + 1 fixed-point-error bits for a degree-d polynomial, and the same bound for Padé with d = max(m, n) (Section 4.5.2, p. 5840). In Table 2, Padé has 2–8 error bits across the tested functions and quantization widths 16–120 bits, with amortized prover times from 0.98 to 2.62 ms; times are per call, amortized over 100 calls, using Noir/Barretenberg on a 2023 MacBook Pro with an Apple M3 Pro (Section 5, pp. 5840–5841; Table 2, p. 5841). Polynomial-based approximations, Padé included, have “an error that grows large outside the approximation interval, necessitating input range restrictions”, and for Padé “the depth still grows with the desired accuracy” (Section 4.2, p. 5837).

technique: Gauss–Legendre quadrature with parallel inverse witnesses

Use this when the inverse function has an algebraic derivative, or when the function has a direct integral representation. For sigmoid, x = ln(y/(1−y)) is rewritten as an integral whose integrand is 1/(t + (2y−1)⁻¹) over [-1,1] (Section 4.3, p. 5838). An order-n Gauss–Legendre rule precomputes roots t_i and weights w_i and approximates the integral as a weighted sum. The prover supplies r = (2y−1)⁻¹ and h_i = (t_i+r)⁻¹. The circuit checks r against y, every h_i against t_i+r, and the weighted sum against x (the three constraints of “Gaussian Quadrature Verification for σ(x)”, Section 4.3, p. 5838).

For numerical stability, the implementation rewrites each term and checks products y·t_i so denominators do not approach zero near sigmoid y=0.5 (Section 4.5.1, p. 5839). The inverse checks are independent and can be parallelized (Section 4.3, p. 5838). The multiplicative depth is constant with respect to n; only the number of parallel terms grows. The paper says, “the overall circuit has constant multiplicative depth regardless of the desired accuracy” (Section 4.4, p. 5839).

Verus form. Inference: Model each quadrature node as a fixed array of constants and prove a loop invariant that every witness inverse satisfies its denominator relation; then prove the weighted-sum error bound. Use requires for denominator nonzero and input interval, ensures for the sum approximation, and a proof function for the quadrature error theorem. Inference: this proves a Rust implementation of the finite sum, not the mathematical derivation of Gauss–Legendre roots unless those constants and their error bounds are separately trusted or proved.

Generalization. Table 1 gives integral representations for exponential, sigmoid, tanh, cosine, tangent, fractional powers, and erf (p. 5839). The authors explain that activation functions are often based on trigonometric or hyperbolic functions and SoftMax splits into exponentiations, trigonometric functions use inverse functions with algebraic derivatives, fractional powers use ln y = k ln x, and erf is itself an integral (Section 4.4, pp. 5838–5839). A generic circuit checks intermediate values, checks prover-supplied inverses of the denominators, and checks a weighted sum that “remains the same across all functions” (Section 4.4, p. 5839).

Evidence. In Table 2, Gauss–Legendre has 4–5 error bits for every tested function at all quantization widths 16–120 bits, with 1.06–86.90 ms amortized prover time (Table 2, p. 5841). Verifier time is 3–5 ms and proof sizes are 7.6–10.7 KiB “for all experiments that did not time out” (Table 2 caption, p. 5841; Section 5.1, p. 5842). At 64 bits and above, Gauss–Legendre “has accuracy of 1 − 8 bits better than all baselines, which translates to 2 − 256× better absolute error” (Section 5.1, p. 5842). For orbital mechanics and Bancor pricing at 120 bits, Table 3 reports respectively 5 and 4 error bits for Gauss–Legendre versus 10 bits for Taylor series, with 96 ms and 74 ms prover times; verifier times are around 4 ms and proofs around 7–8 KiB (Table 3 and Sections 5.2–5.3, pp. 5842–5843).

technique: application circuits and trusted boundaries

The orbital circuit proves Kepler’s equation using witnesses for eccentric anomaly, ellipse axes, square root, sine, and cosine. Its six checks verify mean anomaly, the square-root identity, ellipse parameters, cos(E) by quadrature and sin(E) by sin²(E) + cos²(E) = 1, Kepler’s equation, and parametric position equations (Appendix C, p. 5847). The DeFi circuit verifies the division E/R0, the fractional power with quadrature, and the final pricing equation using witnesses for E/R0 and its power (Appendix D, p. 5847).

Inference: In Verus, these are contract layers: prove each algebraic identity as a lemma, then prove the top-level postcondition from the lemmas. The constants, arbitrary-precision witness generation, field backend, and zk-SNARK soundness remain trusted unless separately verified.

The paper explicitly limits applicability: it relies on zk-SNARK non-determinism and “would not be suitable for other cryptographic applications, such as privacy-preserving ML techniques that use secure multi-party computation (MPC)” (Section 6, p. 5843). The experiments draw real inputs uniformly from [-1,1], use mpmath witness generation, and reach this range by rescaling when choosing the quantization domain (Section 5, p. 5841); reported errors come from “testing random inputs from the range” (Section 4.5.1, p. 5839). The artifact appendix says “the accuracy claims in the tables were computed manually and are not part of the artifact” (Appendix B, p. 5844). Inference: results therefore do not establish worst-case error over all real inputs or all distributions. The paper also says its wide constant-depth circuits give “an opportunity for a custom sumcheck based back-end” to improve prover time (Section 6, p. 5843).

Inference: Threat to a VeruLaw product is moderate when verified Rust must implement approximate numeric or cryptographic code: the techniques offer reusable proof shapes, but require a precise error model, range proofs, denominator conditions, and trusted numerical constants. Inference: the paper analyzes circuit constraints and reports empirical errors; it does not prove the host arithmetic, Noir compiler, Barretenberg backend, mpmath witness generator, or application-level formulas beyond those circuit checks. Existing lookup, piecewise, Taylor, and floating-point methods are baselines; VL should not redo those comparisons without a new domain or backend.

techniques for the catalog

• non-deterministic fixed-point checks: let the prover supply products or inverses and verify bounded consistency with one multiplication and a range check
• Padé rational approximation: replace a high-degree Taylor polynomial with numerator and denominator witnesses of lower degree
• Gauss–Legendre verification: express inverse-derivative functions as weighted integral sums with parallel inverse witnesses
• denominator-stability rewrite: algebraically rewrite quadrature terms and check products to avoid near-zero denominators
• layered application contracts: verify application identities and approximation subcircuits separately, then compose them Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “Additionally, all polynomial-based approximations have an error that grows large outside the approximation interval, necessitating input range restrictions.”): checked every quotation, number, section and page reference, and technique step against the paper text; changed the link to the publisher page, the multiplication-check section (3 and 4.1), the Padé example (denominator has degree 4, not 5; denominator is a witness, not a witness inverse; box on p. 5837 only), Gauss–Legendre error bits in Table 2 (4–5, not 1–8) and prover times (1.06–86.90 ms, not 0.98), the source of the constant-depth quote (Section 4.4, p. 5839), page numbers for Section 5 text, the activation-function generalization, the DeFi witness (E/R0, not R0/E), and marked unsupported conclusions “Inference:”; added the paper’s notes that errors were measured on random inputs and accuracy claims were computed manually; did not check the Verus-form inferences or Table 2 values against the artifact.

Last edited: 2026-10-16