Ahmad and Journee — this one's for her.
Journee pointing at the world she'll inherit.
-blueviolet){kind=icon}
Go faster without becoming different.
JOURNEE is a transformer built around a very specific constraint:
P[emit = x] = p(x)
The runtime is allowed to accelerate the journey from input to output.
It is not allowed to change the target distribution along the way.
JOURNEE is a speculative-decoding transformer architecture that separates proposal from authority.
A smaller or cheaper draft path moves ahead.
The target model remains the source of truth.
INPUT
│
▼
┌─────────────┐
│ Token Embed │
└──────┬──────┘
│
▼
┌─────────────────┐
│ Transformer │
│ Representation │
└────────┬────────┘
│
▼
┌──────────────────┐
│ Draft / Proposal │
│ Path │
└────────┬─────────┘
│
proposed tokens
│
▼
┌────────────────────┐
│ Target Transformer │
│ Verification │
└─────────┬──────────┘
│
accept / reject
│
┌───────────┴───────────┐
▼ ▼
accepted rejected
proposal mass
│ │
└───────────┬───────────┘
▼
OUTPUT TOKEN
The important distinction is:
Draft model:
What might come next?
Target model:
What distribution actually governs the next token?
The draft is allowed to be wrong.
The target is not replaced.
A transformer is fundamentally a sequence-processing machine.
Tokens enter as vectors. Those vectors are repeatedly transformed into representations that encode relationships between positions in the sequence.
A simplified JOURNEE path looks like:
Tokens
│
▼
Embedding
│
▼
Position Information
│
▼
┌──────────────────────────────┐
│ Transformer Block │
│ │
│ ┌────────────────────────┐ │
│ │ Attention │ │
│ │ │ │
│ │ Q ──┐ │ │
│ │ K ──┼──► Attention │ │
│ │ V ──┘ │ │
│ └───────────┬────────────┘ │
│ │ │
│ ▼ │
│ Residual Stream │
│ │ │
│ ▼ │
│ ┌────────────────────────┐ │
│ │ Sparse Boolean MoE │ │
│ │ │ │
│ │ 🧭 Router │ │
│ │ ├── 🧠 Syntax │ │
│ │ ├── 🔢 Quantity │ │
│ │ ├── 🧩 Relation │ │
│ │ └── ⚡ Action │ │
│ └───────────┬────────────┘ │
│ │ │
│ ▼ │
│ Residual Stream │
└──────────────┬───────────────┘
│
▼
Output Logits
│
▼
Probability
Distribution
│
▼
Token
The transformer does not directly produce a word.
It produces a distribution over possible next tokens.
That distinction is fundamental to JOURNEE.
Attention gives the transformer a mechanism for relating one position to other positions in the sequence.
sequence
│
┌──────────┼──────────┐
▼ ▼ ▼
Q K V
│ │ │
└─────┬────┘ │
│ │
▼ │
compatibility │
│ │
▼ │
weights ───────────┘
│
▼
contextual representation
Each token receives information conditioned on the surrounding sequence.
JOURNEE does not treat this machinery as an excuse to abandon the target model. It treats it as the computational substrate from which the target distribution is produced.
Transformer blocks repeatedly modify a shared representation.
┌───────────────┐
│ │
▼ │
Input ───────► Block ───────► Block ───────► Block
│ │ │
└──────────────┴───────────────┘
residual information
After enough layers, the final representation is projected into logits:
Hidden State
│
▼
Output Projection
│
▼
Logits
│
▼
Normalization
│
▼
p(x)
That final distribution is what JOURNEE protects.
JOURNEE's fourth block uses a sparse Boolean mixture-of-experts.
Instead of every expert processing every token, the router selects only the computation that should participate:
Token
│
▼
🧭 Router
│
┌────────┼────────┐
│ │
▼ ▼
🧠 Syntax ⚡ Action
(articles, affixes) (verbs, commands)
│ │
└────────┬────────┘
▼
Combined State
│
🔁 Inverter
│
▼
Residual Output
| Expert | Role | Activates for |
|---|---|---|
| 🧠 Syntax | Agreement, position features | Articles, affixes, punctuation |
| 🔢 Quantity | Count, magnitude, comparison | Numbers, units, quantifiers |
| 🧩 Relation | Link and dependency features | Prepositions, references, entities |
| ⚡ Action | Transition / predicate features | Verbs, operators, commands |
| 🔁 Invert | Complement, correction | Negation, absence, contradiction |
The point of sparsity is computational. The point of the target invariant is semantic. These are separate concerns:
SPARSITY → less computation
SPECULATION → less sequential waiting
TARGET VERIFY → preserve distribution
JOURNEE combines all three.
Normal autoregressive decoding:
Token → Target → Next Token → Target → Next Token → Target → Next Token
The target model repeatedly waits for itself.
Speculative decoding changes the execution pattern:
TARGET
│
▼
verification
│
┌────────────┴────────────┐
│ │
▼ ▼
proposal 1 proposal 2
│ │
└────────────┬────────────┘
▼
verify
│
┌──────┴──────┐
▼ ▼
accept reject
The optimization is not: replace target model.
It is: predict ahead + verify against target.
Let p(x) be the target probability distribution.
Let P[emit = x] be the probability the complete speculative procedure actually emits token x.
JOURNEE requires:
P[emit = x] = p(x)
The implementation can change the path. It cannot change the distribution.
SAME DISTRIBUTION
▲
│
┌──────────────┼──────────────┐
│ │ │
baseline speculative sparse
decoding decoding MoE
│ │ │
└──────────────┼──────────────┘
│
▼
p(x)
That is what target-faithful means.
When a proposed token is rejected, JOURNEE cannot simply discard the probability mass.
The correction must account for the difference between target and draft:
Target distribution
████████████████████████████
Draft distribution
██████████████████
Difference
██████████
│
▼
residual mass
│
▼
correction step
Formally:
P[emit = x]
= min(q(x), p(x)) ← accepted contribution
+ Z · r(x) ← rejected fallback
= min(q(x), p(x)) + max(p(x) - q(x), 0)
= p(x) ← by min/max identity
The residual r(x) = max(p(x) - q(x), 0) / Z is the normalized positive difference — only the mass the draft under-predicted. Sampling from p directly after rejection would double-count already-covered mass. The residual is the mathematically exact correction.
┌─────────────────────────────────────────────┐
│ JOURNEE │
├─────────────────┬───────────────────────────┤
│ Draft │ Move ahead cheaply │
├─────────────────┼───────────────────────────┤
│ Target │ Define the distribution │
├─────────────────┼───────────────────────────┤
│ Runtime │ Execute the procedure │
└─────────────────┴───────────────────────────┘
A faster runtime should not become a new mathematical definition of the model.
FORMAL MODEL
│
┌────────┴────────┐
▼ ▼
Agda Lean 4
│ │
└────────┬────────┘
▼
Formal IR
│
▼
Reference Runtime
│
F# Backend
│
▼
Conformance Tests
│
▼
Rust Runtime
│
┌───────────┼───────────┐
▼ ▼ ▼
CPU WASM Accelerator
The goal is not to make the runtime carry the entire theory. The goal is to make the theory precise enough that multiple runtimes can be judged against the same semantics.
OPTIMIZATION
│
▼
change the path
│
X
change the answer
Acceleration is allowed. Approximation is allowed where the formal procedure permits it. Speculation is allowed. Sparsity is allowed. Different runtimes are allowed.
But the target distribution remains the boundary.
FASTER
│
▼
┌───────────────┐
│ JOURNEE │
└───────┬───────┘
│
▼
SAME p(x)
Go faster without becoming different.
pip install -e ".[dev]"
# Verify the theorem before touching any model
pytest tests/test_exactness.py -v
# Train tiny draft and target
python scripts/train_draft.py --config configs/tiny_draft.toml
python scripts/train_target.py --config configs/tiny_target.toml
# Benchmark speculation
python -m journee.benchmark \
--target checkpoints/target.pt \
--draft checkpoints/draft.pt \
--prompt "The proof obligation is" \
--speculation-length 8 \
--seed 42| Metric | Definition |
|---|---|
| Acceptance rate | Accepted / total proposals |
| Mean accepted run | Tokens before first rejection |
| Target calls / token | Target forward passes / emitted tokens |
| Exactness error | Distance from p on toy distributions |
| TV distance | `TV(p,q) = ½ Σ |
AGPL-3.0-only
Copyright (C) 2026 Ahmad Ali Parr, Jessica L. Williams / SNAPKITTYWEST
Part of the Sovereign Stack — unified paper