From 19e036db80bfc346edcd62d7029003378aabc1b2 Mon Sep 17 00:00:00 2001 From: fluffy314 Date: Fri, 17 Jul 2026 15:34:55 +0800 Subject: [PATCH] fix(agents): recursively decompose proof obligations Focus Critic reasoning on the central stopping claim and recursively reduce unresolved mathematical obligations instead of auditing peripheral facts. Co-authored-by: Cursor --- docs/ops/distributed-prefill-kv-network.md | 12 ++--- scripts/agent_gan_inference_demo.py | 31 +++++++------ scripts/agent_gan_repl.py | 44 +++++++++++-------- .../bridge/test_agent_gan_demo.py | 2 +- .../bridge/test_agent_gan_repl.py | 13 +++--- 5 files changed, 59 insertions(+), 43 deletions(-) diff --git a/docs/ops/distributed-prefill-kv-network.md b/docs/ops/distributed-prefill-kv-network.md index bf6abfb..11d9fda 100644 --- a/docs/ops/distributed-prefill-kv-network.md +++ b/docs/ops/distributed-prefill-kv-network.md @@ -349,11 +349,13 @@ and semantic fallback are forbidden. A global Critic score is valid only when `critic_omitted_tokens=0`. Long Prefill operations emit a heartbeat every 30 seconds; on the 16GB allens worker, full-context Critic Prefill may take 15–25 minutes. -The Critic uses `adversarial_claim_audit_v1`: numeric scores and blanket -approval are forbidden. It must reconstruct the thesis, quote and challenge -each material claim, present the strongest objection, provide a corrected -response, and state residual uncertainty. Epistemic honesty is evaluated -separately from literal task completion. +The Critic uses `recursive_proof_decomposition_v2`: numeric scores and blanket +approval are forbidden. It ignores prizes, money, prestige, style, and other +proof-irrelevant facts. It attacks the central stopping claim, recursively +decomposes it into proof obligations, records arguments/counterarguments and +dependencies for every node, and loops until every leaf is either explicitly +derived or a precisely stated open lemma. It then reports the smallest +unresolved frontier and next adversarial step. The worker reserves estimated final-snapshot capacity before model compute, prevents adaptive shrink from consuming active reservations, then atomically publishes and leases the final snapshot before adding optional intermediate diff --git a/scripts/agent_gan_inference_demo.py b/scripts/agent_gan_inference_demo.py index 2087197..b4f19df 100644 --- a/scripts/agent_gan_inference_demo.py +++ b/scripts/agent_gan_inference_demo.py @@ -47,7 +47,7 @@ def build_critic_context(tokenizer, text: str) -> tuple[str, dict]: "critic_context_tokens": len(full_ids), "critic_omitted_tokens": 0, "review_scope": "full", - "critic_protocol": "adversarial_claim_audit_v1", + "critic_protocol": "recursive_proof_decomposition_v2", } @@ -179,19 +179,22 @@ def main() -> int: critic_history = [{ "role": "system", "content": ( - "You are an adversarial peer reviewer, not a supportive grader. " - "Review the complete Generator response as one semantic argument. " - "Reconstruct its thesis and audit every material factual, logical, " - "and task-completion claim against the strongest counterargument. " - "Quote claims before challenging them. Distinguish an honest " - "boundary from literal task completion; unknown does not mean " - "impossible. Check numbers, quantifiers, awards, assumptions, and " - "claimed consequences. Never output a numeric score or blanket " - "approval without an explicit claim-by-claim audit. Return Thesis " - "Reconstruction, Claim-by-Claim Audit, Strongest Objection, " - "Corrected Response, and Residual Uncertainty. Claim truncation " - "only when completion_status is not EOS or syntax is cut off. " - "Do not sample, summarize, simplify, or use fallback review." + "You are a recursive adversarial proof analyst. Review the complete " + "Generator response as one semantic argument and focus only on the " + "central claim required by the task. Ignore prizes, money, prestige, " + "style, and facts that do not alter the proof chain. Attack any move " + "from unknown or unsolved to impossible. Recursively decompose the " + "central claim into minimal proof obligations. For every node give " + "its argument, strongest counterargument, dependencies, and status " + "as proved, disproved, or unresolved. Replace every broad unresolved " + "node with smaller obligations until each leaf has an explicit " + "derivation or is a precisely stated open lemma. Return Central " + "Claim, Decomposition Loop, Leaf Obligation Ledger, Smallest " + "Unresolved Frontier, and Next Adversarial Step. Never output a " + "numeric score or blanket approval, and never declare the theorem " + "proved unless every leaf is discharged. Claim truncation only when " + "completion_status is not EOS or syntax is cut off. Do not sample, " + "summarize, simplify, or use fallback review." ), }] diff --git a/scripts/agent_gan_repl.py b/scripts/agent_gan_repl.py index 5684f01..254922d 100644 --- a/scripts/agent_gan_repl.py +++ b/scripts/agent_gan_repl.py @@ -51,10 +51,12 @@ def build_generator_messages(prompt: str) -> list[dict[str, str]]: { "role": "system", "content": ( - "Answer rigorously. For open problems, state the accepted " - "boundary and never fabricate a proof. Distinguish unknown " - "from impossible; qualify awards, quantities, and claimed " - "downstream consequences precisely." + "Pursue the requested mathematical argument constructively and " + "rigorously. For an open problem, do not fabricate a proof, but " + "do not stop at 'unsolved': identify the exact global claim, " + "derive known reductions, recursively decompose missing proof " + "obligations, and state the smallest unresolved frontier. " + "Distinguish unknown from impossible." ), }, {"role": "user", "content": prompt}, @@ -72,20 +74,26 @@ def build_critic_messages( { "role": "system", "content": ( - "Act as an adversarial peer reviewer, not a supportive grader. " - "Read the complete response as one semantic argument. Rebuild " - "its thesis and audit every material factual, logical, and " - "task-completion claim against the strongest counterargument. " - "Quote the exact claim before challenging it. Distinguish " - "epistemic honesty from literal task completion: unknown or " - "unsolved does not mean impossible, and an honest refusal does " - "not complete a requested proof. Check numbers, awards, " - "quantifiers, and claimed consequences. Never output a numeric " - "score. Never issue blanket approval unless every material " - "claim has been explicitly audited. Use exactly these sections: " - "Thesis Reconstruction; Claim-by-Claim Audit; Strongest " - "Objection; Corrected Response; Residual Uncertainty. Do not " - "sample, summarize, simplify, or use a fallback review." + "Act as a recursive adversarial proof analyst. Read the complete " + "response as one semantic argument and focus exclusively on the " + "central mathematical claim required by the task. Ignore prizes, " + "money, prestige, style, and other facts that do not change the " + "proof chain. If the response stops at 'unknown', 'unsolved', or " + "'impossible', attack that stopping claim rather than accepting " + "it as an answer. Build a proof-obligation tree: decompose the " + "central claim into minimal necessary subclaims; for each node " + "give the argument, strongest counterargument, dependencies, and " + "status as proved, disproved, or unresolved. Recursively replace " + "every broad unresolved node with smaller obligations until each " + "leaf is either discharged by an explicit derivation or is a " + "precisely stated open lemma. Then identify the smallest " + "unresolved frontier and the next lemma that must be proved. " + "Never output a numeric score or blanket approval. Never claim " + "the original theorem is proved unless every leaf is discharged. " + "Use exactly these sections: Central Claim; Decomposition Loop; " + "Leaf Obligation Ledger; Smallest Unresolved Frontier; Next " + "Adversarial Step. Do not sample, summarize, simplify, or use a " + "fallback review." ), }, { diff --git a/tests/inference_engine/bridge/test_agent_gan_demo.py b/tests/inference_engine/bridge/test_agent_gan_demo.py index 55f73b7..dc1fa58 100644 --- a/tests/inference_engine/bridge/test_agent_gan_demo.py +++ b/tests/inference_engine/bridge/test_agent_gan_demo.py @@ -120,4 +120,4 @@ def test_critic_context_preserves_complete_generator_response(): assert metrics["critic_context_tokens"] == 10 assert metrics["critic_omitted_tokens"] == 0 assert metrics["review_scope"] == "full" - assert metrics["critic_protocol"] == "adversarial_claim_audit_v1" + assert metrics["critic_protocol"] == "recursive_proof_decomposition_v2" diff --git a/tests/inference_engine/bridge/test_agent_gan_repl.py b/tests/inference_engine/bridge/test_agent_gan_repl.py index df8cedc..81f6a53 100644 --- a/tests/inference_engine/bridge/test_agent_gan_repl.py +++ b/tests/inference_engine/bridge/test_agent_gan_repl.py @@ -140,13 +140,13 @@ def test_stage_includes_full_context_metrics(): "critic_context_tokens": 100, "critic_omitted_tokens": 0, "review_scope": "full", - "critic_protocol": "adversarial_claim_audit_v1", + "critic_protocol": "recursive_proof_decomposition_v2", }, ) assert stage["critic_context_tokens"] == 100 assert stage["critic_omitted_tokens"] == 0 assert stage["review_scope"] == "full" - assert stage["critic_protocol"] == "adversarial_claim_audit_v1" + assert stage["critic_protocol"] == "recursive_proof_decomposition_v2" def test_telemetry_timeout_warns_without_stopping_inference( @@ -195,8 +195,11 @@ def test_interactive_prompts_are_deterministic_for_kv_reuse(): combined = repr(generator_a + critic_a) assert "Internal run" not in combined assert "open problem" in combined - assert "adversarial peer reviewer" in combined + assert "recursive adversarial proof analyst" in combined assert "Never output a numeric score" in combined - assert "Claim-by-Claim Audit" in combined - assert "unknown or unsolved does not mean impossible" in combined + assert "Decomposition Loop" in combined + assert "If the response stops at" in combined + assert "attack that stopping claim" in combined + assert "Ignore prizes, money, prestige" in combined + assert "smallest unresolved frontier" in combined assert "sample, summarize, simplify" in combined