Probabilistic Soundness

AKA: Probabilistic Soundness Criterion.
Example(s):
Counter-Example(s):
See: Probabilistically Checkable Proof System, Probabilistic Interference, Bayesian Network.

References

(Wikipedia, 2019) ⇒ https://en.wikipedia.org/wiki/Probabilistically_checkable_proof#Definition Retrieved:2019-6-14.
- Given a decision problem L(or a language L with its alphabet set Σ), a probabilistically checkable proof system for L with completeness c(n) and soundness s(n), where 0 ≤ s(n) ≤ c(n) ≤ 1, consists of a prover and a verifier. Given a claimed solution x with length n, which might be false, the prover produces a proof π which states x solves L (x ∈ L, the proof is a string ∈ Σ^*). And the verifier is a randomized oracle Turing Machine V (the verifier) that checks the proof π for the statement that x solves L(or x ∈ L) and decides whether to accept the statement. The system has the following properties:
  - Completeness: For any x ∈ L, given the proof π produced by the prover of the system, the verifier accepts the statement with probability at least c(n),
  - Soundness: For any x ∉ L, then for any proof π, the verifier mistakenly accepts the statement with probability at most s(n).

(Snelting et al., 2015) ⇒ Gregor Snelting, Dennis Giffhorn, Jurgen Graf, Christian Hammer, Martin Hecker, Martin Mohr, and Daniel Wasserrab. (2015). “Checking Probabilistic Noninterference Using JOANA.” In: it-Information Technology Journal, 57.
- QUOTE: Informally, the soundness property is stated as follows.
  Theorem. If the RLSOD criterion is fulfilled for a program, it is probabilistically noninterferent.
  Soundness is based on a simpler theorem for sequential programs without threads:
  Theorem. If no high data source is in the (contextsensitive) backward slice of a low data sink, a program is (sequentially) noninterferent.

(Ferrer Fioriti & Hermanns, 2015) ⇒ Luis María Ferrer Fioriti, and Holger Hermanns. (2015). “Probabilistic Termination: Soundness, Completeness, and Compositionality.” In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ISBN:978-1-4503-3300-9 doi:10.1145/2676726.2677001
- QUOTE: Theorem 5.6 (Soundness). Let [math]\displaystyle{ P }[/math] be a probabilistic program with semantics [math]\displaystyle{ {(L, X) φ n} }[/math], and a ranking supermartingale [math]\displaystyle{ {Y_n} }[/math] such that [math]\displaystyle{ Y_n = 0 }[/math] implies [math]\displaystyle{ T φ ≤ n }[/math] for all valid schedulers φ. Then, P almost sure terminates, and T ∗ is integrable.

(Backes et al., 2009) ⇒ Michael Backes, Dennis Hofheinz, and Dominique Unruh. (2009). “CoSP: A General Framework for Computational Soundness Proofs.” In: Proceedings of the 16th ACM conference on Computer and communications security. ISBN:978-1-60558-894-0 doi:10.1145/1653662.1653672
- QUOTE: Definition 11 (Computational soundness) A computational implementation A of a symbolic model M = (C, N, T, D, ⊢) is computationally sound for a class P of CoSP protocols iff for every trace property P and for every efficient probabilistic CoSP protocol Πp, we have that (Πp, A) computationally satisfies P whenever the corresponding CoSP protocol Πs of Πp symbolically satisfies P and Πs ∈ P.
  A computational soundness result with respect to a non-trivial message type T (a message type that does not contain all terms) may be useful when embedding a calculus in our model that supports typed messages (e.g., most modern programming languages)...

(Adams, 1975) ⇒ E. W. Adams (1975). "The logic of conditionals: An application of probability to deductive logic" (No. 86). Springer Science & Business Media.
- QUOTE: Our objective as this section is to establish a prima facie case for the appropriateness of assessing the soundness or rationality of deductive inferences in terms of a new requirement or criterion of rationality beyond the usual truth-conditional criterion: that it should be impossible for the premises of an inference to be true while its conclusion is false. The proposed supplementary criterion results when the words 'probable` and 'improbable' are substituted for 'true' and 'false', respectively, in the truth-conditional criterion, yielding the probabilistic soundness criterion: it should be impossible for the premises of an inference to be probable while its conclusion is improbable. This formulation is vague and we shall want to clarify it later, but our present concern is with the legitimacy of demanding that deductive inferences satisfy something like this requirement if they are to be regarded as 'rational'.