isabelle-mcts-rl

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 selection
• value/: 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

https://github.com/chrissiwaffler/bsc-thesis-mcts-rl-isabelle

Model Details

• Framework: PyTorch
• Training Method: MCTS + GRPO
• Benchmark: miniF2F
• Target System: Isabelle theorem prover
• Task: Automated theorem proving