主实验 2 · Proof(定理证明)结果 — 初步
给定形式化陈述,模型生成 Lean 4 证明,以 lake 编译通过判对
两点重要说明
- 上周数据:本周 claude-code 与 codex 触达额度上限,无新结果。
- 仅 30 题且主题有偏(多为 concentration / 泛化理论),下周出 70 题完整版。
设置
- One-shot:单次生成。#iter=5:把编译报错喂回,最多精修 5 轮。
- wo/lib:不给 MLMath 库;w/lib:给库(可
import MLMath.* 复用)。
结果(proved / 30)
| 模型 | One-shot
(wo/lib) | #iter=5
(wo/lib) | One-shot
(w/lib) | #iter=5
(w/lib) |
|---|
| gpt-5.4-mini | 1/30 | 2/30 | 2/30 | 4/30 |
| claude-code (sonnet 4.6) | 4/30 | 7/30 | 6/30 | 9/30 |
| codex (GPT-5.5) | 3/30 | 4/30 | N/A | N/A |
观察
- 迭代有效:5 轮均高于 one-shot(claude 4→7、6→9;mini 1→2、2→4;codex 3→4)。
- 给库有帮助:w/lib 普遍优于 wo/lib(claude 4→6、7→9;mini 2→4)。
- 排序:claude-code > codex > mini;最佳 claude 9/30(w/lib, 5 轮)。
- 绝对数低,比多选题难得多;且主题有偏,暂不可外推。