diff --git a/scripts/summarize/collect.py b/scripts/summarize/collect.py index 5ec0afa4..99ad91b8 100644 --- a/scripts/summarize/collect.py +++ b/scripts/summarize/collect.py @@ -28,6 +28,7 @@ sys.path.insert(0, str(REPO_ROOT)) from scripts.summarize.task import ( # noqa: E402 + PROOF_OUTPUTS, load_provenance, load_records, plaintext_dir, @@ -43,7 +44,9 @@ class Generated: generation: dict[str, str] -def _submitted_row(sample: EvalSample, tool_name: str) -> dict[str, Any] | None: +def _submitted_row( + sample: EvalSample, tool_names: tuple[str, ...] +) -> dict[str, Any] | None: if sample.output and sample.output.completion: try: row = json.loads(sample.output.completion) @@ -53,13 +56,16 @@ def _submitted_row(sample: EvalSample, tool_name: str) -> dict[str, Any] | None: pass for message in reversed(sample.messages or []): for call in getattr(message, "tool_calls", None) or []: - if call.function == tool_name: + if call.function in tool_names: return dict(call.arguments) return None -def extract(log_paths: list[Path], tool_name: str) -> dict[str, Generated]: +def extract( + log_paths: list[Path], tool_name: str | tuple[str, ...] +) -> dict[str, Generated]: """Extract submissions, with later log arguments winning by sample id.""" + tool_names = (tool_name,) if isinstance(tool_name, str) else tool_name generated: dict[str, Generated] = {} seen: set[str] = set() for path in log_paths: @@ -68,7 +74,7 @@ def extract(log_paths: list[Path], tool_name: str) -> dict[str, Generated]: for sample in log.samples or []: sample_id = str(sample.id) seen.add(sample_id) - row = _submitted_row(sample, tool_name) + row = _submitted_row(sample, tool_names) if row is None: continue generated[sample_id] = Generated( @@ -78,7 +84,8 @@ def extract(log_paths: list[Path], tool_name: str) -> dict[str, Generated]: ) missing = sorted(seen - generated.keys()) if missing: - print(f"warning: no {tool_name} submission for: {missing}", file=sys.stderr) + names = " or ".join(tool_names) + print(f"warning: no {names} submission for: {missing}", file=sys.stderr) return generated @@ -131,8 +138,56 @@ def collect_conjectures(args: argparse.Namespace) -> int: return 0 +def _group_proof_outputs( + generated: dict[str, Generated], +) -> dict[str, dict[str, Generated]]: + """Group independently generated summary and full-proof samples.""" + valid_outputs = {output.name for output in PROOF_OUTPUTS} + grouped: dict[str, dict[str, Generated]] = {} + for sample_id, item in generated.items(): + proof_id = item.metadata.get("proof_id") + proof_output = item.metadata.get("proof_output") + if proof_id is None or proof_output is None: + print( + f"warning: incomplete proof output metadata for {sample_id}", + file=sys.stderr, + ) + continue + + proof_id = str(proof_id) + proof_output = str(proof_output) + if proof_output not in valid_outputs: + print( + f"warning: unknown proof output {proof_output!r} for {sample_id}", + file=sys.stderr, + ) + continue + grouped.setdefault(proof_id, {})[proof_output] = item + return grouped + + +def _proof_metadata( + settlement: str, generated: dict[str, Generated] +) -> dict[str, Any]: + outputs: dict[str, dict[str, Any]] = {} + for output in PROOF_OUTPUTS: + item = generated.get(output.name) + value = { + "text": item.row.get(output.field) if item else None, + "generation": item.generation if item else None, + } + outputs[output.name] = value + + return { + "settlement": settlement, + **outputs, + } + + def collect_proofs(args: argparse.Namespace) -> int: - generated = extract(args.eval, "submit_proof_summary") + generated = _group_proof_outputs( + extract(args.eval, ("submit_proof_summary", "submit_full_proof")) + ) run_dir = _output_path(args.run_dir) allowed = {conjecture.id for conjecture in subset_conjectures(args.subset)} solves = { @@ -144,19 +199,14 @@ def collect_proofs(args: argparse.Namespace) -> int: unexpected = sorted(generated.keys() - solves.keys()) if unexpected: print( - f"warning: proof summaries do not match accepted samples in {run_dir}: " + f"warning: proof outputs do not match accepted samples in {run_dir}: " f"{unexpected}", file=sys.stderr, ) written = 0 for sample_id, solve in sorted(solves.items()): - item = generated.get(sample_id) - value = { - "settlement": solve.settlement, - "proof_summary": item.row.get("proof_summary") if item else None, - "generation": item.generation if item else None, - } + value = _proof_metadata(solve.settlement, generated.get(sample_id, {})) write_json(solve.directory / "metadata.json", value) written += 1 print(f"wrote proof metadata for {written} accepted samples under {plaintext_dir(run_dir)}") diff --git a/scripts/summarize/task.py b/scripts/summarize/task.py index 9dfe2f2c..2700a2a1 100644 --- a/scripts/summarize/task.py +++ b/scripts/summarize/task.py @@ -1,9 +1,10 @@ """Inspect tasks for generating normalized OEIS metadata. -The sequence and conjecture tasks are run once for the Lite dataset. Proof -summaries are run once per accepted proof in an evaluation run. Deterministic -collection into ``metadata/*.json`` and per-sample ``metadata.json`` files is -handled by ``collect.py``. +The sequence and conjecture tasks are run once for the Lite dataset. A concise +summary and a full natural-language proof or disproof are generated independently +for each accepted result in an evaluation run. Deterministic collection into +``metadata/*.json`` and per-sample ``metadata.json`` files is handled by +``collect.py``. Examples:: @@ -13,7 +14,7 @@ -T subset=lite -T metadata_dir=metadata \ --model openai/gpt-5.6-sol --log-dir logs/summarize inspect eval scripts/summarize/task.py@summarize_proofs \ - -T run_dir=logs/ -T subset=lite -T metadata_dir=metadata \ + -T run_dir=logs/ -T subset=all -T metadata_dir=metadata \ --model openai/gpt-5.6-sol --log-dir logs/summarize """ @@ -115,10 +116,53 @@ class Solve(NamedTuple): directory: Path +class ProofOutput(NamedTuple): + name: str + field: str + submit_tool: str + instruction: str + + +# The full-proof suggestion is deliberately not a limit: informal proofs in the +# paper's appendix reach roughly 2,000 words. +PROOF_OUTPUTS = ( + ProofOutput( + name="summary", + field="proof_summary", + submit_tool="submit_proof_summary", + instruction=( + "one or two concise sentences explaining the key mathematical " + "ideas of this specific {noun}. Do not restate the sequence or " + "conjecture" + ), + ), + ProofOutput( + name="full_proof", + field="full_proof", + submit_tool="submit_full_proof", + instruction=( + "a complete, self-contained natural-language {noun} with every " + "essential construction, intermediate result, reduction, and case " + "split explained. There is no maximum length: use as much space as " + "the argument needs. For example, a 3,000-word exposition is entirely " + "acceptable if that is what a clear proof requires. This must be " + "the full mathematical argument, not a synopsis or an expanded " + "summary; introduce the necessary notation and explain how every " + "substantive step follows" + ), + ), +) + + def subset_conjectures(subset: str) -> list[Conjecture]: """Return the subset's conjectures in its authoritative order.""" - names = load_subset(OEIS_DIR, subset) - samples = {str(sample.id): sample for sample in oeis_dataset(names=names)} + if subset == "all": + dataset = oeis_dataset() + names = [str(sample.id) for sample in dataset] + else: + names = load_subset(OEIS_DIR, subset) + dataset = oeis_dataset(names=names) + samples = {str(sample.id): sample for sample in dataset} conjectures: list[Conjecture] = [] for name in names: sample = samples.get(name) @@ -253,42 +297,41 @@ def proof_prompt( provenance: dict[str, Any] | None, sequence_description: str | None, conjecture_description: str | None, + output: ProofOutput, ) -> str: noun = "proof" if solve.settlement == "proved" else "disproof" + output_label = output.name.replace("_", " ") + instruction = output.instruction.format(noun=noun) return f"""\ An AI agent {solve.settlement} the conjecture {solve.id} about OEIS sequence {solve.oeis_id}. The accepted {noun} is in {ENTRY_PATH}. -Call submit_proof_summary with one or two concise sentences explaining the key -mathematical ideas of this specific {noun}. Do not restate the sequence or -conjecture. Focus exclusively on the mathematical argument: omit Lean tactics, -library lemmas, proof-assistant architecture, implementation details, and claims -that a computation is "kernel-checked", "verified", or "certified" merely because -it was formalized. Describe a finite or modular computation by its mathematical -role instead. +Call {output.submit_tool} with {instruction}. + +Focus exclusively on the mathematical argument: omit Lean tactics, internal +library-lemma names, proof-assistant architecture, implementation details, and +claims that a computation is "kernel-checked", "verified", or "certified" +merely because it was formalized. State the mathematical content of any invoked +result and describe each finite or modular computation by its mathematical role. Examples of the intended style: - "a kernel-checked finite avoidance computation" becomes "a finite avoidance computation"; - "a verified bit-sieve" becomes "a bit-sieve"; -- "segmented, kernel-checked binary exponentiation" becomes - "segmented binary exponentiation"; -- "Kernel computation checks each candidate" becomes - "Direct computation checks each candidate"; -- "Kernel-checked modular computations establish ..." becomes - "Modular computations establish ...". Plain text with LaTeX math is allowed. -Canonical sequence description: + {sequence_description or "(unavailable)"} + -Canonical conjecture description: + {conjecture_description or "(unavailable)"} + A Lean 4 toolchain with the full Mathlib source tree ({MATHLIB_SOURCE}) is available, along with `rg` and `python`. Investigate the accepted {noun} as much -as useful before summarizing its mathematical argument. +as useful before writing the requested {output_label}. {json.dumps(record, indent=2)} @@ -308,7 +351,7 @@ async def execute(description: str) -> ToolResult: Args: description: Description of the sequence, at most about 10 words. """ - store().set("summary", {"description": description}) + store().set("submission", {"description": description}) return "Submitted." return execute @@ -322,7 +365,7 @@ async def execute(conjecture: str) -> ToolResult: Args: conjecture: One sentence stating the conjecture. """ - store().set("summary", {"conjecture": conjecture}) + store().set("submission", {"conjecture": conjecture}) return "Submitted." return execute @@ -331,12 +374,26 @@ async def execute(conjecture: str) -> ToolResult: @tool def submit_proof_summary() -> Tool: async def execute(proof_summary: str) -> ToolResult: - """Submit a concise summary of the accepted proof or disproof. + """Submit the requested summary of the accepted proof or disproof. + + Args: + proof_summary: Summary respecting the length requested in the prompt. + """ + store().set("submission", {"proof_summary": proof_summary}) + return "Submitted." + + return execute + + +@tool +def submit_full_proof() -> Tool: + async def execute(full_proof: str) -> ToolResult: + """Submit the full exposition of the accepted proof or disproof. Args: - proof_summary: One or two sentences naming the proof's key ideas. + full_proof: Complete natural-language proof with no maximum length. """ - store().set("summary", {"proof_summary": proof_summary}) + store().set("submission", {"full_proof": full_proof}) return "Submitted." return execute @@ -348,11 +405,21 @@ async def solve(state: TaskState, generate: Generate) -> TaskState: if kind == "proof": await sandbox().write_file(ENTRY_PATH, state.metadata["proof"]) tools = [text_editor(), bash(timeout=300)] - submit = AgentSubmit( - tool=submit_proof_summary(), - name="submit_proof_summary", - keep_in_messages=True, - ) + proof_output = state.metadata["proof_output"] + if proof_output == "full_proof": + submit = AgentSubmit( + tool=submit_full_proof(), + name="submit_full_proof", + keep_in_messages=True, + ) + elif proof_output == "summary": + submit = AgentSubmit( + tool=submit_proof_summary(), + name="submit_proof_summary", + keep_in_messages=True, + ) + else: + raise ValueError(f"unknown proof output: {proof_output!r}") elif kind == "conjecture": tools = [] submit = AgentSubmit( @@ -375,9 +442,9 @@ async def solve(state: TaskState, generate: Generate) -> TaskState: ) state = await as_solver(agent)(state, generate) - summary = state.store.get("summary") - if summary is not None: - state.output.completion = json.dumps(summary) + submission = state.store.get("submission") + if submission is not None: + state.output.completion = json.dumps(submission) state.completed = True return state @@ -463,23 +530,27 @@ def summarize_proofs( continue sequence = sequences.get(solve.oeis_id) or {} conjecture = conjectures.get(solve.id) or {} - samples.append( - Sample( - input=proof_prompt( - solve, - records.get(solve.oeis_id, {}), - provenance.get(solve.id), - sequence.get("description"), - conjecture.get("conjecture"), - ), - id=solve.id, - metadata={ - "proof": solve.proof, - "oeis_id": solve.oeis_id, - "settlement": solve.settlement, - }, + for output in PROOF_OUTPUTS: + samples.append( + Sample( + input=proof_prompt( + solve, + records.get(solve.oeis_id, {}), + provenance.get(solve.id), + sequence.get("description"), + conjecture.get("conjecture"), + output, + ), + id=f"{solve.id}__{output.name}", + metadata={ + "proof": solve.proof, + "proof_id": solve.id, + "oeis_id": solve.oeis_id, + "settlement": solve.settlement, + "proof_output": output.name, + }, + ) ) - ) return Task( dataset=MemoryDataset(samples), solver=summarizer("proof"), diff --git a/tests/test_summarize.py b/tests/test_summarize.py index febb3956..5cced012 100644 --- a/tests/test_summarize.py +++ b/tests/test_summarize.py @@ -1,13 +1,22 @@ """Fast checks for the metadata summarization tasks. No model or Docker calls.""" +import json from pathlib import Path -from apn.dataset import OEIS_DIR, fc_commit +from apn.dataset import OEIS_DIR, fc_commit, oeis_dataset from apn.task import get_identifier_for_image +from scripts.summarize.collect import ( + Generated, + _group_proof_outputs, + _proof_metadata, +) from scripts.summarize.task import ( + PROOF_OUTPUTS, get_agent_compose_file, summarize_conjectures, + summarize_proofs, summarize_sequences, + subset_conjectures, ) @@ -19,6 +28,15 @@ def test_lite_catalog_tasks_load_current_dataset(tmp_path: Path) -> None: assert len(conjectures.dataset) == 100 +def test_all_conjectures_load_full_dataset_in_order() -> None: + conjectures = subset_conjectures("all") + + assert len(conjectures) == 492 + assert [conjecture.id for conjecture in conjectures] == [ + str(sample.id) for sample in oeis_dataset() + ] + + def test_proof_summarizer_compose_uses_oeis_pin() -> None: commit = fc_commit(OEIS_DIR) compose = get_agent_compose_file().read_text() @@ -26,3 +44,93 @@ def test_proof_summarizer_compose_uses_oeis_pin() -> None: assert get_identifier_for_image("agent", commit) in compose assert f"FC_COMMIT: {commit}" in compose assert "network_mode: none" in compose + + +def test_proof_task_creates_independent_summary_and_full_proof( + tmp_path: Path, +) -> None: + conjecture = subset_conjectures("lite")[0] + sample_dir = tmp_path / "run" / "test_plaintext" / conjecture.id + submission_dir = sample_dir / "Submission" + submission_dir.mkdir(parents=True) + (sample_dir / "scores.json").write_text( + json.dumps({"proof_scorer": {"value": "C"}}) + ) + (sample_dir / "info.json").write_text( + json.dumps({"oeis_id": conjecture.oeis_id}) + ) + (submission_dir / "Spec.lean").write_text( + "theorem accepted_proof : True := by trivial\n" + ) + metadata_dir = tmp_path / "metadata" + metadata_dir.mkdir() + (metadata_dir / "sequences.json").write_text("{}") + (metadata_dir / "conjectures.json").write_text("{}") + + task = summarize_proofs( + run_dir=str(tmp_path / "run"), metadata_dir=str(metadata_dir) + ) + samples = list(task.dataset) + + assert len(samples) == 2 + sample_metadata = [sample.metadata for sample in samples] + assert all(metadata is not None for metadata in sample_metadata) + metadata_rows = [metadata or {} for metadata in sample_metadata] + assert [metadata["proof_output"] for metadata in metadata_rows] == [ + "summary", + "full_proof", + ] + assert len({sample.id for sample in samples}) == 2 + for sample, metadata, output in zip( + samples, metadata_rows, PROOF_OUTPUTS, strict=True + ): + assert metadata["proof_id"] == conjecture.id + assert output.submit_tool in str(sample.input) + assert "relying on another generated version" not in str(sample.input) + summary_prompt = " ".join(str(samples[0].input).split()) + full_proof_prompt = " ".join(str(samples[1].input).split()) + assert ( + "one or two concise sentences explaining the key mathematical ideas " + "of this specific proof" + in summary_prompt + ) + assert "complete, self-contained natural-language proof" in full_proof_prompt + assert "There is no maximum length" in full_proof_prompt + assert "3,000-word exposition is entirely acceptable" in full_proof_prompt + assert "not a synopsis or an expanded summary" in full_proof_prompt + + +def test_proof_collection_groups_summary_and_full_proof() -> None: + generated = { + "proof-id__summary": Generated( + row={"proof_summary": "Short."}, + metadata={"proof_id": "proof-id", "proof_output": "summary"}, + generation={"model": "summary-model", "source_eval": "summary.eval"}, + ), + "proof-id__full_proof": Generated( + row={"full_proof": "A complete proof with all intermediate steps."}, + metadata={"proof_id": "proof-id", "proof_output": "full_proof"}, + generation={"model": "proof-model", "source_eval": "proof.eval"}, + ), + } + + grouped = _group_proof_outputs(generated) + metadata = _proof_metadata("proved", grouped["proof-id"]) + + assert metadata == { + "settlement": "proved", + "summary": { + "text": "Short.", + "generation": { + "model": "summary-model", + "source_eval": "summary.eval", + }, + }, + "full_proof": { + "text": "A complete proof with all intermediate steps.", + "generation": { + "model": "proof-model", + "source_eval": "proof.eval", + }, + }, + }