Motivated by the mismatch between floating-point arithmetic, which is intrinsically approximate, and verifiable computing protocols for exact computations, we develop a generalization of the sum-check protocol. Our generalization proves claims of the form $$\sum _{x \in \{0,1\}^v} g(x) \approx H$$ , where g is a low-degree v-variate polynomial over an integral domain $$\mathbb {U}$$ . The verifier performs its check in each round of the protocol using a tunable error parameter $$\delta $$ . If $$\varDelta $$ is the error in the prover’s initial claim, then the soundness error of our protocols degrades gracefully with $$\delta /\varDelta $$ . In other words, if the initial error $$\varDelta $$ is large relative to $$\delta $$ , then the soundness error is small, meaning the verifier is very likely to reject. Unlike the classical sum-check protocol, which is fundamentally algebraic, our generalization exploits the metric structure of low-degree polynomials. The protocol can be instantiated over various domains, but is most natural over the complex numbers, where the analysis draws on the behavior of polynomials over the unit circle. We also analyze the protocol under the Fiat-Shamir transform, revealing a new “intermediate security” phenomenon that appears intrinsic to approximation. Prior work on verifiable computing for numerical tasks typically verifies that a prover exactly executed a computation that only approximates the desired function. In contrast, our protocols treat approximation as a first-class citizen: the verifier’s checks are relaxed to accept prover messages that are only approximately consistent with the claimed result. This establishes the first black-box feasibility result for approximate arithmetic proof systems: the protocol compiler is independent of how arithmetic operations are implemented, requiring only that they satisfy error bounds. This opens a path to verifying approximate computations while sidestepping much of the prover overhead imposed by existing techniques that require encoding real-valued data into finite field arithmetic.

Server authentication assures users that they are communicating with a server that genuinely represents a claimed domain. Today, server authentication relies on certification authorities (CAs), third parties who sign statements binding public keys to domains. CAs remain a weak spot in Internet security, as any faulty CA can issue a certificate for any domain.

There has been intense interest over the last decade in implementations of probabilistic proofs (IPs, SNARKs, PCPs, and so on): protocols in which an untrusted party proves to a verifier that a given computation was executed properly, possibly in zero knowledge. Nevertheless, implementations still do not scale beyond small computations. A central source of overhead is the front-end: translating from the abstract computation to a set of equivalent arithmetic constraints. This paper introduces a general-purpose framework, called Distiller, in which a user translates to constraints not the original computation but an abstracted specification of it. Distiller is the first in this area to perform such transformations in a way that is provably safe. Furthermore, by taking the idea of "encode a check in the constraints" to its literal logical extreme, Distiller exposes many new opportunities for constraint reduction, resulting in cost reductions for benchmark computations of 1.3–50×, and in some cases, better asymptotics.