一句话：提出“符号集合”语义域，并给出解释器自动正确性元定理。
概率符号执行能把精确概率推断扩展到表达力更强的语言，但高性能符号执行策略复杂，使此类概率编程语言难以调试、优化和证明正确。作者提出 symbolic sets（符号集合），作为刻画符号执行底层计算的新语义域：符号集合范畴是 Grothendieck topos，因而可用类型论作为元语言操作符号集合与函数。基于此，他们证明一个元定理：一大类用符号集合内部语言写成的 definitional interpreter 对其普通集合论解释自动正确。作为应用，该元定理首次为带有高阶函数、类型导向状态合并、模式匹配和结构递归的符号概率语言给出了完整正确性论证。
Symbolic execution has emerged as a powerful technique for scaling exact probabilistic inference to languages with more expressive features. But, this expressivity comes at a price: probabilistic programming languages based on symbolic execution are difficult to debug, optimize, and prove correct due to the many intricacies inherent to high-performance symbolic execution strategies. We aim to make it easier to work with probabilistic symbolic executors by developing symbolic sets, a new semantic domain that cleanly captures the notion of computation underlying symbolic execution. Just as a symbolic executor replaces ordinary execution with a lifted semantics, symbolic set theory replaces ordinary set theory with a lifted mathematics: the category of symbolic sets is a Grothendieck topos, which allows type theory to be used as a metalanguage for working with symbolic sets and functions. We prove a metatheorem that shows how a large class of definitional interpreters written in the internal language of symbolic sets are automatically correct for their ordinary set-theoretic interpretations. Using this metatheorem, we give the first full correctness argument for a symbolic probabilistic language with higher-order functions, type-directed state merging, pattern matching, and structural recursion.
@article{paperbot3761,
title = {Categorical Semantics of Probabilistic Symbolic Execution},
author = {John M. Li and Jack Czenszak and Steven Holtzen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808343}
}