View publication

As statistical analyses become more central to science, industry and society, there is a growing need to ensure correctness of their results. Approximate correctness can be verified by replicating the entire analysis, but can we verify without replication? Building on a recent line of work, we study proof-systems that allow a probabilistic verifier to ascertain that the results of an analysis are approximately correct, while drawing fewer samples and using less computational resources than would be needed to replicate the analysis. We focus on distribution testing problems: verifying that an unknown distribution is close to having a claimed property.

Our main contribution is a interactive protocol between a verifier and an untrusted prover, which can be used to verify any distribution property that can be decided in polynomial time given a full and explicit description of the distribution. If the distribution is at statistical distance ε from having the property, then the verifier rejects with high probability. This soundness property holds against any polynomial-time strategy that a cheating prover might follow, assuming the existence of collision-resistant hash functions (a standard assumption in cryptography). For distributions over a domain of size N, the protocol consists of 4 messages and the communication complexity and verifier runtime are roughly O~(N/ε2)Õ(\sqrt N / ε^2). The verifier’s sample complexity is O~(N/ε2)Õ(\sqrt N / ε^2), and this is optimal up to polylog(N)polylog(N) factors (for any protocol, regardless of its communication complexity). Even for simple properties, approximately deciding whether an unknown distribution has the property can require quasi-linear sample complexity and running time. For any such property, our protocol provides a quadratic speedup over replicating the analysis.

† Weizmann Institute

Related readings and updates.

We study an extension of the standard two-party communication model in which Alice and Bob hold probability distributions pp and qq over domains XX and YY, respectively. Their goal is to estimate

Exp,yq[f(x,y)]\mathbb{E}_{x \sim p, y \sim q}[f(x, y)]

to within additive error ε\varepsilon for a bounded function ff, known to both parties. We refer to this as the distributed estimation problem. Special cases of this problem arise in a variety of areas…

Read more

This paper was accepted at the MATH-AI 2025 (MATH-AI) Workshop at NeurIPS 2025.

Large Language Models (LLMs) demonstrate impressive mathematical reasoning abilities, but their solutions frequently contain errors that cannot be automatically verified. Formal theorem proving systems such as Lean 4 offer automated verification with complete accuracy, motivating recent efforts to build specialized prover LLMs that generate verifiable proofs in…

Read more