Doubly Sub-linear Interactive Proofs of Proximity
AuthorsNoga Amir†, Oded Goldreich†, Guy N. Rothblum
Doubly Sub-linear Interactive Proofs of Proximity
AuthorsNoga Amir†, Oded Goldreich†, Guy N. Rothblum
We study doubly sub-linear interactive proofs of proximity (dsIPPs): proofs that are ultra-fast to generate, and can be used to prove approximate assertions about a huge input. Proof generation is ultra-fast in the sense that it only requires reading a small (sub-linear) portion of the input. Approximate verification of the proof is even faster (reading an even smaller portion of the input). Similarly to the property testing literature, approximate verification means the sublinear-time honest prover can make the verifier accept each input in the property, but no prover can fool the verifier into accepting an input that is far from the property. Such proof systems can be used to prove (and verify) claims about the properties of a huge input object, even though the prover cannot read the entire object (and the verifier is even more restricted). We construct such a proof system for any property that can be decided by a constant-width read-once oblivious branching program (ROOBP). We also construct proof systems for approximate verification of an input’s Hamming weight, and for a relaxation of bipartiteness in the bounded-degree graph model.
Interactive Proofs for General Distribution Properties
July 16, 2026research area Methods and Algorithmsconference FOCS
Suppose Alice has collected a small number of samples from an unknown distribution, and would like to learn about the distribution. Bob, an untrusted data analyst, claims to have run a sophisticated data analysis on the distribution and makes assertions about its properties. When and how is it possible for Alice to efficiently verify Bob’s claims (using fewer resources than would be needed to run the analysis herself)? We construct interactive…
Hilbert: Recursively Building Formal Proofs with Informal Reasoning
October 2, 2025research area Methods and Algorithms, research area Tools, Platforms, Frameworksconference ICLR, Workshop at NeurIPS
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…