title: LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
summary: Large language models (LLMs) have shown promise in proving formal theorems
  using proof assistants such as Lean. However, existing methods are difficult to
  reproduce or build on, due to private code, data, and large compute
  requirements. This has created substantial barriers to research on machine
  learning methods for theorem proving. This paper removes these barriers by
  introducing LeanDojo: an open-source Lean playground consisting of toolkits,
  data, models, and benchmarks. LeanDojo extracts data from Lean and enables
  interaction with the proof environment programmatically. It contains
  fine-grained annotations of premises in proofs, providing valuable data for
  premise selection: a key bottleneck in theorem proving. Using this data, we
  develop ReProver (Retrieval-Augmented Prover): the first LLM-based prover that
  is augmented with retrieval for selecting premises from a vast math library. It
  is inexpensive and needs only one GPU week of training. Our retriever leverages
  LeanDojo's program analysis capability to identify accessible premises and hard
  negative examples, which makes retrieval much more effective. Furthermore, we
  construct a new benchmark consisting of 96,962 theorems and proofs extracted
  from Lean's math library. It features challenging data split requiring the
  prover to generalize to theorems relying on novel premises that are never used
  in training. We use this benchmark for training and evaluation, and
  experimental results demonstrate the effectiveness of ReProver over
  non-retrieval baselines and GPT-4. We thus provide the first set of open-source
  LLM-based theorem provers without any proprietary datasets and release it under
  a permissive MIT license to facilitate further research.
paper_authors._id: 649b8e7f9fc875a86329f76b
paper_authors.name: Kaiyu Yang
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2023-06-28T07:46:56.863Z
paper_authors._id: 642a6a2816d4d8293c9c0246
paper_authors.avatarUrl: /avatars/c2263d8227418e85845ddc0e22b0fd4e.svg
paper_authors.fullname: Kaiyu Yang
paper_authors.type: user
paper_authors.user: kaiyuy
paper_authors._id: 649b8e7f9fc875a86329f76c
paper_authors.name: Aidan M. Swope
paper_authors._id: 649b8e7f9fc875a86329f76d
paper_authors.name: Alex Gu
paper_authors.status: claimed_verified
paper_authors.statusLastChangedAt: 2023-06-28T20:15:45.744Z
paper_authors._id: 6179abf8ec6ce4dc2e5f2376
paper_authors.avatarUrl: /avatars/d10c6a1b350146b36949a24220471295.svg
paper_authors.fullname: Alex Gu
paper_authors.type: user
paper_authors.user: minimario
paper_authors._id: 649b8e7f9fc875a86329f76e
paper_authors.name: Rahul Chalamala
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2023-06-28T07:47:33.702Z
paper_authors._id: 648abf5f0c2a2d8592ca07e7
paper_authors.avatarUrl: /avatars/333a96e0b2e9420b2abacf538c776c18.svg
paper_authors.fullname: Rahul Chalamala
paper_authors.type: user
paper_authors.user: rchalamala
paper_authors._id: 649b8e7f9fc875a86329f76f
paper_authors.name: Peiyang Song
paper_authors.status: claimed_verified
paper_authors.statusLastChangedAt: 2023-06-28T20:15:48.235Z
paper_authors._id: 649c5cf5c1ae48cf4d7dda34
paper_authors.avatarUrl: /avatars/4b68d0eab119f56a8b82d82fc7955961.svg
paper_authors.fullname: Peiyang Song
paper_authors.type: user
paper_authors.user: p-song1
paper_authors._id: 649b8e7f9fc875a86329f770
paper_authors.name: Shixing Yu
paper_authors._id: 649b8e7f9fc875a86329f771
paper_authors.name: Saad Godil
paper_authors._id: 649b8e7f9fc875a86329f772
paper_authors.name: Ryan Prenger
paper_authors._id: 649b8e7f9fc875a86329f773
paper_authors.name: Anima Anandkumar
paper_title: LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
paper_summary: Large language models (LLMs) have shown promise in proving formal theorems
  using proof assistants such as Lean. However, existing methods are difficult to
  reproduce or build on, due to private code, data, and large compute
  requirements. This has created substantial barriers to research on machine
  learning methods for theorem proving. This paper removes these barriers by
  introducing LeanDojo: an open-source Lean playground consisting of toolkits,
  data, models, and benchmarks. LeanDojo extracts data from Lean and enables
  interaction with the proof environment programmatically. It contains
  fine-grained annotations of premises in proofs, providing valuable data for
  premise selection: a key bottleneck in theorem proving. Using this data, we
  develop ReProver (Retrieval-Augmented Prover): the first LLM-based prover that
  is augmented with retrieval for selecting premises from a vast math library. It
  is inexpensive and needs only one GPU week of training. Our retriever leverages
  LeanDojo's program analysis capability to identify accessible premises and hard
  negative examples, which makes retrieval much more effective. Furthermore, we
  construct a new benchmark consisting of 96,962 theorems and proofs extracted
  from Lean's math library. It features challenging data split requiring the
  prover to generalize to theorems relying on novel premises that are never used
  in training. We use this benchmark for training and evaluation, and
  experimental results demonstrate the effectiveness of ReProver over
  non-retrieval baselines and GPT-4. We thus provide the first set of open-source
  LLM-based theorem provers without any proprietary datasets and release it under
  a permissive MIT license to facilitate further research.
paper_ai_keywords: LeanDojo large language models (LLMs) proof assistants Lean premise selection ReProver Retrieval-Augmented Prover program analysis hard negative examples benchmark GPT-4