Open this publication in new window or tab >>2023 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]
Probabilistic programming languages (PPLs) allow users to express statistical inference problems that the PPL implementation then, ideally, solves automatically. In particular, PPL users can focus on encoding their inference problems, and need not concern themselves with the intricacies of inference. Universal PPLs are PPLs with great expressive power, meaning that users can express essentially any inference problem. Consequently, universal PPL implementations often use general-purpose inference algorithms that are compatible with all such inference problems. A problem, however, is that general-purpose inference algorithms can often not efficiently solve complex inference problems. Furthermore, for certain inference algorithms, there are no formal correctness proofs in the context of universal PPLs.
This dissertation considers research problems related to Monte Carlo inference algorithms—sampling-based general-purpose inference algorithms that universal PPL implementations often apply. The first research problem concerns the correctness of sequential Monte Carlo (SMC) inference algorithms. A contribution in the dissertation is a proof of correctness for SMC algorithms in the context of universal PPLs. The second research problem concerns execution time improvements when suspending executions—a requirement in many Monte Carlo inference algorithms. The dissertation addresses the problem through two separate approaches. The first approach is a compilation technique targeting high-performance platforms. The second approach is a static suspension analysis guiding a selective continuation-passing style (CPS) transformation, reducing overhead compared to a full CPS transformation. The third research problem concerns inference improvements through alignment—a useful and often overlooked property in PPLs. The dissertation contributions are a formal definition of alignment, a static analysis technique that automatically aligns programs, and aligned versions of SMC and Markov chain Monte Carlo (MCMC) inference algorithms. The final research problem is more practical, and concerns the effective implementation of PPLs. Specifically, the contribution is the Miking CorePPL universal PPL and its compiler. Overall, the contributions in the dissertation significantly improve the efficiency of Monte Carlo algorithms as applied in universal PPLs.
Abstract [sv]
Probabilistiska programmeringsspråk (PPL:er) tillåter användare att uttrycka statistiska inferensproblem som PPL-implementationen sedan, i bästa fall, löser automatiskt. I synnerhet kan PPL-användare fokusera på att uttrycka sina inferensproblem utan att behöva bekymra sig om svårigheter tillhörande inferensen. Universella PPL:er är PPL:er med stor uttrycksfullhet, vilket innebär att användare kan uttrycka i princip vilket inferensproblem som helst. Följaktligen använder universella PPL-implementationer ofta inferensalgoritmer för allmänna ändamål som är kompatibla med alla sådana inferensproblem. Ett problem är dock att inferensalgoritmer för allmänna ändamål ofta inte effektivt kan lösa komplexa inferensproblem. Dessutom finns det inga formella korrekthetsbevis för vissa inferensalgoritmer när de används i universella PPL:er.
I denna avhandling behandlas forskningsproblem som rör Monte Carlo-inferensalgoritmer—samplingbaserade inferensalgoritmer för allmänna ändamål som universella PPL-implementationer ofta tillämpar. Det första forskningsproblemet rör korrektheten av sekventiella Monte Carlo-inferensalgoritmer (SMC). Ett bidrag i avhandlingen är ett korrekthetsbevis för SMC-algoritmer i universella PPL:er. Det andra forskningsproblemet rör förbättringar av exekveringstid vid exekveringsavbrott—ett krav i många Monte Carlo-inferensalgoritmer. Avhandlingen behandlar problemet genom två separata tillvägagångssätt. Det första tillvägagångssättet är en kompileringsteknik som riktar sig mot högpresterande plattformar. Det andra tillvägagångssättet är en statisk avbrottsanalys som styr en selektiv transformation till fortsättningsskickande stil (CPS), vilket reducerar exekveringstid jämfört med en fullständig CPS-transformation. Det tredje forskningsproblemet rör inferensförbättringar genom samordning—en användbar och ofta förbisedd egenskap i PPL:er. Avhandlingens bidrag är en formell definition av samordning, en statisk analysteknik som automatiskt samordnar program, samt samordnade versioner av SMC- och Markovkedjebaserade Monte Carlo-inferensalgoritmer (MCMC). Det sista forskningsproblemet är mer praktiskt och rör den effektiva implementationen av PPL:er. Konkret är bidraget den universella PPL:en Miking CorePPL och dess kompilator. Sammanfattningsvis förbättrar avhandlingens bidrag avsevärt effektiviteten hos Monte Carlo-algoritmer som tillämpas i universella PPL:er.
Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2023. p. 272
Series
TRITA-EECS-AVL ; 2023:22
Keywords
Probabilistic programming languages, Compilers, Static program analysis, Monte Carlo inference, Operational semantics, Probabilistiska programmeringsspråk, Kompilatorer, Statisk programanalys, Monte Carlo-inferens, Operationell semantik
National Category
Computer Sciences
Research subject
Information and Communication Technology
Identifiers
urn:nbn:se:kth:diva-324496 (URN)978-91-8040-503-4 (ISBN)
Public defence
2023-03-29, Zoom: https://kth-se.zoom.us/j/69904297956, Sal A, Kistagången 16, Kista, 13:00 (English)
Opponent
Supervisors
Note
QC 20230303
2023-03-032023-03-022023-03-13Bibliographically approved