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

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

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