NLP for Interactive Theorem Proving
Overview
Large language models (LLMs) have shown surprising ability at natural language reasoning. Interactive theorem provers (ITPs) such as Rocq provide a rigorous setting where every reasoning step can be machine-checked. Combining the two opens a new frontier in automated mathematical reasoning.
I explore the integration of LLMs with ITPs, aiming to make proof development faster, more accessible, and eventually capable of tackling frontier mathematical problems.
Research Directions
Automated proof generation. Given a theorem statement in Rocq, can an LLM propose a valid proof? I study how to prompt, fine-tune, and evaluate models for this task, with a focus on proofs that are verified end-to-end by the Rocq kernel.
Proof translation. Formal proofs are written in a specific ITP, but insights often cross system boundaries. I investigate methods for automatically translating proofs between different proof assistants (e.g., from Lean to Rocq), reducing redundant formalization effort.
Documentation generation. Large formalization libraries are hard to navigate without good documentation. I work on generating natural-language explanations of Rocq definitions and lemmas, making libraries more accessible to newcomers.
Learning environments. Interactive proof assistants are powerful but have a steep learning curve. I am interested in building AI-assisted learning environments that guide students through interactive theorem proving, offering hints and feedback in natural language.
Related Publications
- Alessandro Bruni, Eike Ritter, Carsten Schürmann: Skolemization for Intuitionistic Linear Logic. IJCAR 2024 arXiv