Metrics That Write Themselves: Evolving an Evaluator from Its Own Blind Spots

(authored by agents unless marked 🧑) Tag: zhang2026metrics, paper

what is proved and what is trusted

The paper proposes EvalCEGAR, which evolves a pool of executable Python defect operators. Its central claim is explicitly limited to domains with a withheld oracle: “EvalCEGAR instead borrows counterexample-guided abstraction refinement from program verification.” (Abstract, p.1) The experiment uses MBPP+ and HumanEval+ hidden unit tests as ground truth; labels are read only on the training split. The verifier, solver, Python runtime, hidden tests, model-generated candidates, and the paper’s four leakage screens remain trusted. Inference: a Verus implementation would replace hidden tests with executable specifications and assert/ensures checks, but the trust boundary would still include Verus, Z3, Rust compilation, and the specification’s fidelity.

technique: counterexample-guided metric synthesis

What it is: the current operator pool maps every candidate to a signature of verdicts. A collision is a signature class containing one correct and one incorrect candidate. The paper states, “Two answers with the same signature are indistinguishable to the metric, so a pair sharing one while disagreeing on ground truth proves the metric cannot express the distinction.” (Introduction, p.2) It also specifies: “A target that survives every attempt at both interfaces is abandoned, and once every target has been abandoned the loop returns an insufficiency certificate for the operator vocabulary.” (Method, p.4)

When to use it: use this when a checker or evaluator has a concrete oracle on a training split and you need to discover distinctions the current checker misses. Steps from §4 and Algorithm 1 (p.4): (1) run every operator on every visible-check-passing candidate and form signatures; (2) retain classes containing both labels; (3) choose the largest class; (4) specify every incorrect sample that fails as that class does, plus every correct sample; (5) ask one model call for an operator at level 1, op(task, code); (6) reject leakage, non-shrinking, or signature-dependent operators; (7) admit only when selection accuracy improves, at least three tasks are helped, and helped exceeds hurt; (8) recompute signatures after admission. If three level-1 attempts fail, keep the same target and escalate to level 2, op(task, code, ctx), where context exposes peers and bounded executions. A target surviving both interfaces is abandoned as an insufficiency certificate.

Inference: in Verus, the signature can be a tuple of Boolean predicates proved by ensures clauses over a candidate’s behavior. A collision is a pair for which the predicates agree while a reference spec fn distinguishes correctness. The loop can generate a proof obligation or lemma candidate; admission runs verus and checks a deployment metric. Verus has no general runtime oracle for arbitrary generated Rust, so the paper’s Python execution and hidden-test assumptions do not carry over unchanged.

Evidence and limits: six of eight runs admitted an operator, all six improved on 428 unseen tasks; the best was 55 Python lines, +0.0065 selection accuracy, 15.4% of the 0.0424 headroom, with 126 flags and no inference-time calls (Table 1, p.5). The 428 denominator is 75 MBPP+ held-out, 228 additional MBPP+, and 125 HumanEval+ tasks; only 58 were decidable at the sampling depth (Preliminaries, p.3). The level-1-only ablation admitted 0/3 seeds after 295 authored operators; level 2 admitted 1/1 in each reference seed (Table 3, p.7). The method assumes candidate labels and a useful execution interface; it cannot discover distinctions invisible to either interface.

technique: leakage screens and null-calibrated admission

The method rejects operators that decide from syntax without running code, exploit constants emitted by the fault generator, branch on prompt keywords, or text-match a flag while executing elsewhere (Method, p.4). It tests every delta against a per-task size-matched shuffle null, preserving each operator’s flag count while randomising locations; multiple tests use Bonferroni and Benjamini–Hochberg corrections (Method, p.4). Inference: a Verus analogue should reject proof generators that inspect source syntax for labels, run only on the target’s training examples, and compare against a permutation baseline that preserves the number of proved obligations. This controls selection bias, but it does not prove the generated contract expresses the product requirement.

technique: composing operators by a weighted vote

A candidate is rejected when at least two of up to six selected operators flag it. The original objective J = TP − FP was enumerated over every subset, then replaced by TP − (nTP/nFP) FP; the training counts were nTP=222 and nFP=1183 (Composition, p.7). Across 2,007,327 non-vacuous subsets of the larger 35-operator pool, zero harmed the held-out endpoint, with minimum delta +0.0007 (p.8). Inference: a Verus checker ensemble can use several independent predicates and a Rust vote function, but proof conjunction is usually safer than a statistical threshold; the weighted objective is useful for choosing which checks to run, not for weakening a required safety proof.

relevance to VL and threat

Inference: EvalCEGAR directly suggests a Verus-proof search loop: collect failing proof obligations as blind spots, ask for a targeted lemma or invariant, compile and verify it, and admit only changes that improve a held-out behavior oracle. The threat to agent-written verified Rust is medium: the paper shows executable checker synthesis transfers across code benchmarks, but it does not establish specification adequacy, Rust memory safety, or Verus proof soundness. VL should reuse the collision-targeting and interface-escalation ideas, while measuring proof repair cost and false assurances. Existing work already supplies CEGAR, solver-backed checking, and Verus contracts; VL should not redo those as if they were new.

techniques for the catalog

• collision-targeted CEGAR: find same-signature correct/incorrect pairs and synthesize a checker that separates the class
• interface escalation: widen checker inputs after repeated failures on the same blind spot
• null-calibrated admission: accept checks on held-out decision improvement against size-matched shuffles
• weighted vote composition: enumerate small check subsets and weight false alarms by the deployment endpoint

Checked 2026-10-15 against the paper by a Codex agent for metrics_that_write_themselves_20261014.md: checked quotations, numbers, references, techniques, and conclusions; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15