From 62f7462b2036f4174c2477506cad9d2b3f056e4c Mon Sep 17 00:00:00 2001 From: fluffy314 Date: Tue, 21 Jul 2026 17:54:17 +0800 Subject: [PATCH] feat(autoresearch): gate leaves with Lean signatures Require every proposed minimum leaf to typecheck as a safe, explicit Lean/mathlib theorem signature before it can enter the proof ledger. Co-authored-by: Cursor --- .github/workflows/ci.yaml | 12 ++ .gitignore | 1 + KakeyaLeanGate.lean | 1 + KakeyaLeanGate/Prelude.lean | 9 ++ autoresearch/prefill/lean_gate.py | 122 ++++++++++++++++++ autoresearch/prefill/program.md | 7 + lake-manifest.json | 96 ++++++++++++++ lakefile.lean | 11 ++ lean-toolchain | 1 + scripts/agent_gan_repl.py | 87 ++++++++++++- .../bench/test_lean_signature_gate.py | 49 +++++++ .../bridge/test_agent_gan_repl.py | 23 ++++ 12 files changed, 418 insertions(+), 1 deletion(-) create mode 100644 KakeyaLeanGate.lean create mode 100644 KakeyaLeanGate/Prelude.lean create mode 100644 autoresearch/prefill/lean_gate.py create mode 100644 lake-manifest.json create mode 100644 lakefile.lean create mode 100644 lean-toolchain create mode 100644 tests/inference_engine/bench/test_lean_signature_gate.py diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index ce5a63d6..7fe12c3f 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -43,6 +43,18 @@ jobs: - name: Check out uses: actions/checkout@v4 + - name: Install pinned Lean toolchain + run: | + curl -sSf https://elan.lean-lang.org/elan-init.sh \ + | sh -s -- -y --default-toolchain none + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + + - name: Restore mathlib cache and build Lean gate + run: | + lake update + lake exe cache get + lake build + - name: Set up Python ${{ matrix.python-version }} uses: actions/setup-python@v5 with: diff --git a/.gitignore b/.gitignore index 40c73b46..07c4d3cd 100644 --- a/.gitignore +++ b/.gitignore @@ -7,3 +7,4 @@ __pycache__/ .vscode/ .DS_Store .coverage +.lake/ diff --git a/KakeyaLeanGate.lean b/KakeyaLeanGate.lean new file mode 100644 index 00000000..272f637f --- /dev/null +++ b/KakeyaLeanGate.lean @@ -0,0 +1 @@ +import KakeyaLeanGate.Prelude diff --git a/KakeyaLeanGate/Prelude.lean b/KakeyaLeanGate/Prelude.lean new file mode 100644 index 00000000..24491613 --- /dev/null +++ b/KakeyaLeanGate/Prelude.lean @@ -0,0 +1,9 @@ +import Mathlib + +/-! +Minimal import target for AutoResearch theorem-signature validation. + +Generated signatures are compiled in temporary files importing this module. +They may use `sorry` while their status is `FORMALIZED`; a proof obligation can +only become `PROVED` after a separate no-sorry/no-axiom proof gate. +-/ diff --git a/autoresearch/prefill/lean_gate.py b/autoresearch/prefill/lean_gate.py new file mode 100644 index 00000000..5ac429fb --- /dev/null +++ b/autoresearch/prefill/lean_gate.py @@ -0,0 +1,122 @@ +"""Fail-closed Lean theorem-signature gate for proof obligations.""" +from __future__ import annotations + +import hashlib +import re +import subprocess +import tempfile +from dataclasses import dataclass +from pathlib import Path + + +_SIGNATURE_BLOCK = re.compile( + r"^### LEAN_SIGNATURE(?:\s+(\S+))?\s*$" + r"\s*```lean\s*(?P.*?)```", + re.MULTILINE | re.DOTALL, +) +_FORBIDDEN = re.compile( + r"(^|\s)(?:import|axiom|opaque|unsafe|macro|syntax|elab|run_cmd|run_tac|" + r"set_option|def|abbrev|instance|structure|inductive|class|namespace|" + r"section|variable|open|attribute)\b|#(?:eval|check|print|reduce)|" + r"\b(?:IO|System|FilePath)\b", + re.MULTILINE, +) + + +@dataclass(frozen=True) +class LeanSignatureResult: + source: str + signature_hash: str + ok: bool + error: str = "" + + +def extract_lean_signature_blocks(text: str) -> list[tuple[str, str]]: + return [ + ((match.group(1) or "").strip(), match.group("source").strip()) + for match in _SIGNATURE_BLOCK.finditer(text) + ] + + +def _signature_only(source: str) -> str: + match = re.search(r"\s*:=\s*by\b", source) + return source[:match.start()].strip() if match else source.strip() + + +def validate_lean_signature( + source: str, + *, + project_root: Path, + timeout_s: float = 30.0, +) -> LeanSignatureResult: + source = source.strip() + if not source: + return LeanSignatureResult("", "", False, "empty Lean signature") + if len(source) > 12_000: + return LeanSignatureResult("", "", False, "Lean signature too large") + if _FORBIDDEN.search(source): + return LeanSignatureResult( + source, + "", + False, + "forbidden Lean command in generated signature", + ) + declarations = re.findall(r"^\s*theorem\s+([A-Za-z_][\w']*)", source, re.MULTILINE) + if len(declarations) != 1: + return LeanSignatureResult( + source, + "", + False, + "expected exactly one theorem declaration", + ) + if not re.search(r"\s*:=\s*by\b", source): + return LeanSignatureResult( + source, + "", + False, + "theorem signature must end with `:= by` proof scaffold", + ) + signature = " ".join(_signature_only(source).split()) + signature_hash = hashlib.sha256(signature.encode()).hexdigest() + content = ( + "import KakeyaLeanGate\n\n" + "set_option autoImplicit false\n\n" + + source + + "\n" + ) + try: + with tempfile.NamedTemporaryFile( + mode="w", + suffix=".lean", + encoding="utf-8", + delete=False, + ) as handle: + handle.write(content) + path = Path(handle.name) + completed = subprocess.run( + ["lake", "env", "lean", str(path)], + cwd=project_root, + capture_output=True, + text=True, + timeout=timeout_s, + check=False, + ) + except (OSError, subprocess.TimeoutExpired) as exc: + return LeanSignatureResult( + source, + signature_hash, + False, + f"Lean invocation failed: {type(exc).__name__}: {exc}", + ) + finally: + if "path" in locals(): + path.unlink(missing_ok=True) + if completed.returncode != 0: + error = (completed.stderr or completed.stdout).strip() + return LeanSignatureResult( + source, + signature_hash, + False, + f"Lean typecheck failed: {error[-2000:]}", + ) + return LeanSignatureResult(source, signature_hash, True) diff --git a/autoresearch/prefill/program.md b/autoresearch/prefill/program.md index 138568fd..321df721 100644 --- a/autoresearch/prefill/program.md +++ b/autoresearch/prefill/program.md @@ -86,6 +86,13 @@ new assumption, narrower domain, or falsifiable conclusion. Existing semantic duplicates and all descendants beneath them are retained for audit but marked `REJECTED_DUPLICATE`; they are not pending leaves and do not reset stagnation. +Every proposed minimum leaf must include one safe Lean theorem signature with +explicit typed variables, hypotheses, and conclusion. The host compiles it +against pinned Lean/mathlib before persistence and records `FORMALIZED` plus a +signature hash. Missing, unsafe, ill-typed, or duplicate signatures reject the +child. `FORMALIZED` is not `PROVED`: closure still requires a separate proof +with no `sorry` and no added axioms. + 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/lake-manifest.json b/lake-manifest.json new file mode 100644 index 00000000..f9e57a5f --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,96 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.32.0-rc1", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f3f26cc72646205ca167117487c008ee1dafe816", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "41f407a8e85b0fdc00910633a8f14754139b63f4", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e6518a674e62de322b8f79eebeda7bcae2a36bc3", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "7a62bd13860cd39ac98da16ffc8c24d601353f69", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "954dbc9873f3b4534dc9896604593406d0383520", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "406ebb8c8e2f7e852a1b47764b42494022ce652c", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.32.0-rc1", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "kakeya_lean_gate", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 00000000..c6207e8d --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,11 @@ +import Lake + +open Lake DSL + +package «kakeya_lean_gate» + +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" @ "v4.32.0-rc1" + +@[default_target] +lean_lib KakeyaLeanGate diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 00000000..2694eb76 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.32.0-rc1 diff --git a/scripts/agent_gan_repl.py b/scripts/agent_gan_repl.py index 776f1b74..03cf74ff 100644 --- a/scripts/agent_gan_repl.py +++ b/scripts/agent_gan_repl.py @@ -30,6 +30,11 @@ _json_request, ) from inference_engine.bench.prefill_fleet_report import summarize_stages +from autoresearch.prefill.lean_gate import ( + LeanSignatureResult, + extract_lean_signature_blocks, + validate_lean_signature, +) class TimestampedTee: @@ -171,6 +176,10 @@ class ProofObligation: parent_id: str = "" last_run_id: str = "" last_evidence: str = "" + formal_status: str = "UNFORMALIZED" + lean_signature: str = "" + lean_signature_hash: str = "" + formalization_error: str = "" @dataclass @@ -281,7 +290,11 @@ def format_proof_ledger( "pending ID, with `Correction:`, `Derivation:`, and `Remaining gap:`. " "Critic requirement: emit `### ISSUE_VERDICT ` for every pending " "ID, with `Status: PROVED|DISPROVED|UNRESOLVED`, `Evidence:`, and " - "`Missing lemma:`." + "`Missing lemma:`. For every UNRESOLVED verdict, immediately emit " + "`### LEAN_SIGNATURE ` followed by one fenced `lean` block. The " + "block must contain exactly one theorem with explicit typed variables, " + "hypotheses, and conclusion, ending in `:= by sorry`. Do not emit " + "imports, axioms, commands, macros, or executable code." ) @@ -680,8 +693,16 @@ def create_child_obligations( run_id: str, parent_ids: set[str], rejections: list[str] | None = None, + lean_signatures: dict[ + str, + LeanSignatureResult | list[LeanSignatureResult], + ] | None = None, ) -> list[ProofObligation]: created: list[ProofObligation] = [] + available_signatures = { + key: list(value) if isinstance(value, list) else [value] + for key, value in (lean_signatures or {}).items() + } def add_child(parent_id: str, statement: str, evidence: str) -> None: statement = statement.strip().strip("`") @@ -697,6 +718,30 @@ def add_child(parent_id: str, statement: str, evidence: str) -> None: if rejections is not None: rejections.append(f"{statement} :: {rejection}") return + lean_results = available_signatures.get(parent_id, []) + lean_result = lean_results.pop(0) if lean_results else None + if lean_result is None: + if rejections is not None: + rejections.append( + f"{statement} :: missing Lean theorem signature", + ) + return + if not lean_result.ok: + if rejections is not None: + rejections.append( + f"{statement} :: {lean_result.error}", + ) + return + if any( + item.lean_signature_hash + and item.lean_signature_hash == lean_result.signature_hash + for item in ledger.obligations + ): + if rejections is not None: + rejections.append( + f"{statement} :: Lean signature duplicates an ancestor", + ) + return suffix = hashlib.sha256( f"{parent_id}:{normalized}".encode(), ).hexdigest()[:10] @@ -706,6 +751,9 @@ def add_child(parent_id: str, statement: str, evidence: str) -> None: parent_id=parent_id, last_run_id=run_id, last_evidence=evidence, + formal_status="FORMALIZED", + lean_signature=lean_result.source, + lean_signature_hash=lean_result.signature_hash, ) ledger.obligations.append(child) created.append(child) @@ -1731,6 +1779,42 @@ def get_stats(): id_repairs = [] rejected_frontiers = [] if proof_ledger is not None and turn_obligations: + target_ids = { + item.obligation_id + for item in turn_obligations + } + lean_signatures = {} + for model_id, lean_source in extract_lean_signature_blocks( + critic_text, + ): + lean_target = ( + _resolve_model_obligation_id( + model_id, + target_ids, + ) + if model_id else ( + next(iter(target_ids)) + if len(target_ids) == 1 else "" + ) + ) + if not lean_target: + continue + lean_result = validate_lean_signature( + lean_source, + project_root=Path(__file__).resolve().parents[1], + ) + lean_signatures.setdefault( + lean_target, + [], + ).append(lean_result) + print( + "[lean-signature-gate] " + f"target={lean_target} " + f"status={'FORMALIZED' if lean_result.ok else 'REJECTED'} " + f"hash={lean_result.signature_hash or '(none)'} " + f"error={lean_result.error or '(none)'}", + flush=True, + ) applied_verdicts = apply_critic_verdicts( proof_ledger, critic_text, @@ -1756,6 +1840,7 @@ def get_stats(): for item in turn_obligations }, rejected_frontiers, + lean_signatures, ) for model_id, target_id in id_repairs: print( diff --git a/tests/inference_engine/bench/test_lean_signature_gate.py b/tests/inference_engine/bench/test_lean_signature_gate.py new file mode 100644 index 00000000..23f9ae6f --- /dev/null +++ b/tests/inference_engine/bench/test_lean_signature_gate.py @@ -0,0 +1,49 @@ +from pathlib import Path + +from autoresearch.prefill.lean_gate import ( + extract_lean_signature_blocks, + validate_lean_signature, +) + + +ROOT = Path(__file__).resolve().parents[3] + + +def test_extract_and_typecheck_minimal_mathlib_signature(): + text = """ +### LEAN_SIGNATURE RH-C2-leaf +```lean +theorem local_pole_signature + (f : ℂ → ℂ) + (h : Continuous f) : + Continuous f := by + sorry +``` +""" + blocks = extract_lean_signature_blocks(text) + assert len(blocks) == 1 + target, source = blocks[0] + assert target == "RH-C2-leaf" + result = validate_lean_signature(source, project_root=ROOT) + assert result.ok, result.error + assert len(result.signature_hash) == 64 + + +def test_lean_gate_rejects_unknown_type(): + result = validate_lean_signature( + "theorem bad (x : MissingType) : True := by trivial", + project_root=ROOT, + ) + assert not result.ok + assert "unknown" in result.error.lower() + + +def test_lean_gate_rejects_executable_or_axiomatic_commands(): + for source in ( + "axiom hidden : False", + "def hidden : Nat := 1\ntheorem ok : True := by trivial", + "theorem bad : True := by run_tac do pure ()", + "#eval 1 + 1", + ): + result = validate_lean_signature(source, project_root=ROOT) + assert not result.ok diff --git a/tests/inference_engine/bridge/test_agent_gan_repl.py b/tests/inference_engine/bridge/test_agent_gan_repl.py index 3c5513b5..ae990371 100644 --- a/tests/inference_engine/bridge/test_agent_gan_repl.py +++ b/tests/inference_engine/bridge/test_agent_gan_repl.py @@ -5,6 +5,7 @@ import time from pathlib import Path +from autoresearch.prefill.lean_gate import LeanSignatureResult from scripts.agent_gan_repl import ( PrefillHeartbeat, CriticIssueBatch, @@ -48,6 +49,14 @@ def decode(self, token_ids, **_kwargs): return "".join(chr(96 + token) for token in token_ids) +def _valid_lean_signature(suffix=""): + return LeanSignatureResult( + f"theorem frontier{suffix} (p : Prop) : p := by sorry", + f"lean-signature-hash{suffix}", + True, + ) + + def test_timestamped_tee_preserves_terminal_and_flushes_log(tmp_path): terminal = io.StringIO() timestamps = iter(("t1", "t2", "t3")) @@ -522,15 +531,21 @@ def test_missing_lemma_creates_deduplicated_child_and_selects_leaf(): critic, "br_first", {"RH-C2"}, + None, + {"RH-C2": _valid_lean_signature()}, ) assert len(created) == 1 assert created[0].parent_id == "RH-C2" + assert created[0].formal_status == "FORMALIZED" + assert created[0].lean_signature_hash == "lean-signature-hash" assert pending_obligations(ledger) == created assert create_child_obligations( ledger, critic, "br_repeat", {"RH-C2"}, + None, + {"RH-C2": _valid_lean_signature()}, ) == [] @@ -582,12 +597,20 @@ def test_critic_leaf_table_creates_all_target_children_only(): critic, "br_table", {"RH-C2"}, + None, ) created = create_child_obligations( ledger, critic, "br_table", {"RH-C2"}, + None, + { + "RH-C2": [ + _valid_lean_signature("1"), + _valid_lean_signature("2"), + ], + }, ) assert applied == {"RH-C2": "UNRESOLVED"} assert len(created) == 2