diff --git a/autoresearch/prefill/program.md b/autoresearch/prefill/program.md index 627cbd5..87ce340 100644 --- a/autoresearch/prefill/program.md +++ b/autoresearch/prefill/program.md @@ -65,6 +65,12 @@ 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. +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. + Do not optimize output wording, scores, prizes, or other proof-irrelevant content. Prefill performance is a tertiary objective after mathematical decomposition progress, while preserving the complete semantic contract. diff --git a/scripts/agent_gan_repl.py b/scripts/agent_gan_repl.py index e41d99f..4961a18 100644 --- a/scripts/agent_gan_repl.py +++ b/scripts/agent_gan_repl.py @@ -4,6 +4,7 @@ import argparse import atexit +import difflib import hashlib import json import os @@ -282,11 +283,33 @@ def generator_issue_coverage( return covered, required - covered +def _resolve_model_obligation_id( + model_id: str, + allowed_ids: set[str], +) -> str: + if model_id in allowed_ids: + return model_id + if len(allowed_ids) != 1: + return "" + target_id = next(iter(allowed_ids)) + common_prefix = os.path.commonprefix((model_id, target_id)) + prefix_ratio = len(common_prefix) / max(1, len(target_id)) + similarity = difflib.SequenceMatcher( + None, + model_id, + target_id, + ).ratio() + if prefix_ratio >= 0.65 or similarity >= 0.75: + return target_id + return "" + + def apply_critic_verdicts( ledger: ProofObligationLedger, critic_text: str, run_id: str, obligation_ids: set[str] | None = None, + id_repairs: list[tuple[str, str]] | None = None, ) -> dict[str, str]: pending_ids = ( obligation_ids @@ -297,9 +320,15 @@ def apply_critic_verdicts( ) verdicts: dict[str, tuple[str, str]] = {} for match in _ISSUE_VERDICT.finditer(critic_text): - obligation_id = match.group(1) - if obligation_id not in pending_ids: + model_id = match.group(1) + obligation_id = _resolve_model_obligation_id( + model_id, + pending_ids, + ) + if not obligation_id: continue + if model_id != obligation_id and id_repairs is not None: + id_repairs.append((model_id, obligation_id)) body = match.group("body") status_match = re.search( r"^\*{0,2}Status:\*{0,2}\s*" @@ -352,31 +381,97 @@ def _normalize_obligation_statement(statement: str) -> str: return " ".join(re.findall(r"[a-z0-9]+", statement.lower())) +def _lemma_signature(statement: str) -> str: + matches = re.findall( + r"[\"“]([^\"”]{3,120}?lemma)[\"”]", + statement, + re.IGNORECASE, + ) + if not matches: + matches = re.findall( + r"\b([A-Za-z][A-Za-z -]{2,100}\s+Lemma)\b", + statement, + ) + return ( + _normalize_obligation_statement(matches[0]) + if matches else "" + ) + + +def _obligation_terms(statement: str) -> set[str]: + ignored = { + "a", "an", "and", "as", "be", "for", "if", "in", "is", "of", + "on", "or", "that", "the", "then", "there", "to", "where", "with", + "lemma", "proof", "formal", "given", + } + return { + term + for term in _normalize_obligation_statement(statement).split() + if term not in ignored + } + + +def _frontier_rejection_reason( + ledger: ProofObligationLedger, + parent_id: str, + statement: str, +) -> str: + normalized = _normalize_obligation_statement(statement) + terms = _obligation_terms(statement) + signature = _lemma_signature(statement) + parent_by_id = { + item.obligation_id: item.parent_id + for item in ledger.obligations + } + ancestors = set() + cursor = parent_id + while cursor and cursor not in ancestors: + ancestors.add(cursor) + cursor = parent_by_id.get(cursor, "") + for item in ledger.obligations: + existing_normalized = _normalize_obligation_statement(item.statement) + if normalized == existing_normalized: + return f"duplicates existing obligation {item.obligation_id}" + existing_signature = _lemma_signature(item.statement) + if signature and signature == existing_signature: + return f"repeats existing lemma {item.obligation_id}" + if len(terms) < 6: + return "frontier is too vague to be a falsifiable smaller obligation" + for item in ledger.obligations: + existing_terms = _obligation_terms(item.statement) + union = terms | existing_terms + similarity = len(terms & existing_terms) / len(union) if union else 0.0 + threshold = 0.70 if item.obligation_id in ancestors else 0.85 + if similarity >= threshold: + return ( + f"semantically cycles to {item.obligation_id} " + f"(similarity={similarity:.2f})" + ) + return "" + + def create_child_obligations( ledger: ProofObligationLedger, critic_text: str, run_id: str, parent_ids: set[str], + rejections: list[str] | None = None, ) -> list[ProofObligation]: - existing = { - (item.parent_id, _normalize_obligation_statement(item.statement)) - for item in ledger.obligations - } created: list[ProofObligation] = [] def add_child(parent_id: str, statement: str, evidence: str) -> None: statement = statement.strip().strip("`") normalized = _normalize_obligation_statement(statement) - parent = next( - item for item in ledger.obligations - if item.obligation_id == parent_id + if not normalized or normalized in {"none", "no missing lemma"}: + return + rejection = _frontier_rejection_reason( + ledger, + parent_id, + statement, ) - if ( - not normalized - or normalized in {"none", "no missing lemma"} - or normalized == _normalize_obligation_statement(parent.statement) - or (parent_id, normalized) in existing - ): + if rejection: + if rejections is not None: + rejections.append(f"{statement} :: {rejection}") return suffix = hashlib.sha256( f"{parent_id}:{normalized}".encode(), @@ -389,12 +484,14 @@ def add_child(parent_id: str, statement: str, evidence: str) -> None: last_evidence=evidence, ) ledger.obligations.append(child) - existing.add((parent_id, normalized)) created.append(child) for match in _ISSUE_VERDICT.finditer(critic_text): - parent_id = match.group(1) - if parent_id not in parent_ids: + parent_id = _resolve_model_obligation_id( + match.group(1), + parent_ids, + ) + if not parent_id: continue body = match.group("body") status_match = re.search( @@ -457,6 +554,7 @@ def build_autoresearch_verdict( ledger: ProofObligationLedger, applied_verdicts: dict[str, str], created: list[ProofObligation], + rejected_frontiers: list[str] | None = None, ) -> dict: target_id = str(candidate.TARGET_OBLIGATION_ID) target = next( @@ -493,8 +591,11 @@ def build_autoresearch_verdict( else: outcome = "INCONCLUSIVE" evidence = ( - target.last_evidence if target is not None else - "The Critic supplied no structurally valid target verdict." + f"Rejected cyclic or invalid frontier: {rejected_frontiers[0]}" + if rejected_frontiers else ( + target.last_evidence if target is not None else + "The Critic supplied no structurally valid target verdict." + ) ) frontier = ( target.statement if target is not None else @@ -1390,6 +1491,8 @@ def get_stats(): ) applied_verdicts = {} created_obligations = [] + id_repairs = [] + rejected_frontiers = [] if proof_ledger is not None and turn_obligations: applied_verdicts = apply_critic_verdicts( proof_ledger, @@ -1399,6 +1502,7 @@ def get_stats(): item.obligation_id for item in turn_obligations }, + id_repairs, ) created_obligations = create_child_obligations( proof_ledger, @@ -1408,7 +1512,19 @@ def get_stats(): item.obligation_id for item in turn_obligations }, + rejected_frontiers, ) + for model_id, target_id in id_repairs: + print( + "[critic-id-repaired] " + f"model_id={model_id} target_id={target_id}", + flush=True, + ) + for rejection in rejected_frontiers: + print( + f"[proof-obligation-rejected] {rejection}", + flush=True, + ) for obligation_id, status in applied_verdicts.items(): print( f"[critic-verdict] id={obligation_id} " @@ -1432,6 +1548,7 @@ def get_stats(): proof_ledger, applied_verdicts, created_obligations, + rejected_frontiers, ), ensure_ascii=False, sort_keys=True, diff --git a/tests/inference_engine/bridge/test_agent_gan_repl.py b/tests/inference_engine/bridge/test_agent_gan_repl.py index dee7321..0aa95f9 100644 --- a/tests/inference_engine/bridge/test_agent_gan_repl.py +++ b/tests/inference_engine/bridge/test_agent_gan_repl.py @@ -598,6 +598,74 @@ def test_critic_leaf_table_creates_all_target_children_only(): ] +def test_corrupted_critic_id_binds_to_single_host_target(): + target = ( + "RH-C2-0ef53a217d-25557e489d-4f025934ee-3110912e68-" + "763645cd6b-40ef83e052-b80cd1343b" + ) + corrupted = ( + "RH-C2-0ef53a217d-25557e489d-4f025934ee-3110912e68-" + "763645cd6b-40ef83e052-b80cd13rum-40ef83e052-b80cd1343b" + ) + ledger = ProofObligationLedger( + ledger_id="rh-ledger", + obligations=[ProofObligation(target, "Sectorial compatibility.")], + ) + repairs = [] + verdicts = apply_critic_verdicts( + ledger, + f""" +### ISSUE_VERDICT {corrupted} +**Status:** UNRESOLVED +**Evidence:** The local density inference is not justified by the global growth class. +**Missing lemma:** Prove a quantitative sectorial density bound from the indicator function. +""", + "br_corrupt", + {target}, + repairs, + ) + assert verdicts == {target: "UNRESOLVED"} + assert repairs == [(corrupted, target)] + assert "local density inference" in ledger.obligations[0].last_evidence + + +def test_cycle_and_invented_ids_cannot_create_children(): + root = ProofObligation( + "RH-C2-root", + 'The "Angular-Growth Decoupling Lemma": prove angular separation.', + ) + target = ProofObligation( + "RH-C2-root-child", + 'The "Sectorial Compatibility Lemma": prove a sectorial bound.', + parent_id=root.obligation_id, + ) + ledger = ProofObligationLedger( + ledger_id="rh-ledger", + obligations=[root, target], + ) + critic = f""" +### ISSUE_VERDICT {target.obligation_id} +**Status:** UNRESOLVED +**Evidence:** The proposed local density lower bound remains unsupported. +**Missing lemma:** The "Angular-Growth Decoupling Lemma": prove angular separation. + +### Leaf Obligation Ledger +| ID | Status | Evidence | Missing Lemma | +| RH-Cty-0-alpha | UNRESOLVED | invented | Prove an invented temporary lemma. | +""" + rejections = [] + created = create_child_obligations( + ledger, + critic, + "br_cycle", + {target.obligation_id}, + rejections, + ) + assert created == [] + assert len(ledger.obligations) == 2 + assert any("existing obligation" in item for item in rejections) + + def test_recover_complete_checkpoint_from_timestamped_log(tmp_path): path = tmp_path / "agent.log" path.write_text(