Isabelle MCTS RL Models
This repository contains policy and value models trained with Monte Carlo Tree Search (MCTS) and Reinforcement Learning for automated theorem proving in Isabelle.
Model Structure
policy/: Policy model for proof strategy selectionvalue/: Value model for state evaluation
Training
The models were trained using an MCTS-based training loop employing GRPO (Group Relative Policy Optimization). Training was performed on the miniF2F benchmark for formal mathematics.
Usage
These models can be used for proof generation and evaluation in Isabelle. They are part of a larger pipeline that combines LLMs with formal proof systems.
Project
This work is part of a Bachelor thesis on combining MCTS, LLMs, and Reinforcement Learning for automated theorem proving.
Code Repository
Model Details
- Framework: PyTorch
- Training Method: MCTS + GRPO
- Benchmark: miniF2F
- Target System: Isabelle theorem prover
- Task: Automated theorem proving
