Probabilistic model checking and parameter tuning for Bayesian networks

Salmani Barzoki, Bahare; de Raedt, Luc; Katoen, Joost-Pieter

doi:44067

Probabilistic model checking and parameter tuning for Bayesian networks

Salmani Barzoki, Bahare^RWTH*

2024 & 2025

Verantwortlichkeitsangabevorgelegt von Bahare Salmani Barzoki, M. Sc.

ImpressumAachen : RWTH Aachen University 2024

Umfang1 Online-Ressource : Illustrationen

Dissertation, RWTH Aachen University, 2024

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2025

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; de Raedt, Luc (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2024-10-11

Online
DOI: 10.18154/RWTH-2025-00411
URL: http://publications.rwth-aachen.de/record/1002228/files/1002228.pdf

Einrichtungen

Projekte

FRAPPANT - Formal Reasoning About Probabilistic Programs: Breaking New Ground for Automation (787914) (787914)

Inhaltliche Beschreibung (Schlagwörter)
Bayesian networks (frei) ; Markov models (frei) ; formal verification (frei) ; parameter tuning (frei) ; probabilistic graphical models (frei) ; probabilistic model checking (frei) ; sensitivity analysis (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Wahrscheinlichkeitsbasierte Argumentation ist zentral für den Umgang mit Unsicherheiten und das Treffen von Entscheidungen auf der Grundlage unvollständiger Beobachtungen. Bayessche Netzwerke (BNs) sind beliebte probabilistische grafische Modelle in der probabilistischen Entscheidungsfindung und Künstlichen Intelligenz (KI) und finden breite Anwendung in Bereichen wie maschinellem Lernen, Medizin, genregulatorischen Netzwerken und Finanzen. Die zentrale Aufgabe in Bayesschen Netzwerken ist die probabilistische Inferenz, die auf die Berechnung bedingter Wahrscheinlichkeiten hinausläuft. Während es eine Reihe effizienter Algorithmen für die Inferenz in BNs mit bestimmten Topologien, wie solchen mit begrenzter Baumweite, gibt, bleibt probabilistische Inferenz im Allgemeinen rechnerisch schwierig; die theoretische Komplexität ist PP-complete. Probabilistisches Model Checking (PMC) ist ein Bereich der formalen Verifikation, der sich auf die Analyse stochastischer Systeme in Bezug auf eine Menge formal definierter Eigenschaften konzentriert. Die stochastischen Systeme werden typischerweise als Markov-Modelle modelliert, und die Eigenschaften als probabilistische Erweiterungen von LTL oder CTL. Die Eigenschaften werden meist auf eine zentrale Aufgabe reduziert, nämlich die Berechnung von Erreichbarkeitswahrscheinlichkeiten. Neuere Fortschritte in diesem Bereich befassen sich mit parametrischen Erweiterungen von Markov-Modellen, bei denen ein Teil der Wahrscheinlichkeiten im Modell unbekannt ist. In dieser Dissertation stellen wir einen neuartigen Ansatz vor, der auf probabilistischem Model Checking basiert, um Inferenz und Parametertuning in Bayesschen Netzwerken durchzuführen. Die Dissertation gliedert sich in zwei Hauptszenarien: nicht-parametrisch und parametrisch. Im nicht-parametrischen Szenario konzentrieren wir uns auf klassische Bayessche Netzwerke, bei denen das Modell vollständig spezifiziert ist. Wir behandeln die bedingte Inferenz in klassischen BNs: wir präsentieren Abbildungen von Bayesschen Netzwerken in diskrete Markov-Ketten und reduzieren mathematisch die Durchführung der bedingten Inferenz in einem BN auf die Berechnung von Erreichbarkeitswahrscheinlichkeiten in Markov-Ketten. Dies ermöglicht den Einsatz modernster Algorithmen aus PMC sowie Optimierungstechniken wie Bisimulationsminimierung für die Bayessche Inferenz. Wir nutzen explizite und symbolische Methoden und evaluieren unser Framework empirisch im Vergleich zur modernen gewichteten Modellzählung. Im parametrischen Szenario betrachten wir parametrische Bayessche Netzwerke (pBNs), bei denen ein Teil der lokalen Wahrscheinlichkeitsverteilungen als Polynome über Variablen und nicht als konkrete Wahrscheinlichkeiten modelliert ist. Wir behandeln spezifisch Sensitivitätsanalysen und Parameter-Tuning-Probleme (Verhältnis-/Differenzprobleme) aus der BN-Literatur sowie das Problem der Parameterraumaufteilung aus der PMC-Literatur. Wir schlagen einen Algorithmus für das Problem des minimalen Distanz-Parameter-Tunings vor, dessen Ziel es ist, eine Instanziierung der unbekannten Parameter zu finden, die die interessierende Einschränkung erfüllt und gleichzeitig minimal von der ursprünglichen Instanziierung im gegebenen Referenzmodell abweicht. Unsere detaillierten experimentellen Bewertungen zeigen, dass unsere Parameter-Synthese-Techniken Parameter-Synthese für Bayessche Netzwerke (mit Hunderten unbekannter Parameter) behandeln können, was über die Fähigkeiten bestehender Techniken für Bayessche Netzwerke mit unbekannten Wahrscheinlichkeiten hinausgeht. Wir überwinden die strengen Einschränkungen in der Literatur bezüglich der Anzahl unbekannter Parameter, der globalen Abhängigkeiten zwischen den Parametern und der Form der erhaltenen Lösungen.

Probabilistic reasoning is a key to handling uncertainties and making decisions based on partial observations. Bayesian networks (BNs) are popular probabilistic graphical models in probabilistic decision-making and AI and have a wide range of applications, including machine learning, medicine, gene regulatory networks, and finance. The pivotal task in Bayesian networks is probabilistic inference that amounts to computing conditional probabilities. While there is a range of efficient algorithms for inference in BNs with certain topologies, such as those with bounded tree-width, probabilistic inference remains computationally hard in general; the theoretical complexity is PP-complete. Probabilistic model checking (PMC) is a field in formal verification that focuses on analyzing stochastic systems with respect to a set of formally defined properties. The stochastic systems are typically modelled as Markov models, and the properties as probabilistic extensions of LTL or CTL. The properties are mostly reduced to a pivotal task, computing reachability probabilities. Recent advancements in the field consider parametric extensions of Markov models, where a subset of the probabilities in the model is unknown. In this dissertation, we introduce a novel approach based on probabilistic model checking for inference and parameter tuning in Bayesian networks. The dissertation is categorized into two main settings: non-parameteric and parameteric. In the non-parameteric setting, we focus on classical Bayesian networks, where the model is fully specified. We address conditional inference on classical BNs: we present mappings from Bayesian networks into discrete-time Markov chains and mathematically reduce performing conditional inference in the BN to computing reachability probabilities in MCs. This enables applying state-of-the-art algorithms from PMC and optimization techniques such as bisimulation minimization for Bayesian inference. We exploit explicit and symbolic methods and empirically evaluate our framework against the state-of-the-art weighted model counting. In the parametric setting, we consider parametric Bayesian networks (pBNs), where a subset of local probability distributions are based polynomials over variables rather than concrete probabilities. We specifically address sensitivity analysis and ratio/difference parameter tuning problems from the BN literature, and the parameter space partitioning problem from PMC literature. We propose an algorithm for the problem of minimal distance parameter tuning, where the objective is to find an instantiation for the unknown parameters that satisfy the constraint of interest while minimally deviating from the original instantiation in the given reference model. Our detailed experimental evaluations indicate that our parameter synthesis techniques can treat parameter synthesis for Bayesian networks (with hundreds of unknown parameters), which goes beyond the capabilities of existing techniques for Bayesian networks with unknown probabilities. We lift the severe restrictions in the literature on the number of unknown parameters, the global dependencies between the parameters, and the form of obtained solutions.

OpenAccess:
PDF
(additional files)