Experiment Plan | Chapter 7 | Prerequisites: Phase-4 | 28 min read | Home
Phase 5: Scale and Extend (Week 9+, contingent on results)
5.1 Enriched Proof Network
If navigational retrieval underperforms dense retrieval:
- Add LLM-based anchor extraction (Tier 3) for subtle mathematical properties
- Add cross-namespace links from proof co-occurrence analysis
- Experiment with finer-grained bank positions (depth 3-4 instead of 1-2)
5.2 Online Learning with Navigational Wavefront Curriculum
If proof search works but slowly improves:
- Update proof network links based on successful proofs (HTPS-inspired online training)
- Add new anchors discovered from proof patterns
- Re-compute IDF as the network evolves
- Navigational wavefront curriculum: Order new training theorems by distance in the proof network from already-proven results. Spread activation from the set of proven theorems; the frontier (theorems 1-2 hops away with highest activation) defines the next training batch. This addresses the saturation problem: up to 98.5% of proofs during expert iteration are incorrect. By targeting the "cusp of provability" (STP found 47% success on cusp-generated conjectures vs 11.4% on random unproved), training signal is dramatically denser.
5.3 Hybrid Retrieval
If navigational and dense retrieval have complementary strengths:
- Use navigational retrieval for initial candidate set (fast, high recall)
- Re-rank with dense retrieval for top-k precision (one neural forward pass for k candidates)
- Compare to pure-dense and pure-navigational
5.4 Subgoal Decomposition Training
If the SubgoalDecomposer shows promise in ablations:
- Train on DeepSeek-Prover-V2-style
have-chain examples - Evaluate decomposition quality independently
- Measure impact on longer proofs (5+ steps)
Sources: docs/WAYFINDER_PLAN.md