From a614b570c2a141a7d861fd49a571173421cad297 Mon Sep 17 00:00:00 2001 From: Mounir IDRASSI Date: Tue, 24 Mar 2026 15:29:29 +0900 Subject: [PATCH] Gate literature search by worker web-search capability --- DOCS.md | 4 +-- README.md | 6 ++-- openprover/cli.py | 43 +++++++++++++++++--------- openprover/model_caps.py | 20 ++++++++++++ openprover/prover.py | 13 ++++++++ tests/test_cli_validation.py | 59 ++++++++++++++++++++++++++++++++++++ tests/test_model_caps.py | 19 ++++++++++++ 7 files changed, 145 insertions(+), 19 deletions(-) create mode 100644 openprover/model_caps.py create mode 100644 tests/test_cli_validation.py create mode 100644 tests/test_model_caps.py diff --git a/DOCS.md b/DOCS.md index b972e6a..4827630 100644 --- a/DOCS.md +++ b/DOCS.md @@ -86,7 +86,7 @@ When `lean_worker_tools` is enabled, sets up tool calling for workers: | Handler | What it does | |---------|-------------| | `_handle_spawn` | Run worker tasks in parallel via `ThreadPoolExecutor` (up to `--parallelism`). Each worker gets its task description with wikilinks resolved. Results pushed to output window. | -| `_handle_literature_search` | Spawn a web-enabled worker (Claude CLI with `WebSearch` + `WebFetch` tools). Results fed back to planner. | +| `_handle_literature_search` | Spawn a web-enabled worker (currently Claude CLI with `WebSearch` + `WebFetch` tools). Results fed back to planner. | | `_handle_read_items` | Fetch full content of requested repo items, push to output. | | `_handle_write_items` | Create/update/delete repo items. Items with `format="lean"` are auto-verified via `lake env lean`. | | `_handle_write_whiteboard` | Update the whiteboard without spawning workers. | @@ -156,7 +156,7 @@ Archiving: Every call saved to `archive/calls/call_NNN.json` with full prompt, s - `chat()` method for multi-turn tool calling conversations - Same interface as `LLMClient` (web_search and json_schema ignored) - Cost always 0.0 (local model) -- Automatically enforces `--isolation` +- Automatically enforces `--isolation` because local/vLLM workers cannot execute planner-level web search **Key gotchas:** - `--json-schema` puts structured output in `raw["structured_output"]`, not `raw["result"]` diff --git a/README.md b/README.md index 8a7ff08..da02f68 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ With `--lean-project`, workers get access to **lean_verify** (compile Lean 4 cod Modes: - **Interactive** (default): see each step's plan, accept or give feedback - **Autonomous** (`--autonomous`): runs hands-off until proof found or budget exhausted -- **Isolation** (default) / **No-isolation** (`--no-isolation`): by default, workers have no web access. With `--no-isolation`, the planner can use `literature_search` to find relevant papers and results online +- **Isolation** (default) / **No-isolation** (`--no-isolation`): by default, workers have no web access. With `--no-isolation`, the planner can use `literature_search` to find relevant papers and results online when the worker model supports web search (currently Claude workers) - **Formal verification** (`--lean-project`): proof attempts are verified via `lake env lean`, workers can verify code and search Lean libraries ## Requirements @@ -101,7 +101,7 @@ openprover --theorem examples/addition.md \ | `--conclude-after` | `0.99` | Fraction of budget that triggers conclusion phase (0.9-1.0) | | `--autonomous` | off | Run without human confirmation | | `-P, --parallelism` | `1` | Max parallel workers per step | -| `--isolation` / `--no-isolation` | on | Isolation disables web access; use `--no-isolation` to enable `literature_search` | +| `--isolation` / `--no-isolation` | on | Isolation disables web access; `--no-isolation` requires a web-search-capable worker model (`sonnet` or `opus`) | | `--give-up-after` | `0.5` | Fraction of budget before give_up is allowed | | `--lean-project` | | Path to Lean project with lakefile | | `--lean-theorem` | | Path to THEOREM.lean (requires `--lean-project`) | @@ -207,4 +207,4 @@ If you find OpenProver helpful in your research cite simply as: publisher = {GitHub}, url = {https://github.com/kripner/openprover} } -``` \ No newline at end of file +``` diff --git a/openprover/cli.py b/openprover/cli.py index 560d175..d629095 100644 --- a/openprover/cli.py +++ b/openprover/cli.py @@ -11,6 +11,13 @@ from openprover import __version__ from .budget import Budget, parse_duration from .llm import LLMClient, HFClient +from .model_caps import ( + CLAUDE_MODELS, + HF_MODEL_MAP, + TOOL_CAPABLE_MODELS, + VLLM_MODELS, + supports_web_search, +) from .prover import Prover, slugify from .tui import TUI, HeadlessTUI @@ -280,13 +287,6 @@ def _cmd_prove(): (work_dir, theorem_text, lean_theorem_text, proof_md_text, mode, resuming, read_only) = _resolve_inputs(parser, args) - # Map short model names to HuggingFace model IDs - HF_MODEL_MAP = { - "minimax-m2.5": "MiniMaxAI/MiniMax-M2.5", - } - VLLM_MODELS = {"minimax-m2.5"} # served via vLLM (standard OpenAI API) - CLAUDE_MODELS = {"sonnet", "opus"} - TOOL_CAPABLE_MODELS = VLLM_MODELS | CLAUDE_MODELS # ── On resume, load saved config and apply as defaults ── if resuming: @@ -359,9 +359,17 @@ def _cmd_prove(): planner_model = args.planner_model or args.model worker_model = args.worker_model or args.model - # HF-backed models have no web search capability - force isolation - hf_models = {"minimax-m2.5"} - if planner_model in hf_models and not args.isolation: + # literature_search is executed by the worker backend, so web-search + # capability must be checked against the worker model rather than the + # planner model. Older runs may have saved --no-isolation with a local + # worker; correct those to isolation mode. For an explicit new + # --no-isolation request, fail fast with a clear error. + if not args.isolation and not supports_web_search(worker_model): + if _cli_flag_given("--no-isolation"): + parser.error( + "--no-isolation requires a web-search-capable worker model " + "(sonnet or opus)" + ) args.isolation = True if args.headless: @@ -394,10 +402,17 @@ def _cmd_prove(): def _make_client(model_alias, archive_dir): if model_alias in HF_MODEL_MAP: - return HFClient(HF_MODEL_MAP[model_alias], archive_dir, - base_url=args.provider_url, answer_reserve=args.answer_reserve, - vllm=model_alias in VLLM_MODELS) - return LLMClient(model_alias, archive_dir) + client = HFClient( + HF_MODEL_MAP[model_alias], + archive_dir, + base_url=args.provider_url, + answer_reserve=args.answer_reserve, + vllm=model_alias in VLLM_MODELS, + ) + else: + client = LLMClient(model_alias, archive_dir) + client.model_alias = model_alias + return client def make_planner_llm(archive_dir): return _make_client(planner_model, archive_dir) diff --git a/openprover/model_caps.py b/openprover/model_caps.py new file mode 100644 index 0000000..89180bb --- /dev/null +++ b/openprover/model_caps.py @@ -0,0 +1,20 @@ +"""Backend capability helpers shared across the CLI and prover.""" + +HF_MODEL_MAP = { + "minimax-m2.5": "MiniMaxAI/MiniMax-M2.5", +} + +VLLM_MODELS = {"minimax-m2.5"} # served via vLLM (standard OpenAI API) +CLAUDE_MODELS = {"sonnet", "opus"} +TOOL_CAPABLE_MODELS = VLLM_MODELS | CLAUDE_MODELS + + +def supports_web_search(model_alias: str) -> bool: + """Whether a worker model can execute literature_search with web access.""" + return model_alias in CLAUDE_MODELS + + +def llm_supports_web_search(llm) -> bool: + """Runtime web-search capability derived from the same model-alias rules.""" + model_alias = getattr(llm, "model_alias", getattr(llm, "model", "")) + return supports_web_search(model_alias) diff --git a/openprover/prover.py b/openprover/prover.py index a0ba5e4..895ffe4 100644 --- a/openprover/prover.py +++ b/openprover/prover.py @@ -13,6 +13,7 @@ from .budget import Budget from .lean import LeanTheorem, LeanWorkDir, run_lean_check, lean_has_errors, WORKER_TOOLS, execute_worker_tool from .llm import Interrupted, LLMClient +from .model_caps import llm_supports_web_search from .tui import TUI from .tui._colors import YELLOW, GREEN, RESET as _RESET @@ -1370,6 +1371,18 @@ def _handle_literature_search(self, plan: dict, step_dir: Path, self._save_step_meta(step_dir, status="ok", action="literature_search", resp=planner_resp, error="Isolation mode") return "continue" + if not llm_supports_web_search(self.worker_llm): + msg = ( + "Literature search is not available because the worker backend " + "does not support web search." + ) + self.tui.log(msg, color="yellow") + self._push_output(msg) + self._save_step_meta( + step_dir, status="ok", action="literature_search", + resp=planner_resp, error="Worker backend has no web search support", + ) + return "continue" query = plan.get("search_query", "") context = plan.get("search_context", "") diff --git a/tests/test_cli_validation.py b/tests/test_cli_validation.py new file mode 100644 index 0000000..8f0bcbe --- /dev/null +++ b/tests/test_cli_validation.py @@ -0,0 +1,59 @@ +import importlib +import sys +from types import SimpleNamespace + +import pytest + + +def _import_cli_with_stubbed_tty(monkeypatch: pytest.MonkeyPatch): + dummy_termios = SimpleNamespace( + TCSADRAIN=0, + tcgetattr=lambda *args, **kwargs: None, + tcsetattr=lambda *args, **kwargs: None, + ) + dummy_tty = SimpleNamespace(setcbreak=lambda *args, **kwargs: None) + monkeypatch.setitem(sys.modules, "termios", dummy_termios) + monkeypatch.setitem(sys.modules, "tty", dummy_tty) + for name in [ + "openprover.cli", + "openprover.prover", + "openprover.tui", + "openprover.tui.tui", + ]: + sys.modules.pop(name, None) + return importlib.import_module("openprover.cli") + + +def test_no_isolation_requires_web_search_capable_worker( + monkeypatch: pytest.MonkeyPatch, + tmp_path, + capsys: pytest.CaptureFixture[str], +): + theorem = tmp_path / "theorem.md" + theorem.write_text("Prove that 1 = 1.") + + cli = _import_cli_with_stubbed_tty(monkeypatch) + monkeypatch.setattr( + cli.sys, + "argv", + [ + "openprover", + "--theorem", + str(theorem), + "--planner-model", + "opus", + "--worker-model", + "minimax-m2.5", + "--no-isolation", + "--headless", + "--max-time", + "1s", + ], + ) + + with pytest.raises(SystemExit) as exc: + cli._cmd_prove() + + assert exc.value.code == 2 + err = capsys.readouterr().err + assert "--no-isolation requires a web-search-capable worker model" in err diff --git a/tests/test_model_caps.py b/tests/test_model_caps.py new file mode 100644 index 0000000..0b9e1b8 --- /dev/null +++ b/tests/test_model_caps.py @@ -0,0 +1,19 @@ +from types import SimpleNamespace + +from openprover.model_caps import llm_supports_web_search, supports_web_search + + +def test_web_search_capability_matches_worker_backend(): + assert supports_web_search("sonnet") is True + assert supports_web_search("opus") is True + assert supports_web_search("minimax-m2.5") is False + + +def test_llm_supports_web_search_uses_model_alias_when_present(): + claude_like = SimpleNamespace(model_alias="sonnet", model="sonnet") + hf_like = SimpleNamespace(model_alias="minimax-m2.5", model="MiniMaxAI/MiniMax-M2.5") + legacy_claude = SimpleNamespace(model="opus") + + assert llm_supports_web_search(claude_like) is True + assert llm_supports_web_search(hf_like) is False + assert llm_supports_web_search(legacy_claude) is True