open source code

Code, datasets, and benchmarks released alongside our research.

Current project

Chelis

formal verificationprogramming languagesAI agents

The verified tensor language for agent-written code.

Code Website

DeepSynth

ICLR 2026
AI agentsbenchmarkinformation synthesis

A benchmark of 120 real-world tasks testing whether AI agents can gather, combine, and reason over information from multiple sources.

Code Website Dataset Leaderboard Paper

Formal Mathematical Reasoning

autoformalisationtheorem provingLean 4

Bridging natural language mathematics and machine-verifiable proofs through autoformalisation.

GitHub Website

DRIFT

ICLR 2026

Decompose, Retrieve, Illustrate, then Formalize Theorems, retrieving premises for sub-components of informal statements.

Model Paper

TopoAlign

EMNLP 2026

Aligning code to math via topological decomposition, unlocking code repositories as training data for Math LLMs.

Dataset Paper

Conjecturing

arXiv 2025

ConjectureBench and Lean-FIRe, treating conjecturing as a distinct step of formal mathematical reasoning.

Paper

LeanFlow

A Python interface for Lean 4.

Code

DReSD

ACL Findings 2025
speculative decodingdense retrievalefficiency

Dense Retrieval for Speculative Decoding, using approximate nearest neighbour search over contextualised token embeddings.

Code Paper

SparsePO

EMNLP Findings 2025
preference optimisationalignment

Controlling preference alignment of LLMs via sparse token-level masks over KL divergence and reward.

Code Paper

Text-to-Code MRPT

EACL 2024
code generationpre-training

Text-to-code generation with modality-relative pre-training.

Code Dataset Paper

Models

PanGu-Coder 300M PanGu-Coder 300M (partial) PanGu-Coder 300M (full) PyCodeGPT 100M PyCodeGPT 100M (partial) PyCodeGPT 100M (full)

HumanRankEval

NAACL 2024
evaluationconversational assistants

Automatic evaluation of LMs as conversational assistants.

Code Paper