测试6个开源大模型生成可验证的正式数学证明，仅少数成功。
Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study
- 用Coq核验证大模型生成的证明是否逻辑正确
- 成功率3.5%，仅Gemma 4等三模型有成功案例
- 短证明更易通过，适合研究形式化验证的开发者
大型语言模型（LLM）能生成类似数学证明的文本，但外观相似不等于正确。形式化证明检查器通过逻辑规则验证每一步。Coq基于归纳构造演算，定义了系统接受的证明步骤。本初步研究评估了六个开源大模型在100个来自真实Coq项目基准集CoqStoq的定理上的表现。每个模型对每条定理仅尝试一次，温度设为0，所有证明均在原始项目环境中由Coq核验证。只有当Coq内核接受时才算成功。结果：Gemma 4成功12个，Llama 3.3成功8个，DeepSeek Coder V2 Lite成功1个；Qwen 3.5、Mistral Small 3.1和GPT-OSS无成功。21次成功覆盖15个不同定理，其中11个未被标准Coq策略解决。所有成功定理的人类参考证明均为短或中等长度，无长证明成功。因证明长度分析为探索性，无法确认其因果关系。对有成功的三个模型，单次验证平均生成量为741至36,193输出词，耗时14.9至178.0秒，消耗0.0167至0.2000聚合GPU小时。其余模型未产生有效证明，无法计算成本。六模型共600次尝试，仅21次通过，总体成功率为3.5%。研究报告模型间差异，但未进行统计检验，故不能得出普遍性能排序。
原文摘要 · Abstract (English)
Large language models (LLMs) can generate text that resembles a mathematical proof, but resemblance does not establish correctness. A formal proof checker verifies whether each proof step follows established logical rules. Coq bases its rules on the Calculus of Inductive Constructions, a logical framework that defines which proof steps the system may accept. This pilot study evaluated six open-weight LLMs on the same 100 theorems from CoqStoq, a benchmark derived from real Coq projects. Each LLM received one attempt per theorem with the temperature set to 0, and Coq checked every proposed proof in the theorem's original project environment. We counted a proof as successful only if the Coq kernel accepted it. Gemma 4 verified 12 of 100 theorems, Llama 3.3 verified 8, and DeepSeek Coder V2 Lite verified 1. Qwen 3.5, Mistral Small 3.1, and GPT-OSS verified none. The 21 successful model-theorem results covered 15 distinct theorems, 11 of which were not solved by a baseline of standard Coq tactics. All verified theorems had short or medium human-written reference proofs; no model verified a theorem with a long reference proof. Because the proof-length analysis was exploratory, this pattern does not establish that proof length caused the difference. For the three models with at least one success, the total generation cost per verified proof ranged from 741 to 36,193 output tokens, 14.9 to 178.0 seconds, and 0.0167 to 0.2000 aggregate GPU hours. We could not calculate these ratios for models with no verified proofs. Across 600 attempts, the models produced 21 kernel-verified proofs, giving an overall success rate of 3.5%. The study reports descriptive differences among the models but does not statistically test whether one model outperforms another. Therefore, the results do not establish a universal ranking of the six models.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。