跳到正文
DEV Community· Finley Zhou·· 2 小時前AI 評分58

無法被反例推翻的性質不算門檻:AI 智能體補丁的失敗見證

A Property You Cannot Falsify Is Not a Gate: Failure Witnesses for Agent Patches

AI 導讀

AI 智能體生成補丁的合併門檻應要求每項新增性質通過審查者固定的有效樣例,並拒絕審查者撰寫的反例,才計入證據。約 70 行標準庫 Python harness 預設重複執行三次,將檢查分為五種 verdict,並以雜湊固定 fixture;不確定結果須隔離並設定到期日,不應取多數決。此方法不適用於統計性質和存在性質;作者亦披露,文章是 MonkeyCode 的產品推廣內容。

正文

A Property You Cannot Falsify Is Not a Gate: Failure Witnesses for Agent Patches

An agent patch that adds a passing test suite still proves almost nothing. To earn a merge slot, every property it adds should carry a falsification witness: a concrete input that the property must reject, authored by the person reviewing the patch rather than the person who wrote it.

That one requirement converts a boolean "tests pass" signal into something countable. A pinned fixture plus a witness is exactly one bit of evidence: the property admits one payload and rejects another. Twenty assertions without a witness are usually zero bits.

Below is a three-part strategy for agent-generated patches: witness-carrying property checks, fixtures pinned by the reviewer, and a freeze that withdraws any property whose answer changes between repeated runs. The harness is about 70 lines of standard-library Python.

Why a correct property can still carry no evidence

The failure mode worth designing against is not the obvious tautology (a check that returns True for every input). It is the property that is genuinely non-trivial, matches its own stated intent, and is still blind to the class of bad input the reviewer actually cares about.

Start with a spend guard an agent might plausibly write:

def within_cap(payload: dict) -> bool:
    """Admit a ledger whose entries do not exceed its cap."""
    return sum(payload["entries"]) <= payload["cap"]

This is a real invariant. It is not a tautology. It also does not survive contact with one reviewer-authored input:

{"cap": 10, "entries": [12, -3]}   # sum == 9, but 12 was drawn against a cap of 10

The property admits it, because a negative entry masks an over-cap draw. The agent never found this, because the agent only ever supplied fixtures — inputs it expected to pass. It never supplied an input the property had to reject.

Coverage will not catch this either. The line executes. The branch is taken. The suite is green.

Step 1 — Make the witness part of the property contract

A property is not a Callable[[dict], bool]. It is a tuple of three things, and two of them come from the review side.

"""witness_gate.py — a property is evidence only if it rejects a witness it did not author."""
from __future__ import annotations

import hashlib
import json
from dataclasses import dataclass
from typing import Callable


@dataclass(frozen=True)
class Case:
    id: str
    payload: dict


@dataclass(frozen=True)
class Property:
    name: str
    check: Callable[[dict], bool]  # True == payload admitted
    fixture: Case                  # reviewer-pinned: must be admitted
    witness: Case                  # reviewer-authored: must be rejected

With that shape, the two cases instantiate the domain above:

FIXTURE_CAP = Case("f-cap-01", {"cap": 10, "entries": [4, 3]})
WITNESS_CAP = Case("w-cap-01", {"cap": 10, "entries": [12, -3]})

If the patch author cannot produce a witness for a property, the property is not rejected — it is simply reclassified as something that does not count toward the merge decision.

Step 2 — Classify every probe into five verdicts

This is the core of the gate. Note that a probe runs the property more than once: an answer that is not stable is not a measurement.

def run_probe(prop: Property, repeats: int = 3) -> dict:
    seen = []
    for _ in range(repeats):
        try:
            admitted_fixture = bool(prop.check(prop.fixture.payload))
            admitted_witness = bool(prop.check(prop.witness.payload))
        except Exception as exc:
            return {"property": prop.name, "verdict": "ERROR", "detail": repr(exc)}
        seen.append((admitted_fixture, admitted_witness))

    if len(set(seen)) != 1:
        return {
            "property": prop.name,
            "verdict": "NONDETERMINISTIC",
            "detail": sorted(repr(s) for s in set(seen)),
        }

    admitted_fixture, admitted_witness = seen[0]
    if not admitted_fixture:
        return {"property": prop.name, "verdict": "FIXTURE_BROKEN"}
    if admitted_witness:
        return {"property": prop.name, "verdict": "UNFALSIFIED"}
    return {"property": prop.name, "verdict": "WITNESS_HELD"}

Five verdicts, five different meanings for the reviewer:

Verdict Meaning Evidence bit
WITNESS_HELD admits the fixture, rejects the witness 1
UNFALSIFIED admits a payload the reviewer considers invalid 0
FIXTURE_BROKEN rejects a payload the reviewer considers valid 0
NONDETERMINISTIC the same payload gets different answers 0
ERROR the property raised instead of deciding 0

UNFALSIFIED is the interesting one, and it is not an accusation of laziness. It usually means the property encodes a narrower invariant than the reviewer's threat model — exactly the spend-guard case above. The remedy is either a stronger property or an explicit decision to accept the narrower one, written down.

Step 3 — Pin the fixture set outside the patch

Witnesses are cheap to author, which means they are also cheap to weaken. Freeze the fixture side with a digest that the patch cannot edit:

def fixture_digest(cases) -> str:
    blob = json.dumps(
        [{"id": c.id, "payload": c.payload} for c in sorted(cases, key=lambda c: c.id)],
        sort_keys=True,
        separators=(",", ":"),
    ).encode()
    return "sha256:" + hashlib.sha256(blob).hexdigest()

The reviewer stores fixtures.json and its digest in a config file that lives outside the patch's diff. At gate time:

HARD = {"UNFALSIFIED", "FIXTURE_BROKEN", "ERROR"}


def gate(properties, expect_digest: str, repeats: int = 3):
    if fixture_digest([p.fixture for p in properties]) != expect_digest:
        return 3, [{"property": "*", "verdict": "FIXTURE_DRIFT"}]
    rows = [run_probe(p, repeats) for p in properties]
    if any(r["verdict"] in HARD for r in rows):
        return 2, rows
    return 0, rows

A representative run looks like this:

$ python witness_gate.py --expect-digest sha256:9f2c41e8...
P1 within_cap         WITNESS_HELD      fixture=admit witness=reject
P2 cap_monotonic      UNFALSIFIED       witness {"cap":10,"entries":[12,-3]} admitted
P3 entry_non_negative NONDETERMINISTIC  [(True, False), (True, True), (True, False)]
exit 2 — 1 unfalsified, 1 quarantined (nondeterministic), expires 2026-11-15

Step 4 — Read the gate with a decision table

Exit codes are not enough on their own; the reviewer needs to know what each verdict does to the merge decision.

Situation Blocks merge Counts as evidence Reviewer action
All properties WITNESS_HELD no yes merge
Any UNFALSIFIED yes no author a stronger property, or narrow the claim in writing
Any FIXTURE_BROKEN yes no re-pin the fixture deliberately, as its own change
Any ERROR yes no fix the harness first
Only NONDETERMINISTIC no no quarantine with an expiry date
FIXTURE_DRIFT yes no investigate who touched fixtures.json

Exit 0 means every property in the patch measured a bit. Exit 2 means at least one claim is unverified. Exit 3 means the measuring instrument moved.

One operational note: the number of bits is not the number of tests. A patch with two witness-carrying properties carries two bits, regardless of how many parametrized cases wrap them.

Step 5 — Freeze nondeterminism instead of averaging it

A property that admits the witness on one run and rejects it on the next is a coin flip, not a measurement. Repeating it five times and taking the majority does not recover the evidence; it manufactures confidence that the property never supplied.

The freeze here is narrower than a general flaky-test budget: it withdraws the property, not the test. A quarantined property cannot be cited in the merge note, gets an expiry timestamp, and if it is still nondeterministic at expiry it is deleted rather than re-quarantined. Deleting a flaky property is cheaper than defending it.

Limitations, and who should not use this

  • Statistical properties break this. If the invariant is a rate, a distribution, or a sampled threshold, a single witness rejection is meaningless. Use differential or bound-based testing instead.
  • Existence properties have no natural witness. "Some configuration admits the request" cannot be falsified by one payload; skip the witness requirement and say so explicitly.
  • If no one can author a witness, the gate is theater. A reviewer who cannot construct a concrete bad input does not understand the invariant well enough to approve it. That is a staffing constraint, not a tooling one.
  • Small solo scripts should not pay this cost. One file, one caller, no agent in the loop — a fixture and a witness is ceremony. The harness pays off when patches arrive faster than a human reads them.
  • This does not detect wrong-but-self-consistent patches. Both the property and the witness come from the same reviewer. WITNESS_HELD means the property discriminates between two inputs the reviewer chose, nothing more.

Running it next to the patch agent

I drive the patch-producing agent through MonkeyCode's free model access and run this harness on the free server option — both are operator-supplied availability claims, not benchmarks, and the harness itself is portable to any runner with Python.

Disclosure: This article was prepared as part of MonkeyCode's product outreach.

The loop that matters is short: agent proposes a property, reviewer supplies the witness, gate returns one bit or zero bits, and a zero-bit property never reaches the merge note. If you want to try it end to end, the free server option is enough to run the gate beside the agent that wrote the patch.

來源:DEV Community · dev.to