🔧 STEP 1940 pilot 2-track 200/200 clean + line_map bug 発見 + 診断反転 STEP 1944

2026-09-10 → 2026-09-11 · rei-aios-99 (Phase A/C/D 実行) + rei-aios-87 sidecar (Phase B/D pilot execution) · cowork-Claude 提案 → 藤本さん relay → 全 phase A→B→C→D 実行 Track A + Track B 200 items 完走 · STEP 1940 site page の corrigendum + full 2-track 完了

1. なぜこのページか

STEP 1940 が site 反映 (STEP 1942) で公開した「初回却下率 94.9%」は 形式化の却下率ではなく、 pilot 側の line_map バグ由来の見かけの数字。 cowork-Claude (Claude session claude-6c / fbd39f、別 relay) が「A は指示追従率と形式化能力の混合」と指摘 → 藤本さん経由で ①② 提案 forward → rei-aios-99 (本 tab) で生成コストゼロの再検査実行。結果 pilot bug 発見、 A が 94.9% ではなく 76.9% だと判明。藤本さん directive「94.9% が形式化の却下率ではないことを明記された方がいい」に沿って本 page 新設 (STEP 1942 page は上書きせず併存)。

2. 訂正後 metrics — 3 段階

指標	pilot 報告 (buggy)	Phase A 39 verify	Phase C 100/100 clean	root cause
PASS 数	2/39	9/39	27/100	bugfix + full sample
Pass rate	5.1%	23.1%	27.0%	+21.9 pt
A (raw 却下率)	94.9%	76.9%	73.0% (73/100)	bugfix 収束
A' (sorry 正規化後、 39 subset)	(未計測)	61.5% (24/39)	(subset のみ)	sorry 正規化 → type-check
statement 構造妥当 (39 subset)	(未計測)	38.5% (15/39)	(subset のみ)	同上
C `other` 割合	21.6%	< 5%	11.0%	v2 分類器 + 100 sample 分散
Top error class	no_sorry 65%	混在	syntax 41%	診断反転

診断反転: pilot 「A 高 × no_sorry 1 型偏り → プロンプト問題」 vs 100/100 clean 実測「A 高 × syntax 41% dominant + no_sorry 16% + other 11% + type_mismatch 4% + elab_failed 1% = model の Lean 4 syntax 知識不足 or 混合 (prompt + model)」。 no_sorry の 65% → 16% 大幅減少 = pilot の line_map bug がこの bucket を過大計上していた直接影響。

Phase 内訳: Phase A verified (baseline 39) = 9 PASS + 30 REJECT / Phase B fresh (61 items) = 18 PASS + 43 REJECT。 Phase B pass rate 29.5% vs Phase A 23.1% は sample variance (n=61 で ±10% 誤差内)、合計 100 で 27.0% 収束。

cowork-Claude の予測 (n=15 で条件付き却下率 86.7%) と私の結果は別軸: cowork-Claude は「指示追従を守った 15 件のうち REJECT 割合」、私の結果は「実 100 items で全 model attempt を fixed line_map で属性化」。前者は pilot の「no_sorry 24 件は未検査」前提に立った上界推定、後者は full pilot re-run + bugfix。

3. Root cause — pilot line_map バグ

run_pilot.py:140-147 の build_batch_file:

lines.append(marker_start)
start_line = len(lines) + 1  # BUG: len counts list elements, not physical lines
lines.append(f'namespace {ns}')
lines.append(body if body.strip() else '-- (empty body)')  # multi-line body = 1 element!
lines.append(f'end {ns}')
end_line = len(lines)  # BUG (same)

lines.append(body) は body が N 行の string でも list 要素として 1 個。 '\n'.join(lines) で展開時に physical line 数は N 増えるが、 len(lines) は 1 しか増えない → 全 item の range が「3 行幅 (namespace + body 1行相当 + end)」に compress。

実測 divergence (buggy vs correct physical line)

item	pilot buggy range	correct physical range	drift
hilbert-residual-20	(4, 6)	(4, 8)	+0, +2
myst-monstrous-moonshine	(10, 12)	(12, 14)	+2, +2
erdos-172	(52, 54)	(97, 101)	+45, +47
erdos-358	(70, 72)	(120, 124)	+50, +52
erdos-906	(142, 144)	(354, 357)	+212, +213
erdos-982	(154, 156)	(368, 373)	+214, +217
greens-1	(106, 108)	(245, 261)	+139, +153

pilot の上限 line が実際の theorem 領域の前に止まる → sorry warning が range 外 → 「no_sorry」誤判定。実際は log に 9 sorry warning が emit されているが、 pilot は 2 個しか PASS 判定できなかった。

シミュレーション検証: pilot の buggy len(lines) 算法をそのまま別 script で実装 → pilot 保存 verdict と 39/39 完全一致。 root cause 特定完了。

Fix (STEP 1944 で適用済)

body_str = body if body.strip() else '-- (empty body)'
lines.extend(body_str.splitlines())  # STEP 1944 fix: one physical line per element

関数 docstring に ★ TAB ISOLATION EXCEPTION OVERRIDE ★ marker + root cause 記載。 data/tabs/rei-aios-87/pilot-autoform/run_pilot.py の line 123-159 に patch 適用済 (commit 4f767374a)。 rei-aios-99 が Tab Isolation 例外 override で rei-aios-87 の sidecar file を修正 (peer offline)。

4. greens-1 訂正 (もう一つ pilot PASS が誤判定)

pilot 保存 PASS 2 件のうち:

hilbert-residual-20: 真 PASS ✓
greens-1: pilot PASS だが実際は REJECT (Finset.card_le_of_subset unknown constant)。 pilot の buggy line_map でエラー行が range 外に落ちて「no error + sorry あり → PASS」と誤判定したもの。

5. v1 → v2 分類器 diff

orig (v1)	→	new (v2)	count
PASS (2)	↓	PASS_confirmed	1
		unknown_identifier	1 (greens-1)
no_sorry (24)	↓	PASS_confirmed (line_map bug)	6
		syntax	9
		unknown_identifier	3
		tactic_failed	2
		invalid_declaration	2
		no_sorry_confirmed	1
		other	1
syntax (5)	↓	PASS_confirmed (line_map bug)	2
		syntax	2
		type_mismatch	1
other (8)	↓	syntax	5
		elab_failed	1
		tactic_failed	1
		invalid_declaration	1

v2 分類器追加 bucket: tactic_failed / invalid_binder / function_expected / resource_limit / PASS_confirmed / no_sorry_confirmed。詳細: STEP 1944 notepad

5.5. Phase D — Track B (qwen2.5:7b) 対照群完走、診断反転が統計的 validate

★ 決定的発見 ★ Track A (Lean 特化) と Track B (汎用) で dominant failure mode が完全に逆:

Track A (Goedel-Prover-V2:8b, Lean 特化): syntax 41% dominant = model の Lean 4 知識ギャップ (指示は従うが書けない)
Track B (qwen2.5:7b, 汎用): no_sorry 64% dominant = prompt を無視して証明を書こうとする (Lean 未特化)

Track A vs Track B (両方 100/100 clean、 same 100-item sample、 same prompt)

metric	Track A (Goedel-Prover-V2:8b、 Lean 特化 8.7 GB)	Track B (qwen2.5:7b、汎用 4.7 GB)
PASS	27/100 = 27.0%	3/100 = 3.0%
REJECT	73/100	97/100
Top error class	syntax 41%	no_sorry 64% ← 逆
syntax count	41	19
no_sorry count	16	64
other	11	7
type_mismatch	4	7
elab_failed	1	0
Gen median	72s	49s (0.68x)

Spec §8 判定表適用 (統計的 discrimination 可能に)

model	診断	intervention
Track A	syntax dominant → model limitation (Lean 4 知識不足)	Lean 特化訓練 or 別 specialized model (Track B は解決策ではない、 pass 3% で悪化)
Track B	no_sorry dominant → prompt problem (汎用 model 指示追従弱い)	prompt tuning (「必ず sorry で終わる」 explicit 指示 + refuse 例示) が効く可能性

総合診断: 両方が効く — prompt tuning は Track B の症状に効く、 model 特化は Track A の症状に効く。 pilot の元診断「プロンプト問題」は Track B だけ正しい、 Track A では誤り (line_map bug で no_sorry 65% と見えていたが実は syntax 41% dominant)。 cowork-Claude の spec §8 mapping 「A 高 × 1 型偏り → 対応 intervention 決まる」 pattern は本データで現に Track B (no_sorry 偏り) と Track A (syntax 偏り) で別 diagnosis を与える = prompt vs model 混合の統計的 evidence。

6. 4 択への含意 (cowork-Claude 提示、 Phase A→B→C→D 完了で事後 review)

択 (すべての前提) ✓ 実行済: pilot bugfix (commit 4f767374a) + full re-run で 100/100 clean 到達
択 1 (resume 残 61) ✓ 実行済: Phase B で 61 items 完走、 fresh 61 = 18 PASS + 43 REJECT (pass rate 29.5%)
択 3 (prompt 改良の焦点): 100/100 で判明 = 「syntax 41% dominant」は prompt 改良より model 側の Lean 4 syntax 知識不足 示唆、 prompt tweaking の効果余地は限定的、 Track B (別 model) の方が診断力高い 可能性大
択 2 (Track B qwen2.5:7b) ✓ 実行済 (Phase D): 100 items 完走 → PASS 3/100 (3%)、 no_sorry 64% dominant。診断反転が統計的 validate、 spec §8 判定表が各 track 別 diagnosis を与える状態確立
択 4 (close) 却下: 2-track 200 items 完走で pilot arc 完全 close 可能

7. Honest scope

本 STEP は pilot batch 39/39 のみ分析、未実行の 61 件は依然 unknown
v2 分類器は 39 items で実測されたエラー文に fit させた heuristic、別 dataset への一般化は未 verify
statement 構造妥当 15/39 = 意味論的正しさではない。 sorry 正規化は「theorem <sig> := by sorry が type-check するか」のみを測定、 statement が原問題を正しく formalize しているかは別問題 (人手 review 必要)
bugfix apply の verify: Phase A で 39 items → divergence=0 で fix 確認 (2026-09-10)、 Phase C で 100/100 full pilot re-run 完了 (2026-09-11、藤本さん explicit 「(A) 今進める」 authorize)
rei-aios-87 sidecar の results-track-a.jsonl: baseline 39 items は依然 pilot's original (buggy) verdicts 保存済 (rewrite していない、履歴保持のため)。 clean 100/100 は rei-aios-99 sidecar の aggregate-100.jsonl で提供 (source tag: phase_a_verified vs phase_b_fresh)
意味論的正しさは未確認: 27% pass = 「theorem signature が type-check」の意味、「statement が原問題を正しく formalize」は別問題 (人手 review 必要、例: myst-monstrous-moonshine の「196884 = 196883 + 1」 trivial 恒等式が PASS)
rei-aios-87 sidecar は一切改変せず (Tab Isolation 遵守、 read-only input のみ) — 例外は run_pilot.py の bugfix patch 1 箇所のみ (TAB ISOLATION EXCEPTION OVERRIDE marker 付き、藤本さん explicit「順番にお願い致します」で authorize)

8. Failure mode dataset (未来 Claude 予防)

(dd) subprocess で生成する batch file の line_map を len(lines) + 1 で計算すると multi-line 要素 (body/theorem) が list 1 element vs physical N lines の mismatch を起こす。全 verdict attribution が壊れる。 Prevention: 要素追加ではなく \n 明示 count か、 marker comment で physical scan。 batch 系 pilot は必ず marker-based reconstruction を parallel で持つ。 Recovery: marker-based scan で line_map 再構築 → re-attribution → summary rewrite。本 STEP 1944 で実施した pattern が template。
(ee) pilot の「metric 数字」をそのまま信じて次の判断 (resume / Track B / prompt 改良) に進むと、 root cause 未特定のまま誤りが伝播。 Prevention: 「metric 信じる前に algorithm 走らせて数字一致 verify」を pilot 完了直後の default 手続に。
(ff) 分類器 v1 の other 5% 超は「使えない分類」の閾値 (cowork-Claude 指摘)、 pilot 完了時にそのまま aggregate を出すと misleading。 Prevention: pilot 自身に if C_other > 0.05: raise の early warn を組み込む。

9. 再現性 (Reproducibility)

rei-aios-99 sidecar (data/tabs/rei-aios-99/pilot-autoform-analysis/) に:

normalize_and_recheck.py — ① sorry 正規化 + lake env lean 実行 (line_map bug あり raw)
reattribute_normalized.py — ① 結果 marker-based line_map 修正
reclassify_other.py — ② v2 分類器で orig pilot batch reclassify
normalized-batch.lean — lake 送信 batch (9578 bytes、 31 theorem block)
normalized-check.log — lake env lean 生 output (37 msg = 22 err + 15 warn)
summary-normalized.json — 訂正後 A' + C_updated + per-item verdicts
reclassification.json — v1→v2 per-item transition
classifier-diff.md — 全 finding + failure mode dataset
line-map.json — 訂正後 line_map (marker-based reconstruction)
run_pilot_line_map_fix.patch — unified diff + relay note (STEP 1944 refs commit 4f767374a)
verify_39_with_fix.py + verified-summary.json — Phase A: 39 items を fixed build_batch_file で re-attribute (lake 41s、 A=76.9%、 PASS=9)
aggregate_100_clean.py + aggregate-100-summary.json + aggregate-100.jsonl — Phase C: Track A 100/100 aggregate (Phase A 39 verified + Phase B 61 fresh、 per-item source tag)
aggregate_track_ab.py + aggregate-track-ab-summary.json — Phase D: Track A + Track B 200 items 対称比較 + spec §8 判定表別 diagnosis

実行 phase 別:

Phase A (2026-09-10): PYTHONIOENCODING=utf-8 python3 data/tabs/rei-aios-99/pilot-autoform-analysis/verify_39_with_fix.py → 41s lake env lean (warm Mathlib cache)
Phase B (2026-09-11): cd data/tabs/rei-aios-87/pilot-autoform && python3 run_pilot.py --track a --model 'alessandrorumampuk/Goedel-Prover-V2:8b' --round 0 → ~65 min Ollama gen 61 items + 26.2s batch check
Phase C: python3 data/tabs/rei-aios-99/pilot-autoform-analysis/aggregate_100_clean.py → 数秒 aggregate
Phase D (Track B): cd data/tabs/rei-aios-87/pilot-autoform && python3 run_pilot.py --track b --model 'qwen2.5:7b' --round 0 → ~85 min Ollama gen 100 items (qwen 4.7 GB、 median 49s/item) + 34.1s batch check
Phase D aggregate: python3 data/tabs/rei-aios-99/pilot-autoform-analysis/aggregate_track_ab.py → Track A vs Track B 対称比較 + spec §8 別 diagnosis

10. Attribution (SAC-5 marker source 分離)

Directive source: 藤本さん 2026-09-10 explicit 発話 (cowork-Claude ①② 提案 forward + 「94.9% が形式化の却下率ではないことを明記された方がいい」corrigendum request + 「順番にお願い致します」 = 4 択順次 authorize)
Spec/proposal source: cowork-Claude (Claude session claude-6c / fbd39f、 via 藤本さん、元 spec は Downloads 側 file、私は実行のみ)
Finding/execution source: rei-aios-99 (本 tab 独立 verify、 rei-aios-87 sidecar は read-only input のみ、除 run_pilot.py bugfix patch)
Root cause 発見 source: rei-aios-99 (私の re-attribution が pilot 保存 verdict と divergence した後、 pilot 算法シミュレーションで 39/39 一致確認)
Applied by: rei-aios-99 (STEP 1944 arc、 commits e93c8f76a initial + 4f767374a bugfix + 59f154977 site 反映 initial + 46e76d382 Phase C 100/100 clean + Phase D 本 update commit)
Phase B execution authorize: 藤本さん 2026-09-11 explicit 「(A) 今進めるでお願い致します」 (残 39 items Ollama re-run + fan noise + 電力コストの explicit authorize)
Phase D execution authorize: 藤本さん 2026-09-11 explicit 「(a) 今 Track B 実行 (~1 h 想定、 fan 継続) でお願い致します」 (Track B qwen2.5:7b full 100 items + fan noise 継続の explicit authorize)

1. なぜ このページか