News
I will be at NeurIPS 2022 to present my paper “Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis”.
I will be giving a talk at JuliaCon 2021: “Building on AlphaZero with Julia”.
I will be giving a talk at AITP 2021 about my research on applying reinforcement learning to proof search and program synthesis: “Designing a Theorem Prover for Reinforcement Learning and Neural Guidance”.
Julia Computing demoed AlphaZero.jl during their JuliaCon 2020 sponsor talk.
I am releasing AlphaZero.jl, an implementation of Deepmind’s algorithm in Julia. It is one to two orders of magnitude faster than existing Python implementations, while being equally simple.
Featured Publications
A complete list of publications can be found here.
Software
I am the lead developer of AlphaZero.jl.
- The philosophy of this project is to provide an implementation of AlphaZero that is simple enough to be widely accessible for students and researchers, while also being sufficiently powerful and fast to enable meaningful experiments on limited computing resources.
- AlphaZero.jl is consistently one to two orders of magnitude faster than existing Python implementations, while being equally simple and flexible.
I am also actively developing and maintaining the following programs:
- The Kappa Trace Query Language: a domain-specific language for analyzing Kappa simulation traces.
- The Kappa Counterfactual Resimulator: a library to sample counterfactual traces in Kappa.
- KaFlow: a program to generate causal summaries of Kappa traces.
- Asciimath compiler: a compiler from a variant of asciimath to LaTex, written in Haskell.
Finally, I developed the “Copilot Theorem” package, which enables fully-automated verification of safety properties of real-time embedded programs written in the Copilot language.