diff --git a/autoresearch/prefill/program.md b/autoresearch/prefill/program.md index 2062eb3..8e31253 100644 --- a/autoresearch/prefill/program.md +++ b/autoresearch/prefill/program.md @@ -12,8 +12,11 @@ You are optimizing the two-Mac full-context RH proof research system. Use a lexicographic objective: -1. Minimize unresolved Proof Obligation Ledger items. -2. With equal unresolved count, minimize `metric_cold_critic_prefill_s`. +1. Close an unresolved Proof Obligation Ledger item when an experiment supports + a proof step. +2. Otherwise, require a novel falsified hypothesis or a novel, strictly smaller + proof frontier. Rewording an existing obligation is not progress. +3. Subject to (1)-(2), minimize `metric_cold_critic_prefill_s`. ## Hard constraints @@ -29,19 +32,20 @@ Use a lexicographic objective: ## Experiment loop 1. Read `candidate.py` and `results.tsv`. -2. State one concrete performance hypothesis. +2. State one concrete mathematical hypothesis for one unresolved leaf. 3. Modify only `candidate.py`. 4. Deploy the candidate to allens. 5. Clear Primary and allens caches. 6. Run the fixed full-context acceptance workload. 7. Run `prepare.py` against the resulting report. -8. Keep the candidate only if every hard constraint passes and cold Critic - Prefill time improves. Otherwise restore the previous candidate. +8. Keep the candidate only if every hard constraint passes and it closes an + obligation, falsifies a novel hypothesis, or creates a novel smaller + frontier. Otherwise restore the previous candidate. 9. Append the result and repeat. Every candidate must target one current unresolved proof obligation and contain a falsifiable hypothesis plus distinct Generator and Critic directives. Do not optimize output wording, scores, prizes, or other proof-irrelevant -content. Optimize only measured Prefill execution while preserving the complete -semantic contract. +content. Prefill performance is a tertiary objective after mathematical +decomposition progress, while preserving the complete semantic contract. diff --git a/autoresearch/prefill/supervisor.py b/autoresearch/prefill/supervisor.py index 09c22ff..ad48046 100644 --- a/autoresearch/prefill/supervisor.py +++ b/autoresearch/prefill/supervisor.py @@ -106,6 +106,39 @@ def _extract_json(text: str) -> dict: return json.loads(stripped[start:end + 1]) +def parse_research_verdict(output: str, candidate_id: str) -> dict: + matches = list(re.finditer( + r"^(?:critic>\s*)?### AUTORESEARCH_VERDICT\s*$" + r"(?P
.*?)(?=^### |\Z)", + output, + re.MULTILINE | re.DOTALL, + )) + if not matches: + raise ValueError("Critic emitted no AUTORESEARCH_VERDICT") + body = matches[-1].group("body") + fields = {} + for name in ("Candidate ID", "Outcome", "Evidence", "New frontier"): + match = re.search( + rf"^{re.escape(name)}:\s*(.+)$", + body, + re.MULTILINE, + ) + if not match: + raise ValueError(f"research verdict missing {name}") + fields[name] = match.group(1).strip() + if fields["Candidate ID"] != candidate_id: + raise ValueError("research verdict candidate ID mismatch") + if fields["Outcome"] not in {"SUPPORTED", "FALSIFIED", "INCONCLUSIVE"}: + raise ValueError("invalid research verdict outcome") + if len(fields["Evidence"]) < 40 or len(fields["New frontier"]) < 30: + raise ValueError("research verdict lacks substantive evidence/frontier") + return { + "outcome": fields["Outcome"], + "evidence": fields["Evidence"], + "new_frontier": fields["New frontier"], + } + + def propose_candidate( *, address: str, @@ -127,6 +160,9 @@ def propose_candidate( + ", ".join(REQUIRED_CANDIDATE_FIELDS) + ". Allowed prefill_compute_chunk_tokens: 64, 128, 256. " "Do not weaken full context, final-only snapshots, or no-fallback rules." + " The hypothesis must not repeat any hypothesis or hash in RESULTS. " + "It must either construct a concrete object or attempt a concrete " + "counterexample for one smaller decomposition leaf." f"\n\nPROGRAM:\n{program}\n\nCURRENT:\n{json.dumps(current)}" f"\n\nRESULTS:\n{results_text[-12000:]}" f"\n\nLEDGER:\n{json.dumps(ledger)}" @@ -318,17 +354,15 @@ def best_kept(results: list[dict]) -> dict | None: def should_keep(result: dict, baseline: dict | None) -> bool: if not result["accepted"]: return False + if result.get("research_outcome") not in {"SUPPORTED", "FALSIFIED"}: + return False + if not result.get("hypothesis_novel", False): + return False if baseline is None: return True - new_key = ( - int(result["proof_obligations_unresolved"]), - float(result["metric_cold_critic_prefill_s"]), - ) - old_key = ( - int(baseline["proof_obligations_unresolved"]), - float(baseline["metric_cold_critic_prefill_s"]), + return int(result["proof_obligations_unresolved"]) <= int( + baseline["proof_obligations_unresolved"], ) - return new_key < old_key RESULT_FIELDS = ( @@ -338,11 +372,33 @@ def should_keep(result: dict, baseline: dict | None) -> bool: "proof_obligations_total", "proof_obligations_covered", "proof_obligations_unresolved", "compute_chunk_tokens", "candidate_sha256", "report_path", + "hypothesis_sha256", "research_outcome", "research_evidence", + "new_frontier", ) def append_result(path: Path, row: dict) -> None: path.parent.mkdir(parents=True, exist_ok=True) + if path.exists(): + with path.open(newline="") as handle: + reader = csv.DictReader(handle, delimiter="\t") + old_fields = tuple(reader.fieldnames or ()) + old_rows = list(reader) + if old_fields != RESULT_FIELDS: + temporary = path.with_suffix(path.suffix + ".migrating") + with temporary.open("w", newline="") as handle: + writer = csv.DictWriter( + handle, + fieldnames=RESULT_FIELDS, + delimiter="\t", + ) + writer.writeheader() + for old_row in old_rows: + writer.writerow({ + field: old_row.get(field, "") + for field in RESULT_FIELDS + }) + temporary.replace(path) write_header = not path.exists() with path.open("a", newline="") as handle: writer = csv.DictWriter(handle, fieldnames=RESULT_FIELDS, delimiter="\t") @@ -412,6 +468,16 @@ def run_iteration(args, iteration: int) -> dict: ) clear_primary_cache() validate_candidate(proposed) + hypothesis_sha256 = hashlib.sha256( + proposed["hypothesis"].strip().lower().encode(), + ).hexdigest() + seen_hypotheses = { + row.get("hypothesis_sha256", "") + for row in results + if row.get("hypothesis_sha256") + } + if hypothesis_sha256 in seen_hypotheses: + raise ValueError("strategy agent repeated a previous hypothesis") experiment_id = ( f"ar_{int(time.time())}_{iteration}_" f"{hashlib.sha256(candidate_path.read_bytes()).hexdigest()[:8]}" @@ -421,7 +487,7 @@ def run_iteration(args, iteration: int) -> dict: f"[autoresearch] phase=gan-experiment id={experiment_id}", flush=True, ) - run_id, report, _ = run_gan_experiment( + run_id, report, gan_output = run_gan_experiment( repo=root, candidate_path=candidate_path, state_path=state_path, @@ -430,10 +496,21 @@ def run_iteration(args, iteration: int) -> dict: report_path.write_text(json.dumps(report, ensure_ascii=False, indent=2)) candidate_module = _load_candidate(candidate_path) result = evaluate(report, candidate_module) + verdict = parse_research_verdict( + gan_output, + proposed["candidate_id"], + ) + result.update({ + "research_outcome": verdict["outcome"], + "research_evidence": verdict["evidence"], + "new_frontier": verdict["new_frontier"], + "hypothesis_novel": True, + }) keep = should_keep(result, baseline) print( f"[autoresearch] phase=evaluate accepted={result['accepted']} " f"unresolved={result['proof_obligations_unresolved']} " + f"outcome={verdict['outcome']} " f"prefill_s={result['metric_cold_critic_prefill_s']:.3f} " f"decision={'keep' if keep else 'revert'}", flush=True, @@ -463,6 +540,10 @@ def run_iteration(args, iteration: int) -> dict: candidate_path.read_bytes(), ).hexdigest(), "report_path": str(report_path), + "hypothesis_sha256": hypothesis_sha256, + "research_outcome": verdict["outcome"], + "research_evidence": verdict["evidence"], + "new_frontier": verdict["new_frontier"], } append_result(results_path, row) if not keep: diff --git a/scripts/agent_gan_repl.py b/scripts/agent_gan_repl.py index 79e6020..130094e 100644 --- a/scripts/agent_gan_repl.py +++ b/scripts/agent_gan_repl.py @@ -883,6 +883,14 @@ def get_stats(): ))) critic_strategy = str( research_candidate.CRITIC_DIRECTIVE, + ) + ( + "\n\nAt the end, emit exactly:\n" + "### AUTORESEARCH_VERDICT\n" + f"Candidate ID: {research_candidate.CANDIDATE_ID}\n" + "Outcome: SUPPORTED|FALSIFIED|INCONCLUSIVE\n" + "Evidence: