Till innehåll på sidan

Correct and Efficient Monte Carlo Inference for Universal Probabilistic Programming Languages

Tid: On 2023-03-29 kl 13.00

Plats: Sal A, Kistagången 16, Kista

Videolänk: https://kth-se.zoom.us/j/69904297956

Språk: Engelska

Ämnesområde: Informations- och kommunikationsteknik

Respondent: Daniel Lundén , Programvaruteknik och datorsystem, SCS

Opponent: Professor Sam Staton, University of Oxford

Handledare: Professor David Broman, Programvaruteknik och datorsystem, SCS; Doktor Lawrence Murray, Uber AI; Professor Joakim Jaldén, Teknisk informationsvetenskap

Exportera till kalender

QC 20230303

Abstract

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.

urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-324496