Bayesian Inference by Symbolic Model Checking
This paper applies probabilistic model checking techniques for discrete Markov chains to inference in Bayesian networks. We present a simple translation from Bayesian networks into tree-like Markov chains such that inference can be reduced to computing reachability probabilities. Using a prototypical implementation on top of the Storm model checker, we show that symbolic data structures such as multi-terminal BDDs (MTBDDs) are very effective to perform inference on large Bayesian network benchmarks. We compare our result to inference using probabilistic sentential decision diagrams and vtrees, a scalable symbolic technique in AI inference tools.
Code (0)
등록된 구현이 없습니다.
Tasks
Bayesian InferencemodelTranslationSimilar Papers 제목 키워드 기반
Position: Logical Soundness is not a Reliable Criterion for Neurosymbolic Fact-Checking with LLMs
As large language models (LLMs) are increasing integrated into fact-checking pipelines, formal logic is often proposed as a rigorous means by which to mitigate bias, errors and hallucinations in these models' outputs. Fo…
Formal LogicDeep Variational Inference Symbolic Regression
Symbolic regression discovers explicit, interpretable equations without assuming a functional form in advance. A Bayesian approach strengthens this through probability distributions over candidate expressions, thus quant…
Simulation-based inference of Bayesian hierarchical models while checking for model misspecification
This paper presents recent methodological advances to perform simulation-based inference (SBI) of a general class of Bayesian hierarchical models (BHMs), while checking for model misspecification. Our approach is based o…
Neural Model Checking
We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Model checking answers the question of whether every execution of a given system satisfies a de…
modelScalable Stochastic Parametric Verification with Stochastic Variational Smoothed Model Checking
Parametric verification of linear temporal properties for stochastic models can be expressed as computing the satisfaction probability of a certain property as a function of the parameters of the model. Smoothed model ch…
Bayesian InferenceComputational EfficiencyGaussian ProcessesGPU+1