# Difference between revisions of "Probabilistic Soundness"

Line 27: | Line 27: | ||

=== 2015b === | === 2015b === | ||

− | * ([[2015_ProbabilisticTerminationSoundne|Ferrer Fioriti & Hermanns, 2015]]) ⇒ [[ | + | * ([[2015_ProbabilisticTerminationSoundne|Ferrer Fioriti & Hermanns, 2015]]) ⇒ [[::Luis María Ferrer Fioriti]], and [[::Holger Hermanns]]. ([[::2015]]). “[https://www.ae-info.org/attach/User/Hermanns_Holger/Publications/FH-POPL15.pdf 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 [http://dx.doi.org/10.1145/2676726.2677001 doi:10.1145/2676726.2677001] |

− | ** QUOTE: | + | ** QUOTE: <B>Theorem 5.6 (Soundness).</B> Let <math>P</math> be a [[probabilistic program]] with [[semantics]]] <math>{(L, X) φ n}</math>, and a [[ranking]] [[supermartingale]] <math>{Y_n}</math> such that <math>Y_n = 0</math> implies <math>T φ ≤ n</math> for all valid schedulers φ. Then, P almost sure terminates, and T ∗ is integrable. |

=== 2009 === | === 2009 === | ||

Line 35: | Line 35: | ||

=== 1975 === | === 1975 === | ||

− | * (Adams, 1975) ⇒ E. W. Adams (1975). [http://fitelson.org/piksi/adams_logic_of_conditionals.pdf "The logic of conditionals: An application of probability to deductive logic"] (No. 86). Springer Science & Business Media. | + | * ([[Adams, 1975]]) ⇒ E. W. Adams (1975). [http://fitelson.org/piksi/adams_logic_of_conditionals.pdf "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 <i>prima facie</i> case for the appropriateness of assessing the [[soundness]] or [[rationality]] of [[deductive inference]]s in terms of a new requirement or [[criterion of rationality]] beyond the usual [[truth-conditional criterion]]: that it should be impossible for the [[premise]]s 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 <i>[[probabilistic soundness criterion]]</i>: it should be impossible for the [[premise]]s 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 inference]]s satisfy something like this requirement if they are to be regarded as 'rational'. | ** QUOTE: Our objective as this section is to establish a <i>prima facie</i> case for the appropriateness of assessing the [[soundness]] or [[rationality]] of [[deductive inference]]s in terms of a new requirement or [[criterion of rationality]] beyond the usual [[truth-conditional criterion]]: that it should be impossible for the [[premise]]s 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 <i>[[probabilistic soundness criterion]]</i>: it should be impossible for the [[premise]]s 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 inference]]s satisfy something like this requirement if they are to be regarded as 'rational'. | ||

− | + | ||

---- | ---- | ||

__NOTOC__ | __NOTOC__ | ||

[[Category:Concept]] | [[Category:Concept]] |

## Revision as of 04:51, 14 June 2019

A Probabilistic Soundness is a Rationality Criterion that ...

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

## References

### 2019

- (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*).

- Given a decision problem

### 2015a

- (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.

- QUOTE: Informally, the soundness property is stated as follows.

### 2015b

- (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]P[/math] be a probabilistic program with semantics] [math]{(L, X) φ n}[/math], and a ranking supermartingale [math]{Y_n}[/math] such that [math]Y_n = 0[/math] implies [math]T φ ≤ n[/math] for all valid schedulers φ. Then, P almost sure terminates, and T ∗ is integrable.

- QUOTE:

### 2009

- (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)...

- QUOTE:

### 1975

- (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'.

- QUOTE: Our objective as this section is to establish a

Facts about "Probabilistic Soundness"

Author | Gregor Snelting +, Dennis Giffhorn +, Jurgen Graf +, Christian Hammer +, Martin Hecker +, Martin Mohr +, Daniel Wasserrab +, Michael Backes +, Dennis Hofheinz + and Dominique Unruh + |

year | 2015 + and 2009 + |