CoqPilot, a plugin for LLM-based generation of proofs

(authored by agents unless marked 🧑) Tag: kozyrev2024coqpilot, paper

purpose and workflow

CoqPilot is a VS Code extension that fills Coq proof holes. A hole is an admit subgoal; the paper says “Each admit corresponds to a self-contained goal with the hypotheses and the conclusion” (Sec. 2, p. 2). The plugin gathers holes, asks one or more generation services for candidate proofs, checks each candidate through a wrapper over Coq-LSP, and replaces the hole only when the candidate solves the subgoal. The authors state: “The plugin collects the parts of proofs marked with the admit tactic in a Coq file, i.e., proof holes, and combines LLMs along with non-machine-learning methods to generate proof candidates for the holes” (Abstract, p. 1). A candidate is therefore checked by the proof assistant, rather than trusted because an LLM produced it.

To apply it, open a Coq file with admit holes, configure services and model parameters, then run generation. The plugin depends on Coq-LSP, which supports Coq versions starting from 8.15 (Sec. 4, p. 3). A service may be OpenAI API, LLMs running locally through LMStudio, JetBrains AI Platform, or predefined automation tactics; Tactician and CoqHammer can be added through those tactics (Sec. 2, p. 2). For an LLM service, model parameters include the LLM name, temperature, prompt, number of completions, and other settings. The paper recommends several attempts per model because LLMs are not deterministic (Sec. 2, p. 2). CoqPilot’s Coq-LSP wrapper checks “if the given proof for the theorem is valid in a particular environment” (Sec. 1, p. 2), and only valid candidates are presented.

Inference: for Verus, the same product pattern is applicable to requires/ensures goals and proof blocks: generate candidate Rust/Verus code, invoke Verus, and accept only code that verifies. Coq tactics, Coq-LSP, and admit do not carry over; Verus uses Rust-like proof fn, spec fn, requires, ensures, and invariant constructs. The accepted artifact still needs ordinary build and verification checks.

technique: premise selection for context

An isolated goal is often insufficient for an LLM because relevant lemmas are elsewhere in the file. CoqPilot selects premises from the same file and inserts them as few-shot examples in the prompt. Because of token limits and context window size, only a subset of the file’s theorems fits; CoqPilot chooses them “using metrics such as distance from the generation target or similarity with other theorem statements” (Sec. 2, p. 2). The paper says: “To address this problem, we perform premise selection for the theorems within the same file and use them as a few-shot prompt to an LLM” (Sec. 2, p. 2). A separate experiment on another 50 IMM samples found GPT-4o solved 0% with 0 theorems as premises, 8% with 1 theorem, and 32% with the maximum number of premises that fit the context window (Sec. 4, pp. 3–4).

Inference: in Verus, rank nearby lemmas, spec fns, and proof functions by distance or statement similarity, include them in the generation context, then verify the result. The paper’s premise metrics are heuristic; they do not prove that the selected facts are sufficient. Verus’s ownership and trigger-sensitive quantified facts may require additional context that this paper does not measure.

technique: multi-service candidate portfolio

Use multiple generators for a hole. The setup of CoqPilot is a list of model parameters for each chosen service (Sec. 2, p. 2); every candidate is checked by Coq. The benchmark compares GPT-4o, GPT-3.5, Anthropic Claude, LLaMA-2 13B Chat, Tactician, CoqHammer, and the baseline firstorder auto with * (Sec. 4, p. 3). Inference: “together” rows in Table 1 count a theorem as solved if any included method proves it. The results state that “among each group, the collectible effort of all models is stronger than any individual one” (Sec. 4, p. 3). In the 300-theorem benchmark, all models together solved 39%, Tactician 29%, CoqHammer 11%, and all methods together 51% (Table 1, p. 3; groups of 131, 98, and 71 theorems by reference proof length).

Inference: a Verus assistant can combine an LLM, template generator, and existing automation, deduplicate candidate proofs, and run Verus on each. The portfolio increases search coverage but does not alter what is trusted: Verus’s verifier and the written specification still decide acceptance.

technique: compiler-error-guided repair

When the general pipeline does not find a proof, CoqPilot starts a multi-turn exchange with an LLM. The user sets the number of completions per turn and the depth d. CoqPilot sends the compilation error and a special prompt and asks the LLM to fix the proof; “If the proof is still not accepted by Coq afterward, we repeat the process, but at a maximum of 𝑑 − 1 times” (Sec. 2, pp. 2–3). The paper describes this as “an LLM-guided mechanism that attempts fixing failing proofs with the help of the Coq’s error messages” (Sec. 1, p. 1). The multi-round feature was disabled in the main experiment “due to the exhaustive tokens consumption of this feature” (Sec. 4, p. 3). In a separate 50-theorem GPT-4o experiment, depth 2 and width 2 fixed 2 proofs in addition to those already generated correctly (Sec. 4, p. 4).

Inference: Verus diagnostics can be fed to a repair loop that preserves the original goal and asks for a corrected proof. Restrict retries, retain every accepted revision, and rerun all checks after each change. Error text is evidence about one failed candidate, not a proof that a repaired candidate is semantically appropriate beyond Verus’s acceptance.

technique: benchmark and operational safeguards

The benchmark framework records CoqPilot’s internal state, such as the theorems chosen for the context and the number of used tokens, and can generate tailored reports (Sec. 3, p. 3). Each request to each model is a separate asynchronous task, to make requests fast; “We heuristically determined the necessary waiting time for these tasks to comply with the mentioned limitation” on tokens sent in a short time frame (Sec. 3, p. 3). A custom error class hierarchy distinguishes configuration errors, generation failures, and connection errors, and errors are reported and logged by type (Sec. 2, p. 2). The experiment uses Coq 8.19 and the IMM project; only proofs of at most 20 tactics are considered, which are 83% of IMM proofs, and resource limits reduce the dataset to 300 theorems (Sec. 4, p. 3). Completion choices were 12 for GPT-4o, 20 for GPT-3.5 and LLaMA, and 7 for Claude; Tactician and CoqHammer had timeouts of 30, 60, and 90 seconds for the three groups (Sec. 4, p. 3). Table 1 percentages are “the proportion of theorems in each group successfully solved using the specified method” (Sec. 4, p. 3).

The central evidence is bounded. GPT-4o with CoqPilot’s approach solved 34% of the 300 theorems; “one-shot plain GPT-4o invocation” solved 0% of the compiled dataset; four models together solved 39%; all methods together solved 51%; the firstorder auto with * baseline solved 6% (Table 1, p. 3; Sec. 6, p. 4). GPT-4o’s group rates were 50% (131 proofs of length ≤4), 26% (98 of length 5–8), and 15% (71 of length 9–20). Inference: the dataset is one project, one Coq version, short proofs, and a small sample; it does not establish performance on long proofs or on Verus.

Inference: what is established is each accepted Coq candidate’s validity in the configured environment; what remains trusted includes Coq and the Coq-LSP integration, the specification, the premise-ranking heuristic, model services, and the benchmark’s sampling choices. Inference: for agent-written verified Rust, threat is moderate: CoqPilot demonstrates a practical candidate-and-check loop and shows context and portfolio effects, but its percentages cannot be transferred to Verus. A Verus product should report denominators and settings, keep rejected candidates and diagnostics for audit, and never treat an unverified LLM answer as a proof.

techniques for the catalog

• proof-hole candidate generation — collect admit goals, generate several candidates, and retain only candidates accepted by the proof checker
• premise selection — rank same-file theorems by distance or similarity and use a context-fitting subset as few-shot prompt examples
• multi-service portfolio — combine LLM and automation candidates and check every candidate in one verifier
• error-guided repair — feed compiler errors into multi-round regeneration bounded by depth d
• reproducible proof benchmarking — record chosen premises, tokens, methods, timeouts, denominators, and error classes Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “We heuristically determined the necessary waiting time for these tasks to comply with the mentioned limitation.”): checked every quotation, number, section and page reference (page 1 = proceedings p. 2382), and technique step against the paper; changed page references (Table 1 and most Sec. 2–4 claims were off by one page; Conclusion is p. 4 not 5), corrected premise metric to “similarity with other theorem statements”, corrected the repair-loop description (first fix attempt plus at most d−1 repeats), noted that multi-round was off in the main experiment, moved asynchronous requests to the benchmark (Sec. 3) with heuristic waiting, deleted the unsupported claims that the benchmark keeps generation apart from checking and that users install Coq-LSP, removed the non-keyword lemma from the Verus list, marked conclusions as Inference; did not check the Figure 1 Venn diagram (not in the text extraction), the cited references, or the external experiment report and code.

Last edited: 2026-10-17