Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
97 changes: 71 additions & 26 deletions scripts/agent_gan_repl.py
Original file line number Diff line number Diff line change
Expand Up @@ -286,10 +286,15 @@ def apply_critic_verdicts(
ledger: ProofObligationLedger,
critic_text: str,
run_id: str,
obligation_ids: set[str] | None = None,
) -> dict[str, str]:
pending_ids = {
item.obligation_id for item in pending_obligations(ledger)
}
pending_ids = (
obligation_ids
if obligation_ids is not None
else {
item.obligation_id for item in pending_obligations(ledger)
}
)
verdicts: dict[str, tuple[str, str]] = {}
for match in _ISSUE_VERDICT.finditer(critic_text):
obligation_id = match.group(1)
Expand Down Expand Up @@ -358,6 +363,35 @@ def create_child_obligations(
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"}
or normalized == _normalize_obligation_statement(parent.statement)
or (parent_id, normalized) in existing
):
return
suffix = hashlib.sha256(
f"{parent_id}:{normalized}".encode(),
).hexdigest()[:10]
child = ProofObligation(
obligation_id=f"{parent_id}-{suffix}",
statement=statement,
parent_id=parent_id,
last_run_id=run_id,
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:
Expand All @@ -380,32 +414,39 @@ def create_child_obligations(
or missing_match is None
):
continue
statement = missing_match.group(1).strip()
normalized = _normalize_obligation_statement(statement)
parent = next(
item for item in ledger.obligations
if item.obligation_id == parent_id
add_child(
parent_id,
missing_match.group(1),
"Created from Critic ISSUE_VERDICT missing lemma.",
)
if (
not normalized
or normalized in {"none", "no missing lemma"}
or normalized == _normalize_obligation_statement(parent.statement)
or (parent_id, normalized) in existing
):
for line in critic_text.splitlines():
if not line.strip().startswith("|"):
continue
suffix = hashlib.sha256(
f"{parent_id}:{normalized}".encode(),
).hexdigest()[:10]
child = ProofObligation(
obligation_id=f"{parent_id}-{suffix}",
statement=statement,
parent_id=parent_id,
last_run_id=run_id,
last_evidence="Created from Critic missing lemma.",
cells = [
cell.strip().strip("*").strip()
for cell in line.strip().strip("|").split("|")
]
if len(cells) < 4 or cells[1].upper() != "UNRESOLVED":
continue
model_leaf_id, _, evidence, missing = cells[:4]
parent_id = next(
(
parent
for parent in sorted(parent_ids, key=len, reverse=True)
if (
model_leaf_id == parent
or model_leaf_id.startswith(f"{parent}-")
)
),
"",
)
if not parent_id:
continue
add_child(
parent_id,
missing,
f"Created from Critic leaf table: {evidence}",
)
ledger.obligations.append(child)
existing.add((parent_id, normalized))
created.append(child)
if created:
ledger.version += 1
return created
Expand Down Expand Up @@ -1323,6 +1364,10 @@ def get_stats():
proof_ledger,
critic_text,
run_id,
{
item.obligation_id
for item in turn_obligations
},
)
created_obligations = create_child_obligations(
proof_ledger,
Expand Down
38 changes: 38 additions & 0 deletions tests/inference_engine/bridge/test_agent_gan_repl.py
Original file line number Diff line number Diff line change
Expand Up @@ -546,6 +546,44 @@ class Candidate:
assert verdict["created_obligation_ids"] == ["RH-C2-child"]


def test_critic_leaf_table_creates_all_target_children_only():
ledger = ProofObligationLedger(
ledger_id="rh-ledger",
obligations=[
ProofObligation("RH-C1", "Operator construction."),
ProofObligation("RH-C2", "Zero convergence."),
],
)
critic = """
### Leaf Obligation Ledger
| ID | Status | Evidence/Argument | Missing Lemma/Requirement |
| :--- | :--- | :--- | :--- |
| **RH-C2-1** | UNRESOLVED | No compact convergence proof. | Prove locally uniform convergence on compact subsets. |
| **RH-C2-2** | UNRESOLVED | Hurwitz does not cover poles. | Prove a singular-limit zero-counting theorem. |
| **RH-C1-1** | UNRESOLVED | Unrelated operator issue. | Construct a self-adjoint operator. |
"""
applied = apply_critic_verdicts(
ledger,
critic,
"br_table",
{"RH-C2"},
)
created = create_child_obligations(
ledger,
critic,
"br_table",
{"RH-C2"},
)
assert applied == {"RH-C2": "UNRESOLVED"}
assert len(created) == 2
assert all(item.parent_id == "RH-C2" for item in created)
assert ledger.obligations[0].last_run_id == ""
assert pending_obligations(ledger) == [
ledger.obligations[0],
*created,
]


def test_recover_complete_checkpoint_from_timestamped_log(tmp_path):
path = tmp_path / "agent.log"
path.write_text(
Expand Down
Loading