AI-native Rocq tooling — final results

The three objectives, across three policies

Naive compiler baseline → rocq-tools, mean over the three difficulty bins (dev set). Accuracy should rise; cost per solved proof and time per attempt should drop. The interface helps most where the model is weakest, and still pays at the frontier tier.

The ladder — one measured change at a time

Each step was A/B-tested against its predecessor on the same 60 problems (20 per difficulty bucket), same weak policy (claude-haiku-4-5), ≥2 repetitions; kept only if the per-bucket numbers improved. Lines show pass@1 per bucket; reverted steps are part of the record but not of the shipped tool. Hover any point for exact values.

Cost and time — expected spend per solved proof

The experiment's other two objectives. Each chart divides the per-attempt mean by pass@1: the expected cost (or wall-clock, or model-output tokens) to obtain ONE solved proof, failed attempts included. Same ladder steps and buckets as above — solve rate rose while $ and time per proof fell. Hover for values; hard-bucket spikes at early steps reflect near-zero solve rates there.

Policy-neutrality — the headline result (A24)

One server, one neutral prompt, measured at both a weak and a strong policy. The universal config beats the naive interface in every bucket at sonnet (first substrate config to do so) and is best-or-tied at haiku except hard, where the haiku-tuned variant keeps a .075 edge (within ½σ). pass@1, dev60.

Comparison with SOTA (rocq-mcp) — fair integration

github.com/LLM4Rocq/rocq-mcp, measured under the identical harness, gate, problems, and policies (first contact only after our design freeze; REPORT §SOTA). Bars: pass@1. Table: all three dimensions — $/solve = expected cost per solved proof (failures included), wall = mean s/attempt. Numbers from the FAIR rerun (Jul 8): an audit found the original runs started with rocq-mcp's server still connecting in 97-98 % of attempts (our integration artifact — retracted); an instant-handshake proxy fixed it, 120/120 connected. Fair verdict: near accuracy-parity at sonnet, rocq-mcp edges easy at haiku; rocq-tools leads weak-policy medium/hard and costs about half per solved proof at sonnet. See REPORT for the full audit story.

Scalability — N parallel agents on one machine

Each point is one full run of a fixed 24-problem stratified batch (8 per bucket) executed with N = 1, 2, 4, 8 concurrent agents — eight runs total (4 per interface), all in a single night window (Jul 3–4) after two earlier measurement artifacts were caught and disclosed (REPORT §5). Both interfaces scale healthily (flat wall per attempt, ~72–80 % parallel efficiency at N=8); the winner's advantage is its ~2.7× per-attempt speed, compounding to ≈6× solved-proofs-per-hour at N=8. The local prover is never the bottleneck (CPU ≤ 24 % of a 14-core laptop).

Everything else measured

Cross-policy annexes, SOTA comparison, team experiments, in-project probes, held-out — each analyzed in docs/REPORT.md. Raw per-run numbers below; reproduce any row with python3 harness/report.py <run>.