Coqgym

---
name: coqgym
description: Machine learning environment for automated theorem proving with Coq.
---
# CoqGym

Machine learning environment for automated theorem proving with Coq.

## Overview

[CoqGym](https://github.com/princeton-vl/CoqGym) is a learning environment for theorem proving with the Coq proof assistant. It provides:

- **71K human-written proofs** from 123 Coq projects
- **ASTactic** - neural theorem prover using proof state ASTs
- **CoqHammer integration** for automated reasoning
- **Benchmark** for evaluating ML-based provers

Paper: [arXiv:1905.09381](https://arxiv.org/abs/1905.09381)

## Installation

```bash
# Clone repository
git clone https://github.com/princeton-vl/CoqGym
cd CoqGym

# Install dependencies
pip install -r requirements.txt

# Install Coq 8.9.1
opam switch create coq891 4.07.1
opam install coq.8.9.1

# Build CoqGym
python setup.py build
```

## Dataset Structure

```
CoqGym/
├── coq_projects/     # 123 Coq projects
├── data/             # Extracted proof data
│   ├── *.json        # Proof states and tactics
│   └── sexp_cache/   # S-expression cache
├── ASTactic/         # Neural prover
└── coqhammer/        # Hammer integration
```

## Proof State Representation

Each proof state contains:
- **Goals**: Current proof obligations
- **Local context**: Hypotheses in scope
- **Global context**: Available lemmas/definitions
- **Tactic history**: Previous tactics applied

```python
{
    "goals": [...],
    "local_context": [...],
    "tactic": "intros n.",
    "proof_tree": {...}
}
```

## ASTactic Model

Neural network that predicts tactics from proof state ASTs:

```python
from astactic import ASTactic

model = ASTactic.load("models/astactic.pt")
tactic = model.predict(proof_state)
```

Architecture:
- TreeLSTM encoder for AST structure
- Attention over local/global context
- Tactic decoder with copy mechanism

## Training

```bash
# Extract proofs
python extract_proofs.py --project mathcomp

# Train ASTactic
python train.py \
    --data data/train.json \
    --model astactic \
    --epochs 100
```

## Evaluation

```bash
# Evaluate on test set
python evaluate.py \
    --model models/astactic.pt \
    --data data/test.json \
    --timeout 600
```

Metrics:
- **Proof success rate**: % of theorems proved
- **Tactic accuracy**: Top-k tactic prediction
- **Proof length**: Steps vs human proofs

## CoqHammer Integration

Combines ML predictions with automated reasoning:

```coq
(* In Coq *)
Require Import Hammer.

Lemma example : forall n, n + 0 = n.
Proof.
  hammer.  (* Calls external ATPs *)
Qed.
```

## Integration with Gay.jl Verification

Use CoqGym to learn proof strategies for Gay.jl properties:

1. **Extract** proofs from similar PRNG verification projects
2. **Train** on SplitMix64-style proofs
3. **Apply** learned tactics to new Gay.jl lemmas

```python
# Find similar proofs
similar = coqgym.search(
    query="deterministic hash function",
    projects=["compcert", "flocq"]
)
```

## GF(3) Trit

| Role | Trit | Description |
|------|------|-------------|
| Learner | -1 | Extract patterns from proofs |
| Predictor | 0 | Tactic prediction (ergodic) |
| Prover | +1 | Generate complete proofs |

## Key Papers

- [Learning to Prove Theorems via Interacting with Proof Assistants](https://arxiv.org/abs/1905.09381)
- [Graph Neural Networks for Theorem Proving](https://arxiv.org/abs/2003.04883)
- [Automated Theorem Proving with GNNs](https://medium.com/stanford-cs224w/automated-theorem-proving-with-graph-neural-networks-49c091024f81)

## Resources

- [GitHub](https://github.com/princeton-vl/CoqGym)
- [Princeton Vision Lab](https://www.cs.princeton.edu/~kaiyang/)
- [Coq Documentation](https://coq.inria.fr/documentation)

## Related Skills

- `coq-of-rust` - Rust to Coq translation
- `narya-proofs` - Higher observational type theory
- `proofgeneral-narya` - Proof assistant integration
- `forward-forward-learning` - Local learning without backprop


---

## Autopoietic Marginalia

> **The interaction IS the skill improving itself.**

Every use of this skill is an opportunity for worlding:
- **MEMORY** (-1): Record what was learned
- **REMEMBERING** (0): Connect patterns to other skills  
- **WORLDING** (+1): Evolve the skill based on use



*Add Interaction Exemplars here as the skill is used.*