integration: complete GF-T train+infer stack (all 8 PRs, locally verified) (Refs #1764) - #1809
Merged
Conversation
…-> class)
specs/ternary/gft_classifier4.t27 (GftClassifier4): the capstone -- four GF-T16
activations -> hidden layer (2 BitNet neurons, sign->trit) -> re-embed -> output
layer of 4 LOGIT-neurons (raw signed GF-T sum, no activation -> a real-valued
GF-T logit per class) -> argmax over the 4 logits -> predicted class index
{0,1,2,3}. Fuses gft_mlp3 (deep BitNet x GF-T inference) with gft_argmax4 (the
classification head) into one module.
Bit-exact to the ideal oracle over 400 vectors (tests/gft_classifier4_vectors.txt),
iverilog $fscanf. Doubly-grounded oracle: integer HW model AND exact-float64
logit-sum + argmax agree (re-embedded hidden acts are exact +/-1.0/0 so output
sums are exact in float64 -> non-circular; 0/400 disagreements).
No compiler change (on_comb, 20 ports). Fresh seal (seal --verify MATCH).
Refs #1764
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
specs/ternary/gft_argmax4.t27 (GftArgmax4): four signed GF-T16 logits -> the
index {0,1,2,3} of the maximum real value (lowest index wins ties, strict >).
The final stage of a GF-T classifier: gft_mlp3 emits logits, argmax picks the
predicted class. No arithmetic -- a total order on the GF-T encoding: the low 16
bits (offset<<9 | mant) are monotonic in real magnitude and raw 0 is the only
zero, so negatives < zero < positives. gt(a,b) via a 3-way sign category.
Bit-exact to the ideal exact-float64 argmax over 400 vectors
(tests/gft_argmax4_vectors.txt), iverilog $fscanf. Vectors (incl. injected exact
zeros) emitted only where the integer comparator AND the float argmax agree
(0/400 disagreements). Completes the end-to-end GF-T classifier.
No compiler change (on_comb, 4 ports). Fresh seal (seal --verify MATCH).
Refs #1764
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Three parallel deliverables ("все три"):
A2 - specs/ternary/gft_exp2.t27 (GftExp2): a GF-T exp2 primitive, 2^x for a
signed GF-T16 -> positive GF-T16. The missing building block for a GF-T softmax
(softmax = 2^logit / sum 2^logit). |x|->Q16.16 (positive shifts only),
sign-aware floor into k+f, 2^x = 2^k * 2^f; 2^k is an exact GF-T offset, 2^f
mantissa via a Q16 quartic with rounded Horner shifts (coeffs 354,123,29,6).
Prototyped + fitted in Python vs the exact mantissa (<=1 ULP over all 2^16
fractions) and vs true round_to_GFT(2^x) (<=1 ULP) before transcribing. Bit-exact
to the committed oracle 606/606 (iverilog).
B - specs/ternary/gft_layer4.t27 (GftLayer4): extends gft_layer3 to 4 neurons
(M->N=4), 4 trits packed 2 bits each. Doubly-grounded oracle, iverilog 500/500.
C - docs/synth/CLASSIFIER_AX7203.md: owner-gated flow to take gft_classifier4
spec -> yosys -> nextpnr-xilinx -> openFPGALoader on ALINX AX7203 (XC7A200T).
Final JTAG flash needs the user at the board; everything up to the bitstream is
scripted. On-silicon done = replay the conformance vectors, bit-exact on-air.
Fresh seals for GftExp2 + GftLayer4 (seal --verify MATCH). No compiler change.
Refs #1764
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
gft_recip.t27 (GftRecip): 1/x for a signed GF-T16 -- the last missing softmax
primitive. Closed form (no polynomial): 512+m' = round(524288/(512+m)),
off' = 79-o (+renorm). One rounded integer divide -> EXACT (0 ULP) vs true 1/x.
iverilog 506/506 bit-exact.
gft_softmax4.t27 (GftSoftmax4): the complete GF-T softmax over 4 signed GF-T16
logits, base-2, max-stabilized: p_i = 2^(l_i-M) / sum 2^(l_j-M), returns p_sel.
Composes the verified primitives -- max (gt), subtract (sadd+neg), exp2 (<=1 ULP),
sum (sadd), reciprocal (exact), multiply (RNE). Bit-exact to the integer oracle
2000/2000 (iverilog); accuracy <=0.0017 abs probability vs true float softmax
(sum-of-probs in [0.9982,1.0018]; uniform -> 0.25 exact).
Completes the GF-T classifier head: activations -> MLP -> logits ->
{argmax -> class} or {softmax -> calibrated probabilities}.
Fresh seals for GftRecip + GftSoftmax4 (seal --verify MATCH). No compiler change.
Refs #1764
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
gft_log2.t27 (GftLog2): log2(x) for a positive GF-T16 -> signed GF-T16, inverse of exp2. log2(x) = (o-40) + log2(1+m/512); the fractional part is a Q Horner quartic, the integer+fraction value is normalized fixed->GF-T via a flat 31-step priority encoder (yosys-synthesizable). Accuracy <=0.008 abs vs true log2. iverilog 505/505 bit-exact. Bug found+fixed (broken-ruler class): the log2 poly has NEGATIVE coefficients, and t27 emits `>>` as a LOGICAL shift on signed regs -> filled 0 for negative intermediates instead of arithmetic floor. Fixed with an explicit asr9 helper using only non-negative shifts. (exp2's all-positive poly never hit this.) gft_nll.t27 (GftNll): cross-entropy / NLL loss for a one-hot label -- given the softmax probability p of the true class, returns -log2(p) (composes gft_log2 + sign flip). iverilog 403/403; p=1->0, p=0.5->1.0, p=0.25->2.0 (exact). Opens inference -> TRAINING on GF-T: forward softmax->prob, then NLL->loss, with the inverse pair exp2/log2 both verified. Fresh seals for GftLog2 + GftNll (seal --verify MATCH). No compiler change. Refs #1764 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
gft_softmax_grad4.t27 (GftSoftmaxGrad4): the softmax + cross-entropy gradient over four signed GF-T16 logits. For a one-hot target t, dL/dl_i = p_i - y_i (the classic closed form) -- the backward pass is just the softmax forward p_i minus the one-hot label (grad = (i==t) ? sadd(p, -1.0) : p). Composes the verified softmax primitives. Bit-exact to the integer oracle 1600/1600 (iverilog); gradient accuracy <=0.0018 abs vs true p_i-y_i. Uniform logits, target 0 -> grad0 = -0.75 exact, grad1 = 0.25 exact. Forward + backward now complete on GF-T: logits -> softmax -> prob -> NLL loss, and -> gradient p-y. With the exp2/log2 inverse pair, the per-sample training step is fully expressible spec-first and iverilog-verified. Fresh seal for GftSoftmaxGrad4 (seal --verify MATCH). No compiler change. Refs #1764 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
gft_sgd_step.t27 (GftSgdStep): a GF-T SGD weight update, the final brick of an on-device training step. eta positive learning rate, g the signed gradient, w the signed weight. Composes a signed multiply smul (sign = XOR of signs, magnitude = the verified RNE magnitude mul) with subtract (sadd + neg). Bit-exact to the integer oracle 500/500 (iverilog); accuracy to GF-T16 precision (<=1 ULP). Spot: w=1,g=0.5,eta=0.5 -> 0.75 exact; g=0 -> w unchanged; w=1,g=-1,eta=1 -> 2.0. The full on-device training loop is now expressible spec-first on GF-T: logits -> softmax -> prob -> NLL loss (forward) -> gradient p-y (backward) -> w' = w - eta*g (update). Every stage iverilog-verified bit-exact. Fresh seal for GftSgdStep (seal --verify MATCH). No compiler change. Refs #1764 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
tools/gft_train_demo.py + docs/GFT_TRAINING_DEMO.md: a self-contained demo proving the spec-first GF-T primitive stack LEARNS, not just computes correct arithmetic. Trains a linear 4-class classifier by SGD on a toy set using ONLY the GF-T integer models -- bit-for-bit what the synthesized hardware computes (each op is bit-exact to a specs/ternary/*.t27 module with an iverilog conformance test). The same loop runs in float64 as a reference. Result: GF-T loss falls monotonically 2.20 -> 0.22 over 20 epochs and tracks the float64 reference to ~3 decimals the whole way; final 4/4 accuracy. The GF-T datapath trains as well as float. Ties the whole stack together: forward (smul/sadd/softmax) -> loss (nll) -> backward (grad p-y) -> update (w-eta*g), every stage iverilog-verified. Refs #1764 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Dumped every GF-T op the 20-epoch training run performs and replayed it through the COMPILED Verilog: forward softmax 372/372 bit-exact on GftSoftmax4, weight update 640/640 bit-exact on GftSgdStep. So the demo's loss curve is literally the synthesized hardware's -- GF-T learns on real RTL, not just in a model. Closes the "model vs hardware" gap on the actual training run. Refs #1764 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
tools/gft_generalize_demo.py: trains a linear 4-class quadrant classifier by SGD on a random train split using the GF-T integer models (bit-exact to the synthesized hardware), then evaluates on a held-out test split it never saw. Test accuracy climbs from chance (0.48) to 100% -- GF-T SGD learns the underlying rule and generalizes, it doesn't just fit the training set. Extends the training demo from "loss goes down" to "it generalizes." Refs #1764 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
gft_relu.t27 (GftRelu): relu(x)=max(0,x) for signed GF-T16, iverilog 304/304 bit-exact. Unlike the trit quantizer, ReLU has an exact 0/1 gradient -> clean multi-layer backprop on GF-T. tools/gft_deep_demo.py: a linear GF-T classifier fails XOR (47.5%, not linearly separable), a 2-layer net with a ReLU hidden layer trained by full backprop through the hidden layer solves it (98.8%). Proves multi-layer (deep) learning on GF-T, not just linear. All arithmetic bit-exact to the hardware models. Refs #1764 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
gHashTag
enabled auto-merge
August 6, 2026 17:59
This was referenced Aug 6, 2026
Contributor
Contributor
PR DashboardGenerated at: 2026-08-06 22:20:59 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
2 similar comments
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-06 22:30:39 UTC
Summary
Seal Status
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
One-shot integration of the full GF-T stack
Consolidates all eight queued PRs (#1801–#1808) into a single branch so the whole GF-T neural stack can land in one merge once CI runner availability is restored. Every part was verified locally for free (iverilog + cargo + seals) — see the per-op counts below.
What's integrated (10 specs + training demo)
gft_argmax4gft_classifier4gft_exp2gft_layer4gft_recipgft_softmax4gft_log2gft_nllgft_softmax_grad4gft_sgd_steptools/gft_train_demo.pyFull internal suite 1537 passed / 0 failed locally. (One unrelated test,
bitnet_layer, fails on macOS with an iverilog-compile quirk — it also fails on plain master, so it predates this work; it passes on the Linux CI.)Why this branch exists
The 4 required gates (
check,validate,check-now-freshness,check-linked-issue) run onubuntu-latestGitHub-hosted runners, which have been queuing jobs for 12+ hours — the repo's GitHub Actions minutes/spending limit appears exhausted (an owner-side billing setting). Until that's restored, this branch is the free-local consolidation: everything verified on this machine, ready to merge in one action.Supersedes the 8 individual PRs on merge (they can be closed, or merged individually once CI returns).
Refs #1764
🤖 Generated with Claude Code