feat(autoresearch): certify autonomous proof decomposition

Require bounded, isolated proof workers to produce host-validated premise audits and complete Lean reduction certificates so false or irrelevant branches cannot masquerade as mathematical progress.

Co-authored-by: Cursor <cursoragent@cursor.com>

Author: 2 people

autoresearch/prefill/lean_gate.py

@@ -58,6 +58,11 @@ def _signature_only(source: str) -> str:
     return source[:match.start()].strip() if match else source.strip()
 
 
+def lean_theorem_signature_hash(source: str) -> str:
+    signature = " ".join(_signature_only(source).split())
+    return hashlib.sha256(signature.encode()).hexdigest() if signature else ""
+
+
 def _run_lean(
     content: str,
     *,
@@ -212,8 +217,7 @@ def validate_lean_signature(
             status="TYPECHECK_FAILED",
             error="theorem signature must end with `:= by` proof scaffold",
         )
-    signature = " ".join(_signature_only(source).split())
-    signature_hash = hashlib.sha256(signature.encode()).hexdigest()
+    signature_hash = lean_theorem_signature_hash(source)
     content = (
         "import KakeyaLeanGate\n\n"
         "set_option autoImplicit false\n\n"
@@ -289,3 +293,75 @@ def validate_lean_signature(
         elapsed_s=total_elapsed,
         output=output,
     )
+
+
+def validate_lean_proof(
+    source: str,
+    *,
+    project_root: Path,
+    timeout_s: float = 45.0,
+) -> LeanSignatureResult:
+    """Compile one complete theorem without sorry/admit or added axioms."""
+    source = source.strip()
+    if (
+        not source
+        or len(source) > 12_000
+        or _FORBIDDEN.search(source)
+        or re.search(r"\b(?:sorry|admit)\b", source)
+    ):
+        return LeanSignatureResult(
+            source,
+            "",
+            False,
+            status="UNSAFE_REJECTED",
+            error="Lean proof is empty, unsafe, oversized, or incomplete",
+        )
+    declarations = re.findall(
+        r"^\s*theorem\s+([A-Za-z_][\w']*)",
+        source,
+        re.MULTILINE,
+    )
+    if len(declarations) != 1 or not re.search(r"\s*:=\s*by\b", source):
+        return LeanSignatureResult(
+            source,
+            "",
+            False,
+            status="TYPECHECK_FAILED",
+            error="expected exactly one complete theorem declaration",
+        )
+    proof_hash = hashlib.sha256(source.encode()).hexdigest()
+    run = _run_lean(
+        "import KakeyaLeanGate\n\nset_option autoImplicit false\n\n"
+        + source
+        + "\n",
+        project_root=project_root,
+        timeout_s=timeout_s,
+    )
+    if run.timed_out:
+        return LeanSignatureResult(
+            source,
+            proof_hash,
+            False,
+            status="TYPECHECK_TIMEOUT",
+            error=f"Lean proof timed out after {timeout_s:.1f}s",
+            elapsed_s=run.elapsed_s,
+            output=run.output,
+        )
+    if run.returncode != 0:
+        return LeanSignatureResult(
+            source,
+            proof_hash,
+            False,
+            status="TYPECHECK_FAILED",
+            error=f"Lean proof failed: {run.output[-2000:]}",
+            elapsed_s=run.elapsed_s,
+            output=run.output,
+        )
+    return LeanSignatureResult(
+        source,
+        proof_hash,
+        True,
+        status="PROVED",
+        elapsed_s=run.elapsed_s,
+        output=run.output,
+    )

autoresearch/prefill/program.md

@@ -1,6 +1,6 @@
 # Prefill AutoResearch Program
 
-You are optimizing the two-Mac full-context RH proof research system.
+You are optimizing the two-Mac retained-interface RH proof research system.
 
 ## Ownership
 
@@ -36,7 +36,7 @@ Use a lexicographic objective:
 3. Modify only `candidate.py`.
 4. Verify Primary and allens health without restarting either service.
 5. Preserve all KV caches across decomposition iterations.
-6. Run the fixed full-context acceptance workload.
+6. Run the fixed retained-capacity certified-interface acceptance workload.
 7. Run `prepare.py` against the resulting report.
 8. Keep the candidate only if every hard constraint passes and it closes an
    obligation, falsifies a novel hypothesis, or creates a novel smaller
@@ -48,15 +48,55 @@ contain a falsifiable hypothesis plus distinct Generator and Critic directives.
 Normal iterations use the deterministic host candidate and do not call the
 Strategy model. Invoke Strategy Gemma only after three consecutive
 non-progressing runs, after a falsified branch, or via an explicit CLI/trigger
-file request.
-If an optional Strategy replan exceeds its lossless Prefill budget, defer the
+file request. A valid premise invalidation is also an immediate event-driven
+Strategy trigger. It is informative recovery, but does not reset mathematical
+stagnation as proof progress.
+If an optional Strategy replan exceeds its exact-interface retained budget, defer the
 replan and continue immediately with the deterministic host candidate. Never
 truncate the Strategy prompt and never stop the GAN proof loop for this
 control-plane admission failure.
 An unresolved Critic verdict must isolate one strictly smaller missing lemma;
-the host records that lemma as a deduplicated child obligation. Completed GAN
-runs, transcripts, checkpoints, and ledger updates remain durable even when the
-candidate strategy is reverted or fixed evaluation fails.
+that free-form text is only a trigger for certified decomposition and never
+creates a child directly. Completed GAN runs, transcripts, checkpoints, and
+ledger updates remain durable even when the candidate strategy is reverted or
+fixed evaluation fails.
+
+## Certified decomposition
+
+Certified decomposition is the authoritative and only child-persistence path.
+For an unresolved frontier, seven isolated fresh-session workers run in order:
+Definition Auditor, Counterexample Worker, Decomposer, Formalizer, Prover,
+Adversarial Proponent, and Judge. Every role uses allens Prefill and Primary
+decode with no shared session/KV state; only explicit host-packaged artifacts
+and hashes flow forward. Raw transcripts and parsed artifacts are persisted in
+one private atomic manifest. Any timeout, malformed binding, or role failure
+fails open without ledger mutation.
+
+Every role artifact binds the exact target ID, parent statement hash, immutable
+root-goal hash, producer role/run ID, and all upstream artifact hashes.
+Decomposer labels are temporary: only the host assigns persistent IDs after
+the complete certificate passes. The proposed graph must be acyclic, all
+labels must exist, and the one-step certificate must contain exactly one child
+and reduction label. That child—including a definition obligation—must occur
+in the explicit reduction contract. Deeper graphs are discovered recursively
+across later certified iterations.
+
+Formalizer must preserve an existing parent Lean signature/hash exactly, or
+propose a new parent signature only for an `UNFORMALIZED` parent. Parent and
+all child signatures must pass the pinned signature gate. The reduction
+signature may assume the child propositions and declared public assumptions,
+but Prover must provide a complete proof of that exact reduction theorem.
+`sorry`, `admit`, axioms, unsafe commands, placeholders, signature changes,
+disconnected children, semantic duplicates, and vague glossary tasks reject
+the entire bundle. Judge receives only the host-generated verification
+manifest and cannot override a failed host gate.
+
+Lean certification proves only that the formal child propositions and public
+assumptions suffice for the exact formal parent proposition in the accepted
+reduction theorem. The mapping from mathematical prose to Math IR and Lean
+propositions remains model-authored semantic translation; host hashes,
+typechecking, and adversarial review make that translation explicit but do not
+prove it faithfully represents the intended informal mathematics.
 
 Worker lifecycle and cache policy belong to the inference serving plane, not
 the proof experiment. `prefill_compute_chunk_tokens` is immutable during this
@@ -65,21 +105,107 @@ benchmark here. Model/tokenizer/quantization/rope/window/cache-format changes
 must be deployed outside this supervisor. Cold benchmarks are explicit,
 separate invocations of `scripts/benchmark_prefill_architecture.py`.
 
-Prefill budgets are hard admission limits, never truncation instructions.
-Strategy input must fit 8448 tokens by carrying the complete active leaf
-ancestry and its exact experiment records. Generator and Critic inputs must fit
-6144 tokens; the Critic always receives the complete current Generator output.
-Repeated Strategy strings are interned once in `text_by_id`; `_ref` fields
-losslessly reference that exact text.
-If any complete semantic unit exceeds its budget, reject it before remote
-Prefill and preserve the checkpoint. Never slice, sample, summarize, or drop
-the tail of an over-budget input.
+Retained KV capacity—not nominal Prefill admission—is the hard model-call
+limit. The deployed default is sink 4 + window 2048 = 2052 tokens. Every
+Strategy, Generator, Critic, premise, and certified-role chat template is
+counted before append and must fit `min(configured prefill,
+max_retained_tokens)`, including explicit control/decode reserve where needed.
+No call may rely on evicted middle tokens.
+
+Every active model call receives one exact `ProofStepInterface`: immutable root
+hash, exact target statement, exact formal target/parent certificate interface,
+public assumptions, immediate dependency interface, relevant active no-go
+premises, current target evidence, and archive hashes. Eleven-node prose
+ancestry and historical evidence are not active context. They remain durable
+and hash-addressed; this is state selection, not an LLM summary and not a claim
+of arbitrary natural-language full-attention equivalence.
+
+Strategy proposes exactly one next proof step/question. Generator emits exactly
+one bounded ISSUE_RESPONSE. Before Generator decode, the host reserves enough
+retained capacity for Critic's fixed package plus the complete Generator
+output; Critic receives that output byte-for-byte with the same exact
+ProofStepInterface. Certified Decomposer proposes exactly one child per
+certificate; recursive later iterations perform deeper decomposition.
+
+If an exact statement, structured artifact field, ISSUE block, dependency
+node, or Lean source is indivisible and too large, fail closed with
+`SEMANTIC_UNIT_TOO_LARGE`. Never slice tokens or strings, drop tails, or call a
+model summary lossless. Recursive decomposition preserves exact certified
+interfaces and reduction semantics, not arbitrary prose-history equivalence.
+
+The concise stable `STRATEGY_CONTRACT` in `supervisor.py` is the authoritative
+deterministic projection of this human-owned program for Strategy inference.
+It includes the objective, event triggers, obligation/no-go/premise recovery
+rules, exact-target requirement, immutable candidate/runtime constraints, and
+the no-fallback/no-truncation contract. The full program remains authoritative
+for host behavior but is not serialized into every Strategy prompt.
 
 Obligation IDs are host-owned. Treat IDs emitted by Generator/Critic as
 untrusted labels and bind verdicts to the exact current target. Never persist a
 model-invented ID. Reject a proposed child when it duplicates an existing
 statement or lemma name, is highly similar to an ancestor, or is too vague to
-be falsifiable. A rejected cyclic frontier is `INCONCLUSIVE`, not progress.
+be falsifiable. Also reject any child that canonically or semantically repeats
+a persisted no-go premise. A rejected cyclic frontier is `INCONCLUSIVE`, not
+progress.
+
+Every `DISPROVED` ISSUE_VERDICT distinguishes
+`Invalidation: APPROACH|PREMISE_SUSPECTED`. Missing invalidation is legacy
+`APPROACH`; legacy transcript value `PREMISE` is only a suspicion. A suspicion
+must name `Premise refuted`, identify one evidence type, and provide a concrete
+one-line JSON artifact. It never directly closes or quarantines a branch.
+
+The worker automatically runs two fresh, ordered inference roles for every
+structurally valid suspicion. The isolated Premise Auditor returns
+`PREMISE_AUDIT` with `CONFIRMED|NOT_CONFIRMED|INCONCLUSIVE`, evidence
+type/source, confidence, artifact, and analysis. The isolated Adversarial
+Proponent then receives only the immutable goal, host-packaged suspicion, and
+complete Auditor output and returns `PREMISE_DEFENSE` with
+`RESCUED|NOT_RESCUED|INCONCLUSIVE`, exact correction/failure, and evidence.
+Each inference uses a distinct session on allens-prefill/Primary-decode; only
+explicit text crosses role boundaries. Both complete outputs and parsed
+artifacts are durably persisted. Any timeout, malformed output, or worker
+failure is an `INCONCLUSIVE` review and can never invalidate a premise.
+
+The host upgrades to `PREMISE_INVALIDATED` only on a structurally valid
+suspicion, Auditor `CONFIRMED` at confidence >= 0.8, Proponent `NOT_RESCUED`,
+and a deterministically verified artifact. Arithmetic evidence uses one
+host-normalized `FOR_ALL` claim object (`variables`, domain, lhs, claimed
+relation, rhs). The host hashes this exact schema at suspicion time. The
+Auditor must preserve the schema/hash, bind every quantified variable exactly
+once, and provide a finite witness for which the Critic's claimed relation
+evaluates false. Unknown variables, true-but-unrelated arithmetic, missing
+bindings, schema changes, or hash changes are rejected.
+
+Lean evidence is bound to the target's host-recorded `lean_signature_hash` and
+must claim `NEGATION_OF_TARGET_SIGNATURE`. The current stored Lean signature
+format does not permit the host to safely synthesize an exact negation wrapper,
+so Lean artifacts are presently recorded but fail open to `INCONCLUSIVE` even
+if their standalone theorem compiles. Pinned theorem references are likewise
+untrusted until a local exact-assumption registry exists.
+
+Before upgrade, descendants retain their statuses and only reversible
+`SUSPECTED`/temporary-quarantine metadata is recorded. After upgrade, the host
+marks the target `DISPROVED/PREMISE_INVALIDATED`, quarantines descendants,
+stores one bound-schema-hash no-go lesson with confidence/evidence/worker-run
+provenance, and backjumps to the nearest sound unresolved ancestor. A later
+Auditor `NOT_CONFIRMED` or Proponent `RESCUED` deterministically restores prior
+statuses and marks quarantine/no-go records `REVERSED`. `APPROACH` failure
+never quarantines descendants or siblings.
+
+After a structurally valid suspicion completes review without verified
+upgrade (`NOT_CONFIRMED`, `RESCUED`, or `INCONCLUSIVE`), the host clears all
+temporary quarantine, restores descendants, preserves audit provenance, and
+closes only the attempted leaf as `DISPROVED/APPROACH_FAILED`. This fallback
+is allowed only when the original Critic DISPROVED evidence passed the existing
+strong closure gate. It creates no no-go lesson or premise quarantine.
+
+Only a host-upgraded invalidation triggers supervisor `premise-invalidated`.
+Suspicion initiates worker audit but is neither proof progress nor permanent
+falsification. The exact Strategy interface carries only active relevant no-go
+records. New candidates must not assume, rename, or reconstruct them. Lean
+signature typechecking remains merely `FORMALIZED` and does not establish
+premise truth; only the separate complete-proof gate can validate Lean
+evidence.
 
 `DECOMPOSED` is keepable only when the host actually persisted at least one
 new child that passed the ID, novelty, cycle, and falsifiability gates.