Showing 1–2 of 2 results for author: Bedford, A

Quantum Deep Learning: Sampling Neural Nets with a Quantum Annealer

Authors: Catherine F. Higham, Adrian Bedford

Abstract: We demonstrate the feasibility of framing a classically learned deep neural network as an energy based model that can be processed on a one-step quantum annealer in order to exploit fast sampling times. We propose approaches to overcome two hurdles for high resolution image classification on a quantum processing unit (QPU): the required number and binary nature of the model states. With this novel… ▽ More We demonstrate the feasibility of framing a classically learned deep neural network as an energy based model that can be processed on a one-step quantum annealer in order to exploit fast sampling times. We propose approaches to overcome two hurdles for high resolution image classification on a quantum processing unit (QPU): the required number and binary nature of the model states. With this novel method we successfully transfer a convolutional neural network to the QPU and show the potential for classification speedup of at least one order of magnitude. △ Less

Submitted 19 July, 2021; originally announced July 2021.

Coqatoo: Generating Natural Language Versions of Coq Proofs

Authors: Andrew Bedford

Abstract: Due to their numerous advantages, formal proofs and proof assistants, such as Coq, are becoming increasingly popular. However, one disadvantage of using proof assistants is that the resulting proofs can sometimes be hard to read and understand, particularly for less-experienced users. To address this issue, we have implemented a tool capable of generating natural language versions of Coq proofs ca… ▽ More Due to their numerous advantages, formal proofs and proof assistants, such as Coq, are becoming increasingly popular. However, one disadvantage of using proof assistants is that the resulting proofs can sometimes be hard to read and understand, particularly for less-experienced users. To address this issue, we have implemented a tool capable of generating natural language versions of Coq proofs called Coqatoo, which we present in this paper. △ Less

Submitted 11 December, 2017; originally announced December 2017.

Comments: International Workshop on Coq for Programming Languages (CoqPL 2018)