发表机构
Auburn University（奥本大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究在CoqStoq的100个定理上评估6种开源权重LLMs，发现仅Gemma 4等3个模型能生成Coq内核验证的证明，总体成功率3.5%，未确立模型通用排名。
AI 中文摘要
大语言模型（LLMs）可生成类似数学证明的文本，但相似性不代表正确性。形式化证明检查器会验证每个证明步骤是否遵循既定逻辑规则，Coq的规则基于归纳构造演算（Calculus of Inductive Constructions），该逻辑框架定义了系统可接受的证明步骤。本试点研究在来自真实Coq项目的基准CoqStoq的100个相同定理上评估了6种开源权重LLMs，每个LLM对每个定理进行1次尝试，温度设为0，Coq在定理的原始项目环境中检查每个提出的证明，仅当Coq内核接受该证明时才视为成功。Gemma 4验证了100个定理中的12个，Llama 3.3验证了8个，DeepSeek Coder V2 Lite验证了1个，Qwen 3.5、Mistral Small 3.1和GPT-OSS未验证任何定理。21个成功的模型-定理结果涵盖15个不同定理，其中11个未被标准Coq策略的基线解决；所有已验证定理均有短或中等长度的人工参考证明，无模型验证带有长参考证明的定理。由于证明长度分析是探索性的，该模式不能证明证明长度是导致差异的原因。对于至少有1次成功的3个模型，每个已验证证明的总生成成本为741至36193个输出令牌、14.9至178.0秒、0.0167至0.2000累计GPU小时，无法为无已验证证明的模型计算这些比率。在600次尝试中，模型生成了21个内核验证证明，总体成功率为3.5%。该研究报告了模型间的描述性差异，但未统计检验某一模型是否优于另一模型，因此结果未确立6个模型的通用排名。
英文摘要
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.
