Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Automatic Alignment in Higher-Order Probabilistic Programming Languages
KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Programvaruteknik och datorsystem, SCS. KTH, Skolan för elektroteknik och datavetenskap (EECS), Centra, Digital futures.ORCID-id: 0000-0003-3127-5640
KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Programvaruteknik och datorsystem, SCS. KTH, Skolan för elektroteknik och datavetenskap (EECS), Centra, Digital futures.ORCID-id: 0000-0001-9703-6912
Department of Bioinformatics and Genetics, Swedish Museum of Natural History, Stockholm, Sweden; Department of Zoology, Stockholm University, Stockholm, Sweden.ORCID-id: 0000-0002-3929-251X
KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Programvaruteknik och datorsystem, SCS. KTH, Skolan för elektroteknik och datavetenskap (EECS), Centra, Digital futures.ORCID-id: 0000-0001-8457-4105
2023 (engelsk)Inngår i: Programming Languages and Systems, Springer Nature , 2023Konferansepaper, Publicerat paper (Fagfellevurdert)
Abstract [en]

Probabilistic Programming Languages (PPLs) allow users to encode statistical inference problems and automatically apply an inference algorithm to solve them. Popular inference algorithms for PPLs, such as sequential Monte Carlo (SMC) and Markov chain Monte Carlo (MCMC), are built around checkpoints—relevant events for the inference algorithm during the execution of a probabilistic program. Deciding the location of checkpoints is, in current PPLs, not done optimally. To solve this problem, we present a static analysis technique that automatically determines checkpoints in programs, relieving PPL users of this task. The analysis identifies a set of checkpoints that execute in the same order in every program run—they are aligned. We formalize alignment, prove the correctness of the analysis, and implement the analysis as part of the higher-order functional PPL Miking CorePPL. By utilizing the alignment analysis, we design two novel inference algorithm variants: aligned SMC and aligned lightweight MCMC. We show, through real-world experiments, that they significantly improve inference execution time and accuracy compared to standard PPL versions of SMC and MCMC.

sted, utgiver, år, opplag, sider
Springer Nature , 2023.
Serie
Lecture Notes in Computer Science ; 13990
Emneord [en]
Probabilistic programming, Operational semantics, Static analysis
HSV kategori
Forskningsprogram
Datalogi
Identifikatorer
URN: urn:nbn:se:kth:diva-324293DOI: 10.1007/978-3-031-30044-8_20ISI: 001284040300020Scopus ID: 2-s2.0-85161447105OAI: oai:DiVA.org:kth-324293DiVA, id: diva2:1739445
Konferanse
32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023
Merknad

Part of ISBN 9783031300431, 9783031300448

QC 20251002

Tilgjengelig fra: 2023-02-24 Laget: 2023-02-24 Sist oppdatert: 2025-10-02
Inngår i avhandling
1. Correct and Efficient Monte Carlo Inference for Universal Probabilistic Programming Languages
Åpne denne publikasjonen i ny fane eller vindu >>Correct and Efficient Monte Carlo Inference for Universal Probabilistic Programming Languages
2023 (engelsk)Doktoravhandling, med artikler (Annet vitenskapelig)
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.

sted, utgiver, år, opplag, sider
Stockholm: KTH Royal Institute of Technology, 2023. s. 272
Serie
TRITA-EECS-AVL ; 2023:22
Emneord
Probabilistic programming languages, Compilers, Static program analysis, Monte Carlo inference, Operational semantics, Probabilistiska programmeringsspråk, Kompilatorer, Statisk programanalys, Monte Carlo-inferens, Operationell semantik
HSV kategori
Forskningsprogram
Informations- och kommunikationsteknik
Identifikatorer
urn:nbn:se:kth:diva-324496 (URN)978-91-8040-503-4 (ISBN)
Disputas
2023-03-29, Zoom: https://kth-se.zoom.us/j/69904297956, Sal A, Kistagången 16, Kista, 13:00 (engelsk)
Opponent
Veileder
Merknad

QC 20230303

Tilgjengelig fra: 2023-03-03 Laget: 2023-03-02 Sist oppdatert: 2023-03-13bibliografisk kontrollert

Open Access i DiVA

fulltext(817 kB)148 nedlastinger
Filinformasjon
Fil FULLTEXT02.pdfFilstørrelse 817 kBChecksum SHA-512
806b0f16b6e32c6cda0c06d06e37e7cb60b49ac7e961365ab7afb77e112dd3cbd0c73c7eec21f0b961d203b5de5a15bbc7710709066a924ceb0784b49a61d86a
Type fulltextMimetype application/pdf

Andre lenker

Forlagets fulltekstScopus

Person

Lundén, DanielÇaylak, GizemBroman, David

Søk i DiVA

Av forfatter/redaktør
Lundén, DanielÇaylak, GizemRonquist, FredrikBroman, David
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar
Totalt: 195 nedlastinger
Antall nedlastinger er summen av alle nedlastinger av alle fulltekster. Det kan for eksempel være tidligere versjoner som er ikke lenger tilgjengelige

doi
urn-nbn

Altmetric

doi
urn-nbn
Totalt: 1037 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf