Reinforcement Learning with Verification
Training methodology that uses formal verification as reward signal for reinforcement learning, providing much stronger feedback than statistical approaches like RLHF or GRPO. Pioneered by axiom-math as core component of verified-ai systems.
Core Concept
Stronger Reward Signals: Instead of relying on statistical approximations (GRPO, RLHF), verification provides binary correct/incorrect feedback through lean-proofs verification. This is analogous to compiling and testing code rather than guessing correctness.
Training Loop:
- Model generates mathematical reasoning or proofs
- lean-proofs verifier checks correctness mechanically
- Verification result provides immediate, precise reward signal
- Model learns from definitive feedback rather than statistical approximations
Advantages
Sample Efficiency: Precise feedback enables faster learning compared to statistical methods that rely on human preferences or approximations.
Maximum Performance: Verification provides objective ceiling for correctness rather than subjective quality assessments.
Compounding Training Data: Verified proofs become high-quality training examples that can be trusted for future training, unlike informal reasoning that may contain subtle errors.
Objective Optimization: Removes human preference biases and statistical noise from training signal.
Technical Implementation
Verification Integration: Uses formal verification engines (like Lean theorem prover) as part of training infrastructure rather than post-hoc validation.
Reward Structure: Binary correct/incorrect signals provide cleaner optimization landscape compared to continuous preference scores.
Curriculum Learning: Can progressively tackle more complex proofs as verification capabilities improve.
Performance Results
axiom-math reports significant advantages using this approach:
- Perfect 12/12 putnam-mathematical-competition score
- 99% (187/189) on proofgen-benchmark vs OpenAI o3's 4.9%
- Superior performance to models trained with statistical methods
Comparison with Statistical Methods
GRPO/RLHF Limitations:
- Rely on human preferences or statistical approximations
- Subject to bias and inconsistency
- Cannot compound knowledge reliably
- Provide weaker optimization signals
Verification Advantages:
- Mathematically precise feedback
- Enables knowledge compounding
- Objective optimization target
- Higher sample efficiency
Implementation Challenges
Lean Generation Difficulty: Current LLMs struggle to generate valid lean-proofs directly, requiring specialized training approaches.
Specification Bottleneck: Must translate informal problems into formal specifications that can be verified.
Computational Overhead: Formal verification adds computational cost compared to statistical approximations.