LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation

This repository contains the implementation of our DoBeVi proposed in the paper: LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation [📄 arXiv:2505.12031]

We thank LeanDojo for its significant contributions to the ATP community, upon which our DoBeVi framework is proudly built.

---

📁 Directory Structure

llm_base_atp/
├── README.md                    # Project documentation
├── Visual/                      # The visualization of tree-search proof results for MiniF2F
├── DoBeVi/                      # Core implementation of DoBeVi
│   ├── requirements.txt         # Python dependencies
│   └── src/                     # Source code
│       ├── __init__.py          # Package initializer
│       ├── dojo/                # Lightweight LeanDojo wrapper for Lean 4 interaction
│       ├── search/              # Proof search algorithms and logic
│       ├── eval.py              # Entry point for evaluation
│       ├── config.py            # Configuration settings 
│       ├── utils.py             # Utility functions
│       └── .env.template        # Template for environment setup

---

⚙️ Setup Instructions

1. Create and Activate Conda Environment

conda create -n dobevi python=3.11 -y
conda activate dobevi

2. Install Python Dependencies

pip install -r requirements.txt

3. Install Graphviz (Required for Visualization)

conda install -c conda-forge graphviz

4. Download the Policy Model

Please download the pretrained policy model from Hugging Face.

---

🧪 Evaluation

Step 1: Prepare a Lean 4 Project

Ensure you have a Lean 4 repository that builds successfully using:

lake build

Step 2: Configure Environment Variables

Copy and edit the template config file to match your local setup:

cd src/
cp .env.template .env

You’ll need to set values for:

• Benchmark project path
• Model path
• Tree search budget
• Output path for results

Step 3: Run the Evaluation

python -m eval

---

🚧 TODO / Future Work

• Release code for synthetic data generation
• Add support for whole-proof methods and fine-tuning

---

🙋 Contributing & Issues

We welcome issues, feature requests, and feedback from the community. Please feel free to open an issue if you encounter any problems or have suggestions!

---

🔗 Related Links

• Hugging Face Model Page

---

📚 Citation

If you use this work in your research, please cite:

@article{lai2025llm,
  title={LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation},
  author={Lai, Junyu and Zhang, Jiakun and Xu, Shuo and Chen, Taolue and Wang, Zihang and Yang, Yao and Zhang, Jiarui and Cao, Chun and Xu, Jingwei},
  journal={arXiv preprint arXiv:2505.12031},
  year={2025}
}