proceval

proceval is a procedural benchmark generator for algorithmic problem solving. Every emitted instance carries machine-checked proof obligations: Z3 discharges a first-order-logic satisfiability query and proves the answer unique by model exclusion, an independent brute-force oracle must agree with the solver's witness, and the reference solution is required to achieve a survivor-free 100% AST mutation kill rate before the problem may ship. The result is a benchmark family where every label is provably correct and every task is guaranteed to have exactly one admissible answer.

• Dataset: Giavy/proceval-v1 — 300 problems (100 arrays · 100 DAGs · 100 automata) split evenly across four difficulty tiers, with SHA-256-pinned artifacts.
• Engine: Python 3.11+, pydantic v2, z3-solver, typer/rich, httpx, matplotlib.

Technical approach

Z3 first-order-logic uniqueness proofs. Each task variant is encoded declaratively over the concrete instance — equilibrium sums, transitive set-closure for reachability, min-fixpoint distance relations, BFS-depth-chained product automata, greedy-minimality schedules — so the solver, not the constructor, certifies that (a) a solution exists and (b) no second solution exists. Blocking the witness model and re-solving to UNSAT is the uniqueness argument; a SAT or unknown verdict rejects the instance. All solver calls run under a hard 5-second timeout.

Survivor-free mutation engine. Reference solutions are fuzzed with single-site AST mutations — comparison flips (> ↔ >=, == ↔ !=), boundary arithmetic (+ 1 ↔ - 1), and boolean-flag inversions — executed in a resource-limited subprocess. A mutant survives only if every test still passes; any survivor is a release blocker. The references are written so that every mutable site is categorically fatal (flips crash, time out, or produce a different answer on every valid instance), which is what makes a durable 100% kill rate possible rather than incidental. The official release audits 391/391 mutants across 300 problems.

Asynchronous evaluation with unbiased Pass@k. The harness samples models through OpenAI-compatible, Anthropic, and OpenRouter endpoints (with retries, Retry-After-aware backoff, and sliding-window rate limiting) or a fully deterministic offline mock, executes completions in an isolated sandbox (RLIMIT_CPU/AS/FSIZE, process-group SIGKILL watchdog), and scores them with the unbiased estimator Pass@k = 1 − C(n−c, k)/C(n, k) alongside per-sample latency, token accounting, and a five-way failure taxonomy.

Streamlit console. A three-tab dashboard for auditing the corpus and runs: problem explorer with the Z3 encodings, side-by-side mutation diffs with kill logs, and Plotly leaderboards (Pass@k, failure heatmap, compute–accuracy frontiers).

30-second quickstart

pip install -e ".[ui,hf]"
proceval demo
proceval ui

proceval demo synthesizes a DAG problem, walks the Z3 uniqueness proof live, kills every injected mutant, and scores a 3-sample mock evaluation — no configuration, no network. proceval ui opens the dashboard on http://localhost:8501.

Architecture

flowchart LR
    subgraph Generation["proceval generate"]
        A["CLI --domain --difficulty"] --> B["Domain generators<br/>(arrays / graphs / automata)"]
        B --> C["Z3 verifier<br/>SAT + uniqueness (model exclusion)"]
        C --> D["VerifiedProblem<br/>+ oracle cross-check"]
    end
    subgraph Quality["Verification gates"]
        D --> E["AST mutator"]
        E --> F["100% kill-score gate"]
    end
    subgraph Evaluation["proceval eval"]
        D --> G["runner / search<br/>(flat, best-of-N, repair)"]
        G --> H["Pass@k + token accounting"]
    end
    subgraph Delivery["Delivery & analytics"]
        D --> I["JSONL / Parquet"]
        I --> J["HF Hub (push-hf)"]
        H --> K["Pareto / heatmap figures"]
        D --> L["Streamlit UI"]
        H --> L
    end

Loading

CLI reference

Command	Purpose
proceval generate --num-samples N --domain [arrays|graphs|automata] --difficulty [easy|medium|hard|extreme] --seed S --output D.jsonl	Generate Z3-verified problems.
proceval verify D.jsonl	Re-prove satisfiability + uniqueness for every stored problem.
proceval audit D.jsonl	AST-mutation fuzzing of references; exit 1 on any survivor.
proceval eval --dataset D.jsonl --model M --output R.json --samples N [--mock] [--strategy flat|best-of-n|sequential-repair] [--max-turns M]	Evaluate a model (live via provider env keys, or --mock offline).
proceval report R.json	Rich tables: Pass@k, latencies, failure breakdowns.
proceval plot --results R.json --output-dir ./figures [--dataset D.jsonl]	Pareto, failure heatmap, mutation-vs-accuracy figures.
proceval export-hf D.jsonl --output-dir ./hf_export	Parquet export with standard HF columns.
proceval push-hf D.jsonl --repo-id user/name [--private]	Hub upload with auto-generated dataset card ($HF_TOKEN).
proceval ui [--dataset D.jsonl] [--results R.json] [--port P]	Interactive dashboard.

Domains and difficulty tiers

Variant	Domain	Task	Uniqueness argument
equilibrium_index	arrays	Index splitting a strictly positive array into equal sums.	Strict positivity ⇒ at most one.
monotonic_split	arrays	Smallest index k with A[k] >= T.	Minimality of first qualifying index.
dag_reachability	graphs	Count vertices reachable from a source.	Exact set characterization (closure + support).
dag_shortest_path	graphs	Minimum-weight path between two vertices.	Min-fixpoint over distance variables.
dag_topological_position	graphs	Removal round under lexicographic Kahn's algorithm.	Greedy-minimality implications pin one schedule.
dfa_string_acceptance	automata	Count length-L strings a DFA accepts.	Layer-DP flow conservation fixpoint.
dfa_product_reachability	automata	Reachable pairs in a product of two equivalent DFAs.	BFS-depth chain excludes cycles.

--difficulty scales instance dimensions (explicit --min-length/--max-length override):

Tier	Arrays n	Graph vertices	DFA states	String length
easy	3–5	3–4 (ρ≈0.22)	2–3	2
medium	5–12	4–7 (ρ≈0.35)	3–5	2–4
hard	10–14	6–8 (ρ≈0.45)	4–6	3–6
extreme	15–24	7–8 (ρ≈0.55)	5–6	5–9

Evaluation

proceval eval --dataset artifacts/proceval_v1.jsonl --model gpt-4o-mini \
              --output results.json --samples 5
proceval eval --dataset artifacts/proceval_v1.jsonl --model mock-gpt \
              --output results.json --samples 3 --mock
proceval report results.json
proceval plot --results results.json --output-dir ./figures

Test-time scaling strategies with full token accounting:

proceval eval --dataset artifacts/proceval_v1.jsonl --model claude-3-5-haiku \
              --strategy sequential-repair --samples 1 --max-turns 4 \
              --output repair_results.json
python scripts/run_frontier_evals.py --models mock-gpt,gpt-4o-mini,claude-3-5-haiku

The frontier runner aggregates artifacts/multi_model_results.json, overlays all model frontiers in docs/assets/multi_model_pareto.png, and renders LEADERBOARD.md (per-domain accuracy, Pass@1, Pass@5, average token cost).

Release artifacts

The official dataset is published at Giavy/proceval-v1. Reproduce or extend it:

python scripts/generate_official_v1.py                 # 300 problems -> artifacts/
python scripts/generate_assets.py                      # docs/assets figures
python scripts/publish_release.py --repo-id Giavy/proceval-v1
proceval push-hf artifacts/proceval_v1.jsonl --repo-id Giavy/proceval-v1 --private

publish_release.py verifies SHA-256 hashes, row counts, domain/difficulty distributions, and per-row verification evidence before uploading, and skips gracefully when HF_TOKEN is unset. build_benchmark.py --publish chains the same gates into one command. Both require the hf extra.

Sample figures

Development & Agentic Harness

proceval was bootstrapped and iterated using a spec-driven agentic workflow powered by Ox Alpha (1M context) via OpenCode, paired with deterministic verification gates:

• Formal Invariant Verification: Every generated domain schema is validated against First-Order Logic constraints via Z3 before inclusion.
• AST Mutation Gates: Automated AST-level fuzzer verifies that 100% of synthetic mutants are killed by reference test suites.
• Spec Verification Loop: Changes were validated continuously against ./scripts/verify.sh (Ruff, MyPy, Pytest, and sandbox smoke runs).

pip install -e ".[dev,hf,ui]"
ruff check src tests scripts && ruff format --check src tests scripts
mypy src
pytest -v
./scripts/verify.sh            # ruff + mypy + pytest + smoke release build

CI (.github/workflows/ci.yml) runs lint, format checks, mypy, and the full pytest suite on Python 3.11/3.12, plus a Docker build smoke test.

Sandbox notes

src/core/sandbox.py executes code with [sys.executable, "-I", "-c", <code>] in its own process group under RLIMIT_CPU / RLIMIT_AS / RLIMIT_FSIZE / RLIMIT_CORE, with a wall-clock watchdog that SIGKILLs the group. Quotas are authoritative on Linux; macOS does not strictly enforce RLIMIT_AS. Combine with docker run --memory --cpus for host-level isolation.

License

MIT.