-
Notifications
You must be signed in to change notification settings - Fork 9
benchmarks: add finite Hadwiger minor certificate #599
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from 2 commits
Commits
Show all changes
11 commits
Select commit
Hold shift + click to select a range
4ad0bab
benchmarks: add finite Hadwiger minor certificate
2c18c68
fix(benchmarks): address hadwiger-minor verifier review comments
morluto bb4c1a7
fix(benchmarks): bound raw submission, remove evidence cap, refresh c…
morluto 28b5274
fix(benchmarks): repair hadwiger-triangle-free-minor-certificate CI c…
cursoragent 3031fa4
fix(benchmarks): parse mathematics independently, remove stale cap, p…
morluto d2dc004
fix(benchmarks): refresh hadwiger minor certificate contract
cursoragent 158df54
refactor hadwiger verifier complexity
cursoragent b31ad2f
fix(benchmarks): address Hadwiger minor certificate review comments
morluto efe6e27
fix(benchmarks): rename duplicate entries variable to fix mypy no-redef
morluto c0e4850
ci: trigger CI re-run
morluto 6b1e6be
fix: format validation_plan.py
morluto File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
13 changes: 13 additions & 0 deletions
13
...atasets/conjecture-probes-v1/hadwiger-triangle-free-minor-certificate/README.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| # Hadwiger triangle-free minor certificate | ||
|
|
||
| Regression-family task from retained row C-008. Its sole objective is a fully | ||
| checkable finite coloring/minor relationship: exhaustive rejection of all | ||
| three-colorings plus a connected `K4` branch-set model. Triangle-free and | ||
| minimum-degree requirements prevent a trivial complete-graph witness. | ||
|
|
||
| The verifier accepts vertex relabelings and alternative qualifying graphs. | ||
| Difficulty is provisional Hard due to simultaneous construction, coloring, | ||
| exhaustive lower-bound verification, and minor connectivity/adjoinment. | ||
|
|
||
| Source context: <https://mathworld.wolfram.com/HadwigerConjecture.html>, status | ||
| checked 2026-08-06. The authored finite fixture does not prove the conjecture. |
3 changes: 3 additions & 0 deletions
3
...sets/conjecture-probes-v1/hadwiger-triangle-free-minor-certificate/environment/Dockerfile
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,3 @@ | ||
| FROM python:3.12-slim@sha256:57cd7c3a7a273101a6485ba99423ee568157882804b1124b4dd04266317710de | ||
| COPY input.json submission_schema.json /app/ | ||
| WORKDIR /app |
1 change: 1 addition & 0 deletions
1
...sets/conjecture-probes-v1/hadwiger-triangle-free-minor-certificate/environment/input.json
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| {"task_id":"jacobian/hadwiger-triangle-free-minor-certificate","conjecture_id":"C-008","vertex_count":11,"edge_count":20,"required_chromatic_number":4,"required_minor_order":4,"require_triangle_free":true,"scope":"triangle-free-11-vertex-hadwiger-instance-v1"} |
136 changes: 136 additions & 0 deletions
136
...ure-probes-v1/hadwiger-triangle-free-minor-certificate/environment/submission_schema.json
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,136 @@ | ||
| { | ||
| "$defs": { | ||
| "branch": { | ||
| "items": { | ||
| "maximum": 10, | ||
| "minimum": 0, | ||
| "type": "integer" | ||
| }, | ||
| "maxItems": 8, | ||
| "minItems": 1, | ||
| "type": "array", | ||
| "uniqueItems": true | ||
| }, | ||
| "edge": { | ||
| "items": { | ||
| "maximum": 10, | ||
| "minimum": 0, | ||
| "type": "integer" | ||
| }, | ||
| "maxItems": 2, | ||
| "minItems": 2, | ||
| "type": "array" | ||
| } | ||
| }, | ||
| "$schema": "https://json-schema.org/draft/2020-12/schema", | ||
| "additionalProperties": false, | ||
| "properties": { | ||
| "claimed_assurance": { | ||
| "enum": [ | ||
| "UNVERIFIED", | ||
| "COMPUTED", | ||
| "CHECKED", | ||
| "VERIFIED" | ||
| ] | ||
| }, | ||
| "completeness": { | ||
| "const": "COMPLETE" | ||
| }, | ||
| "conclusion": { | ||
| "const": "FINITE_HADWIGER_K4_CERTIFICATE" | ||
| }, | ||
| "evidence": { | ||
| "items": { | ||
| "additionalProperties": false, | ||
| "properties": { | ||
| "path": { | ||
| "const": "evidence/answer.txt" | ||
| }, | ||
| "sha256": { | ||
| "pattern": "^sha256:[0-9a-f]{64}$", | ||
| "type": "string" | ||
| } | ||
| }, | ||
| "required": [ | ||
| "path", | ||
| "sha256" | ||
| ], | ||
| "type": "object" | ||
| }, | ||
| "maxItems": 1, | ||
| "minItems": 1, | ||
| "type": "array" | ||
| }, | ||
| "limitations": { | ||
| "const": [ | ||
| "ONE_TRIANGLE_FREE_11_VERTEX_GRAPH", | ||
| "EXHAUSTIVE_THREE_COLOR_REJECTION", | ||
| "NO_GLOBAL_HADWIGER_CONCLUSION" | ||
| ] | ||
| }, | ||
| "result": { | ||
| "additionalProperties": false, | ||
| "properties": { | ||
| "branch_sets": { | ||
| "items": { | ||
| "$ref": "#/$defs/branch" | ||
| }, | ||
| "maxItems": 4, | ||
| "minItems": 4, | ||
| "type": "array" | ||
| }, | ||
| "chromatic_number": { | ||
| "const": 4 | ||
| }, | ||
| "edges": { | ||
| "items": { | ||
| "$ref": "#/$defs/edge" | ||
| }, | ||
| "maxItems": 20, | ||
| "minItems": 20, | ||
| "type": "array", | ||
| "uniqueItems": true | ||
| }, | ||
| "four_coloring": { | ||
| "items": { | ||
| "maximum": 3, | ||
| "minimum": 0, | ||
| "type": "integer" | ||
| }, | ||
| "maxItems": 11, | ||
| "minItems": 11, | ||
| "type": "array" | ||
| }, | ||
| "minor_order": { | ||
| "const": 4 | ||
| } | ||
| }, | ||
| "required": [ | ||
| "edges", | ||
| "four_coloring", | ||
| "branch_sets", | ||
| "chromatic_number", | ||
| "minor_order" | ||
| ], | ||
| "type": "object" | ||
| }, | ||
| "scope": { | ||
| "const": "triangle-free-11-vertex-hadwiger-instance-v1", | ||
| "type": "string" | ||
| }, | ||
| "task_id": { | ||
| "const": "jacobian/hadwiger-triangle-free-minor-certificate" | ||
| } | ||
| }, | ||
| "required": [ | ||
| "task_id", | ||
| "conclusion", | ||
| "result", | ||
| "claimed_assurance", | ||
| "scope", | ||
| "completeness", | ||
| "evidence", | ||
| "limitations" | ||
| ], | ||
| "type": "object" | ||
| } |
31 changes: 31 additions & 0 deletions
31
...ts/conjecture-probes-v1/hadwiger-triangle-free-minor-certificate/instruction.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,31 @@ | ||
| # Construct a nontrivial finite Hadwiger certificate | ||
|
|
||
| Submit a simple connected triangle-free graph on vertices `0..10` with exactly | ||
| 20 edges and minimum degree at least 3. Supply a proper four-coloring and four | ||
| pairwise-disjoint nonempty branch sets witnessing a `K4` minor: every branch | ||
| set must induce a connected subgraph and every pair must have a crossing edge. | ||
|
|
||
| The verifier independently rejects every possible three-coloring by exact | ||
| backtracking, checks the submitted four-coloring, and validates the complete | ||
| minor model. Complete graphs, triangles, isolated padding, and label-only | ||
| chromatic claims are rejected. | ||
|
|
||
| Evidence is matching JSON with exactly `schema_version`, `task_id`, `result`, | ||
| and `limitations`, at most 2 MiB. This checks one finite graph only and does not | ||
| prove Hadwiger's conjecture. | ||
|
|
||
| <!-- BEGIN PUBLIC CONTRACT SUBMISSION BLOCK --> | ||
| ## Submission | ||
|
|
||
| Exact finite coloring and minor replay only; no global Hadwiger conclusion. | ||
|
|
||
| Write `/app/submission.json` to the exact schema in `environment/submission_schema.json`. The submission envelope requires `task_id`, `conclusion`, `result`, `claimed_assurance`, `scope`, `completeness`, `evidence`, and `limitations`. | ||
|
|
||
| - **Conclusion:** exactly `FINITE_HADWIGER_K4_CERTIFICATE` | ||
| - **Assurance:** scoreable values are `UNVERIFIED`, `COMPUTED`, `CHECKED` (ceiling `CHECKED`); the submission schema accepts any of `UNVERIFIED`, `COMPUTED`, `CHECKED`, `VERIFIED` but only scoreable assurances receive credit. | ||
| - **Scope:** the exact value declared in `submission_schema.json` | ||
| - **Completeness:** `COMPLETE`. | ||
| - **Evidence:** 1-1 item(s); allowed path(s): `evidence/answer.txt`; digest must match `^sha256:[0-9a-f]{64}$`. | ||
| - **Evidence media types:** `text/plain`. | ||
| - **Required artifact filenames:** `evidence/answer.txt`. | ||
| <!-- END PUBLIC CONTRACT SUBMISSION BLOCK --> | ||
77 changes: 77 additions & 0 deletions
77
.../datasets/conjecture-probes-v1/hadwiger-triangle-free-minor-certificate/solution/solve.py
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,77 @@ | ||
| from __future__ import annotations | ||
|
|
||
| import argparse | ||
| import hashlib | ||
| import json | ||
| from pathlib import Path | ||
|
|
||
| TASK_ID = "jacobian/hadwiger-triangle-free-minor-certificate" | ||
| LIMITATIONS = [ | ||
| "ONE_TRIANGLE_FREE_11_VERTEX_GRAPH", | ||
| "EXHAUSTIVE_THREE_COLOR_REJECTION", | ||
| "NO_GLOBAL_HADWIGER_CONCLUSION", | ||
| ] | ||
|
|
||
|
|
||
| def main(): | ||
| parser = argparse.ArgumentParser() | ||
| parser.add_argument("--root", type=Path, default=Path("/app")) | ||
| root = parser.parse_args().root | ||
| edges = [ | ||
| [0, 1], | ||
| [0, 4], | ||
| [0, 6], | ||
| [0, 9], | ||
| [1, 2], | ||
| [1, 5], | ||
| [1, 7], | ||
| [2, 3], | ||
| [2, 6], | ||
| [2, 8], | ||
| [3, 4], | ||
| [3, 7], | ||
| [3, 9], | ||
| [4, 5], | ||
| [4, 8], | ||
| [5, 10], | ||
| [6, 10], | ||
| [7, 10], | ||
| [8, 10], | ||
| [9, 10], | ||
| ] | ||
| result = { | ||
| "edges": edges, | ||
| "four_coloring": [0, 1, 0, 1, 2, 0, 1, 0, 1, 2, 3], | ||
| "branch_sets": [[0], [1], [2, 6], [3, 4, 5]], | ||
| "chromatic_number": 4, | ||
| "minor_order": 4, | ||
| } | ||
| payload = { | ||
| "schema_version": "1", | ||
| "task_id": TASK_ID, | ||
| "result": result, | ||
| "limitations": LIMITATIONS, | ||
| } | ||
| e = root / "evidence/answer.txt" | ||
| e.parent.mkdir(parents=True, exist_ok=True) | ||
| e.write_text(json.dumps(payload, sort_keys=True, separators=(",", ":")) + "\n") | ||
| s = { | ||
| "task_id": TASK_ID, | ||
| "conclusion": "FINITE_HADWIGER_K4_CERTIFICATE", | ||
| "result": result, | ||
| "claimed_assurance": "CHECKED", | ||
| "scope": "triangle-free-11-vertex-hadwiger-instance-v1", | ||
| "completeness": "COMPLETE", | ||
| "evidence": [ | ||
| { | ||
| "path": "evidence/answer.txt", | ||
| "sha256": "sha256:" + hashlib.sha256(e.read_bytes()).hexdigest(), | ||
| } | ||
| ], | ||
| "limitations": LIMITATIONS, | ||
| } | ||
| (root / "submission.json").write_text(json.dumps(s, sort_keys=True) + "\n") | ||
|
|
||
|
|
||
| if __name__ == "__main__": | ||
| main() |
3 changes: 3 additions & 0 deletions
3
.../datasets/conjecture-probes-v1/hadwiger-triangle-free-minor-certificate/solution/solve.sh
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,3 @@ | ||
| #!/bin/sh | ||
| set -eu | ||
| python /solution/solve.py |
39 changes: 39 additions & 0 deletions
39
benchmarks/datasets/conjecture-probes-v1/hadwiger-triangle-free-minor-certificate/task.toml
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,39 @@ | ||
| schema_version="1.4" | ||
| artifacts=["/app/submission.json","/app/evidence"] | ||
| [task] | ||
| name="jacobian/hadwiger-triangle-free-minor-certificate" | ||
| version="1.0.0" | ||
| description="Construct a triangle-free 4-chromatic graph with an exact K4 minor certificate." | ||
| keywords=["hadwiger","graph-coloring","clique-minor","triangle-free"] | ||
| [metadata] | ||
| evaluation_kind="conjecture-probe" | ||
| domain="mathematical-sciences" | ||
| primary_domain="graph-theory" | ||
| field="graph-minors" | ||
| assurance_ceiling="CHECKED" | ||
| answer_visibility="public" | ||
| provenance_class="authored-conjecture-probe" | ||
| fixture_digest="sha256:fc4ba259102fdf0f361c0393e7b540738ef18969631ebfb44a499c70b41ba0a5" | ||
| required_provider="core" | ||
| author_name="Jacobian contributors" | ||
| difficulty="hard" | ||
| category="mathematics" | ||
| tags=["difficulty-provisional","graph-coloring","clique-minor","exhaustive-verification","offline"] | ||
| case_version="conjecture-probes-v1" | ||
| contamination_class="authored-finite-conjecture-probe" | ||
| derivation="Derived from retained spreadsheet row C-008; the finite graph contract is authored and independently checked." | ||
| [agent] | ||
| timeout_sec=600.0 | ||
| [verifier] | ||
| timeout_sec=120.0 | ||
| environment_mode="separate" | ||
| [environment] | ||
| network_mode="no-network" | ||
| cpus=1 | ||
| memory_mb=1024 | ||
| storage_mb=4096 | ||
| [verifier.environment] | ||
| network_mode="no-network" | ||
| cpus=1 | ||
| memory_mb=1024 | ||
| storage_mb=4096 |
7 changes: 7 additions & 0 deletions
7
...s/datasets/conjecture-probes-v1/hadwiger-triangle-free-minor-certificate/tests/Dockerfile
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,7 @@ | ||
| FROM python:3.12-slim@sha256:57cd7c3a7a273101a6485ba99423ee568157882804b1124b4dd04266317710de | ||
| LABEL jacobian.task="jacobian/hadwiger-triangle-free-minor-certificate" \ | ||
| jacobian.checksum="97c73358d2fcc15771a1fa7401bc7dc7041549e11f1b4e9604ac6eb039b87726" | ||
| RUN python -m pip install --no-cache-dir attrs==26.1.0 jsonschema==4.26.0 jsonschema-specifications==2025.9.1 referencing==0.37.0 rpds-py==2026.6.3 typing-extensions==4.16.0 | ||
| COPY input.json public_contract.json test.sh verifier.py verifier_support.py /tests/ | ||
| COPY input.json /app/input.json | ||
| RUN chmod +x /tests/test.sh && python -c 'import json; assert json.load(open("/tests/input.json"))["task_id"] == "jacobian/hadwiger-triangle-free-minor-certificate"' |
1 change: 1 addition & 0 deletions
1
...s/datasets/conjecture-probes-v1/hadwiger-triangle-free-minor-certificate/tests/input.json
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| {"task_id":"jacobian/hadwiger-triangle-free-minor-certificate","conjecture_id":"C-008","vertex_count":11,"edge_count":20,"required_chromatic_number":4,"required_minor_order":4,"require_triangle_free":true,"scope":"triangle-free-11-vertex-hadwiger-instance-v1"} |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.