summaryrefslogtreecommitdiff
path: root/README.md
diff options
context:
space:
mode:
authorOscar Wan <oscarwan@stanford.edu>2026-07-24 20:45:42 -0700
committerOscar Wan <oscarwan@stanford.edu>2026-07-24 20:45:42 -0700
commit15efc30e9e7179accd30375d3edb2e34a3b4dc5f (patch)
treeba1c49eb128e7906ba451141723d763e1dcda53a /README.md
parent708f2af9c6985e9cb5cd53e434a7d3b8dfa2b4ac (diff)
updated generation process
Diffstat (limited to 'README.md')
-rw-r--r--README.md82
1 files changed, 54 insertions, 28 deletions
diff --git a/README.md b/README.md
index b1a3f8c..2a34006 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,9 @@
# GAP minimal reproduction package
-This repository provides a one-item end-to-end reproduction of GAP: four
-surface-renaming families and one verified kernel variant.
+This repository provides a one-item end-to-end reference implementation of
+GAP: four surface-renaming families and one verified kernel variant. The
+default kernel path executes the manuscript's five conceptual operations as
+five typed, separately saved model calls.
## One-click reproduction
@@ -10,14 +12,17 @@ Open `GAP_End_to_End.ipynb` and choose **Run All**. The notebook:
1. installs the package;
2. loads one canonical Putnam problem;
3. generates the four surface variants;
-4. extracts the kernel proof plan and mutable slots;
-5. generates a new question and complete solution with the same plan;
-6. runs five judges until the unchanged candidate receives two consecutive
+4. constructs a concrete proof DAG whose nodes are intermediate claims;
+5. abstracts one content-free method label per DAG node;
+6. records guarded old/new replacements and propagates them node by node;
+7. renders the diffused terminal claim into a new question and solution;
+8. runs five judges until the unchanged full-provenance bundle receives two consecutive
unanimous rounds;
-7. exports and validates one machine-readable GAP record.
+9. exports and validates one machine-readable GAP record.
-The default model is `o3`. Set `OPENAI_API_KEY` before starting Jupyter, or
-enter it in the notebook's hidden prompt. The key is never saved.
+The default model is `o3`. Set `OPENAI_API_KEY`, place
+`OPENAI_API_KEY=...` in the gitignored `.env` file, or enter it in the
+notebook's hidden prompt. The key is never written to run artifacts.
For a no-API software check:
@@ -31,25 +36,28 @@ mathematics.
## Prompt fidelity
-Generation, surface-renaming, judge, and repair prompts are copied verbatim
-from the original author source and the prompt listing in the paper. Their
-UTF-8 SHA-256 digests are pinned in `PROMPT_SHA256SUMS` and enforced by
-`tests/test_prompts.py`.
+The historical two-call Prompt-A/Prompt-B, surface-renaming prompts, and
+review/repair prompts recovered from `PutnamVariants@c3bed737` remain byte
+pinned in `src/gap_pipeline/prompts.py`, `PROMPT_SHA256SUMS`, and
+`tests/test_prompts.py`. They document the actual original generator.
-The OpenAI adapter does not send `temperature`; this is compatible with `o3`,
-whose supported value is its default.
+The executable manuscript-aligned prompts are in
+`src/gap_pipeline/kernel_prompts.py`. They refine the historical intent into
+five explicit contracts because the recovered original generator only made
+two calls and did not emit a concrete DAG, applied replacement map, or
+node-by-node diffusion trace. This distinction is deliberate and auditable,
+not hidden as prompt identity.
-The conceptual five stages are represented explicitly in saved artifacts.
-The original implementation batches stages 1–3 into Prompt-A and stages 4–5
-into Prompt-B; the wrapper does not change those prompts. See `STAGE_MAP.md`.
+The OpenAI adapter does not send `temperature`; this is compatible with `o3`,
+whose supported value is its default. See `STAGE_MAP.md` for the exact
+paper-to-code and historical-source maps.
-Prompt-A's ordered core steps instantiate a path-structured proof-plan DAG:
-each step is a typed node and each edge records the dependency on the preceding
-step. `ProofPlanDAG` validates unique node IDs, known dependencies, acyclicity,
-connectivity to the terminal node, and the extracted order. This path structure
-is the precise graph induced by an ordered minimal proof chain. Judges receive
-the same method-label sequence with stable node IDs and must report a check for
-every node before their verdict is counted.
+`ProofDAG` supports branching dependencies and validates topological order,
+known dependencies, acyclicity, and terminal connectivity. Replacement plans
+record the exact old/new value, source node, guard condition, and guard
+justification. Diffusion must preserve every node ID, dependency, and method
+label. Judges must cover every proof-node ID and replacement-slot ID before
+their verdict counts.
## Install and test
@@ -65,6 +73,14 @@ PYTHONPATH=src pytest
PYTHONPATH=src python -m gap_pipeline.cli --help
```
+PowerShell equivalents:
+
+```powershell
+$env:PYTHONPATH = "src"
+python -m pytest
+python -m gap_pipeline.cli --help
+```
+
## Live one-item commands
Generate the kernel variant:
@@ -79,6 +95,9 @@ PYTHONPATH=src python -m gap_pipeline.cli generate-kernel \
--judge-model o3
```
+In PowerShell, use `$env:OPENAI_API_KEY = "..."` and backticks for line
+continuation, or use the gitignored `.env` file through the notebook.
+
Generate all surface variants:
```bash
@@ -103,7 +122,14 @@ PYTHONPATH=src python -m gap_pipeline.cli export-release \
## Verification protocol
Kernel verification uses `J=5` judges, requires `K=2` consecutive unanimous
-rounds for the same candidate, and allows at most `T=15` rounds. A rejected
-round resets the streak and triggers a complete question-and-solution repair.
-Every call, stage output, iteration, and final record is saved under the chosen
-run directory.
+rounds for the same complete provenance bundle, and allows at most `T=15`
+rounds. A rejected round resets the streak and reruns stages 3--5 from a new
+guarded replacement plan using the judge feedback. Every call, stage output,
+iteration, and final record is saved under the chosen run directory.
+
+## Scope
+
+This package demonstrates and tests the one-item software path. It does not
+reconstruct unavailable proposal/rejection logs from the original 1,051-item
+generation run, and a successful LLM verification loop is not a substitute for
+the separate blinded mathematical audit described in the rebuttal plan.