~/research
[ 7 write-ups ] each lists its model, data, code, and open issues
write-ups
- 2026-09-26 — agents / formal verification I used agents and Lean to cut a compiled PyTorch workload’s runtime by 26% Agents declared a torch.compile kernel’s size arguments 32-bit, proved in Lean when that is exact, and cut a changing-shape workload’s time by 26% on one L4. The opt-in patch is an open PyTorch PR. One program on one NVIDIA L4; the patch recognizes one kernel class and has not been reviewed upstream.
- 2026-09-25 — agents / formal verification I used agents to find 25 bugs in free-threaded CPython Agents confirmed 25 bugs in the no-GIL build, with no earlier report found for 18. TLAPS and Lean proofs of the locking model held; replays of real runs showed five places CPython leaves it. One macOS arm64 machine; five bugs filed upstream so far, the rest described by class only.
- 2026-09-24 — agents / formal verification I used formal verification and agents to make an algorithm 105× faster and prove it behaves the same Claude Opus 5.5 rewrote four deliberately slow Dafny routines under a frozen spec it could not edit. Seven rewrites verified, and one ran 105× faster on a workload it never saw. Dafny compiled to Python, against deliberately naive baselines; one run per routine on a noisy machine.
- 2026-05-26 — rl / sampling bias A 50-step RL update reduces categorical sampling bias Fifty RL steps on one random-integer task moved nine untrained pick-one tasks toward uniform on Qwen3-30B-A3B-Instruct. Scores fixed answer lists, not open-ended creativity. Partly replicated on Llama 3.1 8B.
- 2026-04-25 — interp / probes Hidden-state probes outperform self-reported confidence A linear probe on Llama 3.1 8B’s hidden states ranks claim correctness better than the model’s stated confidence. Better correctness ranking in legal QA and biographies; better Brier score only on biographies.
- 2026-04-25 — rlvr / exploratory Training on sometimes-solvable math problems: one RL run One RL run on the problems a panel-style adapter solved on some but not all of 8 attempts raised its held-out score from 14% to 29%. Single run, 100 held-out problems; the thinking-model run was not completed.
- 2026-04-24 — reasoning / tokens Panel-style reasoning trades accuracy for shorter completions Against Qwen’s thinking model, a panel-style adapter was 31.5 points less accurate on MATH500 L5 and used about 5× fewer completion tokens per correct answer. Base-model LoRA vs. Qwen’s production thinking model; post-training differs too.
corrections and withdrawn notes
model adapters
-
Random-choice adapter
A Qwen adapter for experiments with fixed-list sampling behavior.
-
Panel-reasoning adapter
The Qwen adapter used in the accuracy and completion-length comparison.