Phase 9: RL-Guided Exploration (tentative)

[quinn-dougherty]

Phase 9: RL-Guided Exploration

Tentative / long-term. DeepSeek-Prover v2 demonstrated that an RL-trained AI system can exploit subtle Lean bugs. This validates our LLM-guided approach and suggests RL-based exploration as a high-leverage future direction.

Status: NOT STARTED (speculative/long-term)

Ref: docs/design-plan.md Phase 9

---

Reward signal design

Use the tiered corpus classification (Phase 4) as the reward function:

Outcome	Reward
Prefix doesn't compile	0.0
Prefix compiles, golden suffix has type error	0.3
Prefix compiles, golden suffix fails with "proof not found"	0.7 (Tier 0)
Prefix compiles, golden suffix succeeds (soundness bug!)	1.0

Policy architecture

• Fine-tune a small LM (e.g., CodeLlama-7B or similar) to generate prefixes
• Training data: Tier 0/1 prefixes from Phases 1-6 as positive examples
• Rejection sampling initially, then PPO/DPO once enough signal accumulates
• Input: attack category + optional seed prefix; Output: complete prefix

Integration with UCB1 bandits

• UCB1 bandits from Phase 5 select attack categories at the macro level
• Within each category, RL policy generates specific prefixes
• Two-level exploration: bandits explore which attack surfaces, RL explores how to attack each surface

Prerequisites

• Sufficient training data from Phases 1-6 (likely thousands of Tier 0/1 prefixes)
• Demonstrated ceiling on LLM-guided generation without RL
• Compute budget for RL training runs

Earliest feasible start: after Phases 1-5 are mature and producing corpus data.