Skip to content

README.md

Latest commit

 

History

History
41 lines (29 loc) · 1.23 KB

README.md

File metadata and controls

41 lines (29 loc) · 1.23 KB
Raw

Training Component

This component contains the verl-based training stack used by OProver. The public examples area is intentionally minimal: only files actually used by the OProver RL/SFT pipeline are kept.

Supported Entrypoints

RL training:

bash components/verl/examples/grpo_trainer/prover_rl_new/oprover_32b.sh

SFT examples:

components/verl/examples/sft/oprover/

OProver data preprocessing helpers:

components/verl/examples/data_preprocess/

Core Implementation Areas

  • recipe/dapo/: DAPO/GSPO trainer entry and configs
  • verl/: trainer, rollout, dataset, and reward implementation
  • verl/utils/reward_score/lean4_verifier.py: Lean verifier reward
  • examples/grpo_trainer/prover_rl_new/oprover_32b.sh: parameterized RL launcher
  • examples/grpo_trainer/prover_rl_new/run_commands_on_ray_cluster.py: Ray node command helper
  • examples/grpo_trainer/prover_lean4_server/run_local_lean4.sh: Lean verifier server helper

Relation to upstream verl

This tree is a snapshot of volcengine/verl with non-OProver recipes (prime, retool, spin, r1, gspo, …) and CI configuration removed. Install upstream verl directly if you want the full recipe catalog.