Probabilistic proof systems—Part I

Author(s):  
Salil Vadhan
Philosophies ◽  
2021 ◽  
Vol 6 (4) ◽  
pp. 83
Author(s):  
Kristen Carlson

Methods are currently lacking to prove artificial general intelligence (AGI) safety. An AGI ‘hard takeoff’ is possible, in which first generation AGI1 rapidly triggers a succession of more powerful AGIn that differ dramatically in their computational capabilities (AGIn << AGIn+1). No proof exists that AGI will benefit humans or of a sound value-alignment method. Numerous paths toward human extinction or subjugation have been identified. We suggest that probabilistic proof methods are the fundamental paradigm for proving safety and value-alignment between disparately powerful autonomous agents. Interactive proof systems (IPS) describe mathematical communication protocols wherein a Verifier queries a computationally more powerful Prover and reduces the probability of the Prover deceiving the Verifier to any specified low probability (e.g., 2−100). IPS procedures can test AGI behavior control systems that incorporate hard-coded ethics or value-learning methods. Mapping the axioms and transformation rules of a behavior control system to a finite set of prime numbers allows validation of ‘safe’ behavior via IPS number-theoretic methods. Many other representations are needed for proving various AGI properties. Multi-prover IPS, program-checking IPS, and probabilistically checkable proofs further extend the paradigm. In toto, IPS provides a way to reduce AGIn ↔ AGIn+1 interaction hazards to an acceptably low level.


1994 ◽  
Vol 1 (28) ◽  
Author(s):  
Oded Goldreich

Various types of <em>probabilistic</em> proof systems have played a central role in the development of computer science in the last decade. In this exposition, we concentrate on three such proof systems -- <em>interactive proofs</em>, <em>zero-knowledge proofs</em>, and <em>probabilistic checkable proofs</em> -- stressing the essential role of randomness in each of them.<br /> <br />This exposition is an expanded version of a survey written for the proceedings of the International Congress of Mathematicians (<em>ICM94</em>) held in Zurich in 1994. It is hope that this exposition may be accessible to a broad audience of computer scientists and mathematians.


2020 ◽  
Vol 34 (06) ◽  
pp. 10194-10201
Author(s):  
Negin Karimi ◽  
Petteri Kaski ◽  
Mikko Koivisto

We present a novel framework for parallel exact inference in graphical models. Our framework supports error-correction during inference and enables fast verification that the result of inference is correct, with probabilistic soundness. The computational complexity of inference essentially matches the cost of w-cutset conditioning, a known generalization of Pearl's classical loop-cutset conditioning for inference. Verifying the result for correctness can be done with as little as essentially the square root of the cost of inference. Our main technical contribution amounts to designing a low-degree polynomial extension of the cutset approach, and then reducing to a univariate polynomial employing techniques recently developed for noninteractive probabilistic proof systems.


Author(s):  
Kristen Carlson

Methods are currently lacking to prove artificial general intelligence (AGI) safety. An AGI &lsquo;hard takeoff&rsquo; is possible, in which first generation AGI1 rapidly triggers a succession of more powerful AGIn that differ dramatically in their computational capabilities (AGIn≪AGIn+1). No proof exists that AGI will benefit humans or of a sound value-alignment method. Numerous paths toward human extinction or subjugation have been identified. We suggest that probabilistic proof methods are the fundamental paradigm for proving safety and value-alignment between disparately powerful autonomous agents. Interactive proof systems (IPS) describe mathematical communication protocols wherein a Verifier queries a computationally more powerful Prover and reduces the probability of the Prover deceiving the Verifier to any specified low probability (e.g., 2-100). IPS procedures can test AGI behavior control systems that incorporate hard-coded ethics or value-learning methods. Mapping the axioms and transformation rules of a behavior control system to a finite set of prime numbers allows validation of &lsquo;safe&rsquo; behavior via IPS number-theoretic methods. Many other representations are needed for proving various AGI properties. Multi-prover IPS, program-checking IPS, and probabilistically checkable proofs further extend the paradigm. In toto, IPS provides a way to reduce AGIn&harr;AGIn+1 interaction hazards to an acceptably low level.


Sign in / Sign up

Export Citation Format

Share Document