We research the intersection of Large Language Models and Formal Verification. Our goal is to bridge natural language mathematics and machine-verifiable proofs through autoformalisation.
| Project | Description | Venue | Links |
|---|---|---|---|
| DRIFT | Decomposing informal mathematical statements into smaller, more tractable sub-components improves autoformalisation performance, especially on out-of-distribution benchmarks. | ICLR 2026 | Paper · Code |
| TopoAlign | TopoAlign unlocks widely available code repositories as training resources for Math LLMs by structurally aligning code to formal mathematical statements. | Preprint | Paper · Code |
| Conjecturing | Conjecturing is an overlooked step in formal mathematical reasoning with LLMs and introduce ConjectureBench to evaluate conjecture generation across three settings: as a standalone task, during autoformalisation, and during proving. | Preprint | Paper · Code |
| Tool | Description | Links |
|---|---|---|
| LeanFlow | A Python interface for Lean 4 enabling programmatic interaction and proof verification. | Code |