Coqgym

CoqGym

Machine learning environment for automated theorem proving with Coq.

Overview

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

Installation

# 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

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

ASTactic Model

Neural network that predicts tactics from proof state ASTs:

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

# Extract proofs
python extract_proofs.py --project mathcomp

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

Evaluation

# 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:

(* 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

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

GF(3) Trit

Key Papers

• Learning to Prove Theorems via Interacting with Proof Assistants
• Graph Neural Networks for Theorem Proving
• Automated Theorem Proving with GNNs

Resources

• GitHub
• Princeton Vision Lab
• Coq 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.