search

lean-dojo / LeanCopilot

LLMs as Copilots for Theorem Proving in Lean
https://leandojo.org
MIT License
852 stars 77 forks source link
formal-mathematics lean lean4 llm-inference machine-learning theorem-proving

readme

Lean Copilot: LLMs as Copilots for Theorem Proving in Lean

Lean Copilot allows large language models (LLMs) to be used in Lean for proof automation, e.g., suggesting tactics/premises and searching for proofs. You can use our built-in models from LeanDojo or bring your own models that run either locally (w/ or w/o GPUs) or on the cloud.

https://github.com/lean-dojo/LeanCopilot/assets/114432581/ee0f56f8-849e-4099-9284-d8092cbd22a3

Table of Contents

  1. Requirements
  2. Using Lean Copilot in Your Project
    1. Adding Lean Copilot as a Dependency
    2. Getting Started with Lean Copilot
      1. Tactic Suggestion
      2. Proof Search
      3. Premise Selection
  3. Advanced Usage
    1. Tactic APIs
    2. Model APIs
    3. Bring Your Own Model
  4. Caveats
  5. Getting in Touch
  6. Acknowledgements
  7. Citation

Requirements

Using Lean Copilot in Your Project

:warning: Your project must use a Lean version of at least lean4:v4.3.0-rc2.

Adding Lean Copilot as a Dependency

  1. Add the package configuration option moreLinkArgs := #["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"] to lakefile.lean. For example, 
    package «my-package» {
moreLinkArgs := #[
"-L./.lake/packages/LeanCopilot/.lake/build/lib",
"-lctranslate2"
]
}
  2. Add the following line to lakefile.lean, including the quotation marks: 
    require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "LEAN_COPILOT_VERSION"
    LEAN_COPILOT_VERSION depends on your lean-toolchain: lean-toolchain Recommended Lean Copilot version
    v4.10.0-rc1 v1.4.1
    v4.9.0 v1.4.0
    v4.9.0-rc3 v1.3.3
    v4.9.0-rc2 v1.3.2
    v4.9.0-rc1 v1.3.1
    v4.8.0 v1.3.0
    v4.8.0-rc2 v1.2.2
    v4.8.0-rc1 v1.2.1
    v4.7.0 v1.2.0
    v4.7.0-rc2 v1.1.2
    v4.6.0-rc1 v1.1.1
    v4.5.0 v1.1.0
    v4.5.0-rc1 v1.1.0
  3. Run lake update LeanCopilot
  4. Run lake exe LeanCopilot/download to download the built-in models from Hugging Face to ~/.cache/lean_copilot/
  5. Run lake build

Here is an example of a Lean package depending on Lean Copilot. If you have problems building the project, our Dockerfile, build.sh or build_example.sh may be helpful.

Getting Started with Lean Copilot

Tactic Suggestion

After import LeanCopilot, you can use the tactic suggest_tactics to generate tactic suggestions. You can click on any of the suggested tactics to use it in the proof.

suggest_tactics

You can provide a prefix (e.g., simp) to constrain the generated tactics:

suggest_tactics_simp

Proof Search

The tactic search_proof combines LLM-generated tactics with aesop to search for multi-tactic proofs. When a proof is found, you can click on it to insert it into the editor.

search_proof

Premise Selection

The select_premises tactic retrieves a list of potentially useful premises. Currently, it uses the retriever in LeanDojo to select premises from a fixed snapshot of Lean and mathlib4.

select_premises

Running LLMs

You can also run the inference of any LLMs in Lean, which can be used to build customized proof automation or other LLM-based applications (not limited to theorem proving). It's possible to run arbitrary models either locally or remotely (see Bring Your Own Model).

run_llms

Advanced Usage

This section is only for advanced users who would like to change the default behavior of suggest_tactics, search_proof, or select_premises, e.g., to use different models or hyperparameters.

Tactic APIs

Model APIs

Examples in ModelAPIs.lean showcase how to run the inference of different models and configure their parameters (temperature, beam size, etc.).

Lean Copilot supports two kinds of models: generators and encoders. Generators must implement the TextToText interface:

class TextToText (τ : Type) where
  generate (model : τ) (input : String) (targetPrefix : String) : IO $ Array (String × Float)

We provide three types of Generators:

Encoders must implement TextToVec:

class TextToVec (τ : Type) where
  encode : τ → String → IO FloatArray

Similar to generators, we have NativeEncoder, ExternalEncoder, and GenericEncoder.

Bring Your Own Model

In principle, it is possible to run any model using Lean Copilot through ExternalGenerator or ExternalEncoder (examples in ModelAPIs.lean). To use a model, you need to wrap it properly to expose the APIs in external_model_api.yaml. As an example, we provide a Python API server and use it to run a few models, including llmstep-mathlib4-pythia2.8b.

Caveats

Getting in Touch

Acknowledgements

Citation

If you find our work useful, please consider citing our paper:

@article{song2024towards,
  title={Towards Large Language Models as Copilots for Theorem Proving in {Lean}},
  author={Peiyang Song and Kaiyu Yang and Anima Anandkumar},
  year={2024},
  journal={arXiv preprint arXiv: Arxiv-2404.12534}
}