CoProver: A Recommender System for Proof Construction

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

scope and relation to earlier notes

CoProver is a human-facing recommender for the Prototype Verification System (PVS). It learns from polished proof traces and recommends either the next proof command or a relevant lemma. Unlike systems intended to automate every proof, it is designed to keep a human in the loop. Earlier notes on learned proof search cover autonomous tactic generation; this study focuses on CoProver’s sequent featurization, transformer command ranking, Siamese lemma retrieval, top-N interaction, deployment boundary, and exact PVS measurements.

The paper’s abstract says: “CoProver employs a neurally learnt sequence-based encoding of sequents, capturing long distance relationships between terms and hidden cues therein.” It evaluates recommendation, not end-to-end proof completion. Its conclusion reports: “the top 3 − 5 commands” capture “50% − 70% of the original prediction correctly on the validation set.”

technique 1: normalize PVS proof states into transformer token streams

What it is. CoProver turns a structured sequent, selected proof history, and a lemma into compact token sequences for RoBERTa. Function and operator symbols remain; variable and constant names are replaced by placeholders or types so the model does not memorize project-specific names.

When to use it. Use this representation when formulas are too long for a raw structured encoding and symbol renaming should preserve the useful proof pattern.

How the paper does it.

1. Keep function and operator symbols as written (Section 3.2, p. 4).
2. Replace constant and variable names with a generic placeholder for command prediction; for lemma retrieval, replace them with type names so argument types can match (Section 3.2, pp. 4–5).
3. Retain integer values and omit parentheses; token order approximately preserves syntax (Section 3.2, p. 4).
4. Add <ANT>, <CONS>, and <HID> to mark antecedent, consequent, and hidden formulas (Section 3.2, p. 5).
5. Prefix command-prediction sequences with cmd1; append the previous three commands when history is enabled (Section 3.2, p. 5).
6. Train a domain-specific Byte Pair Encoding vocabulary, then apply RoBERTa’s masked-language self-supervision for 1,100,000 steps over the dataset (Section 3.2, p. 6).

The paper notes: “As Transformer models have fixed width input, a more parsimonious encoding that strips away boilerplate while retaining the original semantics will allow longer formulas to work without truncating them.” (Section 3.2, p. 4)

Verus form. Inference: serialize a Verus goal with requires, ensures, loop invariants, visible hypotheses, and recent proof actions. Keep Rust/Verus keywords and predicate names; normalize local variable names only where identity is irrelevant. Include types and ownership-relevant markers for lemma retrieval. Run any suggested action through Verus, because token equivalence does not establish type, borrow, or trigger correctness.

Evidence and limits. The authors use 20,000 proof steps for command prediction and 20,221 lemma pairs for retrieval, drawn from PVSLib. They explicitly assume the current state is enough for prediction, then add three previous commands as a limited non-Markovian signal. Higher-order and custom PVS types are placeholders, leaving those matches for future work.

technique 2: transformer next-command recommendation

What it is. A RoBERTa encoding of the featurized state feeds a T5 sequence-to-sequence classifier that predicts the next command an expert used. The system emits a top-N window, so a user can inspect several recommendations.

When to use it. Use command recommendation to help a human navigate a large command vocabulary or to let an agent try several likely actions in a background branch.

How the paper does it.

1. Featurize the sequent and optional command history (Section 3.2, p. 5).
2. Encode the token stream repeatedly with RoBERTa self-attention (Section 4, pp. 6–7).
3. Use T5/Huggingface training to map the encoding to the command in the expert trace (Section 4, p. 6).
4. Emit the top-N highest-confidence commands instead of only the first prediction (Section 4, p. 7).
5. Present commands to the user or run them speculatively and show the resulting proof states; this look-ahead use is proposed in the conclusion (Section 9, pp. 14–15).

Verus form. Inference: train a classifier on Verus proof traces with the current diagnostic and recent proof actions as input. Recommend assert, reveal, broadcast proof, a helper lemma call, or an invariant edit. For an agent, run each top-N candidate in an isolated branch and retain only branches that Verus accepts; for a human, show diagnostics and preserve the original file until selection.

Evidence and limits. Command prediction uses a random 90/10 split of 20,000 proof-step pairs and ten training epochs on four RTX 3090 GPUs (Section 6.1, p. 8). With sequent plus command history, CoProver’s test accuracy is 0.48 ± 7.3×10−3, versus 0.30 ± 1.1×10−2 for Linear SVC and 0.28 ± 1.0×10−2 for k-NN (Table 1, p. 9). The top-7 window contains the correct command over 70% of the time (Figure 5, p. 10). Accuracy is recommendation accuracy, not a verified proof rate.

technique 3: supervised Siamese lemma retrieval

What it is. CoProver treats the current sequent as a query and a library lemma as a document. Two RoBERTa encoders produce token representations, average pooling creates one vector per input, and cosine similarity ranks candidate lemmas. Positive pairs are user-selected imports; randomly sampled pairs are negative examples.

When to use it. Use this when a library contains thousands of lemmas and users may not know a useful theory or lemma name.

How the paper does it.

1. Collect explicit lemma-import events from completed PVSLib proofs and record the sequent plus imported lemma (Section 6.2, p. 10).
2. Encode the sequent and lemma token streams with the RoBERTa-based Siamese architecture (Section 5, pp. 7–8).
3. Average token vectors into one sequent vector and one lemma vector (Section 5, p. 8).
4. Label observed pairs 1 and sample an equal number of random pairs labeled 0 (Section 6.2, p. 11).
5. Score every candidate lemma with cosine similarity and rank the library (Section 5, p. 8; Section 6.2, p. 11).
6. Evaluate the ground-truth lemma’s rank with mean reciprocal rank (MRR) (Section 6.2, p. 11).

Verus form. Inference: index Verus spec fns, lemmas, and proof ensures by tokenized contracts and definitions. Encode the current unsatisfied obligation and each candidate helper lemma, retrieve a ranked list, then invoke only candidates whose requires can be established. Cosine ranking is a suggestion; Verus must check the call and its postcondition. Store library versions and module paths so retrieval cannot silently select a changed lemma.

Evidence and limits. The retrieval test has 12,132 training pairs and 8,089 test pairs from 20,221 explicit lemma pairs, against 9,468 lemmas in 747 theories (Section 6.2, p. 11). MRR is 0.51 for CoProver, 0.043 for TF-IDF, 0.0030 for count, and 0.0015 for the baseline (Table on p. 11). The authors say MRR 0.51 corresponds to average mean rank 1.98, approximately position 2. The labels reflect only user-selected lemmas; another equally useful lemma is treated as negative or uncredited.

technique 4: use history and structural information rather than bag-of-words

What it is. CoProver combines the current sequent with the previous three commands. Baselines use TF-IDF symbol counts, with an additional n-gram experiment testing whether local sequence structure helps.

When to use it. Use short command history when the same proof state can invite different actions depending on what was just tried. Use n-grams as a cheap baseline, but preserve longer-range transformer context when formulas have nonlocal relationships.

How the paper evaluates it. CoProver is tested with command history plus sequent, sequent only, and history only. Table 1 shows 0.48 ± 0.0073, 0.28 ± 0.0098, and 0.21 ± 0.0093 respectively (p. 9). Baseline classifiers generally improve as maximum n-gram degree grows from one to three (Table 2, p. 9), supporting some structural information, but they remain below the full CoProver setting. The paper’s conclusion cautions that attention may learn structural cues rather than deep reasoning.

Verus form. Inference: include the last few failed and successful proof actions, plus a normalized diagnostic, in the VL state. A history window can prevent repeating a failed assert or can suggest a follow-up reveal. Keep this as a ranker feature and never as a proof assumption.

technique 5: deploy recommendations behind a proof-assistant service

What it is. The models are wrapped as Flask web services. PVS sends a JSON sequent; the service returns command hypotheses or lemma objects that PVS displays directly.

When to use it. Use a service boundary when the recommender is optional and must not alter the trusted prover or proof artifact.

How the paper does it. Convert the current sequent to JSON, call the command or lemma endpoint, return hypotheses as JSON, and display them in PVS (Section 7, p. 12). The authors report internal developers found top-five command suggestions generally useful, while a larger user study was still being prepared.

Verus form. Inference: expose a local service that receives a serialized Verus obligation and returns ranked suggestions. The client should apply a suggestion only as source text in a branch and run Verus locally. Keep network/model outputs outside the trusted computing base, and attach source hashes and tool versions to each recommendation.

what is proved, measured, and trusted

The paper measures recommendation quality, not theorem validity. Command data: 20,000 sampled proof steps, 90/10 train/test, Table 1 accuracies, bootstrap variance estimates, and a two-sample t-test at α=0.001. Lemma data: 12,132 train and 8,089 test pairs from 20,221 explicit imports, 9,468 candidate lemmas in 747 theories, and MRR values above. The 184,335 total PVSLib proof steps are the source corpus, while the 20,000 and 20,221 subsets are different denominators.

Trusted or assumed are PVS, PVSLib and Prelude traces, the featurization rules, RoBERTa/T5/SBERT implementations, labels that user-selected imports are relevant, and cosine ranking. The authors explicitly warn that neural mechanisms may learn structural cues rather than deep reasoning; attention did not consistently match expert intuition. No result proves that a top-ranked command will advance a proof.

Threat to a product of agent-written verified Rust. Inference: medium productivity benefit and low direct soundness risk if the service remains advisory. The featurization, top-N look-ahead, supervised lemma retrieval, and service boundary map well to VL. Rust/Verus contracts need richer type and ownership features, and a retrieved lemma can fail its requires. Soundness risk rises if an agent treats recommendation confidence as proof or lets a remote service alter specifications without local re-verification.

techniques for the catalog

• normalized proof-state tokens — preserve logical symbols, normalize names and types, mark sequent regions, and encode recent commands
• transformer command recommender — fine-tune RoBERTa/T5 on proof traces and return a top-N next-command window
• Siamese lemma retrieval — encode sequents and library lemmas separately, train positive/negative pairs, and rank by cosine similarity
• short-history conditioning — append recent proof actions so recommendations reflect what has already been tried
• structural baseline comparison — test n-grams and TF-IDF to measure the value of sequence structure over symbol counts
• advisory prover service — return JSON suggestions through a web endpoint while leaving proof checking in the local assistant Checked 2026-10-13: audit record yeh2023coprover; paper-study comparison complete; gate executed; experiments not rerun

Last edited: 2026-10-14