Let's Explore Step by Step

Official implementation for the paper:

[ICLR'26] Let's Explore Step by Step: Generating Provable Formal Statements with Deductive Exploration

Qi Liu, Kangjie Bao, Yue Yang, Xinhao Zheng, Renqiu Xia, Qinxiang Cao, Junchi Yan*

School of Computer Science & School of Artificial Intelligence, Shanghai Jiao Tong University

Shanghai Innovation Institute

(∗Corresponding author)

🤗Collection 📃Paper

Quick Start

1. Install and Build Dependencies: Follow Python Dependencies and Lean 4 Dependencies.
2. Download Model: Download 🤗purewhite42/DExplorer-8B.
3. Generate Formal Statements & Proofs: Deploy the model(s) and run DExplorer:

# Deploy DExplorer (replace /path/to/DExplorer-8B with the real path)
python -m vllm.entrypoints.openai.api_server \
    --model /path/to/DExplorer-8B \
    --port 37210 \
    --dtype bfloat16 \
    --api-key iclr26_dexploration \
    --trust-remote-code \
    --enable-prefix-caching \
    --disable-log-requests \
    --max-model-len 8192 &

# Explore mathematics step-by-step under Lean verification
ulimit -s unlimited;
python -m agent.problem_generation \
    --log_root output/DExplorer-8B \
    --num_generation_attempt 5000 \
    --base_url http://0.0.0.0:37210/v1 \
    --api_key iclr26_dexploration \
    --model_name /path/to/DExplorer-8B \
    --n_servers 1 \
    --falsify_n_servers 0 \
    --project_root /path/to/mathlib4 \
    --num_concurrency 16

Note: Set falsify_n_servers to:

• -1: Disable contradiction detection
• 0: Use Aesop (default) for contradiction detection
• N > 0: Use N additional LLM-based provers for contradiction detection

Optional: Enhanced Contradiction Detection

For stronger contradiction detection, deploy an additional lightweight LLM prover:, e.g. DeepSeek-Prover-V2-7B (non-CoT):

# Deploy contradictory prover (replace /path/to/DeepSeek_nonCoT-Prover-V2-7B with the real path; Add "nonCoT" in the model name to dispatch to the non-CoT prompt template.)
python -m vllm.entrypoints.openai.api_server \
    --model /path/to/DeepSeek_nonCoT-Prover-V2-7B \
    --port 37211\
    --dtype bfloat16 \
    --api-key theorem_proving \
    --trust-remote-code \
    --enable-prefix-caching \
    --disable-log-requests \
    --max-model-len 8192 &

Then add these arguments to the DExplorer command:

    --falsify_base_url http://0.0.0.0:37211/v1 \
    --falsify_api_key theorem_proving \
    --falsify_model_name /path/to/DeepSeek_nonCoT-Prover-V2-7B \
    --falsify_n_servers 1 \

Generated formal statements and their proofs are saved under output/DExplorer-8B/. Each result is a JSON file containing the generated theorem statement, its proof, and the exploration trajectory.

Project Structure

.
├── agent/
│   ├── problem_generation.py   # DExploration agent (main entry point)
│   └── proof_generation.py     # Best-first proof search agents & Whole-proof generation agents
├── common/
│   ├── pantograph/             # Lean 4 interaction via Pantograph REPL
│   │   ├── server.py           # Pantograph server
│   │   ├── dataclasses.py      # Lean data types (GoalState, Goal, etc.)
│   │   └── parsing_server.py   # Pantograph server w/ finer-grained delaboration
│   ├── constants.py            # Prompts, regex patterns, Lean options
│   └── utils.py                # Shared utilities (code extraction, formatting)
├── data/
│   ├── conditions.json         # Exploration conditions
│   └── pantograph.patch        # Patch for Pantograph v0.2.25
├── train_recipes/
│   └── DExplorer-8B.py         # XTuner SFT training configuration
├── requirements.txt            # Python dependencies
└── README.md

Installation

Python Dependencies

pip install -r requirements.txt

Key packages and tested versions:

Lean 4 Dependencies

We recommend using elan to manage Lean versions:

# Install elan
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

# Set default Lean version
elan default leanprover/lean4:v4.15.0 

# Verify installation
lean --version  # Should show v4.15.0

# Clone and build Pantograph
git clone https://github.com/leanprover/Pantograph.git
cd Pantograph
git checkout v0.2.25

# Apply our patch (enables variable-level goal tracking needed by DExploration)
git apply /path/to/main_project/data/pantograph.patch

# Build the project
lake build

# Create symbolic links
ln -s $(pwd)/lean-toolchain /path/to/main_project/common/pantograph/lean-toolchain
ln -s $(pwd)/.lake/build/bin/repl /path/to/main_project/common/pantograph/pantograph-repl

The final structure will look like this:

.
├── common
│   ├── pantograph
│   │   ├── lean-toolchain -> /path/to/Pantograph/lean-toolchain
│   │   ├── pantograph-repl -> /path/to/Pantograph/.lake/build/bin/repl

🎓 Training

Data Preparation

The training data consists of 301,909 (Proof State, DExploration Action) single-step pairs extracted from 39,509 DExploration trajectories, organized as single-turn conversations:

Download from HuggingFace or prepare your own data in the same format.

Training Configuration

Our model is supervised fine-tuned (SFT) from Goedel-Prover-V2-8B with the following hyperparameters (see train_recipes/DExplorer-8B.py):

• Learning rate: 2e-5
• Batch size: 1 per device × 64 accumulative counts × 8 GPUs = 512 global batch size
• Max length: 8192 tokens
• Epochs: 3
• Warmup ratio: 0.03

Launch Training

# Launch training on 8 devices
NPROC_PER_NODE=8 xtuner train ./train_recipes/DExplorer-8B.py --deepspeed deepspeed_zero2;

# Convert checkpoint to HuggingFace format
# (XTuner saves training ckpts at `./work_dirs`)
xtuner convert pth_to_hf \
    train_recipes/DExplorer-8B.py \
    work_dirs/DExplorer-8B/epoch_1.pth \
    models/DExplorer-8B/

Note: The training config defaults to Ascend NPU (backend='hccl'). If using CUDA devices, change line 183 of the training config to backend='nccl'. For other accelerators (XPU/TPU), adjust accordingly.

📄 Citation

If you find our work useful in your research, please cite:

@inproceedings{
liu2026lets,
title={Let's Explore Step by Step: Generating Provable Formal Statements with Deductive Exploration},
author={Qi Liu and Kangjie Bao and Yue Yang and Xinhao Zheng and Renqiu Xia and Qinxiang Cao and Junchi Yan},
booktitle={The Fourteenth International Conference on Learning Representations},
year={2026},
url={https://openreview.net/forum?id=Njrkeo3DiJ}
}

©️ License

This project is released under the Apache 2.0 license. See LICENSE for details.

🤝 Contributing

We welcome contributions! Please feel free to submit issues or pull requests.

📧 Contact

For questions about the paper, data, or code:

• Qi Liu: [email protected]
• Issues: GitHub Issues

👍 Acknowledgments

• NuminaMath-LEAN for the high-quality statement-proof data.
• Goedel-Prover for the base model.
• Pantograph for Lean 4 interaction.
• And many other open-source projects!