gradcheck 0.1.0

Finite-difference gradient checking for Rust ML frameworks. Verifies an autodiff engine against an independent numerical oracle, with a negative control that must fail.
# v4 validation campaign — results

By **Henos D** ([@4ktLuffy](https://github.com/4ktLuffy)) · <henosd19@gmail.com>

`record` · Run against the burn corpus, 2026-08-06. Read with
[`objective-observability.md`](objective-observability.md), which came out of step 0.

This records what the v4 comparator was measured to do, so later claims can be checked
against evidence rather than memory. It is a results record, not a design note.

The campaign was pre-registered in three steps with outcomes agreed **before** running, so
that a null result could not be rationalised afterwards.

---

## Pre-registered outcomes

- **A** — v4 finds defects v3 could not. Best case.
- **B** — v4 finds no new defects but reclassifies a meaningful portion of the previous
  corpus as unverified. Also a success: calibration improved.
  **Guard:** abstention must concentrate below the certification floor. Abstention spread
  across large-magnitude components would be a tolerance bug, not honesty — B must be able
  to fail.
- **C** — v4 changes almost nothing, and known defects are still detected. Also valuable:
  it measures diminishing returns on this axis, and the response is to stop extending it.

---

## Step 0 — re-adjudicate the existing corpus

349 recorded cases, re-judged not re-run. No framework code executed that had not executed
before.

| | Pass | Unchecked | Mismatch |
|---|---|---|---|
| v3 | 340 || 9 |
| v4 | 230 | **110** | 9 |

Components: 7,716 of 9,663 adjudicated (79.8%).

**Guard result: passed.** Abstention by component magnitude:

| magnitude | pass | abstain | abstain % |
|---|---|---|---|
| 0 | 0 | 1635 | 100% |
| 1e-10 … 1e-7 | 0 | 312 | 100% |
| ≥ 1e-4 | 7449 | 0 | **0%** |

Every abstention sits at magnitude ≤ 1e-7. Nothing abstains above the floor. The
reclassification is justified rather than indiscriminate.

**Verdict: outcome B**, plus a finding neither outcome anticipated — six operations were
reported clean without a single component ever being compared. See
[`objective-observability.md`](objective-observability.md).

---

## Step 1 — positive control on the oracle itself

v4 is stricter about certifying, so it had to be shown at least as good at rejecting.
Checked defect-by-defect, because an aggregate count can hold constant while one defect
stops being detected and another starts.

| known defect | cases | v3 rejected | v4 rejected |
|---|---|---|---|
| transposed matmul (#5304) | 15 | 4 | 4 |
| `avg_pool1d` backward (#5308) | 3 | 2 | 2 |
| `max_pool1d` | 4 | 3 | 3 |
| pooling forward, plain | 143 | 44 | 44 |
| pooling forward, grad-tracked | 144 | 76 | 76 |
| pooling backward | 144 | 90 | 90 |
| **total (780 cases)** | | **219** | **219** |

Cases that stopped being rejected: **0**.

On the finite-difference path (`tests/fd_positive_control.rs`), against a defect known to
be present in the published build:

- ndarray — 4/4 certified, 0 rejected, 0 abstained
- cpu — **c=2,4 rejected** (`worst_rel` = 1.0), c=1,3 certified, 0 abstained

Note that `regression_5304` returns `Pass` on cpu, and that is correct rather than a miss:
the crate links the *published* burn, where #5304 does not reproduce. It cannot serve as a
control. The pooling defect is the only known defect present in that build.

**Verdict: no detection lost on either oracle.**

---

## Step 2 — the regimes v3 could not reach

v3 was structurally blind in three places: gradients below ~2e-2 (the additive-tolerance
hole), inputs large enough that the perturbation rounds away, and NaN paths. Everything
previously swept used well-conditioned data in roughly [-3, 3] — precisely where v3 was
already adequate.

Weighted objectives were required first, since `Σ softmax(x)` is constant at every width.
No API change was needed: multiplying by `w` inside the function under test makes
`sum(f_w(x)) = ⟨w, f(x)⟩`.

### Observability restored, and load-bearing

Measured on ndarray (`tests/observability.rs`), 4×8 softmax:

| objective | checked | max \|grad\| | ×1.5 corruption |
|---|---|---|---|
| `Σ softmax` | **0/32** | 2.98e-8 | **invisible** |
| `w = ones` (degenerate control) | 0/32 | ~0 | invisible |
| `w = ramp` | 14/32 | 2.16e-2 | **rejected** |
| `w = rademacher` | **32/32** | 3.60e-1 | **rejected** |
| `w = zeros3` | 31/32 | 3.81e-1 | **rejected** |

The last column is the one that matters. A weighted objective that produced non-zero numbers
but still couldn't reject a wrong gradient would be useless. It rejects.

`w = ones` reproducing the degenerate case is the control that confirms the mechanism.

**Design finding: Rademacher beats ramp** — 32/32 versus 14/32 adjudicated, because a
ramp's small entries produce gradients below the certification floor. Rademacher should be
the default weight.

### The hunt

40 cases, ndarray versus cpu: **0 mismatches**, 5,334 of 6,096 components adjudicated
(87.5%).

Softmax at width, previously unmeasurable:

| case | checked | median \|grad\| |
|---|---|---|
| `softmax` summed (before) | **0 / 97** | 3e-8 |
| `W_softmax_n8` | 16/16 | 1.3e-1 |
| `W_softmax_n64` | 128/128 | 1.6e-2 |
| `W_softmax_n256` | 512/512 | 3.5e-3 |
| `W_softmax_n512` | 923/1024 | 1.5e-3 |

Every abstention traces to a genuinely zero gradient:

- `tanh`/`sigmoid` at |x| ≥ 10 — saturated, gradient ~1e-7 or exactly 0.
- `softplus` at ±10 — exactly 16/32, because the data alternates sign and
  `sigmoid(-10) ≈ 4.5e-5`.
- masked positions in the attention probes — zero by construction.

**Attention masks are clean on both backends**: 0 NaN, 0 Inf, and `-inf` and `-1e9` produce
identical gradients. That path had never been checked, because v3 passed NaN silently.

**Verdict: outcome C for defect-finding.** The extreme regimes on this framework are clean,
so this axis should not be extended further here. **Outcome A for capability:** a whole
operation family moved from never-compared to verified.

---

## What this campaign does and does not license

**Supported:** on this framework, for the recorded shapes, weights and backends, the
softmax family agrees between an independent numerical oracle and two backends, at widths
to 512. Known defects remain detected. Abstention is confined to components whose gradients
are genuinely zero.

**Not supported:** any claim about operations outside the recorded set; any claim about
shared defects, since a cross-backend differential is silent when both sides are wrong; any
claim about second-order behaviour, which this framework does not support at all
(`unimplemented!("Only first-order autodiff is supported")`).

Every published claim should carry the weight set and the checked fraction. "Verified"
without those is not a meaningful statement.

---

## Before extending this axis again

Ask what class of defect the next version could find that this one structurally cannot. If
there is no answer, the returns have been measured and the effort belongs elsewhere.