# Coqstoq Eval

> 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. Use when the user wants to benchmark on CoqStoq, or asks about evaluating this task. Reports Theorems Proven.

- Skill: `qhjqhj00/coqstoq-eval` (Agent Skill)
- Install (CLI): `npx skillmds add qhjqhj00/coqstoq-eval`
- Raw SKILL.md: https://api.skillmd.com/api/skills/qhjqhj00/coqstoq-eval/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- Author: qhjqhj00 (https://skillmd.com/u/qhjqhj00)
- Updated: 2026-09-08
- Page: https://skillmd.com/skills/qhjqhj00/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

```python
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

```bibtex
@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