GAR Base Dataset

This repository contains the base dataset used in the paper GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving.

GAR (Generative Adversarial Reinforcement learning) is a comprehensive RL training framework that jointly trains a problem composer and a solver in an adversarial loop. This dataset serves as the starting point for the implicit curriculum learning mechanism, which aligns task difficulty with the prover's evolving capability to improve training efficiency in verifiable languages like Lean.

• Repository: https://github.com/RickySkywalker/GAR-Official
• Paper: GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

Usage

You can load the dataset and transform it into the JSON format required for the GAR training pipeline using the following snippet:

from datasets import load_dataset

# Load the dataset
ds = load_dataset("RickyDeSkywalker/GAR_baseDataset_NuminaMath")

# Transform the dataset into JSON form for training
ds["train"].to_json("./base_data/GAR_base_data_Numina-Math.json")

Citation

@article{wang2025gar,
  title={GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving},
  author={Wang, Ruida and Yao, Jiarui explorer, Pan, Rui and Diao, Shizhe and Zhang, Tong},
  journal={arXiv preprint arXiv:2510.11769},
  year={2025}
}