Goedel-LM/RL_dataset_V2
收藏Hugging Face2026-03-02 更新2026-04-05 收录
下载链接：
https://hf-mirror.com/datasets/Goedel-LM/RL_dataset_V2
下载链接
链接失效反馈官方服务：
资源简介：
---
pretty_name: Goedel-Prover-V2 RL Dataset
language: en
license: apache-2.0
tags:
- theorem-proving
- lean4
- code
size_categories: 100K<n<1M
configs:
- config_name: default
data_files:
- split: train
path: data/train-*
dataset_info:
features:
- name: subset
dtype: string
- name: messages
list:
- name: content
dtype: string
- name: role
dtype: string
splits:
- name: train
num_bytes: 1059173933.03536
num_examples: 98632
download_size: 336508509
dataset_size: 1059173933.03536
---
# Goedel-Prover-V2 RL Dataset
This dataset contains RL data with two task subsets.
- `lean4_completion`: Whole Proof Generation
- `lean4_revision`: self-revision
See [Goedel-Prover-V2 paper](https://arxiv.org/abs/2508.03613).
## Citation
```
@article{lin2025goedel,
title={Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction},
author={Lin, Yong and Tang, Shange and Lyu, Bohan and Yang, Ziran and Chung, Jui-Hui and Zhao, Haoyu and Jiang, Lai and Geng, Yihan and Ge, Jiawei and Sun, Jingruo and others},
journal={arXiv preprint arXiv:2508.03613},
year={2025}
}
```
提供机构：
Goedel-LM
