lean-reinforcement 0.1.1

Reinforcement learning for Lean theorem proving

LeanReinforcement

Repository for LeanReinforcement (LR), a Monte Carlo Tree Search (MCTS) agent building on the ReProver system.

Gym-like

This repository builds on the gym-like LeanDojo interface for interacting with Lean. See the LeanDojo documentation for more information on how to use it.

Monte Carlo Tree Search

Relevant sources will be added here as the project progresses.

TODO

• Import ReProver weights to Snellius
• Set up premise retrieval code
• Create gym environment with LeanDojo and OpenAI Gym
• Decide PPO vs MCTS => MCTS on top of ReProver
• Update Snellius environment
• Import LeanDojo benchmark to Snellius
• Look into LeanDojo step time, value functions, etc.
• Implement runner script to run MCTS agent on LeanDojo environment
• Implement appropriate DataLoader training and evaluation
• Implement training loop
• Run experiments on Snellius
• Finish in-comment ToDo's
  • Checkpoint saving and loading
  • Subtree reusage
  • Reimplement tactic generator fine-tuning
• Implement ValueHead Dataset creation
• Set up wandb/tensorboard equivalent logging