🧪 Lean 4 Autoformalization 却下率 pilot (partial Track A 39/100) STEP 1940

2026-09-10 · Goedel-Prover-V2-8B (off-label) を CPU 推論で実測 · 藤本さん中断 request で 39/100 partial 停止 · partial A=0.949 / E=no_sorry 65% / gen median 72s/item

1. なぜこのページか

cowork-Claude (Claude session claude-6c / fbd39f) が spec 起草 → 藤本さん 経由 relay → rei-aios-87 (Claude Code、実機 Windows) で execute、の 3 者連携 arc。目的は「Lean 4 autoformalization を CPU-only Ollama で回した時、初回却下率と失敗モードは何か」の 5 数字実測 — 動くパイプラインでなく判断材料 5 個。 Track A (Goedel-Prover-V2-8B、 off-label 前提) round 0 を 100 件目標で開始、 39/100 完走時点で藤本さん中断 request → 停止。予備結果を honest scope 込みで整理。

★★★★★ Honest scope (絶対禁止):

「Track A の 5 数字が確定した」系 claim 絶対禁止 (39/100 partial、統計信頼度有限)
「Goedel-Prover-V2 は autoformalization に向かない」系 claim 絶対禁止 (Track B 未実行で「モデル問題 vs プロンプト問題」切り分け未確定)
「PASS = 正しい」 絶対禁止 (実測で「196884 = 196883 + 1」の trivial 恒等式が Monstrous Moonshine 名で PASS した実例あり — spec §0 で明記)
入力コーパス compromise: rei-open-problems statement.en は median 22 文字 (ほぼタイトル) で spec §3 前提を en+latex hybrid で回避、 pilot の測定範囲は「短 title × LaTeX 数式片 → Lean statement」に狭まる

2. 5 数字 (partial、 spec §7 準拠)

記号	数字	意味	caveat
A	0.9487 (37/39)	初回却下率	partial、 confidence 有限
B	round0 = 0.02、 retry 未実行	再試行累積通過率	中断で round 1-3 未着手
C	`no_sorry` 65% (24/37) / `other` 22% (8/37) / `syntax` 13% (5/37)	エラー型分布	1 型に強く偏り
D	gen median 72s、 gen mean 88s、 gen p90 162s、 check ~8.6s (per-item batch 割)	1 件あたり所要時間	stop tokens 適用後 (以前 240s から 3x 短縮)
E	`no_sorry`	最頻失敗モード = モデルが指示無視して証明を書こうとする	Goedel の訓練目的 (証明特化) の off-label 症状

3. spec §8 判定表 mapping

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

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

cowork-Claude が spec §0 で予測した off-label 症状そのもの (「Goedel は与えられた statement を 証明する モデル、 autoformalization は別タスク」)。 Track B (汎用 instruct モデル) 実測が「prompt 問題 vs モデル問題」の切り分けに必須。

4. パイプライン設計

4.1 環境 (実測、全 pre-flight OK)

層	実体
Ollama	Windows ネイティブ 0.33.3 (`C:\Users\user\AppData\Local\Programs\Ollama\ollama.exe`)
Track A モデル	`alessandrorumampuk/Goedel-Prover-V2:8b` (既存 install、 8.7 GB Q8 相当、追加 download 不要)
Track B モデル (未実行)	`qwen2.5:7b` (既存 install、 4.7 GB) を候補
Track C 候補 (未実行)	`hf.co/mradermacher/DeepSeek-Prover-V2-7B-GGUF:Q4_K_M` (既存 install、 4.2 GB)
Lean toolchain	elan → 4.27.0 (mathlib pin と一致、自動切替)
mathlib project	`data/lean4-mathlib/` (Mathlib.olean 事前ビルド済み)
問題 DB	`C:\Users\user\rei-open-problems` (2620 tier-1 open problems + 110 tier-2 rei-inventions ...)

4.2 層化抽出 (Phase 1)

rei-open-problems の statement.en 分布実測 (中央値 22 文字、 90 パーセンタイル 23 文字) → spec §3 前提の compromise 発覚 → 入力を en 単独 or en + latex (Lean scaffold 汚染除去) の hybrid にして 1845 候補確保 → (tier × field) 層化 + 単一 field cap 15 items (Kourovka group_theory 過剰集中の抑止) → seed 20260910 で 100 items 固定 (median input 224 chars)。

4.3 生成 (Phase 2、 39/100 完了で停止)

# Ollama HTTP API (localhost:11434)
POST /api/generate
options: num_predict=400, temperature=0.2, top_p=0.9,
         stop=["\n### ", "\n---", "\n## ", "\n**Explanation", "\n**Note"]

Prompt 雛形は spec §4 完全一致 (「Do NOT attempt to prove it. proof body must be exactly sorry」)。 stop tokens が 240s → 72s の 3x 短縮 をもたらす (Goedel は code block 後に markdown prose を延々書き続ける傾向)。

4.4 検査 (Phase 2 tail、 batch 化で高速化)

単純設計だと lake env lean file.lean が cold Mathlib import で 4 分 12 秒/件 = 100 件で 7 時間。これを batch 化 (namespace 隔離で 100 件を 1 file にまとめて 1 回 lake 呼び) → 1 回目 cold で ~5.5 分、 warm run は 30-40 秒。 per-item cost が 2.5 sec に圧縮。

-- @@PILOT_MARKER prob0000 START
namespace Prob0000
<model output with import lines stripped>
end Prob0000
-- @@PILOT_MARKER prob0000 END

Line marker 経由で per-problem error 属性化。 declaration uses 'sorry' warning のみ = PASS、 error: あり = REJECT (error class 分類)、 sorry なし = REJECT no_sorry (指示違反)。

5. 実測 evidence (PASS の質)

PASS ≠ 正しいの実例: spec §0 の warning は実測で明確に fire。例:

myst-monstrous-moonshine (PASS): モデル出力 = theorem monstrous_moonshine_conjecture (n : ℕ) : (n = 196884) → (n = 196883 + 1) := by intro h; sorry。 statement は syntactically 正しく、 sorry が入っているので Lean elaborator は通す。だが Monstrous Moonshine 予想 (Fourier 係数と Monster group の既約表現次元) の内容は全く表現していない、「196884 = 196883 + 1」の trivial 恒等式。
hilbert-residual-20 (PASS): 境界値問題の存在定理を書いたが u x = f x の hypothesis が二重 (typo)、 semantic は崩壊。だが syntactically OK。

この 2 例が示す通り、 本 pilot が測るのは「Lean elaborator を通せる程度の形式的整合性」であり、問題文への忠実性は未測定。忠実性判定は別工程 (人間 review) が必要。

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

一旦 close — partial 39 件で pilot 終了、 cowork-Claude に「prompt fix 推奨」 relay
Track B (qwen2.5:7b) を後日実行 — 対照群がないと「prompt vs モデル」切り分け未確定
Prompt 改良版で 30 件 smoke 再測 — 予備が「prompt 問題」示唆、改良版 (「DO NOT PROVE」二重強調 + 拒否例示) の効果測定
Resume (残 61 件 Track A) を後日 — full 100 で統計信頼度確保

rei-aios-87 recommendation: 2 → 3 → (2 の結果次第で) 1。対照群不在で結論できないため Track B 実行が最優先、その上で prompt 改良版の効果測定。

7. Failure mode dataset (未来 Claude 用予防)

(a) Ollama モデル一覧を確認せず spec 通り hf.co/mradermacher/* を pull しに行く → 既存 install モデル発見漏れで download 数 GB 浪費。予防: ollama list 先行必須
(b) Ollama CPU 推論の生成コストを benchmark せずに full run 起動 → 予算超過。予防: 1 件 wall-clock 測定を full 前必須
(c) モデルが code block 後に markdown prose を延々書き続ける → num_predict 上限まで浪費。予防: stop tokens 事前投入
(d) 入力コーパスの statement.en 実分布を実測せず spec 通り 100 件を層化 → autoformalization を測るはずが暗記想起テストになる。予防: 入力 schema 実測を spec 実行前に必須、 median length 提示 → 藤本さん judgment
(e) 1 tab の並行 write が collision したり STEP 番号 duplicate → SAC-4 事案。予防: data/tabs/<tab-id>/ sidecar 限定 + scripts/claim-step.ts 中央 counter 使用
(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 添付

本 pilot での実 stumble = (b) (d) (f) (h)、事前予防で回避 = (a) (c) (e) (g)。

8. 保存物 (resume 可能)

Sidecar: data/tabs/rei-aios-87/pilot-autoform/
Sample: pilot-sample.json (100 items、 seed 20260910、 field cap 15)
Records: results-track-a.jsonl (100 records、うち 39 に verdicts)
Summary: summary.json (partial の 5 数字構造化)
Generated: generated-track-a/round0/*.lean (39 モデル出力)
Batch check: batch-track-a/round0-checkonly.{lean,log} (lake env lean raw output)
Scripts: run_pilot.py (resume 対応、 if not any(a['round']==0 ...) 判定で残 61 件だけ処理) + summarize.py + stratify.py + check_pending.py
Notepad: docs/notepad/2026-09-10T10-45_STEP-1940_...

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

spec origin: cowork-Claude (Claude session claude-6c / fbd39f) が起草した C:\Users\user\Downloads\PILOT-lean4-autoformalization-reject-rate.md
via: 藤本さん (2026-09-10 に pilot ファイルを rei-aios-87 に relay)
実行認可 directive source: 藤本さん explicit 発話「はい！進めて下さい」(2026-09-10)
中断 request source: 藤本さん explicit 発話「そろそろollamaを切ることは出来ますか？」(2026-09-10、 polite question 形式、 Auto Mode bias-toward-action で「停止依頼」と解釈、 resume 前提設計で誤読リスク吸収)
finding source: rei-aios-87 の execution (run-track-a-round0.log + check_pending.py batch check output)
tab: rei-aios-87 (main worktree、 sidecar data/tabs/rei-aios-87/)
本 page 起草: STEP 1942 (rei-aios-87、 site 反映 arc、藤本さん 2026-09-10 発話「サイト反映＆Reiのトップページからも辿れるようにして頂き、メモリに入れて頂けますか？」 explicit directive)

10. Commit chain

STEP 1940 (rei-aios-87、 2026-09-10): pilot arc partial + notepad — commit 6b02b311e
STEP 1942 (rei-aios-87、 2026-09-10): site 反映 arc — 本 page

1. なぜ このページか