無法被反例推翻的性質不算門檻:AI 智能體補丁的失敗見證
A Property You Cannot Falsify Is Not a Gate: Failure Witnesses for Agent Patches
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_HELDmeans 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