Neural tools for formal verification

We develop practical tools that make formal proof assistants easier to use. For example, LLMstep uses language models to provide verified next-step suggestions in Lean.
LLMstep integrates language models and the Lean proof assistant.
LLMstep suggestions on a real-world formalization of the Amazon Web Services Cedar Policy Language.

Related publications

2023

  1. llmstep: LLM proofstep suggestions in Lean
    Sean Welleck, and Rahul Saha
    In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS’23, 2023