An evaluation of how probabilistic and differentiable programming languages ought to be written in order to preserve correctness and flexibility

评估应如何编写概率性和可微分的编程语言以保持正确性和灵活性

• 批准号: 2421783
• 金额: --
• 依托单位: University of Oxford
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2020
• 资助国家: 英国
• 起止时间: 2020 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2421783
• 关键词: evaluation; how; probabilistic; differentiable; programming

Probabilistic and differentiable programming languages are programming languages that can work together to perform Bayesian machine learning. Bayesian machine learning is an increasingly popular, model-based approach to machine learning, that has a mathematical foundation which allows it to deal well with uncertainty and explainability. To emphasise the increasing importance of probabilistic programming, it is noteworthy that probabilistic and differentiable programming languages have recently been developed by high profile corporations, such as Uber (Pyro), Facebook (HackPPL) and Google (Edward, Jax). As probabilistic and differentiable programming languages become increasingly used in important decision-making systems (e.g. insurance), more scrutiny will be applied to the models, algorithms, and hardware reliability, but also the code and programming languages themselves. If implementations of probabilistic and differentiable programming languages can be shown to be correct with respect to a mathematical specification, then this will allow society to have increased confidence in the predictions given by systems which rely on probabilistic and differentiable programming languages. Programming language semantics tie computer code that is written to a mathematical domain, allowing for the rigorous assessment of the denotation and relative consistency of a programming language. The utility of this notion is demonstrated by considering a nuclear power station. If one runs code in a nuclear reactor, one would like to be able to mathematically prove properties about the code in critical components. Semantics also justify the validity of the way in which programs can be transformed (whilst preserving the underlying semantics), which is important not only for compilers and optimisers, but also in guiding the programmer in the first place. To date, PPLs tend to be implemented without explicit focus to a particular semantics. In addition, PPLs tend to be written in languages, which whilst easy to prototype in, are not easy to assess the correctness of with respect to a semantics (using compile time guarantees, for instance). This project aims to assess how probabilistic and differentiable programming languages can be implemented in functional programming languages, which allow for extensive compile time guarantees on the correctness of code. This will be performed by implementing a probabilistic and differentiable programming library in Haskell, with explicit reference to a semantics. The focus will not only be on the correctness of the programming language, but also on the flexibility, compositionality and modularity of the code involved. To do this, this project will investigate contemporary techniques in pure functional programming languages. One example of a cutting-edge technique in programming languages research are algebraic effects and their handlers. They are a language construct that allow programmers to manipulate the composition of language features in a modular and sophisticated manner, by elegantly separating syntax and semantics. This project will investigate algebraic effects and handlers in context of probabilistic and differentiable programming. Once, a clearer idea of how these languages should be written is established, then an investigation into how this applies to the discovery of new drugs will occur using probabilistic programming. Representing molecules and their simulation will be a focal point for this project. This project is interdisciplinary by nature and will use ideas from (quantum) chemistry and structural biology. This project falls within the EPSRC Information and Communication Technologies (Verification and Correctness) research area. No private enterprise is currently involved in this research

概率和可微编程语言是可以一起工作来执行贝叶斯机器学习的编程语言。贝叶斯机器学习是一种日益流行的基于模型的机器学习方法，它具有数学基础，可以很好地处理不确定性和可解释性。为了强调概率编程日益增长的重要性，值得注意的是，最近一些知名公司开发了概率和可微分编程语言，如Uber （Pyro）、Facebook （HackPPL）和谷歌（Edward, Jax）。随着概率和可微分编程语言越来越多地用于重要的决策系统（例如保险），更多的审查将应用于模型，算法和硬件可靠性，以及代码和编程语言本身。如果概率和可微编程语言的实现可以被证明是正确的数学规范，那么这将使社会对依赖于概率和可微编程语言的系统给出的预测增加信心。编程语言语义将编写到数学领域的计算机代码联系起来，允许对编程语言的外延和相对一致性进行严格的评估。这个概念的实用性可以通过考虑一个核电站来证明。如果在核反应堆中运行代码，人们希望能够从数学上证明关键组件中代码的性质。语义还证明了程序转换方式的有效性（同时保留底层语义），这不仅对编译器和优化器很重要，而且对程序员的指导也很重要。迄今为止，ppp的实现往往没有明确关注特定的语义。此外，ppl倾向于用语言编写，这些语言虽然易于原型化，但不容易评估语义的正确性（例如，使用编译时间保证）。该项目旨在评估如何在函数式编程语言中实现概率和可微分编程语言，这允许在代码正确性的广泛编译时间保证。这将通过在Haskell中实现一个概率和可微分编程库来实现，并显式引用语义。重点不仅在于编程语言的正确性，还在于所涉及的代码的灵活性、组合性和模块化。为此，本项目将研究纯函数式编程语言中的当代技术。在程序设计语言研究中，前沿技术的一个例子是代数效应及其处理程序。它们是一种语言结构，允许程序员通过优雅地分离语法和语义，以模块化和复杂的方式操纵语言特性的组合。这个项目将研究概率和可微规划背景下的代数效应和处理程序。一旦对如何编写这些语言有了更清晰的认识，就可以使用概率编程来研究如何将其应用于新药的发现。表示分子和它们的模拟将是这个项目的焦点。这个项目本质上是跨学科的，将使用（量子）化学和结构生物学的思想。该项目属于EPSRC信息和通信技术（验证和正确性）研究领域。目前没有私营企业参与这项研究