Coqstoq Eval

---
name: coqstoq-eval
description: 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.
metadata:
  skill_kind: dataset_eval
  source_arxiv: 2412.14063
  bibtex_key: [REDACTED]
  confidence: high
---

# 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