Coqstoq Eval

coqstoq-eval

Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification — Thompson et al. (2024) (arXiv:2412.14063, 2024)

What this evaluates

Evaluates a language model's ability to synthesize complete formal proofs in Coq by dynamically retrieving relevant project-specific lemmas and proofs. It measures how effectively retrieval-augmented proving and search strategies improve theorem synthesis success rates over time.

Datasets

• CoqStoq — total 10396; splits: test (10396), ablation (500), post_cutoff (1171); repo https://github.com/rkthomps/coq-modeling

Metrics

• Theorems Proven (primary) — range: percent
  • Percentage of theorems successfully proven within a 10-minute timeout per theorem. Calculated as (Number of Proven Theorems / Total Theorems in Benchmark) × 100.

Input / output format

Input: Per proof step: current proof state, theorem statement, partial proof script, and up to 1,536 tokens of retrieved context (1,024 tokens for proofs, 512 tokens for lemmas).

Output: Next Coq tactic to apply (up to 128 tokens).

Scoring recipe

proven = 0
for theorem in benchmark:
    state = init_state(theorem)
    for step in range(max_steps):
        context = retrieve_relevant_proofs_and_lemmas(state, project_db)
        tactic = model.generate(state, theorem, context, max_tokens=128)
        state = apply_tactic(state, tactic)
        if state.is_proven():
            proven += 1
            break
        if step_timeout_exceeded(10 * 60):
            break
success_rate = (proven / len(benchmark)) * 100

Common pitfalls

• Timeouts are strictly 10 minutes per theorem and explicitly exclude file loading/compilation initialization time.
• Cross-version comparisons (e.g., Graph2Tac) require exact statement matching, which does not guarantee proof transferability due to potential definition changes between project versions.
• Performance on CoqStoq may be inflated by pretraining memorization since all benchmark projects predate the LLM's cutoff date.

Evidence (verbatim from paper)

TABLE II: Comparison of Theorems Proven between Rango and state-of-the-art proof synthesis tools. In Table[II], we report the results for Rango, Tactician, and Proverbot on the $10,396$ theorems in the CoqStoq benchmark. Rango finds $29%$ more proofs than Tactician, and $66%$ more proofs than Proverbot. We use a 10 minute timeout for all of our proof attempts. Our timeout does not include the initialization costs of loading and compiling the file.

Citation

@misc{thompson2024rango,
  title={Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification},
  author={Thompson et al. (2024)},
  year={2024},
  note={arXiv:2412.14063}
}

• arXiv: 2412.14063