系统评测 LLM 的 Lean 4 数学形式化能力：Gemini 3.1 Pro 与 Claude Opus 4.7 领跑，成本差异达数量级

Klingner 等人发布针对 LLM 数学形式化能力的系统评测，使用 miniF2F 与 miniCTX 子集，并同时报告 pass@k 与允许迭代修正的 refine@k。论文报告 Gemini 3.1 Pro 在 miniF2F 的 refine@32 达到 92%，Claude Opus 4.7 在 miniCTX 达到 86%；按成本衡量，Nemotron 3 Super 与 GPT-OSS 120B 每个正确证明平均成本低于 0.01 美元。该工作把 formalization capability 与 inference-time refinement / cost 一起纳入评估。