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

概率和可微编程语言是可以一起执行贝叶斯机器学习的编程语言。贝叶斯机器学习是一种越来越流行的基于模型的机器学习方法，它具有数学基础，可以很好地处理不确定性和可解释性。为了强调概率编程的重要性，值得注意的是，最近一些知名公司开发了概率和可微编程语言，如Uber（Pyro），Facebook（HackPPL）和Google（Edward，Jax）。随着概率和可微编程语言越来越多地用于重要的决策系统（例如保险），更多的审查将应用于模型，算法和硬件可靠性，以及代码和编程语言本身。如果概率和可微编程语言的实现可以证明在数学规范方面是正确的，那么这将使社会对依赖于概率和可微编程语言的系统所给出的预测具有更高的信心。编程语言语义将编写的计算机代码绑定到数学域，允许严格评估编程语言的外延和相对一致性。这一概念的效用是通过考虑核电站来证明的。如果一个人在核反应堆中运行代码，他希望能够在数学上证明关键组件中代码的属性。语义也证明了程序转换方式的有效性（同时保留底层语义），这不仅对编译器和优化器很重要，而且首先指导程序员。到目前为止，PPL往往是在没有明确关注特定语义的情况下实现的。此外，PPL往往是用语言编写的，这些语言虽然易于原型化，但不容易评估语义的正确性（例如使用编译时保证）。该项目旨在评估概率和可微编程语言如何在函数编程语言中实现，这些语言允许对代码的正确性进行广泛的编译时间保证。这将通过在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