-
Vibhav Gogate and Pedro Domingos.
Probabilistic Theorem Proving.
arXiv:1202.3724 [cs],
February 2012.
Keyword(s): probability.
Abstract: |
Many representation schemes combining first-order logic and probability have been proposed in recent years. Progress in unifying logical and probabilistic inference has been slower. Existing methods are mainly variants of lifted variable elimination and belief propagation, neither of which take logical structure into account. We propose the first method that has the full power of both graphical model inference and first-order theorem proving (in finite domains with Herbrand interpretations). We first define probabilistic theorem proving, their generalization, as the problem of computing the probability of a logical formula given the probabilities or weights of a set of formulas. We then show how this can be reduced to the problem of lifted weighted model counting, and develop an efficient algorithm for the latter. We prove the correctness of this algorithm, investigate its properties, and show how it generalizes previous approaches. Experiments show that it greatly outperforms lifted variable elimination when logical structure is present. Finally, we propose an algorithm for approximate probabilistic theorem proving, and show that it can greatly outperform lifted belief propagation. |
@article{gogateProbabilisticTheoremProving2012,
title = {Probabilistic {{Theorem Proving}}},
author = {Gogate, Vibhav and Domingos, Pedro},
year = {2012},
month = feb,
abstract = {Many representation schemes combining first-order logic and probability have been proposed in recent years. Progress in unifying logical and probabilistic inference has been slower. Existing methods are mainly variants of lifted variable elimination and belief propagation, neither of which take logical structure into account. We propose the first method that has the full power of both graphical model inference and first-order theorem proving (in finite domains with Herbrand interpretations). We first define probabilistic theorem proving, their generalization, as the problem of computing the probability of a logical formula given the probabilities or weights of a set of formulas. We then show how this can be reduced to the problem of lifted weighted model counting, and develop an efficient algorithm for the latter. We prove the correctness of this algorithm, investigate its properties, and show how it generalizes previous approaches. Experiments show that it greatly outperforms lifted variable elimination when logical structure is present. Finally, we propose an algorithm for approximate probabilistic theorem proving, and show that it can greatly outperform lifted belief propagation.},
archivePrefix = {arXiv},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4166-Gogate_Domingos (2012) - Probabilistic Theorem Proving.pdf},
journal = {arXiv:1202.3724 [cs]},
keywords = {probability},
}
-
Ugo Dal Lago and Margherita Zorzi.
Probabilistic Operational Semantics for the Lambda Calculus.
RAIRO - Theoretical Informatics and Applications,
46(3):413-450,
July 2012.
ISSN: 0988-3754, 1290-385X.
Keyword(s): calculus,
probability.
Abstract: |
Probabilistic operational semantics for a nondeterministic extension of pure {$\lambda$}-calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics, inductively and coinductively defined, are given. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by-value and in call-by-name. Plotkin's CPS translation is extended to accommodate the choice operator and shown correct with respect to the operational semantics. Finally, the expressive power of the obtained system is studied: the calculus is shown to be sound and complete with respect to computable probability distributions. |
@article{lagoProbabilisticOperationalSemantics2012,
title = {Probabilistic Operational Semantics for the Lambda Calculus},
author = {Lago, Ugo Dal and Zorzi, Margherita},
year = {2012},
month = jul,
volume = {46},
pages = {413--450},
issn = {0988-3754, 1290-385X},
doi = {10.1051/ita/2012012},
abstract = {Probabilistic operational semantics for a nondeterministic extension of pure {$\lambda$}-calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics, inductively and coinductively defined, are given. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by-value and in call-by-name. Plotkin's CPS translation is extended to accommodate the choice operator and shown correct with respect to the operational semantics. Finally, the expressive power of the obtained system is studied: the calculus is shown to be sound and complete with respect to computable probability distributions.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4406-Lago_Zorzi (2012) - Probabilistic operational semantics for the lambda calculus.pdf},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {calculus,probability},
number = {3}
}
-
Diogo Araújo Carvalho Vilaça Moreira.
Finite Probability Distributions in Coq.
April 2012.
Keyword(s): Coq,
probability.
Abstract: |
When building safety-critical systems, guaranteeing properties like correctness and security are one of the most important goals to achieve. Thus, from a scientific point of view, one of the hardest problems in cryptography is to build systems whose security properties can be formally demonstrated. In the last few years we have assisted an exponential growth in the use of tools to formalize security proofs of primitives and cryptographic protocols, clearly showing the strong connection between cryptography and formal methods. This necessity comes from the great complexity and sometimes careless presentation of many security proofs, which often contain holes or rely on hidden assumptions that may reveal unknown weaknesses. In this context, interactive theorem provers appear as the perfect tool to aid in the formal certification of programs due to their capability of producing proofs without glitches and providing additional evidence that the proof process is correct. Hence, it is the purpose of this thesis to document the development of a framework for reasoning over information theoretic concepts, which are particularly useful to derive results on the security properties of cryptographic systems. For this it is first necessary to understand, and formalize, the underlying probability theoretic notions. The framework is implemented on top of the fintype and finfun modules of SSREFLECT, which is a small scale reflection extension for the COQ proof assistant, in order to take advantage of the formalization of big operators and finite sets that are available. |
@article{moreiraFiniteProbabilityDistributions2012,
title = {Finite Probability Distributions in {{Coq}}},
author = {Moreira, Diogo Ara{\'u}jo Carvalho Vila{\c c}a},
year = {2012},
month = apr,
abstract = {When building safety-critical systems, guaranteeing properties like correctness and security are one of the most important goals to achieve. Thus, from a scientific point of view, one of the hardest problems in cryptography is to build systems whose security properties can be formally demonstrated. In the last few years we have assisted an exponential growth in the use of tools to formalize security proofs of primitives and cryptographic protocols, clearly showing the strong connection between cryptography and formal methods. This necessity comes from the great complexity and sometimes careless presentation of many security proofs, which often contain holes or rely on hidden assumptions that may reveal unknown weaknesses. In this context, interactive theorem provers appear as the perfect tool to aid in the formal certification of programs due to their capability of producing proofs without glitches and providing additional evidence that the proof process is correct. Hence, it is the purpose of this thesis to document the development of a framework for reasoning over information theoretic concepts, which are particularly useful to derive results on the security properties of cryptographic systems. For this it is first necessary to understand, and formalize, the underlying probability theoretic notions. The framework is implemented on top of the fintype and finfun modules of SSREFLECT, which is a small scale reflection extension for the COQ proof assistant, in order to take advantage of the formalization of big operators and finite sets that are available.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4370-Moreira (2012) - Finite probability distributions in Coq.pdf},
keywords = {Coq,probability},
}
-
Paula G. Severi and Fer-Jan J. de Vries.
Pure Type Systems with Corecursion on Streams: From Finite to Infinitary Normalisation.
ACM SIGPLAN Notices,
47(9):141-152,
September 2012.
ISSN: 0362-1340.
Keyword(s): calculus,
coinduction.
Abstract: |
In this paper, we use types for ensuring that programs involving streams are well-behaved. We extend pure type systems with a type constructor for streams, a modal operator next and a fixed point operator for expressing corecursion. This extension is called Pure Type Systems with Corecursion (CoPTS). The typed lambda calculus for reactive programs defined by Krishnaswami and Benton can be obtained as a CoPTS. CoPTSs allow us to study a wide range of typed lambda calculi extended with corecursion using only one framework. In particular, we study this extension for the calculus of constructions which is the underlying formal language of Coq. We use the machinery of infinitary rewriting and formalise the idea of well-behaved programs using the concept of infinitary normalisation. The set of finite and infinite terms is defined as a metric completion. We establish a precise connection between the modal operator ( extbullet{} A) and the metric at a syntactic level by relating a variable of type ( extbullet{} A) with the depth of all its occurrences in a term. This syntactic connection between the modal operator and the depth is the key to the proofs of infinitary weak and strong normalisation. |
@article{severiPureTypeSystems2012,
title = {Pure Type Systems with Corecursion on Streams: From Finite to Infinitary Normalisation},
author = {Severi, Paula G. and {de Vries}, Fer-Jan J.},
year = {2012},
month = sep,
volume = {47},
pages = {141--152},
issn = {0362-1340},
doi = {10.1145/2398856.2364550},
abstract = {In this paper, we use types for ensuring that programs involving streams are well-behaved. We extend pure type systems with a type constructor for streams, a modal operator next and a fixed point operator for expressing corecursion. This extension is called Pure Type Systems with Corecursion (CoPTS). The typed lambda calculus for reactive programs defined by Krishnaswami and Benton can be obtained as a CoPTS. CoPTSs allow us to study a wide range of typed lambda calculi extended with corecursion using only one framework. In particular, we study this extension for the calculus of constructions which is the underlying formal language of Coq. We use the machinery of infinitary rewriting and formalise the idea of well-behaved programs using the concept of infinitary normalisation. The set of finite and infinite terms is defined as a metric completion. We establish a precise connection between the modal operator ( extbullet{} A) and the metric at a syntactic level by relating a variable of type ( extbullet{} A) with the depth of all its occurrences in a term. This syntactic connection between the modal operator and the depth is the key to the proofs of infinitary weak and strong normalisation.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4385-Severi_de Vries (2012) - Pure type systems with corecursion on streams.pdf},
journal = {ACM SIGPLAN Notices},
keywords = {calculus,coinduction},
number = {9}
}