主实验 1 · Statement Verification(多选题)
给定非正式陈述,判断哪个 Lean 形式化忠实(或「以上都不对」)· 含 formal_context
任务
- 每题:非正式陈述 + 证明,四个 Lean 选项 A/B/C/D,其中 D = 「以上都不对」。
- 选出忠实形式化;若三个 Lean 选项都有缺陷,选 D。
- 干扰项是语义扰动,在自然语言层面不可见。
- 主表用平衡设定:一半题目(35/70)正解为「以上都不对」。
结果(「都不对」占比 = 50%,70 题)
| 模型 | 总正确率 | acc·real
(有真解) | acc·「都不对」
(无真解) |
|---|
| Claude sonnet-4.6 | 0.800 | 0.971 | 0.629 |
| GPT-5.5 | 0.771 | 0.943 | 0.600 |
| GPT-5.4-mini | 0.586 | 0.229 | 0.943 |
| GPT-5.4-nano | 0.486 | 0.514 | 0.457 |
要点
- Claude ≈ GPT-5.5 最强(0.80 / 0.77)。
- 大模型会认忠实选项(acc·real ~0.95),但识别"全是缺陷"弱(acc·「都不对」~0.6)。
- mini 倾向于选择「以上都不对」:acc·real 仅 0.23、acc·「都不对」却 0.94;nano 接近随机。
- 总正确率会被答题偏好扭曲(mini 偏好选择「以上都不对」),需结合 acc·real / acc·「都不对」看。
更难、更有意思的在 ablation:把「都不对」占比从 0% 扫到 100%(大模型正确率单调下降、mini 反而上升)、各模型校准与 precision/recall、不同扰动类型的"奏效率"。见
NOTA Ablation 与
错题 Case Study。