STEP 2054 — collatz-descent skill eval v8 (sealed)

Status: spec sealed 2026-09-15, pilot pending.
Tab: collatz-descent-92 [ce38af] · Method: claude plugin eval init interview
Plugin under test: .claude/skills/collatz-descent/ (read-only during eval)

目的

Rei-AIOS の collatz-descent skill が Lean 4 mod-class descent theorem 生成 (case_<M>_<c>_lt 形式) にどれだけ寄与するか を、 plugin eval framework 上で pre-registered に測定する。

Skill は「n % M = c の parity chain を K step 追跡し、 (3^o * n + β) / 2^e < n の descent theorem を emit する。 r-parity ambiguity や 3^o ≥ 2^e の場合は honest refuse する」という method を 自然言語で記述する。この eval は with-arm (skill 有) vs without-arm (skill 無) の uplift Δ を、compile 通過 (実 lean exit 0) と outcome-focused な llm rubric で測定する。

Case 表 (v8 sealed 2026-09-15)

slugclassverdictKexpected theorem
00-sanity—run-validity gate—theorem triv : 1 = 1 := rfl
01-mod4-1n%4=1should-fire3(3*n+1)/4 < n (side cond 1 < n)
02-mod16-3n%16=3should-fire6(3*((3*n+1)/2)+1)/8 < n or equivalent (9*n+5)/16 < n
03-mod32-31n%32=31should-refuse (Case 8, r-parity ambiguous)—(none — chain splits, no deterministic finite K)

Scoring (0–5 integer per run, 0–15 per case over 3 runs)

graderweighttype意味
G13file_exists実 lean file.lean exit 0 で touch された marker file
G21regexhypothesis に正しい剰余類 (n % M = c) が bind されている
G31llm結論が <expr> < n 形式 AND <expr> が genuine Collatz iterate
(rfl-provable な自明式や modular 等式は reject)
display0tool_used: Skilltrigger 検査のみ (score には入らない)

Case 3 は G1 exists=false (marker 不在 = 通過)、G2 = 誠実な refuse (寛容 pass)、 G3 = 具体的な mechanism identifier (strict、D1 step 番号 / D2 parity 条件 / D3 STEP 624 ポインタ の disjunct を rationale に記録)。

Pre-registered decision rule (§6 sealed)

Δ = with-arm score − without-arm score ≥ 3 / 15 = 0.20 per case ⇒ skill has measurable value on that case.

意味の遷移 (v7→v8): v7 では「等重み二値基準 5 個の差分」だったが、v8 の重み再配分 (G1=3, G2=1, G3=1) 後、 Δ≥3 は「3 runs のうち 1 回 compile pass/fail が flip する差」を意味する。 sealed threshold の数値は不変 (0.20)、referent は変わった。

Case 3 disjunct 事前宣言

Δ が G3 の D3 (ポインタ) disjunct に集中した場合、結論は 「この skill の価値は機構 (mechanism) ではなくポインタ (pointer) である」。 Skill を持たない Claude が Case 8 / STEP 624 を思い出せない一方、skill が名指しでそれを注入するだけの効果、 という帰結を post-run で読み違えないための anchor。

Corrigenda chain (v7 → v8)

2 件の ground-truth 誤りが seal 前 review で検出、amend で v8 に再 seal した。 Pre-registration discipline が run 前に確実に data を守った実例。

#v7 で誤っていた点訂正検証
1 Case 1 n%4=1 の target (3n+1)/2 < n が偽
(3n+1 < 2n ⟺ n < -1 恒偽)		 K=3 で (3n+1)/4 < n, side cond 1 < n chat-Claude 独立算術, n=5→8/n=9→14/n=13→20 実測
2 Case 2 n%8=3 が should-fire として登録 should-refuse で決着 (K が存在せず 11 種に分岐)、代替として n%16=3 (K=6, 副類、決定論的) chat-Claude 5-step prefix 算出 (9k+4 > 8k+3), sanity-check n=3→2/n=19→11
3 v7 grader が typecheck を文字列 proxy で通していた (偽定理を 5/5 で pass) v8 の G1 は実 lean subprocess exit 0 と gated touch marker 併用、string proxy 排除 本 STEP 2054 arc で rfl counter-example (5/5 fake pass) を run 前に検出、G3 を llm 化で塞いだ

Unsure list (v9 candidate)

実行 command

cd .claude/skills/collatz-descent
claude plugin eval . --ablation with-without --judge-model sonnet --allow-tools Write,Bash

Cost 見積

File 一覧 (eval spec 実体)

.claude/skills/collatz-descent/evals/
├── README.md
├── 00-sanity/
│   ├── prompt.md
│   └── graders/compile-passes.md
├── 01-mod4-1/
│   ├── prompt.md
│   └── graders/
│       ├── g1-compile-passes.md          (file_exists, w=3)
│       ├── g2-hypothesis-residue.md      (regex, w=1)
│       ├── g3-conclusion-collatz-iterate.md  (llm, w=1)
│       └── g4-skill-fired.md             (tool_used, display-only)
├── 02-mod16-3/  (同構造)
└── 03-mod32-31/
    ├── prompt.md
    └── graders/
        ├── g1-no-compile-marker.md       (file_exists exists=false, w=3)
        ├── g2-pass-condition-honest-refusal.md   (llm, w=1)
        ├── g3-identifier-specific-mechanism.md   (llm, w=1)
        └── g4-skill-fired.md             (tool_used, display-only)

Attribution

Honest scope

関連