benchmarks: add triplewise-empty extremal proof audit - #413
benchmarks: add triplewise-empty extremal proof audit#413yuelgrace1810-ops wants to merge 3 commits into
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a3034f51b8
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| for item in family | ||
| ): | ||
| return False | ||
| if any(value < 0 or value >= n for item in family for value in item): |
There was a problem hiding this comment.
When a submission replaces the empty set in each otherwise valid construction with [NaN], Python's json.loads accepts the token and both range comparisons here evaluate false, so valid_family returns true even though NaN is not an element of any submitted ground set; the verifier can consequently award full reward to invalid mathematical witnesses. Require type(value) is int before applying the range check, which also prevents integral floats from bypassing the schema's integer requirement.
AGENTS.md reference: AGENTS.md:L111-L112
Useful? React with 👍 / 👎.
| contract | ||
| and "distinct subsets" in folded |
There was a problem hiding this comment.
When an otherwise valid submission uses a scope such as does not cover distinct subsets with triplewise empty intersection, both substring tests pass, so scope_accuracy is reported as 1 and the submission receives full reward despite explicitly disclaiming the task's scope. Compare against a canonical scope or use structured, clause-aware scope fields instead of rewarding keyword presence.
Useful? React with 👍 / 👎.
| and isinstance(submission.get("limitations"), list) | ||
| and all(type(item) is str for item in submission.get("limitations", [])) |
There was a problem hiding this comment.
When limitations is an empty list, all(...) is vacuously true and the contract still passes, allowing full reward even though the agent-visible schema requires minItems: 1. Enforce nonempty cardinality here so submissions cannot omit the limitation that communicates the finite-check and general-proof boundary.
Useful? React with 👍 / 👎.
| math_correct = False | ||
| try: | ||
| certificate = result["upper_bound_certificate"] | ||
| constructions = {item["n"]: item["family"] for item in result["constructions"]} |
There was a problem hiding this comment.
When a submission appends a fourth construction whose n duplicates one of the three canonical probes, this dictionary comprehension silently overwrites that entry; the resulting key set and families still pass, so the verifier awards full reward despite the public schema's maxItems: 3 contract. Validate that the raw construction list has exactly three entries with unique n values before converting it to a dictionary.
Useful? React with 👍 / 👎.
| and evidence_list_is_bound( | ||
| data.get("evidence"), expected_path="evidence/answer.txt" | ||
| ) |
There was a problem hiding this comment.
When an agent writes an empty or unrelated evidence/answer.txt and updates its descriptor digest, this call still marks evidence_validity true because it checks only the path and hash; with a valid typed result, the submission receives full reward without supplying any inspectable proof-repair evidence. Either document and validate semantic obligations for this file or remove it from the reward-bearing evidence contract.
AGENTS.md reference: AGENTS.md:L18-L20
Useful? React with 👍 / 👎.
| if not target.is_relative_to(root) or not target.is_file(): | ||
| return None | ||
| try: | ||
| if descriptor["sha256"] != sha256_uri(target): |
There was a problem hiding this comment.
When evidence/answer.txt is an enormous sparse regular file, even a deliberately wrong digest makes the verifier stream the entire file before rejecting it because this path has no size check. An agent can therefore exceed the 120-second verifier budget and prevent reward.json from being emitted without consuming equivalent physical storage; apply a bounded regular-file check before calling sha256_uri.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: aea673230b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| @@ -0,0 +1,4 @@ | |||
| FROM python:3.12-slim@sha256:57cd7c3a7a273101a6485ba99423ee568157882804b1124b4dd04266317710de | |||
| WORKDIR /app | |||
| COPY input.json /app/input.json | |||
There was a problem hiding this comment.
The environment Dockerfile copies only input.json, so the evaluated agent cannot access submission_schema.json; the instruction also omits the required /app/submission.json path and envelope names such as SOURCE_BOUND_REPAIRED and upper_bound_certificate. Outside the Oracle, an agent therefore has no visible way to discover the verifier's required output contract. Copy the schema into /app and state the output and evidence paths in the instruction.
AGENTS.md reference: AGENTS.md:L141-L144
Useful? React with 👍 / 👎.
| TESTS = Path("/tests") | ||
| MAX_SUBMISSION_BYTES = 16 * 1024 * 1024 | ||
| MAX_INPUT_BYTES = 16 * 1024 * 1024 | ||
| MAX_EVIDENCE_BYTES = 16 * 1024 * 1024 |
There was a problem hiding this comment.
Adding MAX_EVIDENCE_BYTES changes the canonical helper, but this commit updates only the new task's vendored copy. Running python tools/sync_harbor_verifier_support.py --check on the reviewed tree reports drift for all 133 pre-existing task bundles, so the benchmark contract gate fails and those verifier images retain the old unbounded evidence handling. Run the repository sync and include every generated copy.
AGENTS.md reference: AGENTS.md:L141-L144
Useful? React with 👍 / 👎.
| contract | ||
| and result["maximum_formula"] == "1+n+floor(n/2)" |
There was a problem hiding this comment.
When the submitted construction is mathematically correct but an unrelated envelope field is malformed—for example, evidence is missing or limitations has the wrong shape—strict_submission_contract makes contract false and this condition reports correctness: 0. The resulting diagnostics cannot distinguish a protocol failure from wrong mathematics, even though aggregate reward may still fail closed; validate the result's mathematical structure independently and apply the full envelope contract only at the aggregate boundary.
AGENTS.md reference: AGENTS.md:L111-L112
Useful? React with 👍 / 👎.
| certificate = result["upper_bound_certificate"] | ||
| constructions = {item["n"]: item["family"] for item in result["constructions"]} |
There was a problem hiding this comment.
An otherwise canonical submission can add arbitrary properties to result or to each construction object and still receive reward 1, because the verifier reads only the named fields and never checks either object's key set. This contradicts both additionalProperties: false declarations in the submission schema and allows contradictory or malformed claim data to accompany an accepted witness; validate the exact nested object shapes before constructing the lookup.
AGENTS.md reference: AGENTS.md:L141-L144
Useful? React with 👍 / 👎.
2 participants
Summary
Adds one independent Hard-provisional Regression benchmark,
triplewise-empty-extremal-audit, from Xerv-AI/GRAD train row 59 at immutable revision71595210590450202b7b69225bc07e9e01b13c5c(MIT).The source answer claims an extremal size of
2n. The task requires repairing that argument by:1+n+floor(n/2).Curation
n=7,8,11, and alternative maximum matchings are accepted.Verification boundary
The verifier independently reconstructs every submitted family, checks distinctness and exact triple intersections, checks element frequencies and the incidence budget, and validates the general typed certificate. Assurance is capped at
COMPUTED; no proof-assistant theorem is claimed.Validation
git diff --check: passjcb-postdoc-019host-contention failure passed immediately in isolated rerunnetwork_mode='no-network'provider-detection rejection--network none: full applicable reward 1.0The required GitHub Linux exact-task Oracle must pass before this draft is considered complete.