feat(benchmarks): add symmetric polynomial divisibility certificate - #334
Conversation
c8127fd to
95a26b4
Compare
![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: c8127fdc2e
ℹ️ 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".
|
Codex Review: Didn't find any major issues. What shall we delve into next? Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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: fca3890e3c
ℹ️ 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: a92b99b37e
ℹ️ 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: 590f211611
ℹ️ 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: 0db173fbe8
ℹ️ 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: 4f9c953062
ℹ️ 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 verifier.py for symmetric-polynomial-divisibility was updated without refreshing the jacobian.checksum label in tests/Dockerfile, so the Benchmark Prospective Digest Checks gate failed with "verifier checksum label is stale". Update the label to sha256(verifier.py), which is the canonical value Harbor's check_harbor_dataset expects. 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: c316ac4059
ℹ️ 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: dc06808243
ℹ️ 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: ac4d66d877
ℹ️ 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".
| """Parse a submission as one JSON object, rejecting malformed input.""" | ||
|
|
||
| try: | ||
| value = json.loads(path.read_text()) |
There was a problem hiding this comment.
With this task's 4 GB agent storage and 1 GB verifier memory limit, an agent can leave a multi-gigabyte submission.json; read_text() attempts to load the entire file and can OOM before reward.json is written, rather than scoring the malformed submission as a non-conclusion. Reject symlinks, non-regular files, and files above a small size limit before reading, as the bounded workflow verifiers do.
AGENTS.md reference: AGENTS.md:L86-L89
Useful? React with 👍 / 👎.
| and all(term in scope_text for term in ("ideal", "integer", "divis")) | ||
| and not re.search( | ||
| r"(?:\b(?:no|not|without|excluding|exclude|only)\b" | ||
| r"[\s_-]{0,20}(?:ideal|integer|divis)|" | ||
| r"\bno[_-](?:ideal|integer|divis))", |
There was a problem hiding this comment.
Fresh evidence after the prior scope fix is that the new negative-lookaround still accepts negation placed after the keywords: a valid certificate with scope ideal integer divisibility are all false satisfies these checks and receives full scope credit and aggregate reward. Since expected.json supplies required_scope, compare against that declared value rather than attempting to infer meaning from keyword order.
Useful? React with 👍 / 👎.
morluto
changed the title
2 participants
Summary
Adds
symmetric-polynomial-divisibility, an independent Regression Harbor benchmark derived fromlm-provers/FineProofs-SFTtrain row 323 at immutable revision73661e62811cf2940a0d3f82788a4f4332204c2f(Apache-2.0).The task asks the agent to synthesize exact sparse-polynomial multipliers proving that a quartic symmetric target belongs to the ideal generated by the two divisibility hypotheses.
Quality gate
Shortcut audit
Numeric substitutions, checking a bounded residue range, or asserting the divisibility conclusion cannot pass. The verifier parses canonical rational sparse polynomials, independently multiplies each submitted multiplier by its generator, and compares every resulting coefficient with the target. Any mathematically valid certificate within the degree bound is accepted.
The public source proof remains a contamination limitation, so this task is regression evidence rather than held-out capability evidence.
Deduplication
Checked against main and all active drafts by source, statement, workflow, verifier strategy, failure mode, and assurance boundary. Unlike the continuant and trigonometric recurrence tasks, this benchmark tests multivariate ideal membership and modular transfer; it has no recurrence, valuation, or finite-search objective.
Validation
make harbor-check— 458 passedmake complexity-check— baseline unchangedgit diff --check— passedAssurance boundary
The clean-room verifier establishes the submitted polynomial identity exactly over
QQ. The modular conclusion follows for integer inputs from closure of divisibility under integer-polynomial linear combinations. No proof-assistant verification record is produced, so the maximum assurance isCOMPUTED.