benchmarks: expose infinite-dimensional eigenvalue-set scope - #331
Conversation
e92ca74 to
71a32a2
Compare
yuelgrace1810-ops
changed the title
![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: 71a32a2ed9
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 71a32a2ed9
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3ee770b146
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 39d772a5e7
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 97c256ebb6
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: eedf538e40
ℹ️ 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".
The Publish Benchmark Timings job writes `.benchmark-timings.json` (a dotfile) and uploads it with `actions/upload-artifact`. Since v4.4.0 that action excludes hidden files by default, and the pinned action logs `include-hidden-files: false` regardless of the input, so with `if-no-files-found: error` the upload failed with "No files were found with the provided path: .benchmark-timings.json" on every benchmark PR run that reached the timings job (e.g. PR #331 run 30749872475, PR #321 run 30750885213). Keep `.benchmark-timings.json` as the collector output so the planner cache-restore and the main-branch cache-save (which use actions/cache, unaffected by the hidden-file exclusion) keep working unchanged. Add a minimal `cp` step after collection that stages a non-hidden `benchmark-timings.json`, and point only the Upload timing evidence step at that non-hidden file. No benchmark verifier or collector code changes. Generated with [Devin](https://devin.ai) Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
The Publish Benchmark Timings job writes `.benchmark-timings.json` (a dotfile) and uploads it with `actions/upload-artifact`. Since v4.4.0 that action excludes hidden files by default, and the pinned action logs `include-hidden-files: false` regardless of the input, so with `if-no-files-found: error` the upload failed with "No files were found with the provided path: .benchmark-timings.json" on every benchmark PR run that reached the timings job (e.g. PR #331 run 30749872475, PR #321 run 30750885213). Keep `.benchmark-timings.json` as the collector output so the planner cache-restore and the main-branch cache-save (which use actions/cache, unaffected by the hidden-file exclusion) keep working unchanged. Add a minimal `cp` step after collection that stages a non-hidden `benchmark-timings.json`, and point only the Upload timing evidence step at that non-hidden file. No benchmark verifier or collector code changes. Generated with [Devin](https://devin.ai) Co-authored-by: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 70fe21336d
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 357b90cd60
ℹ️ 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".
| rf"\bzero\b{relation_gap}\b(?:eigenvalue|eigenvector|" | ||
| rf"nontrivial kernel|nonzero kernel vector)\b{relation_gap}\b{zero}\b", | ||
| rf"\b{zero}\b{relation_gap}\b(?:zero eigenvalue|zero vector|" | ||
| rf"eigenvector|nontrivial kernel|nonzero kernel vector|kills|" |
There was a problem hiding this comment.
For the canonical orientation, an otherwise valid answer saying only ST has eigenvector e_1 receives full evidence credit because this alternative accepts bare eigenvector. Here e_1 is a 1-eigenvector of ST, so the evidence does not establish the structured claim that zero is an eigenvalue; require a zero eigenvector, the declared e_0, or another relation that specifically proves the zero eigenvalue.
AGENTS.md reference: AGENTS.md:L18-L19
Useful? React with 👍 / 👎.
| identity_role = positive_relation( | ||
| ( | ||
| rf"\bidentity\b{relation_gap}\b{identity}\b", | ||
| rf"\b{identity}\b{relation_gap}\b(?:identity|one-to-one|injective)\b", |
There was a problem hiding this comment.
An otherwise canonical submission whose evidence says only TS is injective receives full reward through this alternative, but injectivity does not establish the structured identity_product claim—the unilateral right shift itself is an injective non-identity operator. Require an explicit identity assertion or all-basis identity equation so the evidence is bound to the outcome being scored.
AGENTS.md reference: AGENTS.md:L18-L19
Useful? React with 👍 / 👎.
| if not isinstance(item, str) or "lean" not in item.casefold(): | ||
| continue |
There was a problem hiding this comment.
An otherwise canonical submission with the valid limitation Only the point spectrum is assessed, not the full operator spectrum receives zero reward because every item lacking the token lean is skipped. The instruction only says not to claim Lean compilation, and the schema exposes arbitrary limitation strings, so an agent cannot know that it must affirmatively restate non-compilation; either advertise this required limitation in the contract or accept submissions that make no positive Lean claim.
AGENTS.md reference: AGENTS.md:L21-L24
Useful? React with 👍 / 👎.
| @@ -0,0 +1 @@ | |||
| {"$schema":"https://json-schema.org/draft/2020-12/schema","type":"object","additionalProperties":false,"required":["task_id","conclusion","result","claimed_assurance","scope","completeness","evidence","limitations"],"properties":{"task_id":{"const":"jacobian/infinite-shift-spectrum-counterexample"},"conclusion":{"enum":["MISSING_FINITE_DIMENSIONAL_SCOPE","INSUFFICIENT_EVIDENCE"]},"result":{"type":"object","additionalProperties":false,"required":["orientation","basis_window","actions","zero_eigenvalue_product","identity_product","zero_eigenvector_basis_index","spectral_conclusion","missing_assumption"],"properties":{"orientation":{"enum":["S_RIGHT_T_LEFT","S_LEFT_T_RIGHT"]},"basis_window":{"type":"array","minItems":2,"maxItems":2,"prefixItems":[{"const":0},{"const":8}],"items":false},"actions":{"type":"array","minItems":9,"maxItems":9,"items":{"type":"object","additionalProperties":false,"required":["basis_index","s_output","t_output","st_output","ts_output"],"properties":{"basis_index":{"type":"integer"},"s_output":{"type":["integer","null"]},"t_output":{"type":["integer","null"]},"st_output":{"type":["integer","null"]},"ts_output":{"type":["integer","null"]}}}},"zero_eigenvalue_product":{"enum":["ST","TS"]},"identity_product":{"enum":["ST","TS"]},"zero_eigenvector_basis_index":{"const":0},"spectral_conclusion":{"const":"EIGENVALUE_SETS_DIFFER"},"missing_assumption":{"const":"FINITE_DIMENSIONALITY"}}},"claimed_assurance":{"enum":["UNVERIFIED","COMPUTED","CHECKED","VERIFIED"]},"scope":{"type":"string"},"completeness":{"enum":["COMPLETE","PARTIAL","UNKNOWN"]},"evidence":{"type":"array","minItems":1,"maxItems":1,"items":{"type":"object","additionalProperties":false,"required":["path","sha256"],"properties":{"path":{"const":"evidence/answer.txt"},"sha256":{"type":"string","pattern":"^sha256:[0-9a-f]{64}$"}}}},"limitations":{"type":"array","minItems":1,"items":{"type":"string"}}}} | |||
There was a problem hiding this comment.
For S_RIGHT_T_LEFT, an agent following the instruction's equation L(e_0)=0 can naturally submit integer 0 for t_output and st_output; that representation satisfies this schema but the verifier accepts only JSON null. Nothing agent-visible explains that integers denote basis-vector indices while null denotes the zero vector, so expose that encoding in the schema or instruction to prevent mathematically correct action tables from receiving zero reward.
AGENTS.md reference: AGENTS.md:L21-L24
Useful? React with 👍 / 👎.
2 participants
Summary
Adds
infinite-shift-spectrum-counterexample, an Assurance Harbor benchmark derived from ProofNet test row 65 (Axler|exercise_5_11) at immutable dataset revisioncb8e75614830035a37f3a2a11de5e625eaf0bc31(MIT).The proposed theorem states equality of the eigenvalue sets of
STandTSfor arbitrary endomorphisms, omitting finite dimensionality. The agent must construct unilateral left/right shifts on finitely supported rational sequences and replay both compositions on an exact basis window.Curation
Shortcut audit
No finite matrix can witness the required zero-eigenvalue asymmetry, so tiny finite brute force does not solve the task. A bare theorem citation or fixed label fails. The verifier derives every
S,T,ST, andTSbasis action from the selected symbolic shift orientation, requires all indices 0–8, and accepts both valid assignments of left/right shifts.Deduplication
Compared against main and all active benchmark PRs by source, statement, reasoning workflow, verifier strategy, failure mode, and assurance boundary. Unlike finite matrix counterexamples or informal/formal operator substitutions, this task specifically tests a theorem that becomes false when an infinite-dimensional scope restriction is omitted.
Validation
make harbor-check— 458 passedVERIFIED, incomplete scope, and unhashable assurancemake complexity-check— baseline unchanged; no new C901 violationgit diff --check— passedAssurance boundary
Maximum assurance is
COMPUTED. “Eigenvalue set” means the point spectrum, not the full operator spectrum. The finite basis window checks consistency with the declared unilateral-shift rules; the general composition identities follow from those symbolic rules rather than finite enumeration alone. The verifier does not claim Lean parsing, elaboration, compilation, complete-spectrum analysis, or theorem verification.