Bridging natural language mathematics and machine-verifiable proofs through autoformalisation
Our research sits at the intersection of Large Language Models and Formal Verification. LLMs have demonstrated remarkable fluency and creativity in natural language, but they often struggle with logical consistency and produce "hallucinations" in mathematical reasoning. Formal Verification, on the other hand, provides certainty through interactive theorem provers like Lean, yet suffers from a steep learning curve that limits accessibility.
We aim to build a bridge that combines the intuition and creativity of LLMs with the rigor and precision of Formal Verification. Our goal is to automatically translate natural language mathematical problems into machine-verifiable proofs, making mathematical knowledge both more accessible and more reliable.
Our recent research on autoformalisation and formal reasoning
Decomposing informal mathematical statements into smaller, more tractable sub-components improves autoformalisation performance, especially on out-of-distribution benchmarks.
TopoAlign unlocks widely available code repositories as training resources for Math LLMs by structurally aligning code to formal mathematical statements.
Conjecturing is an overlooked step in formal mathematical reasoning with LLMs. We introduce ConjectureBench to evaluate conjecture generation across three settings.
Open-source software for formal mathematics
A Python interface for Lean 4 enabling programmatic interaction and proof verification.