~/research
[ 12 write-ups in 9 projects ] newest first, with earlier and follow-up stages under their project; each lists its model, data, code, and open issues
write-ups
- 2026-10-23 — interp / patching Agents traced a lookup pathway in Qwen3 Agents traced how Qwen3 looks up the value for a named item: three stages of attention heads. Interventions at six head locations from Qwen3-0.6B, fixed in advance and joined to stages a separate search found in Qwen3-1.7B, moved its answer preference in the predicted direction on 92.2–100% of held-out prompts. Synthetic lookup prompts; answer preference, not free generation; the transfer passed its gates, the 0.6B three-stage study and the repair did not; evidence private.
- 2026-10-23 — interp / SAEs A search for internal signals in Gemma, built and tested by agents Agents built a search for what Gemma 3 1B tracks as it reads. It recovered parenthesis and quotation state, and one direction passed a preregistered steering test on fresh text: Δ 1.49 against at most 0.75 for 99 same-subspace random directions. One model; screens calibrated on parenthesis labels; steering confirmed at layer 12 only; Gemma Scope 2 already represents the direction.
- 2026-10-18 — interp / probes What Llama’s internal signals reveal about factual accuracy The follow-up tests a probe of Llama 3.1 8B’s internal activity against stronger baselines and confounds. On 742 held-out FActScore claims it reaches AUROC 0.802 against 0.735 for P(True), and a preregistered decomposition attributes most of its direct signal to attention heads. One model and layer; no clear advantage over subject popularity (0.740) once whole biographies are resampled; the knockout missed its preregistered criterion; code unreleased.
- 2026-10-05 — agents / formal verification Agents reused proofs of OpenSSL routines across three callers Agents verified three experimental x86-64 callers in HOL Light by applying machine-checked contracts for two unchanged Debian OpenSSL routines, instead of re-deriving them in each caller’s proof. The held-out caller missed its three-hour cap, then completed in a recorded successor. Pinned x86-64 model; loaded image and extraction trusted; not all of OpenSSL; replay assets unpublished; human review pending.
- 2026-09-27 — agents / formal verification Agents turned a one-kernel Lean proof into a checker that certified 25 PyTorch kernels One Lean theorem and a small checker certified 32-bit size arguments for 25 torch.compile kernels, 10 of them from 24 held out, each proof bound to the live compilation’s guards. Two of nine tuned kernels got faster. 1D pointwise kernels on one L4; the guarantee holds under captured guards, with a trusted frontend; research prototype, not upstream.
- 2026-09-25 — agents / formal verification 25 bugs in free-threaded CPython, found by agents Agents hunted concurrency bugs in CPython’s free-threaded build and confirmed 25, 18 with no earlier report found in the tracker search. Of the five I reported upstream, two now have fixes merged into CPython main. One macOS arm64 machine; I have reported four of the 25 so far; the proofs cover a locking model, not CPython.
- 2026-09-24 — agents / formal verification · early pilot, before the PyTorch work Agents optimized four naive routines without changing their specifications Claude Opus 5.5 rewrote four deliberately naive Dafny routines while the verifier held each change to a frozen specification. Seven rewrites verified, six of them known algorithmic fixes, and the run-length encoder ran 105× faster than its naive start on a held-out workload. Naive starts, still 5–7,400× slower than Python built-ins; one optimization run per routine; harness unpublished.
- 2026-05-26 — rl / sampling bias Training on random integers changes fixed-list choices across tasks Fifty GRPO steps on one pick-an-integer task moved Qwen3-30B-A3B-Instruct’s choices over fixed answer lists toward uniform on all nine untrained tasks (mean distance from uniform 0.74 to 0.38). On Llama-3.1-8B-Instruct the shift was narrower and concentrated on integer tasks. Fixed answer lists, not open-ended text; the trained model was sampled on three tasks; Qwen per-task records unpublished.
- 2026-04-24 — reasoning / tokens · exploratory A panel-format adapter produces shorter answers with lower accuracy An RL-only panel-of-experts LoRA on Qwen3-30B-A3B-Base wrote far shorter answers than Qwen’s thinking model but was less accurate: 31.5 points lower on matched MATH500 level-5 samples and 50.6 on a 20-problem AIME subset. Format and training history are confounded; one run per training stage; the token measure is retrospective.
corrections and withdrawn notes
model adapters
-
Random-choice adapter
A Qwen adapter for experiments with fixed-list sampling behavior.
-
Panel-reasoning adapter
The post-MATH Qwen adapter from the exploratory accuracy and completion-length comparison.