paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Abstract Hidden Markov Models: a monadic account of quantitative information flow

抽象隐马尔可夫模型:定量信息流的单子式刻画
LMCS vol.Volume 15, Issue 12019匹配度 3/10 · 论文属于概率程序形式语义与定量信息流,涉及HMM、单子、熵和安全序,与贝叶斯/概率程序分析有边缘关联;但未涉及LLM/Agent、静态分析在机器学习系统中的应用、浮点程序分析或LLM改进静态分析等核心方向。引用 0 inbox
Annabelle McIver, Carroll Morgan, Tahiry Rabehaja
crossref: 2026-09-10

AI 速览

一句话:用 Giry 单子与抽象 HMM 为隐藏状态概率程序建立信息流语义、安全序与不确定性变换。

隐马尔可夫模型(HMM)描述状态隐藏但会泄漏信息的马尔可夫过程,通常表示为三路联合概率分布。本文把 HMM 重构为抽象 HMM,作为概率隐藏状态序列程序在 Giry 单子中的指称,并用 D X → D² X 而非传统 X → D X 来编码隐藏状态,同时赋予其递增安全性的偏序。作者用一个小型 Haskell 原型展示该构造,提出推广现有概率熵的不确定性测度,分析其解析性质及与安全序的交互,并给出与正向抽象 HMM 对偶的后向不确定性变换语义。最后指出统计数据库的 Dalenius 期望本质上是组合性问题,并给出处理思路。

问题
如何为具有隐藏状态的概率序列程序提供指称语义,并刻画信息泄漏与安全性?传统 HMM 通常仅表示为联合概率分布,缺乏组合式程序语义。
方法
将 HMM 重构为 Giry 单子中的抽象 HMM,用 D X → D² X 类型编码隐藏状态;用小型 Haskell 原型演示,并引入不确定性测度与后向不确定性变换语义。
评估
通过单子语义构造和熵的解析性质分析说明方法,并以 Haskell 原型展示构造;最终论证 Dalenius 期望在统计数据库中可归结为组合性问题。
原文摘要(Abstract)

Hidden Markov Models, HMM's, are mathematical models of Markov processes with state that is hidden, but from which information can leak. They are typically represented as 3-way joint-probability distributions. We use HMM's as denotations of probabilistic hidden-state sequential programs: for that, we recast them as `abstract' HMM's, computations in the Giry monad $\mathbb{D}$, and we equip them with a partial order of increasing security. However to encode the monadic type with hiding over some state $\mathcal{X}$ we use $\mathbb{D}\mathcal{X}\to \mathbb{D}^2\mathcal{X}$ rather than the conventional $\mathcal{X}{\to}\mathbb{D}\mathcal{X}$ that suffices for Markov models whose state is not hidden. We illustrate the $\mathbb{D}\mathcal{X}\to \mathbb{D}^2\mathcal{X}$ construction with a small Haskell prototype. We then present uncertainty measures as a generalisation of the extant diversity of probabilistic entropies, with characteristic analytic properties for them, and show how the new entropies interact with the order of increasing security. Furthermore, we give a `backwards' uncertainty-transformer semantics for HMM's that is dual to the `forwards' abstract HMM's - it is an analogue of the duality between forwards, relational semantics and backwards, predicate-transformer semantics for imperative programs with demonic choice. Finally, we argue that, from this new denotational-semantic viewpoint, one can see that the Dalenius desideratum for statistical databases is actually an issue in compositionality. We propose a means for taking it into account.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot809,
  title = {Abstract Hidden Markov Models: a monadic account of quantitative information flow},
  author = {Annabelle McIver and Carroll Morgan and Tahiry Rabehaja},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 15, Issue 1},
  year = {2019},
  doi = {10.23638/lmcs-15(1:36)2019}
}