09:29
官方一手arXiv: DeepSeek@Ahmed Ryan, Md Erfan, Akond Ashfaque Ur Rahman, Md Rayhanur Rahman
推荐理由：这几个开源模型里Gemma 4最会写Coq证明，但100道题也只过12道，别指望它们太靠谱。
DeepSeek Coder
共 1 条相关 AI 资讯
8月7日
09:29
一项初步研究让6个开源权重LLM各尝试证明CoqStoq基准中的100个定理，每个定理只有一次机会，温度设为0，并用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策略未能解决的。所有被验证的定理都只有短或中等人写参考证明，长证明定理无一成功。600次尝试中共产生21个内核验证证明，总体成功率3.5%。