Coq 相关 AI 资讯 · AI 热点

8月7日

09:29

09:29

官方一手arXiv: DeepSeek@Ahmed Ryan, Md Erfan, Akond Ashfaque Ur Rahman, Md Rayhanur Rahman

一项初步研究让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%。

论文 Coq Gemma 4 Llama 3.3

推荐理由：这几个开源模型里Gemma 4最会写Coq证明，但100道题也只过12道，别指望它们太靠谱。

7月8日

10:16

10:16

官方账号arXiv cs.AI@Shuangxiang Kan, Shuanglong Kan, Sebastian Ertel

Aria系统将Claude Code等通用LLM代码智能体与验证框架结合，无需预设策略即自动生成Coq证明。在Iris分离逻辑的4257个引理和Rust标准库的217个引理上，Aria全部证明成功，零失败。在reglang基准上，此前LLM证明器仅能证明八分之一（约40个），Aria则证明了全部318个。在iris-lean的Lean 4移植中，Aria还自动证明了72个未移植引理，表明该方法不限于Coq。所用模型为Claude Opus 4.7。

论文 Aria Claude Code 形式化验证

推荐理由：Aria让代码智能体自由探索，不用手动设计策略，就能把Iris和reglang上所有定理都自动证出来，比之前的方法强太多了。