Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study

This study investigates the capability of general-purpose open-weight Large Language Models (LLMs) to generate formal mathematical proofs in Coq, a proof assistant that relies on a trusted kernel to verify logical correctness. Unlike previous studies that often use fine-tuned models or interactive repair loops, this pilot evaluates six models (Llama 3.3, Qwen 3.5, Gemma 4, Mistral Small 3.1, GPT-OSS, and DeepSeek Coder V2 Lite) using a strict, one-attempt, zero-temperature protocol. The researchers selected 100 theorems from the CoqStoq benchmark, ensuring each proof was verified within its original project environment to account for specific dependencies and library configurations.

Across 600 total attempts, the models produced 21 kernel-verified proofs, representing a 3.5% success rate. Performance varied significantly by model: Gemma 4 verified 12 theorems, Llama 3.3 verified 8, and DeepSeek Coder V2 Lite verified 1. The remaining three models failed to verify any theorems. Notably, 11 of the 15 distinct theorems successfully proven by the models were not solved by a baseline of standard Coq automation tactics. The researchers observed that all verified theorems had short or medium-length human reference proofs, suggesting a potential correlation between proof complexity and model success, though this remains an exploratory observation rather than a confirmed causal link.

This study provides a transparent, reproducible baseline for evaluating LLMs on formal verification tasks without the confounding variables of fine-tuning or interactive feedback. By measuring computational resource usage alongside verification rates, the authors offer a realistic look at the current efficiency of open-weight models in formal settings. The findings highlight that while LLMs can occasionally solve problems beyond basic automation, their overall reliability remains low, emphasizing the necessity of kernel-level verification for any LLM-generated formal output.