Research | Chapter 4 | Prerequisites: 2-Theoretical-Framework | 56 min read | Home
3. Architecture Specification
3.1 System Overview
┌──────────────────────────────────────────────────────────────────────┐
│ WAYFINDER v1 │
│ │
│ [Lean Goal State Text] │
│ │ │
│ ▼ │
│ ┌─────────────────────────────────────────────┐ │
│ │ GOAL ENCODER (math-native, see §3.2) │ │
│ │ Model: TBD (Qwen3.5/DeepSeek-Math/pruned) │ │
│ │ Output: h_enc ∈ ℝ^embed_dim │ │
│ └─────────────┬───────────────────────────────┘ │
│ │ │
│ ┌────────┴────────┐ │
│ │ │ │
│ ┌────▼─────┐ ┌──────▼───────────────────────────┐ │
│ │ DOMAIN │ │ GOAL ANALYZER │ │
│ │ GATE │ │ (continuous, learnable) │ │
│ │ │ │ Output: features ∈ ℝ^256 │ │
│ │ Binary: │ │ + bank positions (6 banks) │ │
│ │ in/out │ │ + anchor logits │ │
│ └──────────┘ └──────────┬───────────────────────┘ │
│ │ │
│ ┌─────────────────────────▼───────────────────────────────┐ │
│ │ SUBGOAL DECOMPOSER │ │
│ │ Ternary decision: decompose? {-1, 0, +1} │ │
│ │ If +1: predict 'have' subgoals, recurse │ │
│ │ If 0/-1: proceed with current goal │ │
│ └─────────────────────────┬───────────────────────────────┘ │
│ │ (per subgoal) │
│ ┌─────────────────────────▼───────────────────────────────┐ │
│ │ INFORMATION BRIDGE │ │
│ │ Continuous → discrete transition │ │
│ │ Compression to bridge_dim (128) │ │
│ │ LayerNorm + projection │ │
│ └─────────────────────────┬───────────────────────────────┘ │
│ │ │
│ ┌─────────────────────────▼───────────────────────────────┐ │
│ │ PROOF NAVIGATOR (ternary decoder, 6-bank) │ │
│ │ Weights ∈ {-1, 0, +1}, trained via STE │ │
│ │ │ │
│ │ Output heads (3^6 = 729 coarse direction bins): │ │
│ │ • structure_direction ∈ {-1, 0, +1} │ │
│ │ • domain_direction ∈ {-1, 0, +1} │ │
│ │ • depth_direction ∈ {-1, 0, +1} │ │
│ │ • automation_direction ∈ {-1, 0, +1} │ │
│ │ • context_direction ∈ {-1, 0, +1} │ │
│ │ • decompose_direction ∈ {-1, 0, +1} │ │
│ │ • anchor_logits ∈ ℝ^|anchors| (sigmoid) │ │
│ │ • progress ∈ ℝ^1 (remaining) │ │
│ │ • critic ∈ ℝ^1 (solvable?) │ │
│ │ │ │
│ │ Loss: L_nav + λ₁·L_anchor + λ₂·L_progress + λ₃·L_critic│ │
│ │ (adaptive λ via learned log-σ uncertainty) │ │
│ └─────────────────────────┬───────────────────────────────┘ │
│ │ │
│ ┌─────────────────────────▼───────────────────────────────┐ │
│ │ STRUCTURED RESOLUTION (deterministic, no NN) │ │
│ │ │ │
│ │ navigate(tactic_network, directions + anchors) → tactic │ │
│ │ navigate(premise_network, directions + anchors) → lemmas │ │
│ │ spread(proof_network, current_goals) → search priority │ │
│ └─────────────────────────┬───────────────────────────────┘ │
│ │ │
│ ┌─────────────────────────▼───────────────────────────────┐ │
│ │ DETERMINISTIC LOWERING │ │
│ │ Tactic + premises → Lean syntax string │ │
│ └─────────────────────────┬───────────────────────────────┘ │
│ │ │
│ ▼ │
│ [Lean 4 Kernel: verify tactic, return new goals or error] │
│ │ │
│ ▼ │
│ [Update proof network: new goals → new seeds for spread()] │
└──────────────────────────────────────────────────────────────────────┘
3.2 Goal Encoder
Status: Encoder selection is an active design decision. The original prototype used all-MiniLM-L6-v2, but the encoder is the system's perceptual bottleneck and deserves more aggressive investment.
The problem with small general-purpose encoders: Lean goal states are formal syntax with type annotations, unicode math symbols, and dependent type structure — not natural language. A sentence-transformer trained on English text will produce mediocre embeddings for ⊢ ∀ (x : α) [inst : TopologicalSpace α], IsOpen (⋃ i, s i). If two goal states are semantically different in math but look similar as strings, the encoder conflates them, and no amount of downstream projection can recover the lost information.
Encoder strategy — four tiers under evaluation:
1. Byte-level models (strong candidate). ByT5-small (299M) is the de facto standard for Lean, used by ReProver, LeanAgent, and Lean Copilot. Its byte-level operation handles Lean's Unicode symbols (∀, ⊢, →, ℕ, ⋃) without tokenization artifacts — a critical advantage over subword tokenizers that fragment mathematical notation. ByT5-small produces 1472-dimensional embeddings via average pooling. Training requires only 120 GPU hours. A Lean-specific retrained tokenizer variant (arXiv 2501.13959) achieves 30.74% vs ReProver's 28.28% on MiniF2F. However, ByT5 has no mathematical pretraining — it is a generic byte-level model.
2. Math-native models (preferred if byte-level gap is addressed). Recent releases like Qwen 3.5, DeepSeek-Math, and InternLM-Math are trained on mathematical corpora including formal languages. These models understand Lean-like syntax natively. A math-native encoder (even at 1-7B parameters) will produce dramatically better embeddings for goal states than any general-purpose sentence transformer. The risk: most math-native models use subword tokenizers that may fragment Lean syntax. Evaluate both byte-level and subword-based math models.
3. Ternary/BitNet encoder (architecturally distinctive). BitNet b1.58 (ternary weights, 1.58 bits/parameter) at 2B matches full-precision models on mathematical reasoning benchmarks with 2.7× speedup and 3.5× memory reduction — but no one has applied ternary architectures to formal theorem proving. Since Wayfinder already uses ternary weights in the decoder (TernaryLinear with STE), extending ternary quantization to the encoder would be architecturally consistent and could enable real-time premise retrieval. A ternary encoder is the most distinctive option and would make the full pipeline ternary-native.
4. Aggressively pruned large models. Recent work on structured pruning demonstrates that ~95-99% of nodes can be removed from large generalist models while retaining domain-specific performance, especially when followed by brief fine-tuning on in-domain data. Quantization to 4-bit introduces up to 32% accuracy degradation on math benchmarks, but fine-tuning on just 545 task-specific examples for 3 minutes can recover full performance. A 4-bit quantized 14B still outperforms its dense 7B counterpart. Techniques: structured pruning (SparseGPT, Wanda), layer dropping, distillation, and post-pruning fine-tuning on Mathlib goal states.
Key design constraint: The encoder may be frozen or fine-tuned, but the downstream architecture (GoalAnalyzer, Bridge, Navigator) must work with either. The encoder's output dimensionality is a configuration parameter (embed_dim in configs/base.yaml), not hardcoded.
Evaluation criterion: Encoder quality is measured by navigational accuracy at Phase 1 (smoke test). If navigational accuracy on 1-2 step proofs plateaus below 60% after 500 training steps, the encoder is the prime suspect and should be upgraded before debugging other components.
3.3 Goal Analyzer
Parameters: ~100K (learnable) Input: 384-dim embedding from encoder Output: 256-dim feature vector + bank position estimates + anchor logits
The GoalAnalyzer serves three functions:
1. Feature projection: Linear projection from 384 to 256 dimensions. Extracts proof-relevant features from the general-purpose sentence embedding. 2. Bank position estimation: Six classification heads, one per proof bank. Each predicts (sign, depth) for the goal state. Used to position the current goal in the semantic network. 3. Anchor extraction: Multi-label classification over the anchor dictionary. Predicts which semantic labels apply to the current goal state.
Bank positions and anchors enable the navigational queries that follow. The analyzer bridges the continuous embedding space and the structured semantic network.
3.4 Subgoal Decomposer
Parameters: ~50K (learnable) Input: 256-dim features from GoalAnalyzer Output: Ternary decomposition decision + subgoal projections
Inspired by DeepSeek-Prover-V2's proof sketching, the SubgoalDecomposer decides whether to decompose the current goal into subgoals via have statements:
- -1 (atomize): The goal is already atomic. Proceed directly to tactic prediction.
- 0 (neutral): No decomposition signal. Proceed with current goal.
- +1 (decompose): The goal should be broken into subgoals. Predict subgoal count and project features for each subgoal.
When decomposing, each subgoal gets its own feature vector (via learned projection heads) and is processed independently through the rest of the pipeline. This implements Mutation Theory Phase 3's separableIndependentTesting: independent subgoals can be solved independently.
3.5 Information Bridge
Parameters: ~33K (learnable) Input: 256-dim features Output: 128-dim compressed representation
The bottleneck between continuous and discrete space. LayerNorm + linear projection compresses the feature representation to a dimensionality suitable for the ternary decoder.
Information-theoretic role: The bridge tests the hypothesis that the mutual information between goal understanding and tactic selection is low-dimensional. If a 128-dim bridge suffices for accurate navigation, the goal→tactic mapping has low intrinsic dimensionality.
3.6 Proof Navigator (Ternary Decoder)
Parameters: ~200K (learnable, ternary hidden layers) Input: 128-dim bridge output Output: 6 navigational directions + anchor logits + progress + critic
The core innovation. Unlike a traditional decoder that classifies into a tactic vocabulary, the Proof Navigator outputs directions in proof space. The expanded 6-bank design (see Section 2.5) gives 3^6 = 729 coarse direction bins, resolving the many-to-one problem where semantically distinct tactics collapsed to the same coordinates.
Ternary direction heads (hidden layers use TernaryLinear with STE, one per navigable bank):
structure_direction ∈ {-1, 0, +1}: Simplify / maintain / complexifydomain_direction ∈ {-1, 0, +1}: Concrete / general / abstractdepth_direction ∈ {-1, 0, +1}: Shallow / moderate / deepautomation_direction ∈ {-1, 0, +1}: Automate / mixed / manualcontext_direction ∈ {-1, 0, +1}: Reduce context / maintain / enrich contextdecompose_direction ∈ {-1, 0, +1}: Atomize / maintain / decompose
Continuous heads (standard linear, on top of ternary hidden layers):
anchor_logits ∈ ℝ^|anchors|: Which semantic labels should the next tactic/premises haveprogress ∈ ℝ^1: Estimated remaining proof steps (MSE loss against ground truth). Connects to Mutation Theory's Lyapunov convergence guarantee (T7.5) — when progress decreases monotonically, convergence is formally guaranteed. LeanProgress showed that including proof history boosts accuracy from 61.8% to 75.1%. We incorporate this by concatenating embeddings of previously closed goals into the bridge input (see Section 3.10 for details).critic ∈ ℝ^1: Estimated distance to proof completion (MSE loss), NOT binary solvability. HTPS found that hard binary critic targets (solvable/not-solvable) are worse than no critic at all — even worse than random. Soft targets dramatically outperform: 78.1% vs 63.1% on their benchmark. AlphaProof similarly trains its value function to predict remaining tactic count rather than binary provability, because all proven states have probability 1.0, destroying the training signal. Our critic head predicts a continuous distance metric (normalized remaining steps / budget consumed), trained with MSE loss.
Training loss (UW-SO adaptive weighting via learned log-σ):
L_total = (1/2σ₁²)·L_nav + (1/2σ₂²)·L_anchor + (1/2σ₃²)·L_progress
+ (1/2σ₄²)·L_critic + log(σ₁σ₂σ₃σ₄)
Where:
L_nav: Cross-entropy on navigational directions (ternary classification, 6 banks, summed)L_anchor: Binary cross-entropy on anchor predictionsL_progress: MSE on remaining-step predictionL_critic: MSE on normalized distance-to-completion (soft target, NOT binary BCE — per HTPS finding)
The navigable_banks configuration parameter controls which banks are active. Setting navigable_banks: [STRUCTURE, AUTOMATION, DECOMPOSITION] reverts to 3-bank navigation (27 bins) if the full 6-bank version proves too hard to learn.
3.7 Proof Network (Semantic Database)
Storage: SQLite database (single file, ~100MB for full Mathlib) Entities: Lemmas, tactics, proof patterns Schema (adapted from ModelAtlas):
-- Mathematical entities (lemmas, definitions, instances)
CREATE TABLE entities (
entity_id TEXT PRIMARY KEY,
kind TEXT, -- 'lemma', 'def', 'instance', 'tactic'
namespace TEXT,
display TEXT
);
-- Bank positions (6 proof banks)
CREATE TABLE entity_positions (
entity_id TEXT REFERENCES entities(entity_id),
bank TEXT,
sign INTEGER,
depth INTEGER,
PRIMARY KEY (entity_id, bank)
);
-- Anchor dictionary
CREATE TABLE anchors (
anchor_id INTEGER PRIMARY KEY AUTOINCREMENT,
label TEXT UNIQUE,
bank TEXT,
source TEXT DEFAULT 'deterministic'
);
-- Entity ↔ anchor links
CREATE TABLE entity_anchors (
entity_id TEXT REFERENCES entities(entity_id),
anchor_id INTEGER REFERENCES anchors(anchor_id),
confidence REAL DEFAULT 1.0,
PRIMARY KEY (entity_id, anchor_id)
);
-- Explicit links (dependency, co-occurrence)
CREATE TABLE entity_links (
source_id TEXT REFERENCES entities(entity_id),
target_id TEXT REFERENCES entities(entity_id),
relation TEXT, -- 'depends_on', 'commonly_precedes', 'same_namespace'
weight REAL DEFAULT 1.0,
PRIMARY KEY (source_id, target_id, relation)
);
-- IDF cache
CREATE TABLE anchor_idf (
anchor_id INTEGER PRIMARY KEY,
idf_value REAL
);
Population: Deterministic extraction from Mathlib's Lean source: 1. Parse all theorem/lemma declarations → entities table 2. Extract types and namespaces → bank positions 3. Analyze proof text for tactic usage → anchors 4. Walk import graph → dependency links 5. Compute IDF from anchor frequencies
3.8 Structured Resolution
The resolution layer converts the Proof Navigator's output into concrete tactics and premises. No neural inference — pure symbolic operations:
def resolve(nav_output, proof_network, current_context):
"""Convert navigational coordinates to tactic + premises."""
# Build structured query from ternary directions + anchor logits
query = StructuredQuery(
structure=nav_output.structure_direction,
automation=nav_output.automation_direction,
decomposition=nav_output.decompose_direction,
prefer_anchors=top_k_anchors(nav_output.anchor_logits, k=8),
avoid_anchors=current_context.recently_failed,
)
# Navigate tactic space
tactic_candidates = navigate(proof_network.tactic_table, query, limit=5)
# Navigate premise space
premise_candidates = navigate(proof_network.lemma_table, query, limit=16)
# Spreading activation from current proof context
context_activation = spread(
proof_network,
seeds=current_context.used_lemmas + current_context.open_goals,
banks=["DOMAIN", "STRUCTURE"],
max_depth=3,
)
# Combine: navigate score × spreading activation
for p in premise_candidates:
p.score *= context_activation.get(p.entity_id, 0.1)
return tactic_candidates, sorted(premise_candidates, key=lambda p: p.score, reverse=True)
3.9 Deterministic Lowering
Template-based conversion from (tactic, premises) to Lean syntax:
def lower_step(tactic, premises, context):
if tactic.name in NULLARY_TACTICS: # omega, ring, linarith, ...
return tactic.name
if tactic.name in PREMISE_TACTICS: # apply, exact, rw, ...
return f"{tactic.name} {' '.join(p.name for p in premises)}"
if tactic.name == "have":
return f"have {premises[0].name} := by"
# ... etc
This is the existing lowering.py module, adapted to accept navigational resolution output instead of tier tokens.
3.10 Lean Kernel Interaction
The outer proof search loop interacts with the Lean kernel via Pantograph (LeanDojo's interaction protocol):
while open_goals:
goal = select_goal(open_goals, critic_scores, progress_estimates)
# Neural forward pass (ONCE per goal)
embedding = encoder.encode(goal.state)
features = analyzer(embedding)
nav_output = navigator(bridge(features))
# Symbolic resolution (fast, no NN)
tactics, premises = resolve(nav_output, proof_network, context)
# Try candidates (interaction with Lean kernel)
for tactic, premise_set in product(tactics[:3], premise_combinations(premises)):
lean_text = lower_step(tactic, premise_set, context)
result = lean_kernel.try_tactic(goal.state, lean_text)
if result.success:
open_goals.remove(goal)
open_goals.extend(result.new_goals)
context.record_success(tactic, premise_set)
break
else:
context.record_failure(tactic, premise_set)
Goal selection uses the critic head (estimated distance-to-completion) and progress head (estimated remaining steps). Prioritize goals with lowest combined distance estimate.
Proof history input. LeanProgress demonstrated a 13-point accuracy improvement (61.8% → 75.1%) from including proof history in progress prediction. The spreading activation mechanism captures this symbolically (seeds from already-used lemmas), but the neural side also benefits. At each goal, the encoder receives not just the current goal state but also a summary of proof context: embeddings of previously closed goals are mean-pooled and concatenated to the bridge input. This gives the progress and critic heads access to "where we've been," not just "where we are."
Sources: docs/WAYFINDER_RESEARCH.md