Search

Zero-knowledge succinct arguments of knowledge (zkSNARKs) enable efficient privacy-preserving proofs of membership for general NP languages. Our focus in this work is on post-quantum zkSNARKs, with a focus on minimizing proof size. Currently, there is a 1000x gap in the proof size between the best pre-quantum constructions and the best post-quantum ones. Here, we develop and implement new lattice-based zkSNARKs in the designated-verifier preprocessing model. With our construction, after an initial preprocessing step, a proof for an NP relation of size 2^20 is just over 16 KB. Our proofs are 10.3x shorter than previous post-quantum zkSNARKs for general NP languages. Compared to previous lattice-based zkSNARKs (also in the designated-verifier preprocessing model), we obtain a 42x reduction in proof size and a 60x reduction in the prover's running time, all while achieving a much higher level of soundness. Compared to the shortest pre-quantum zkSNARKs by Groth (Eurocrypt 2016), the proof size in our lattice-based construction is 131x longer, but both the prover and the verifier are faster (by 1.2x and 2.8x, respectively). Our construction follows the general blueprint of Bitansky et al. (TCC 2013) and Boneh et al. (Eurocrypt 2017) of combining a linear probabilistically checkable proof (linear PCP) together with a linear-only vector encryption scheme. We develop a concretely-efficient lattice-based instantiation of this compiler by considering quadratic extension fields of moderate characteristic and using linear-only vector encryption over rank-2 module lattices.

Our story is about hardness of problems in P, but its roots begin with two algorithmic approaches that have been developed to cope with NP-hard problems: approximation algorithms and fasterthan- brute-force algorithms. Approximation algorithms were proposed as a response for NP-hardness almost immediately (in historical perspective of almost half a century), and have been one of the most celebrated success stories of our eld. An outstanding complexity result in this area, which has since turned into a sub- eld of its own, is the Probabilistically Checkable Proof (PCP) Theorem. For many problems like Max-3-SAT we now have nearly tight hardness-of-approximation results.

The PCP theorem has recently been shown to hold as well in the real number model of Blum, Shub, and Smale (Baartse and Meer, 2015). The proof given there structurally closely follows the proof of the original PCP theorem by Dinur (2007). In this paper we show that the theorem also can be derived using algebraic techniques similar to those employed by Arora etal. (Arora etal., 1998; Arora and Safra, 1998) in the first proof of the PCP theorem. This needs considerable additional efforts. Due to severe problems when using low degree algebraic polynomials over the reals as codewords for one of the verifiers to be constructed, we work with certain trigonometric polynomials. This entails the necessity to design new segmentation procedures in order to obtain well structured real verifiers appropriate for applying the classical technique of verifier composition.We believe that designing as well an algebraic proof for the real PCP theorem on one side leads to interesting questions in real number complexity theory and on the other sheds light on which ingredients are necessary in order to prove an important result as the PCP theorem in different computational models.

We show that it is quasi-NP-hard to color 2-colorable 12-uniform hypergraphs with $2^{(\log n)^{\Omega(1) }}$ colors where $n$ is the number of vertices. Previously, Guruswami Harsha, H\aa stad, Srinivasan, and Varma showed that it is quasi-NP-hard to color 2-colorable 8-uniform hypergraphs with $2^{2^{\Omega(\sqrt{\log \log n})}}$ colors. Their result is obtained by composing a standard outer probabilistically checkable proof (PCP) with an inner PCP based on the short code of superconstant degree. Our result is instead obtained by composing a new outer PCP with an inner PCP based on the short code of degree two.

In this work, we will reason on how a given focused proof, where atoms are assigned with some polarity, can be transformed into another focused proof, where the polarity assignment to atoms is changed. This will allow, in principle, transforming a proof obtained using one proof system into a proof using another proof system. More specifically, using the intuitionistic focused system LJF restricted to Harrop formulas, we define a procedure, introducing cuts, for transforming a focused proof where an atom is assigned with positive polarity into another focused proof where the same atom is assigned negative polarity and vice-versa. Then we show how to eliminate these cuts, obtaining a very interesting result: while the process of eliminating a cut on a positive atom gives rise to a proof with one smaller cut, in the negative case the number of introduced cuts grows exponentially. We end the paper by showing how to use maximal multi-focusing identify proofs in LJF, giving rise to a 1-1 translation between maximal proofs in LJF and proofs in the natural deduction system for intuitionistic logic NJ, restricted to Harrop formulas.

Canetti, Lin and Paneth in TCC 2013 showed a $O(\log^{1+\varepsilon}{n})$ rounds public-coin concurrent zero-knowledge argument system (CZK) based on the existence of collision resistant hash functions, which is currently known as round optimal public-coin CZK from standard assumptions. In this paper, we further address this problem and present an alternative construction of public-coin CZK argument system with succinct slot. The key technique involves a new variant of Baraks non-black-box simulate approach. In particular, the original protocol uses $n$ commitments in each slot, while our construction uses one commitment in each slot. Through our simulation techniques, the simulator recovers any previous state needed for the probabilistically checkable proof (PCP from the current committed state, which, in our view, may be of independent interest. Furthermore, the public-coin CZK argument system can be transformed into a resettable security protocol based on the one way functions assumption. Therefore, we present a new construction of the simultaneous resettable zero-knowledge argument system.

We introduce and study the notion of fully linear probabilistically checkable proof systems. In such a proof system, the verifier can make a small number of linear queries that apply jointly to the input and a proof vector.

We initiate a study of non-interactive proofs of proximity. These proof systems consist of a verifier that wishes to ascertain the validity of a given statement, using a short (sublinear length) explicitly given proof, and a sublinear number of queries to its input. Since the verifier cannot even read the entire input, we only require it to reject inputs that are far from being valid. Thus, the verifier is only assured of the proximity of the statement to a correct one. Such proof systems can be viewed as the N P (or more accurately MA) analogue of property testing. We explore both the power and limitations of non-interactive proofs of proximity. We show that such proof systems can be exponentially stronger than property testers, but are exponentially weaker than the interactive proofs of proximity studied by Rothblum, Vadhan and Wigderson (STOC 2013). In addition, we show a natural problem that has a full and (almost) tight multiplicative trade-off between the length of the proof and the verifier’s query complexity. On the negative side, we also show that there exist properties for which even a linearly-long (non-interactive) proof of proximity cannot significantly reduce the query complexity.

The Probabilistically Checkable Proof (PCP) theorem (Arora and Safra in J ACM 45(1):70---122, 1998; Arora et al. in J ACM 45(3):501---555, 1998) asserts the existence of proofs that can be verified by reading a very small part of the proof. Since the discovery of the theorem, there has been a considerable work on improving the theorem in terms of the length of the proofs, culminating in the construction of PCPs of quasi-linear length, by Ben-Sasson and Sudan (SICOMP 38(2):551---607, 2008) and Dinur (J ACM 54(3):241---250, 2007). One common theme in the aforementioned PCP constructions is that they all rely heavily on sophisticated algebraic machinery. The aforementioned work of Dinur (2007) suggested an alternative approach for constructing PCPs, which gives a simpler and arguably more intuitive proof of the PCP theorem using combinatorial techniques. However, this combinatorial construction only yields PCPs of polynomial length and is therefore inferior to the algebraic constructions in this respect. This gives rise to the natural question of whether the proof length of the algebraic constructions can be matched using the combinatorial approach. In this work, we provide a combinatorial construction of PCPs of length $${n\cdot\left(\log n\right)^{O(\log\log n)}}$$n·lognO(loglogn), coming very close to the state-of-the-art algebraic constructions (whose proof length is $${n\cdot\left(\log n\right)^{O(1)}}$$n·lognO(1)). To this end, we develop a few generic PCP techniques which may be of independent interest. It should be mentioned that our construction does use low-degree polynomials at one point. However, our use of polynomials is confined to the construction of error-correcting codes with a certain simple multiplication property, and it is conceivable that such codes could be constructed without the use of polynomials. In addition, we provide a variant of the main construction that does not use polynomials at all and has proof length $${n^{4} \cdot\left(\log n\right)^{O(\log\log n)}}$$n4·lognO(loglogn). This is already an improvement over the aforementioned combinatorial construction of Dinur.

This work studies decision problems related to graph properties from the perspective of nondeterministic distributed algorithms. For a yes-instance there must exist a proof that can be verified with a distributed algorithm: all nodes must accept a valid proof, and at least one node must reject an invalid proof. We focus on locally checkable proofs that can be verified with a constant-time distributed algorithm. For example, it is easy to prove that a graph is bipartite: the locally checkable proof gives a 2-coloring of the graph, which only takes 1 bit per node. However, it is more difficult to prove that a graph is not bipartite—it turns out that any locally checkable proof requires W(log n) bits per node. In this work we classify graph properties according to their local proof complexity, i. e., how many bits per node are needed in a locally checkable proof. We establish tight or near- tight results for classical graph properties such as the chromatic number. We show that the local proof complexities form a natural hierarchy of complexity classes: for many classical

Patterned self-assembly tile set synthesis (pats) aims at minimizing the number of distinct DNA tile types used to self-assemble a given rectangular color pattern. For an integer k, k-pats is the subproblem of pats that restricts input patterns to those with at most k colors. We give an efficient [InlineEquation not available: see fulltext.] verifier, and based on that, we establish a manually-checkable proof for the NP-hardness of 11-pats; the best previous manually-checkable proof is for 29-pats.

In this work we study interactive proofs for tractable languages. The (honest) prover should be efficient and run in polynomial time or, in other words, a “muggle”.1 The verifier should be super-efficient and run in nearly linear time. These proof systems can be used for delegating computation: a server can run a computation for a client and interactively prove the correctness of the result. The client can verify the result’s correctness in nearly linear time (instead of running the entire computation itself). Previously, related questions were considered in the holographic proof setting by Babai et al. [1991b] in the argument setting under computational assumptions by Kilian, and in the random oracle model by Micali [1994]. Our focus, however, is on the original interactive proof model where no assumptions are made on the computational power or adaptiveness of dishonest provers. Our main technical theorem gives a public coin interactive proof for any language computable by a log-space uniform boolean circuit with depth d and input length n . The verifier runs in time n · poly( d , log( n )) and space O (log( n )), the communication complexity is poly( d , log( n )), and the prover runs in time poly( n ). In particular, for languages computable by log-space uniform NC (circuits of polylog( n ) depth), the prover is efficient, the verifier runs in time n · polylog( n ) and space O (log( n )), and the communication complexity is polylog( n ). Using this theorem we make progress on several questions. --- We show how to construct 1-round computationally sound arguments with polylog communication for any log-space uniform NC computation. The verifier runs in quasi-linear time. This result uses a recent transformation of Kalai and Raz from public coin interactive proofs to 1-round arguments . The soundness of the argument system is based on the existence of a PIR scheme with polylog communication. --- We construct interactive proofs with public coin, log-space, poly-time verifiers for all of P are given. This settles an open question regarding the expressive power of proof systems with such verifiers. --- We construct zero-knowledge interactive proofs are given with communication complexity quasi-linear in the witness length for any NP language verifiable in NC , based on the existence of 1-way functions. --- We construct probabilistically checkable arguments (a model due to Kalai and Raz) of size polynomial in the witness length (rather than instance length) for any NP language verifiable in NC , under computational assumptions, are provided.

Proof development in proof assistants such as HOL, Coq, Mizar, etc. is an activity where authors usually produce proofs by typing out proof scripts or system tactics. Quite frequently, however, authors also have to read existing proof scripts, either to imitate smart proof pieces, or to refactor fragments of reasoning to make some theorem stronger, more easily applicable and so on. Therefore, it is important to develop techniques to improve legibility of proofs, since it directly affects productivity of script writers. To analyze the legibility of natural deduction proofs, we investigate proof graphs that represent the flow of information in given reasoning. Our analysis of the information flow leads to methods of improving proof readability based on Behaghel's First Law, which states that in legible text relevant pieces of information must occur close to each other. The presented method maximizes the number of close connections between premises and steps that use these steps as justification. In this paper we show that our optimization method is NP-hard.

In this article, we disprove a conjecture of Goemans and Linial; namely, that every negative type metric embeds into ℓ 1 with constant distortion. We show that for an arbitrarily small constant δ > 0, for all large enough n , there is an n -point negative type metric which requires distortion at least (log log n ) 1/6-δ to embed into ℓ 1 . Surprisingly, our construction is inspired by the Unique Games Conjecture (UGC), establishing a previously unsuspected connection between probabilistically checkable proof systems (PCPs) and the theory of metric embeddings. We first prove that the UGC implies a super-constant hardness result for the (nonuniform) S PARSEST C UT problem. Though this hardness result relies on the UGC, we demonstrate, nevertheless, that the corresponding PCP reduction can be used to construct an “integrality gap instance” for S PARSEST C UT . Towards this, we first construct an integrality gap instance for a natural SDP relaxation of U NIQUE G AMES . Then we “simulate” the PCP reduction and “translate” the integrality gap instance of U NIQUE G AMES to an integrality gap instance of S PARSEST C UT . This enables us to prove a (log log n ) 1/6-δ integrality gap for S PARSEST C UT , which is known to be equivalent to the metric embedding lower bound.

In order to compare the quality of proofs, it is necessary to measure artifacts of the proofs, and evaluate the measurements to determine differences between the proofs. This paper discounts the approach of ranking measurements of proof artifacts, and takes the position that different proofs are good proofs. The position is based on proofs in the TSTP solution library, which are generated by Automated Theorem Proving (ATP) systems applied to first-order logic problems in the TPTP problem library.

In this paper, we give a no-signaling linear probabilistically checkable proof (PCP) system for polynomial-time deterministic computation, i.e., a PCP system for \({\mathcal {P}}\) such that (1) the PCP oracle is a linear function and (2) the soundness holds against any (computational) no-signaling cheating prover, who is allowed to answer each query according to a distribution that depends on the entire query set in a certain way. To the best of our knowledge, our construction is the first PCP system that satisfies these two properties simultaneously.

This paper presents an interactive verifier for logic programs. These logic programs are constructed by a schema-based method. Each program is associated with proof schemes due to the program development method. The correctness proof of a program is guided by its associated proof schemes. The main components of the verifier are the prover which carries out the proof steps, the knowledge base (KB) which includes representations of all theories and transformation rules, the KB update which supports the update of KB and the graphical user interface (GUI). The emphasis in the design of this proof checker is on effective guidance of the proof based on the activated proof schemes and on performance by the verifier of tedious, trivial and time consuming tasks. The difficult proof decisions are taken by the user, then, the proof checker applies them. The design of the interface is based on providing the user the required support for the proof of a theorem and for the update of KB. This system is an effective and useful tool for the interactive verification of non-trivial logic programs.

We describe a method of forcing against weak theories of arithmetic and its applications in propositional proof complexity.

It is known that constant-depth Frege proofs of some tautologies require exponential size. No such lower bound result is known for more general proof systems. We consider tree-like sequent calculus proofs in which formulas can contain modular connectives and only the cut formulas are restricted to be of constant depth. Under a plausible hardness assumption concerning small-depth Boolean circuits, we prove exponential lower bounds for such proofs. We prove these lower bounds directly from the computational hardness assumption. We start with a lower bound for cut-free proofs and "lift" it so it applies to proofs with constant-depth cuts. By using the same approach, we obtain the following additional results. We provide a much simpler proof of a known unconditional lower bound in the case where modular connectives are not used. We establish a conditional exponential separation between the power of constant-depth proofs that use different modular connectives. We show that these tree-like proofs with constant-depth cuts cannot polynomially simulate similar dag-like proofs, even when the dag-like proofs are cut-free. We present a new proof of the non-finite axiomatizability of the theory of bounded arithmetic I Δ0(R). Finally, under a plausible hardness assumption concerning the polynomial-time hierarchy, we show that the hierarchy $${G_i^*}$$ of quantified propositional proof systems does not collapse.

International audience; We present a framework for processing formulas in automatic theorem provers, with generation of detailed proofs. The main components are a generic contextual recursion algorithm and an extensible set of inference rules. Clausification, skolemization, theory-specific simplifications, and expansion of 'let' expressions are instances of this framework. With suitable data structures, proof generation adds only a linear-time overhead, and proofs can be checked in linear time. We implemented the approach in the SMT solver veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced, which is important for independent checking and reconstruction in proof assistants. To validate the framework, we implemented proof reconstruction in Isabelle/HOL.

We study the maximization version of the fundamental graph coloring problem. Here the goal is to color the vertices of a k -colorable graph with k colors so that a maximum fraction of edges are properly colored (i.e. their endpoints receive different colors). A random k -coloring properly colors an expected fraction $1-\frac{1}{k}$ of edges. We prove that given a graph promised to be k -colorable, it is NP-hard to find a k -coloring that properly colors more than a fraction of edges. Previously, only a hardness factor of $1- O\bigl(\frac{1}{k^2}\bigr)$ was known. Our result pins down the correct asymptotic dependence of the approximation factor on k . Along the way, we prove that approximating the Maximum 3-colorable subgraph problem within a factor greater than $\frac{32}{33}$ is NP-hard. Using semidefinite programming, it is known that one can do better than a random coloring and properly color a fraction $1-\frac{1}{k} +\frac{2 \ln k}{k^2}$ of edges in polynomial time. We show that, assuming the 2-to-1 conjecture, it is hard to properly color (using k colors) more than a fraction $1-\frac{1}{k} + O\left(\frac{\ln k}{k^2}\right)$ of edges of a k -colorable graph.

The purpose behind zero-knowledge proofs are to deliver a mystification to the verifier, so that the verifier will not comprehend the information sent by the prover. Cryptography and complexity theory have gained a lot of importance because of zero-knowledge proofs. An enigmatic outset was dignified, that lead to the foundation zero-knowledge proof systems. Zero-knowledge proofs are generally used to verify a prover's theorem to a verifier, in such a way that the verifier will not be able to discover any supplementary evidence other than the proof given to him. In this paper, we have reviewed different zero-knowledge argument / proof techniques. We have also reviewed the proof system implications in the presence of malicious prover and malicious verifier. We have removed the outliers of the experiment by using Mahalanobis distance. Examples associated to zero-knowledge argument systems are also given.

International audience; Proof constructivization is the problem of automatically extracting constructive proofs out of classical proofs. This process is required when classical theorem provers are integrated in intuitionistic proof assistants. We use the ability of rewrite systems to represent partial functions to implement heuristics for proof constructivization in Dedukti, a logical framework based on rewriting in which proofs are first-class objects which can be the subject of computation. We benchmark these heuristics on the proofs output by the automated theorem prover Zenon on the TPTP library of problems.

The celebrated IP=PSPACE Theorem of Lund et-al. (J.ACM 1992) and Shamir (J.ACM 1992), allows an all-powerful but untrusted prover to convince a polynomial-time verifier of the validity of extremely complicated statements (as long as they can be evaluated using polynomial space). The interactive proof system designed for this purpose requires a polynomial number of communication rounds and an exponential-time (polynomial-space complete) prover. In this paper, we study the power of more efficient interactive proof systems. Our main result is that for every statement that can be evaluated in polynomial time and bounded-polynomial space there exists an interactive proof that satisfies the following strict efficiency requirements: (1) the honest prover runs in polynomial time, (2) the verifier is almost linear time (and under some conditions even sub linear), and (3) the interaction consists of only a constant number of communication rounds. Prior to this work, very little was known about the power of efficient, constant-round interactive proofs (rather than arguments). This result represents significant progress on the round complexity of interactive proofs (even if we ignore the running time of the honest prover), and on the expressive power of interactive proofs with polynomial-time honest prover (even if we ignore the round complexity). This result has several applications, and in particular it can be used for verifiable delegation of computation. Our construction leverages several new notions of interactive proofs, which may be of independent interest. One of these notions is that of unambiguous interactive proofs where the prover has a unique successful strategy. Another notion is that of probabilistically checkable interactive proofs (PCIPs) where the verifier only reads a few bits of the transcript in checking the proof (this could be viewed as an interactive extension of PCPs).

Cryptography and complexity theory have gained a lot of importance because of zero-knowledge proofs. The motive behind zero-knowledge proofs are to provide an obfuscation to the verifier, so that the verifier will not understand the information sent by the prover. Zero-knowledge proofs are normally used to verify a prover's theorem to a verifier, in such a way that the verifier will not be able to discover any supplementary evidence other than the proof given to him. An enigmatic conception was formalized, that lead to the formation zero-knowledge proof systems. In this paper, we have reviewed different zero-knowledge argument / proof techniques. We have also reviewed the proof system implications in the presence of malicious prover and malicious verifier. Examples related to zero-knowledge argument systems are also given.

This is a survey of work on proof complexity and proof search from a logico-algorithmic viewpoint, as motivated by the P versus NP problem. We discuss propositional proof complexity, Cook’s program, proof automatizability, proof search, algorithms for satisfiability, and the state of the art of our (in)ability to separate P and NP .

This paper investigates the depth of resolution proofs, that is to say, the length of the longest path in the proof from an input clause to the conclusion. An abstract characterization of the measure is given, as well as a discussion of its relation to other measures of space complexity for resolution proofs

The last two decades have seen enormous progress in the development of sublinear-time algorithms -- i.e., algorithms that examine/reveal properties of "data" in less time than it would take to read all of the data. A large, and important, subclass of such properties turn out to be "linear". In particular, these developments have contributed to the rich theory of probabilistically checkable proofs (PCPs) and locally testable codes (LTCs). In this survey, we focus on some of the general technical themes at work behind the many results in this area.

Starting with Kilian (STOC `92), several works have shown how to use probabilistically checkable proofs (PCPs) and cryptographic primitives such as collision-resistant hashing to construct very efficient argument systems (a.k.a. computationally sound proofs), for example with polylogarithmic communication complexity. Ishai et al. (CCC `07) raised the question of whether PCPs are inherent in efficient arguments, and to what extent. We give evidence that they are, by showing how to convert any argument system whose soundness is reducible to the security of some cryptographic primitive into a PCP system whose efficiency is related to that of the argument system and the reduction (under certain complexity assumptions).

This paper considers the existence of constant-round zero-knowledge proofs of knowledge for NP under standard assumptions. By introducing a new interactive proof model, we construct a 3-round zero-knowledge proof of knowledge system for the NP-relation under the assumption that factoring is intractable. Our construction not only shows the existence of constant-round zero-knowledge proofs of knowledge, but also gives a positive answer to the open problem of the existence of 3-round zero-knowledge proofs for NP.

Linear and semidefinite programming are highly successful approaches for obtaining good approximations for NP-hard optimization problems. For example, breakthrough approximation algorithms for Max Cut and Sparsest Cut use semidefinite programming. Perhaps the most prominent NP-hard problem whose exact approximation factor is still unresolved is Vertex Cover. Probabilistically checkable proof (PCP)-based techniques of Dinur and Safra [Ann. of Math./ (2), 162 (2005), pp. 439-486] show that it is not possible to achieve a factor better than 1.36; on the other hand no known algorithm does better than the factor of 2 achieved by the simple greedy algorithm. There is a widespread belief that semidefinite programming (SDP) techniques are the most promising methods available for improving upon this factor of 2. Following a line of study initiated by Arora et al. [Theory Comput., 2 (2006), pp. 19-51], our aim is to show that a large family of linear programming (LP)- and SDP-based algorithms fail to produce an approximation for Vertex Cover better than 2. Lovasz and Schrijver [SIAM J. Optim., 1 (1991), pp. 166-190] introduced the systems $LS$ and $LS_+$ for systematically tightening LP and SDP relaxations, respectively, over many rounds. These systems naturally capture large classes of LP and SDP relaxations; indeed, $LS_+$ captures the celebrated SDP-based algorithms for Max Cut and Sparsest Cut mentioned above. We rule out polynomial-time SDP-based $2-\Omega(1)$ approximations for Vertex Cover using $LS_+$. In particular, for every $\epsilon>0$ we prove an integrality gap of $2-\epsilon$ for Vertex Cover SDPs obtained by tightening the standard LP relaxation with $\Omega(\sqrt{\log n/\log\log n})$ rounds of $LS_+$. While tight integrality gaps were known for Vertex Cover in the weaker $LS$ system [G. Schoenebeck, L. Trevisan, and M. Tulsiani, Proceedings of the 39th Annual ACM Symposium on Theory of Computing, ACM Press, New York, 2007, pp. 302-310], previous results did not rule out a $2-\Omega(1)$ approximation after even two rounds of $LS_+$.

We show a construction of a PCP with both sub-constant error and almost-linear size. Specifically, for some constant 0

We initiate the study of the trade-off between the length of a probabilistically checkable proof of proximity (PCPP) and the maximal soundness that can be guaranteed by a 3-query verifier with oracle access to the proof. Our main observation is that a verifier limited to querying a short proof cannot obtain the same soundness as that obtained by a verifier querying a long proof. Moreover, we quantify the soundness deficiency as a function of the proof-length and show that any verifier obtaining “best possible” soundness must query an exponentially long proof. In terms of techniques, we focus on the special class of inspective verifiers that read at most 2 proof-bits per invocation. For such verifiers, we prove exponential length-soundness trade-offs that are later on used to imply our main results for the case of general (i.e., not necessarily inspective) verifiers. To prove the exponential trade-off for inspective verifiers, we show a connection between PCPP proof length and property-testing query complexity that may be of independent interest. The connection is that any linear property that can be verified with proofs of length ℓ by linear inspective verifiers must be testable with query complexity ≈ logℓ.