feat(autoresearch): supervise real GAN experiments

Connect strategy proposal, candidate deployment, cache-isolated GAN execution, fixed evaluation, lexicographic baseline comparison, keep/revert, and append-only experiment history into a hard-fail AutoResearch loop.

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

Author: 2 people

autoresearch/prefill/candidate.py

@@ -1,5 +1,19 @@
-"""The only Prefill strategy file the autoresearch agent may edit."""
+"""The only strategy file the AutoResearch agent may edit."""
 
+CANDIDATE_ID = "baseline-v1"
+TARGET_OBLIGATION_ID = "RH-C1"
+HYPOTHESIS = (
+    "Force each experiment to attack one unresolved proof obligation with a "
+    "concrete construction or counterexample."
+)
+GENERATOR_DIRECTIVE = (
+    "Focus on RH-C1. Propose one explicit non-circular operator definition, "
+    "including domain, kernel/action, and the exact theorem still required."
+)
+CRITIC_DIRECTIVE = (
+    "Attempt to falsify the proposed RH-C1 operator. Reject placeholders and "
+    "identify the first invalid domain, self-adjointness, or spectrum step."
+)
 PREFILL_COMPUTE_CHUNK_TOKENS = 256
 SNAPSHOT_MODE = "final_only"
 MAX_SEGMENT_SECONDS = 300.0

autoresearch/prefill/prepare.py

@@ -54,13 +54,28 @@ def evaluate(report: dict, candidate) -> dict:
             estimated_max_segment_s <= candidate.MAX_SEGMENT_SECONDS
         ),
         "final_only_snapshot": candidate.SNAPSHOT_MODE == "final_only",
+        "candidate_requires_full_context": (
+            candidate.REQUIRE_FULL_CONTEXT is True
+        ),
+        "candidate_forbids_fallback": candidate.ALLOW_FALLBACK is False,
     }
     return {
         "accepted": all(constraints.values()),
         "metric_cold_critic_prefill_s": warmup_s,
         "measured_prefill_tps": measured_tps,
         "estimated_max_segment_s": estimated_max_segment_s,
         "compute_chunk_tokens": candidate.PREFILL_COMPUTE_CHUNK_TOKENS,
+        "candidate_id": candidate.CANDIDATE_ID,
+        "target_obligation_id": candidate.TARGET_OBLIGATION_ID,
+        "proof_obligations_total": int(
+            critic.get("proof_obligations_total", 0),
+        ),
+        "proof_obligations_covered": int(
+            critic.get("proof_obligations_covered", 0),
+        ),
+        "proof_obligations_unresolved": int(
+            critic.get("proof_obligations_unresolved", 0),
+        ),
         "constraints": constraints,
     }
 

autoresearch/prefill/program.md

@@ -1,6 +1,6 @@
 # Prefill AutoResearch Program
 
-You are optimizing the two-Mac full-context Prefill system.
+You are optimizing the two-Mac full-context RH proof research system.
 
 ## Ownership
 
@@ -10,7 +10,10 @@ You are optimizing the two-Mac full-context Prefill system.
 
 ## Objective
 
-Minimize `metric_cold_critic_prefill_s`. Lower is better.
+Use a lexicographic objective:
+
+1. Minimize unresolved Proof Obligation Ledger items.
+2. With equal unresolved count, minimize `metric_cold_critic_prefill_s`.
 
 ## Hard constraints
 
@@ -36,6 +39,9 @@ Minimize `metric_cold_critic_prefill_s`. Lower is better.
    Prefill time improves. 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.