Publications

Diagonalisation SGD: Fast & Convergent SGD for Non-Differentiable Models via Reparameterisation and Smoothing

It is well-known that the reparameterisation gradient estimator, which exhibits low variance in practice, is biased for non-differentiable models. This may compromise correctness of gradient-based optimisation methods such as stochastic gradient descent (SGD). We introduce a simple syntactic framework to define non-differentiable functions piecewisely and present a systematic approach to obtain smoothings for which the reparameterisation gradient estimator is unbiased. Our main contribution is a novel variant of SGD, …

Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing

We study the foundations of variational inference, which frames posterior inference as an optimisation problem, for probabilistic programming. The dominant approach for optimisation in practice is stochastic gradient descent. In particular, a variant using the so-called reparameterisation gradient estimator exhibits fast convergence in a traditional statistics setting. Unfortunately, discontinuities, which are readily expressible in programming languages, can compromise the correctness of this approach. We consider a simple …

Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere

We study the differential properties of higher-order statistical probabilistic programs with recursion and conditioning. Our starting point is an open problem posed by Hongseok Yang: what class of statistical probabilistic programs have densities that are differentiable almost everywhere? Our main result is that almost surely terminating SPCF programs, generated from a set of primitive functions satisfying mild closure properties, have weight and value functions that are almost everywhere differentiable.

Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses

We present initial limit Datalog, a new extensible class of constrained Horn clauses for which the satisfiability problem is decidable. The class may be viewed as a generalisation to higher-order logic (with a simple restriction on types) of the first-order language limit DatalogZ (a fragment of Datalog modulo linear integer arithmetic), but can be instantiated with any suitable background theory.

HoCHC: a Refutationally-complete and Semantically-invariant System of Higher-order Logic Modulo Theories

We present a simple resolution proof system for higher-order constrained Horn clauses (HoCHC)—a system of higher-order logic modulo theories generalising (1st-order) constrained Horn clauses—and prove its soundness and refutational completeness w.r.t. both standard and Henkin semantics. As corollaries, HoCHC shares desirable properties (such as semi-decidability and a canonical model property) and deciable fragments with its 1st-order counterpart.

Talks

Recent & Upcoming

On the Reparameterisation Gradient for Non-Differentiable but Continuous Models

A Language and Smoothed Semantics for Convergent Stochastic Gradient Descent

A Language and Smoothed Semantics for Convergent Stochastic Gradient Descent

A Language and Smoothed Semantics for Convergent Stochastic Gradient Descent

Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere

HoCHC: a Refutationally-complete and Semantically-invariant System of Higher-order Logic Modulo Theories

Theses

Fast and Correct Variational Inference for Probabilistic Programming: Differentiability, Reparameterisation and Smoothing

Resolution for Higher−Order Constrained Horn Clauses

Design and Implementation of a CDCL(LA) Calculus

Teaching

Graduate Teaching and Research Scholar (Oriel College, Oxford):

Teaching Assistant (University of Oxford):

Teaching Assistant (Saarland University):

  • Fundamentals of Algorithms and Data Structures (winter semester 2016 / 17)
  • Mentor of Mathematical Preparatory Course (Sep / Oct 2016 / 17)

Contact