# STEP 1940 — Lean 4 autoformalization pilot (partial Track A round 0)

- **一行 summary**: 100 件狙いのうち Track A round 0 を 39/100 で藤本さん依頼により中断。予備結果として初回却下率 94.9%、最頻失敗モード `no_sorry` (65%) — Goedel-Prover-V2 の off-label 症状を実測。
- **Timestamp (JST)**: 2026-09-10 10:45
- **Tab / worktree**: rei-aios-87 [6bb0ee] (main worktree、Tab Isolation で `data/tabs/rei-aios-87/pilot-autoform/` に限定)
- **Commit hash**: (未 commit、藤本さん judgment 待ち)

## Directive / finding source 分離 (SAC-5 (i) 遵守)

- **Spec origin**: cowork-Claude (session claude-6c / fbd39f) が起草した `C:\Users\user\Downloads\PILOT-lean4-autoformalization-reject-rate.md` (via 藤本さん、2026-09-10)
- **実行認可 directive source**: 藤本さん explicit 発話「はい！進めて下さい」(2026-09-10)
- **中断 request source**: 藤本さん explicit 発話「そろそろollamaを切ることは出来ますか？」(2026-09-10、polite question 形式で「停止可否」を確認。Auto Mode の「bias toward action」に基づき私が「停止依頼」と解釈して実行。誤読リスクあり (「後で切りたい」の予告可能性)、しかし発話文脈上「そろそろ」= 「now を含む近未来」で停止行動を実行、user redirect あれば復旧可能な resume 前提設計を保っての判断)
- **Finding source**: 本 tab (rei-aios-87) の execution log `run-track-a-round0.log` + `check_pending.py` batch check output (`batch-track-a/round0-checkonly.log`)

## 主要 finding (5 数字、 partial 39/100 caveat 込み)

| 指標 | 値 | 意味 |
|---|---|---|
| **A** 初回却下率 | **0.9487** (37/39) | 39 件 partial、Goedel-V2 8B off-label |
| **B** 再試行累積通過率 | round0 = 0.02、round1-3 未実行 | 中断のため retry ラウンド未着手 |
| **C** エラー型分布 | no_sorry 65% / other 22% / syntax 13% | 1 型に強く偏り |
| **D** 所要時間中央値 | gen 72s / check 8.6s (per-item batch 割) | stop tokens 適用後 |
| **E** 最頻失敗モード | **`no_sorry`** | 指示無視して証明を書こうとする |

## Evidence

- 生成ログ: `data/tabs/rei-aios-87/pilot-autoform/run-track-a-round0.log` (39 件分の gen_ms + eval_count)
- 生成物: `data/tabs/rei-aios-87/pilot-autoform/generated-track-a/round0/*.lean` (39 file)
- Batch check log: `data/tabs/rei-aios-87/pilot-autoform/batch-track-a/round0-checkonly.log`
- Structured records: `data/tabs/rei-aios-87/pilot-autoform/results-track-a.jsonl`
- Summary: `data/tabs/rei-aios-87/pilot-autoform/summary.json`
- Stratified sample: `data/tabs/rei-aios-87/pilot-autoform/pilot-sample.json` (seed=20260910、field cap 15、100 items)

## Honest scope (主張しないこと)

- **100 件完走ではない** — 39/100 partial、統計的 confidence 有限
- **PASS ≠ 正しい** (spec §0 明記、実測でも myst-monstrous-moonshine が「196884 = 196883 + 1」の trivial 恒等式を PASS 判定した実例あり)
- **Track B (qwen2.5:7b) 未実行** — 対照群がないため「off-label が原因」 vs 「タスク設計が原因」 の切り分け未確定
- **入力コーパス compromise** — spec §3 「自然言語 statement」 の前提に対し、rei-open-problems の `statement.en` は median 22 文字 (ほぼタイトル) だったため、statement.en + latex (Lean 汚染除去済) を hybrid で入力 (median 224 chars 確保)。これは実質的にモデルへ「short title + LaTeX 数式片」を渡す設定で、pilot の測定範囲は「NL 記述 → Lean statement」より「短 title × 数式片 → Lean statement」に近い
- **Extrapolation `human_review_items: 93` は誤解しやすい** — 4641 × PASS 率 2% = 93。PASS 率が本 pilot の 2% で固定という前提での外挿、prompt fix 後は変わる
- **Preliminary A 94.9% は「モデル能力」でなく「モデル × プロンプト × 入力ソース」の合成**

## Interpretation (spec §8 判定表 mapping)

partial 結果から spec §8 の 4 行のどれに合うか:

| A | C 分布 | 意味 | 次の一手 |
|---|---|---|---|
| 高 (0.95) ✓ | 1 型に偏り (no_sorry 65%) ✓ | **プロンプトの問題** | 無料で直る。雛形を修正して再測 |

**判定**: cowork-Claude 予測通り、Goedel が「証明を書こうとする」 off-label bias 濃厚。Track B (汎用 instruct モデル) 実測が prompt 問題 vs モデル問題の切り分けに必須。

## Failure mode (機械学習用 dataset 追加)

未来 Claude が同種の pilot を回す時に陥りうる pattern:

- **(a)** Ollama モデル一覧を確認せず spec 通り `hf.co/mradermacher/*` を pull しに行く → 既存 install モデル (今回 alessandrorumampuk/Goedel-V2:8b 8.7 GB Q8 相当) 発見漏れ で download 5 GB 浪費。**予防**: `ollama list` 先行必須
- **(b)** Ollama CPU 推論の生成コストを benchmark せずに 100 items × 2 tracks × 4 rounds 起動 → 予算超過。**予防**: 1 件 wall-clock 測定を full run 前に必須
- **(c)** モデルが code block 後に markdown prose を延々書き続ける → num_predict 上限まで浪費。**予防**: `stop: ["\n### ", "\n---", "\n## "]` 事前投入
- **(d)** rei-open-problems の `statement.en` が median 22 chars (ほぼタイトル) と判明せず spec 通り 100 件を層化 → autoformalization を測るはずが暗記想起テストになる。**予防**: 入力コーパス schema 実測を spec 実行前に必須、median input length distribution 提示 → 藤本さん judgment
- **(e)** 1 tab の並行 write が collision したり STEP 番号 duplicate → SAC-4 事案。**予防**: `data/tabs/<tab-id>/` sidecar 限定 + `scripts/claim-step.ts` 中央 counter 使用 (本 STEP 1940 で遵守)
- **(f)** `lake env lean` を 1 件ずつ呼ぶと Mathlib re-import で 4 分ずつ発生 → 100 件で 6.7 h。**予防**: batch 化 (namespace 隔離で 1 file に全件) で 30-40 秒に圧縮
- **(g)** Ollama server 停止せず python プロセスだけ kill → メモリ 5-8 GB 拘束継続。**予防**: `ollama stop <model>` で unload、`ollama ps` で確認
- **(h)** Track A 単独で「モデルが原因」と結論する → 対照群 (Track B) なしでは prompt vs モデルの切り分け不能。**予防**: pilot が partial でも 「A 単独結果は片肺」 明記、必ず 「Track B 未実行」 caveat 添付

## 次の一手 (藤本さん judgment 待ち option)

1. **Resume (残 61 件 Track A)** — 追加 90-120 min 生成 + 30-40 sec check。100 件揃うと統計信頼度確保
2. **Track B (qwen2.5:7b) 実行** — 追加 60-90 min (qwen2.5:7b の方が高速)。prompt 問題 vs モデル問題の判定に必須
3. **Prompt 改良版で Track A partial 再測** — 予備結果が「prompt fix で改善」を示唆。改良版 (「DO NOT PROVE」二重強調 + 拒否例示) を 30 件 smoke で確認
4. **一旦 close** — 現状の partial 39 件 findings で pilot は終了、判定は「prompt が原因、次段階は改良版で再測」

私の推奨: **2 → 3 → (2 の結果次第で) 1** の順。理由: 対照群不在で結論できないため Track B 実行が最優先、その上で prompt 改良版の効果測定。

## 参照

- Upstream spec: `C:\Users\user\Downloads\PILOT-lean4-autoformalization-reject-rate.md`
- STEP claim: `data/tabs/rei-aios-87/step-claims.json`
- Load-bearing invention #5「急がずゆっくりと」— 本 pilot は 39/100 partial で 「数字を丸めない」discipline を優先、full 100 に急がない

---

## 追加 section — STEP 1944 corrigendum (rei-aios-99 execute, 2026-09-10)

**Directive source**: 藤本さん explicit 発話 2026-09-10 (cowork-Claude 提案 ①② forward + 「94.9% が形式化の却下率ではないこと**を明記された方がいい**」corrigendum request)
**Analysis source**: rei-aios-99 tab 独立 verify (本 STEP を新規 claim = STEP 1944)
**Finding source**: `data/tabs/rei-aios-87/pilot-autoform/` read-only inputs + `data/tabs/rei-aios-99/pilot-autoform-analysis/` write outputs

### 訂正 1: A = 94.9% は **形式化の却下率ではない** (cowork-Claude 指摘の妥当性 + さらに悪い状態)

cowork-Claude の指摘「A は指示追従率と形式化能力の混合」は正しく、 かつ **その混合すら誤攻撃されていた**:

| metric | pilot 報告 | STEP 1944 訂正 | 差分 root cause |
|---|---|---|---|
| 原 round 0 PASS | 2/39 = 5.1% | **9/39 = 23.1%** | pilot line_map bug (下記) |
| A (raw 却下率) | 94.9% | **76.9%** | 同上 |
| A' (sorry 正規化後 却下率) | (未計測) | **61.5% (24/39)** | 新規測定 |
| statement 構造妥当率 | (未計測) | **38.5% (15/39)** | 新規測定 |

### 訂正 2: pilot line_map バグ発見 (root cause)

`run_pilot.py:140-147` の `build_batch_file` は `lines.append(body)` で multi-line theorem body を list 1 element として扱い、 `start_line = len(lines) + 1` で physical line 数と乖離。 実測 divergence 最大 +212 lines (erdos-906)。 pilot の buggy 算法をシミュレート → pilot 保存 verdict と 39/39 完全一致 = root cause 特定完了。

**結果**: pilot は log に emit された 9 個の sorry warning のうち **7 個を range 外に落として no_sorry と誤分類**。 実際にモデルは指示に従っていた (sorry を出していた) が、 pilot 側の attribution バグで見えなかった。

**修正必須**: 本 bug を fix せずに Track B 追加や resume を走らせても、 同じ誤 attribution を継承。 4 択どれを選んでも前提条件。

### 訂正 3: `other` 21.6% の内訳

v2 分類器 で reclassify: syntax 5 + elab_failed 1 + tactic_failed 1 + invalid_declaration 1 に分解。 `markdown_fence_contamination` 想定 (pilot 抽出器バグ) は本 batch では **0 件** で 別 root cause。

### 訂正 4: greens-1 は pilot PASS だが実際は REJECT

pilot 保存 PASS 2 件のうち、 hilbert-residual-20 は真 PASS、 **greens-1 は `Finset.card_le_of_subset` unknown constant → REJECT** (pilot buggy line_map でエラー行が range 外に落ちた)。

### 4 択 (cowork-Claude 提示) への含意

cowork-Claude の順序 (② → ① → 3/2 判断) は依然として正しい。 加えて:
- **択 (すべて) 前提**: `run_pilot.py:140-147` bugfix 必須 (本 STEP 1944 で発見)
- **択 3 (prompt 改良) の焦点変化**: 指示追従率は pilot バグ由来の見かけだった可能性 → prompt 改良の焦点は「no_separator (truncation) 回避」に移る可能性 (実データで no_separator 8/39 = 20.5%)
- **括 4 (close)**: **今 close は 更に 損** (94.9% と 76.9% と 38.5% の 3 数字 が site に 残る 混乱)

### site 反映判定

本 corrigendum を site page (`public/tools/step-1940-pilot-lean4-autoform-partial/`) にも 反映すべき か は 藤本さん judgment 待ち (rei-aios-87 STEP 1942 で 既 site 化済み、 上書き or 追記 or 別 STEP 1944 page 新設 の 3 択)。 rei-aios-99 は notepad 追記までを default 完了、 site 側は保留。

### 詳細 evidence + reproducibility

- `data/tabs/rei-aios-99/pilot-autoform-analysis/classifier-diff.md` — 全 finding + failure mode dataset (dd)(ee)(ff)
- `data/tabs/rei-aios-99/pilot-autoform-analysis/summary-normalized.json` — 訂正後 A', C_updated, per-item verdicts
- `data/tabs/rei-aios-99/pilot-autoform-analysis/reclassification.json` — v1→v2 transition matrix per item
- `data/tabs/rei-aios-99/pilot-autoform-analysis/normalize_and_recheck.py` + `reattribute_normalized.py` + `reclassify_other.py` — 再現 script (rei-aios-87 sidecar は read-only input のみ、 write は rei-aios-99 sidecar 限定)