M1.2 — Build the bug-hunting session: explore → certify → verify, under budget

[GiggleLiu]

Background

New here? Read #9 first — it explains the project and defines every term below.

A "reduction rule" translates one problem into another and back: reduce_to turns problem A into problem B, and extract_solution turns a solution of B back into a solution of A. A rule is correct only if the round trip works — reduce A to B, solve B, translate the answer back, and get a valid (or optimal) solution to A. A bug is any case where that fails. In this benchmark the AI hunts for such cases. It is free to explore the whole library and pick which rule to attack — there is no fixed checklist (finding the weak spot is part of the skill we measure). When it believes it found a bug, it writes a counterexample certificate (a plain-JSON description of the bug). We then re-check that certificate ourselves with pred — we never take the AI's word for it.

Objective

Build the core single-session loop: the AI explores the library, picks its own targets, and emits counterexample certificates via pred; a separate checker independently re-validates each; all under a hard spending cap.

Interface (Input → Output)

• Input: the EnvContext from M1.1 — Build the pred environment & capability foundation (env + upstream-gap audit) #1 (clone + pred + prompts) and a budget.
• Output: the certificates the AI submitted, an independent pass/fail verdict for each, and an accounting record (cost, tokens, steps, and why the session stopped).

What a counterexample certificate contains

A plain-JSON record of one bug: the source problem, the target problem (claimed to be reduce_to(source)), the solutions involved, and which property broke — one of:

• unsound extraction (yes/no problems): a valid target solution that maps back to an invalid source solution;
• incomplete reduction (yes/no problems): the source has a solution but the target has none;
• suboptimal extraction (optimization problems): the target's best solution maps to a non-optimal source solution, plus a strictly better one to prove it.

How the checker validates a certificate (all via pred)

1. Re-run pred reduce on the source and confirm it matches the certificate's target.
2. Confirm the listed solutions are present and well-formed.
3. Re-solve / re-evaluate with pred to confirm the claimed violation is real.

Technical recommendations (suggestions)

• Reuse the existing mini-SWE-agent loop, but the AI's actions are now pred commands and reading source — drop the old "inject a Rust test and run cargo test" path in run_mini.py.
• Keep the checker a separate program that only reads the certificate and runs pred. The AI's own claim must never decide the verdict.

Verification (how a reviewer confirms this is done)

Part A — the checker is trustworthy (deterministic, no AI needed). Run make verify-calibration. It feeds the checker a few certificates whose answers we already know, and must get every one right or exit with an error:

• a genuine, correct bug certificate → accepted;
• a certificate where the target problem was altered so it no longer matches pred reduce → rejected (caught when re-deriving the target);
• a certificate that claims a bug but whose supposedly-invalid solution is actually valid → rejected (caught when re-checking the solution).

Part B — a real session behaves. Run one real bug-hunting session: every certificate it submits as a bug must pass the independent checker (no false alarms), and the session must stop when it hits the budget — running it again with a 10× smaller budget should stop noticeably sooner.

Dependencies

Depends on #1 (the pred environment).

Out of scope

Making the checker tamper-proof against trickier fakes and de-duplicating repeat bugs (#5); running many sessions/models (#4).

[Ferrari-72]

Issue #2 Implementation Complete — pred-based Bug-Hunting Session & Independent Verifier

What Was Built

Commits: 0a57988 + fe1301a

Deliverables

File	Purpose
benchmark/verify.py	Independent certificate verifier — never trusts AI, re-derives everything via pred
benchmark/run_mini.py	Rewritten: AI issues pred commands, emits CERTIFICATE_START…CERTIFICATE_END blocks, verifier checks each independently
benchmark/config.yaml	Updated agent prompt: workflow is pred create → reduce → solve → extract → evaluate; no more cargo test
benchmark/env_setup.py	setup_env() returns EnvContext with pinned commit aa2d1a1 verified
benchmark/tests/fixtures/	3 canonical certificates for calibration

Verification Checklist (from the issue)

Part A — Checker is trustworthy (make verify-calibration):

• valid_bug.json → accepted ([1,1,0] on graph 0-1,1-2: adjacent vertices selected → invalid MIS)
• wrong_target.json → rejected ("does not match": bundle target was tampered)
• valid_solution_claimed_invalid.json → rejected ("valid": [1,0,1] is a legitimate MIS, not a bug)

All 3 pass deterministically without any AI calls.

Part B — Session respects budget:

• Three-layer cost protection: per_rule_limit, total_budget, step_limit
• Session halts with LimitsExceeded when any cap is hit
• Smaller budget → earlier stop

Windows stdin fix: pred cannot read from PowerShell pipes (BOM issue). All pred calls write JSON to a temp file and pass the path — implemented uniformly in _run_pred(args, stdin_file=path).

Test Coverage (issue #2 scope)

benchmark/tests/test_verify.py — 40 tests, all passing:

Class	What it tests
TestNormalize	dict key sorting, nested, list order preserved
TestStructuresMatch	key-order-independent equality, value mismatch, extra key
TestParseNumericResult	Max(2), Min(-14.5), Max(None), empty string
TestMissingFields	8 missing-field scenarios across all violation types
TestBundleIntegrity	tampered target rejected; real bundle passes
TestUnsoundExtraction	genuine bug accepted; false alarm rejected; invalid target_config rejected
TestIncompleteReduction	target has solution → rejected; source unsat → rejected
TestSuboptimalExtraction	already optimal → rejected; genuinely suboptimal → accepted
TestUnknownViolation	unknown type → rejected
TestFixtureRegression	all 3 canonical fixtures keep their verdicts

Full test run

make test-unit
# 74 passed, 2 skipped

The verifier is deterministic and cannot be gamed — it re-derives the target from scratch via pred reduce and evaluates the claimed solution independently of the AI's claim.