检索结果-内蒙古大学图书馆

Step-Indexed Logical Relations for Countable Nondeterminism and probabilistic Choice

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2023年第POPL期7卷 33-60页

作者： Aguirre, Alejandro Birkedal, Lars Aarhus Univ Abogade 34 DK-8200 Aarhus Denmark

Developing denotational models for higher-order languages that combine probabilistic and nondeterministic choice is known to be very challenging. In this paper, we propose an alternative approach based on operational techniques. We study a higher-order language combining parametric polymorphism, recursive types, discrete probabilistic choice and countable nondeterminism. We define probabilistic generalizations of may- and must-termination as the optimal and pessimal probabilities of termination. Then we define step-indexed logical relations and show that they are sound and complete with respect to the induced contextual preorders. For may-equivalence we use step-indexing over the natural numbers whereas for must-equivalence we index over the countable ordinals. We then show than the probabilities of may- and must-termination coincide with the maximal and minimal probabilities of termination under all schedulers. Finally we derive the equational theory induced by contextual equivalence and show that it validates the distributive combination of the algebraic theories for probabilistic and nondeterministic choice.

关键词： Functional Languages probabilistic programming Logical Relations

来源：评论

学校读者我要写书评

暂无评论

Distributions for Compositionally Differentiating Parametric Discontinuities

引用

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2024年第OOPSLA期8卷 893-922页

作者： Michel, Jesse Mu, Kevin Yang, Xuanda Bangaru, Sai Praveen Collins, Elias Rojas Bernstein, Gilbert Ragan-Kelley, Jonathan Carbin, Michael Li, Tzu-Mao MIT Cambridge MA 02139 USA Univ Washington Seattle WA USA Univ Calif San Diego San Diego CA USA Univ Washington Cambridge MA USA

Computations in physical simulation, computer graphics, and probabilistic inference often require the differentiation of discontinuous processes due to contact, occlusion, and changes at a point in time. Popular differentiable programming languages, such as PyTorch and JAX, ignore discontinuities during differentiation. This is incorrect for parametric discontinuities-conditionals containing at least one real-valued parameter and at least one variable of integration. We introduce Potto, the first differentiable first-order programming language to soundly differentiate parametric discontinuities. We present a denotational semantics for programs and program derivatives and show the two accord. We describe the implementation of Potto, which enables separate compilation of programs. Our prototype implementation overcomes previous compile-time bottlenecks achieving an 88.1x and 441.2x speed up in compile time and a 2.5x and 7.9x speed up in runtime, respectively, on two increasingly large image stylization benchmarks. We showcase Potto by implementing a prototype differentiable renderer with separately compiled shaders.

关键词： Differentiable programming Denotational Semantics Differentiable Rendering Distribution Theory probabilistic programming

来源：评论

学校读者我要写书评

暂无评论

Towards Verified Stochastic Variational Inference for probabilistic Programs

引用

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2020年第POPL期4卷 1–33页

作者： Lee, Wonyeol Yu, Hangyeol Rival, Xavier Yang, Hongseok Korea Adv Inst Sci & Technol Sch Comp Daejeon South Korea INRIA Paris Dept Informat ENS Paris France PSL Univ CNRS Paris France

probabilistic programming is the idea of writing models from statistics and machine learning using program notations and reasoning about these models using generic inference engines. Recently its combination with deep learning has been explored intensely, which led to the development of so called deep probabilistic programming languages, such as Pyro, Edward and ProbTorch. At the core of this development lie inference engines based on stochastic variational inference algorithms. When asked to find information about the posterior distribution of a model written in such a language, these algorithms convert this posterior-inference query into an optimisation problem and solve it approximately by a form of gradient ascent or descent. In this paper, we analyse one of the most fundamental and versatile variational inference algorithms, called score estimator or REINFORCE, using tools from denotational semantics and program analysis. We formally express what this algorithm does on models denoted by programs, and expose implicit assumptions made by the algorithm on the models. The violation of these assumptions may lead to an undefined optimisation objective or the loss of convergence guarantee of the optimisation process. We then describe rules for proving these assumptions, which can be automated by static program analyses. Some of our rules use nontrivial facts from continuous mathematics, and let us replace requirements about integrals in the assumptions, such as integrability of functions defined in terms of programs' denotations, by conditions involving differentiation or boundedness, which are much easier to prove automatically (and manually). Following our general methodology, we have developed a static program analysis for the Pyro programming language that aims at discharging the assumption about what we call model-guide support match. Our analysis is applied to the eight representative model-guide pairs from the Pyro webpage, which include sophisticated neural ne

关键词： probabilistic programming static analysis semantics correctness

来源：评论

学校读者我要写书评

暂无评论

Functional programming for Modular Bayesian Inference

引用

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2018年第ICFP期2卷 1–29页

作者： Scibior, Adam Kammar, Ohad Ghahramani, Zoubin Univ Cambridge Dept Engn Trumpington St Cambridge CB2 1PZ England MPI Intelligent Syst Empir Inference Dept Spemannstr 34 D-72076 Tubingen Germany Univ Oxford Dept Comp Sci Wolfson BldgParks Rd Oxford OX1 3QD England Uber AI Labs San Francisco CA USA

We present an architectural design of a library for Bayesian modelling and inference in modern functional programming languages. The novel aspect of our approach are modular implementations of existing state-of-the-art inference algorithms. Our design relies on three inherently functional features: higher-order functions, inductive data-types, and support for either type-classes or an expressive module system. We provide a performant Haskell implementation of this architecture, demonstrating that high-level and modular probabilistic programming can be added as a library in sufficiently expressive languages. We review the core abstractions in this architecture: inference representations, inference transformations, and inference representation transformers. We then implement concrete instances of these abstractions, counterparts to particle filters and Metropolis-Hastings samplers, which form the basic building blocks of our library. By composing these building blocks we obtain state-of-the-art inference algorithms: Resample-Move Sequential Monte Carlo, Particle Marginal Metropolis-Hastings, and Sequential Monte Carlo Squared. We evaluate our implementation against existing probabilistic programming systems and find it is already competitively performant, although we conjecture that existing functional programming optimisation techniques could reduce the overhead associated with the abstractions we use. We show that our modular design enables deterministic testing of inherently stochastic Monte Carlo algorithms. Finally, we demonstrate using OCand that an expressive module system can also implement our design.

关键词： probabilistic programming functional programming Bayesian inference higher-order functions inductive types type-classes module systems monads monad transformers machine learning Anglican WebPPL Markov Chain Monte Carlo Sequential Monte Carlo Monte Carlo samplers

来源：评论

学校读者我要写书评

暂无评论

Higher Order Bayesian Networks, Exactly

引用

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2024年第POPL期8卷 2514-2546页

作者： Faggian, Claudia Pautasso, Daniele Vanoni, Gabriele Univ Paris Cite CNRS IRIF Paris France Univ Turin Turin Italy

Bayesian networks are graphical first-order probabilistic models that allow for a compact representation of large probability distributions, and for efficient inference, both exact and approximate. We introduce a higher-order programming language-in the idealized form of a lambda-calculus-which we prove sound and complete w.r.t. Bayesian networks: each Bayesian network can be encoded as a term, and conversely each (possibly higher-order and recursive) program of ground type compiles into a Bayesian network. The language allows for the specification of recursive probability models and hierarchical structures. Moreover, we provide a compositional and cost-aware semantics which is based on factors, the standard mathematical tool used in Bayesian inference. Our results rely on advanced techniques rooted into linear logic, intersection types, rewriting theory, and Girard's geometry of interaction, which are here combined in a novel way.

关键词： lambda calculus intersection types Bayesian networks probabilistic programming denotational semantics

来源：评论

学校读者我要写书评

暂无评论

Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized probabilistic Inference

引用

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2023年第POPL期7卷 1454-1482页

作者： Li, Jianlin Ven, Leni Shi, Pengyuan Zhang, Yizhou Univ Waterloo David R Cheriton Sch Comp Sci 200 Univ Ave West Waterloo ON N2L 3G1 Canada

In probabilistic programming languages (PPLs), a critical step in optimization-based inference methods is constructing, for a given model program, a trainable guide program. Soundness and effectiveness of inference rely on constructing good guides, but the expressive power of a universal PPL poses challenges. This paper introduces an approach to automatically generating guides for deep amortized inference in a universal PPL. Guides are generated using a type-directed translation per a novel behavioral type system. Guide generation extracts and exploits independence structures using a syntactic approach to conditional independence, with a semantic account left to further work. Despite the control-flow expressiveness allowed by the universal PPL, generated guides are guaranteed to satisfy a critical soundness condition and, moreover, consistently improve training and inference over state-of-the-art baselines for a suite of benchmarks.

关键词： probabilistic programming amortized inference type systems guide generation

来源：评论

学校读者我要写书评

暂无评论

ADEV: Sound Automatic Differentiation of Expected Values of probabilistic Programs

引用

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2023年第POPL期7卷 121-153页

作者： Lew, Alexander K. Huot, Mathieu Staton, Sam Mansinghka, Vikash K. MIT 77 Massachusetts Ave Cambridge MA 02139 USA Univ Oxford Oxford England

Optimizing the expected values of probabilistic processes is a central problem in computer science and its applications, arising in fields ranging from artificial intelligence to operations research to statistical computing. Unfortunately, automatic differentiation techniques developed for deterministic programs do not in general compute the correct gradients needed for widely used solutions based on gradient-based optimization. In this paper, we present ADEV, an extension to forward-mode AD that correctly differentiates the expectations of probabilistic processes represented as programs that make random choices. Our algorithm is a source-to-source program transformation on an expressive, higher-order language for probabilistic computation, with both discrete and continuous probability distributions. The result of our transformation is a new probabilistic program, whose expected return value is the derivative of the original program's expectation. This output program can be run to generate unbiased Monte Carlo estimates of the desired gradient, which can then be used within the inner loop of stochastic gradient descent. We prove ADEV correct using logical relations over the denotations of the source and target probabilistic programs. Because it modularly extends forward-mode AD, our algorithm lends itself to a concise implementation strategy, which we exploit to develop a prototype in just a few dozen lines of Haskell (https://***/probcomp/adev).

关键词： probabilistic programming automatic differentiation denotational semantics logical relations functional programming correctness machine learning theory

来源：评论

学校读者我要写书评

暂无评论

Lilac: A Modal Separation Logic for Conditional Probability

引用

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2023年第PLDI期7卷 148-171页

作者： Li, John M. Ahmed, Amal Holtzen, Steven Northeastern Univ Boston MA 02115 USA

We present Lilac, a separation logic for reasoning about probabilistic programs where separating conjunction captures probabilistic independence. Inspired by an analogy with mutable state where sampling corresponds to dynamic allocation, we show how probability spaces over a fixed, ambient sample space appear to be the natural analogue of heap fragments, and present a new combining operation on them such that probability spaces behave like heaps and measurability of random variables behaves like ownership. This combining operation forms the basis for our model of separation, and produces a logic with many pleasant properties. In particular, Lilac has a frame rule identical to the ordinary one, and naturally accommodates advanced features like continuous random variables and reasoning about quantitative properties of programs. Then we propose a new modality based on disintegration theory for reasoning about conditional probability. We show how the resulting modal logic validates examples from prior work, and give a formal verification of an intricate weighted sampling algorithm whose correctness depends crucially on conditional independence structure.(1)

关键词： probabilistic programming separation logic

来源：评论

学校读者我要写书评

暂无评论

Automated Expected Value Analysis of Recursive Programs

引用

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2023年第PLDI期7卷 1050-1072页

作者： Avanzini, Martin Moser, Georg Schaper, Michael INRIA Sophia Antipolis Mediterranee Route Lucioles BP 93 Valbonne France Univ Innsbruck Innsbruck Austria Build Informed Innsbruck Austria

In this work, we study the fully automated inference of expected result values of probabilistic programs in the presence of natural programming constructs such as procedures, local variables and recursion. While crucial, capturing these constructs becomes highly non-trivial. The key contribution is the definition of a term representation, denoted as infer[center dot], translating a pre-expectation semantics into first-order constraints, susceptible to automation via standard methods. A crucial step is the use of logical variables, inspired by previous work on Hoare logics for recursive programs. Noteworthy, our methodology is not restricted to tail-recursion, which could unarguably be replaced by iteration and wouldn't need additional insights. We have implemented this analysis in our prototype ev-imp. We provide ample experimental evidence of the prototype's algorithmic expressibility.

关键词： probabilistic programming expected value analysis weakest pre-expectation semantics automation

来源：评论

学校读者我要写书评

暂无评论

Quantitative Bounds on Resource Usage of probabilistic Programs

引用

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2024年第OOPSLA期8卷 362-391页

作者： Chatterjee, Krishnendu Goharshady, Amir Kafshdar Meggendorfer, Tobias Zikelic, Dorde Inst Sci & Technol Austria ISTA Klosterneuburg Austria Hong Kong Univ Sci & Technol Hong Kong Peoples R China Univ Lancaster Leipzig Germany Singapore Management Univ Singapore Singapore

Cost analysis, also known as resource usage analysis, is the task of finding bounds on the total cost of a program and is a well-studied problem in static analysis. In this work, we consider two classical quantitative problems in cost analysis for probabilistic programs. The first problem is to find a bound on the expected total cost of the program. This is a natural measure for the resource usage of the program and can also be directly applied to average-case runtime analysis. The second problem asks for a tail bound, i.e. given a threshold C the goal is to find a probability bound p such that P[total cost >= t] <= p. Intuitively, given a threshold C on the resource, the problem is to find the likelihood that the total cost exceeds this threshold. First, for expectation bounds, a major obstacle in previous works on cost analysis is that they can handle only non-negative costs or bounded variable updates. In contrast, we provide a new variant of the standard notion of cost martingales, that allows us to find expectation bounds for a class of programs with general positive or negative costs and no restriction on the variable updates. More specifically, our approach is applicable as long as there is a lower bound on the total cost incurred along every path. Second, for tail bounds, all previous methods are limited to programs in which the expected total cost is finite. In contrast, we present a novel approach, based on a combination of our martingale-based method for expectation bounds with a quantitative safety analysis, to obtain a solution to the tail bound problem that is applicable even to programs with infinite expected cost. Specifically, this allows us to obtain runtime tail bounds for programs that do not terminate almost-surely. In summary, we provide a novel combination of martingale-based cost analysis and quantitative safety analysis that is able to find expectation and tail cost bounds for probabilistic programs, without the restrictions of non-negative

关键词： probabilistic programming Static Analysis Quantitative Bounds Cost Analysis Martingales

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：