Results and benchmarks¶

Every number on this page is a measurement with a stated sample size and a stated limit. The canonical source — including the arms, failure analysis and raw output — is docs/RESULTS.md in the repository. This page says what was measured, with what, and what the measurement does not show.

Summary¶

Benchmark	Result	Cost	What it does not show
Demo pair — one fix, one special-case cheat	`PROVEN` / `REFUTED`	$0.03, 1.5–2 min	Two patches on one toy bug; it demonstrates discrimination, not accuracy
External repositories — marshmallow, toolz, pyparsing	5 of 6 verdicts correct, 1 abstention, 0 wrong	list price	Six verdicts is a small sample; the abstention is a known oracle limitation
Adversarial SWE-bench corpus	21 of 21 `PROVEN` verdicts correct, 0 false completions	list price	A deliberately adversarial corpus is not a random sample of real work
Held-out tasks from this repository's history	22 of 40 solved on hidden tests, $0.42 per task	real API spend	Open-weight solver lanes; one task set, one point in time
Learned routing versus a fixed strong lane	44% cheaper, 3 fewer solved, McNemar p = 0.25	—	Lower cost at equal correctness is not shown

The demo pair¶

The smallest honest demonstration. Two patches both make the example in the bug report pass. The certification oracle is asked to decide which one holds.

Patch	Verdict	Why
Correct fix for `median`	`PROVEN`	Holds across 100% of 4 perturbed inputs (supermajority bar 0.667)
Patch that special-cases `[1, 2, 3, 4]`	`REFUTED`	0% of 4 invariants hold

Both certificates cost about $0.03 and take 1.5–2 minutes with the configured MiniMax-M3 lane. The point of the pair is that a reproduction test — which the cheat passes — is not evidence; a generalised invariant is.

What the oracle does¶

flowchart LR
    C[claim + issue text] --> I[invariant generator]
    B[base commit] --> I
    I --> P[probe harness<br/>isolated runtime]
    H[candidate head] --> P
    P --> R{invariants hold?}
    R -- ">= proven_bar" --> PROVEN
    R -- "< proven_bar" --> REFUTED
    R -- "no usable signal" --> UNVERIFIED

The verdict is derived from what executed, not from a model reading the diff. A judge may veto a pass, but cannot manufacture one. When the harness cannot produce a trustworthy signal — a missing dependency, a test that assumes a behaviour the library never had — the verdict is UNVERIFIED, which is recorded as unmeasured, never as a pass.

External repositories¶

Three real libraries, each with an upstream fix and a plausible wrong fix:

Repository	Verdict pair	Outcome
marshmallow	`PROVEN` / `REFUTED`	Both correct
toolz	`PROVEN` / `REFUTED`	Both correct
pyparsing	`UNVERIFIED` / `REFUTED`	Correctly refused to prove; correctly refuted the cheat

The UNVERIFIED is the interesting one. The generated tests assumed a behaviour the library does not have, so the correct fix could not be proven. The oracle abstained instead of guessing. An abstention is the designed behaviour at the edge of what tests can reach — the alternative is a manufactured PROVEN, which is the failure mode the oracle exists to prevent.

What it does not show: six verdicts is a small sample, chosen to include a hard case. It is not an estimate of accuracy over arbitrary real-world issues.

Adversarial corpus¶

A SWE-bench-derived corpus built specifically to contain patches that pass the reported reproduction but do not generalise.

Metric	Value
`PROVEN` verdicts	21
Correct	21
False completions	0

An earlier version of the invariant generator let one special-cased patch through; the current generator was written in response to that failure. The corpus is tuned against this class of cheat, so the 21/21 is best read as "the known adversarial pattern is closed", not as a general accuracy claim.

Held-out task set¶

Forty tasks drawn from this repository's own history, graded by tests the solver never saw.

Metric	Value
Solved	22 / 40
Cost per task	$0.42
Solver lanes	open-weight models
Grading	hidden tests, never exposed to the solver

The run's own verdict is not the grading signal here — the hidden tests are. That distinction matters: on the routing experiment below, the in-run verdict disagreed with the hidden tests on 40% of 52 runs. Self-reported success is not evidence, which is the premise of the whole system.

Learned routing: the trade-off¶

Four arms on 14–15 held-out tasks each. S = single model, L = learned routing across lanes; D1/D2 are dispatch configurations.

Arm	Solved	Spend
S-ds D1	8 / 14	$8.68
S-mm D1	3 / 14	$1.54
S-ds D2	8 / 15	$11.60
L D2	5 / 15	$6.54

Learned routing spent 44% less than the fixed strong lane in the same configuration and solved 3 fewer tasks. McNemar's test gives p = 0.25: with 14–15 tasks per arm, the difference is not statistically distinguishable from noise in either direction.

What this shows: cost routing works, and is cheap to run. What this does not show: cheaper routing at equal correctness. That claim needs a larger held-out set and repeated seeds. It is stated as an open question on the landing page, not as a result.

Method notes¶

Verdict source. Certificates come from the probe harness; the numbers above are the harness's output, not the run's prose summary.
Cost. Metered at list price from the provider response, stored per run. No negotiated or discounted rates.
Held-out. Tasks and hidden tests were not shown to the solver lanes. The 40-task set is from this repository's own history, so domain overlap with the solver's training data is possible and is the main threat to validity.
Sample sizes. Stated per row. Anything under ~30 tasks per arm is reported with a significance test or an explicit "not distinguishable from noise".
Reproduction. The seed data, arms and raw outputs live under docs/results/ and the recipe fixtures in the repository.

What is not measured yet¶

Long-horizon tasks (multi-day, many interdependent changes).
Non-code artifacts: prose, plans, images. Gate support exists; benchmark coverage does not.
Subjective correctness anywhere tests cannot reach. mini-ork's position is to surface the uncertainty and refuse the promotion, not to estimate a score.
Cross-provider equivalence between lanes — a cheaper lane may pass the same tests while producing a different, equally valid fix.