diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 000000000..6a82d52ed --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "third_party/formal-conjectures"] + path = third_party/formal-conjectures + url = https://github.com/google-deepmind/formal-conjectures.git diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 3da9351f7..45aab501e 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -362,3 +362,58 @@ Please include: - Area of expertise - Type of contribution (algorithmic/research problem) - Brief description of your proposed contribution + +## Formal Conjectures (Lean) Problems + +`research/problems/formal_conjectures/` hosts one problem per conjecture +statement from [google-deepmind/formal-conjectures](https://github.com/google-deepmind/formal-conjectures) +(categories `research open` and `research solved`). The source of truth is the +git submodule at `third_party/formal-conjectures`, pinned to a `bench-*` +release tag; **problem directories are generated from it and are not +committed** (see the `.gitignore` there). Materialization is automatic: the +first `frontier list|eval|show` touching these problems initializes the +submodule and runs the generator (`src/frontier_cs/lazy_problems.py`), stamping +the submodule commit plus a generator hash in `_generator/.generated-ref` so +later accesses serve the files directly (and template changes in `generate.py` +re-materialize automatically). To materialize manually: + +```bash +git submodule update --init third_party/formal-conjectures +python3 research/problems/formal_conjectures/_generator/generate.py +``` + +- The generator parses the submodule's Lean sources directly (namespaces, + `@[category ...]` attributes) — no Lean toolchain needed. "Fill-in-the-answer" + statements (`answer(sorry)`) elaborate with a placeholder (`True` for Props), + so the plain "prove this" contract would misstate them. Those of the exact + binder-free shape `answer(sorry) ↔ Q` become mode `prove_or_disprove` + problems (submit a proof of `Q` or of `¬Q`; the trusted checker extracts `Q` + from the compiled `True ↔ Q` type and fails closed on anything else). The + rest — value-style answers, statements referencing section `variable`s or + sorry-containing defs — are skipped rather than misrepresented. After a + submodule bump, validate with + `research/problems/formal_conjectures/_generator/shape_check.sh` (requires + docker + the eval image): it rechecks every prove-or-disprove target's + compiled shape. +- Solutions are Lean 4 proofs, checked in a Docker image with Lean + Mathlib + + formal-conjectures prebuilt (`research/problems/formal_conjectures/docker/`). +- Scoring is binary: 1.0 iff the submitted proof compiles without `sorry`, + proves a statement definitionally equal to the conjecture, and uses only the + standard axioms. See `research/problems/formal_conjectures/common/`. +- These problems are **excluded from CI validation** (the `.skip-validation` + marker): open conjectures cannot have a reference solution scoring > 0. + They are also excluded from `research/scripts/problems.txt` and the README + problem count. + +To bump the submodule to a new upstream release: + +```bash +git -C third_party/formal-conjectures checkout +research/problems/formal_conjectures/docker/build.sh --push # rebuild eval image +python3 research/problems/formal_conjectures/_generator/generate.py --wipe +git add third_party/formal-conjectures # only the pointer changes +``` + +The parser can be cross-checked against upstream's own extractor: +`docker run --rm lake exe extract_names > /tmp/extract.json` +then `generate.py --check-against /tmp/extract.json`. diff --git a/research/README.md b/research/README.md index 9d3231b56..061848ed3 100644 --- a/research/README.md +++ b/research/README.md @@ -35,9 +35,9 @@ frontier batch research --status # Check progress ## Python API ```python -from frontier_cs import SingleEvaluator +from frontier_cs import SingleEvaluator -evaluator = SingleEvaluator() +evaluator = SingleEvaluator() # Single problem (uses SkyPilot by default for research) result = evaluator.evaluate("research", problem_id="flash_attn", code=my_code) @@ -135,3 +135,27 @@ class Solution: Check each problem's `readme` for the specific `solve()` signature and return type. + +## Formal Conjectures (Lean) Problems + +`formal_conjectures//` problems ask for a Lean 4 proof of a +formalized conjecture from +[google-deepmind/formal-conjectures](https://github.com/google-deepmind/formal-conjectures). +Problem directories are generated from the `third_party/formal-conjectures` +submodule and are not committed — the framework materializes them +automatically on first access (list/eval/show): + +```bash +# List them (generates the problem dirs on first run) +uv run frontier list research | grep formal_conjectures + +# Evaluate a proof (Docker backend; the image bundles Lean + Mathlib prebuilt) +uv run frontier eval research formal_conjectures/erdos_problems/Erdos1.erdos_1 \ + proof.lean --backend docker +``` + +A submission is a single Lean file declaring a top-level +`theorem solution : := ` (see each problem's readme). +Score is binary: 1.0 iff the proof compiles without `sorry`, the statement +matches the conjecture up to definitional equality, and no axioms beyond +`propext`, `Classical.choice`, `Quot.sound` are used. diff --git a/research/problems/formal_conjectures/.gitignore b/research/problems/formal_conjectures/.gitignore new file mode 100644 index 000000000..2e7715a90 --- /dev/null +++ b/research/problems/formal_conjectures/.gitignore @@ -0,0 +1,8 @@ +# Problem directories are generated from the third_party/formal-conjectures +# submodule and are not committed. Materialize them with: +# python3 research/problems/formal_conjectures/_generator/generate.py +/*/ +!/_generator/ +!/common/ +!/docker/ +/_generator/.generated-ref diff --git a/research/problems/formal_conjectures/.skip-validation b/research/problems/formal_conjectures/.skip-validation new file mode 100644 index 000000000..a126a0752 --- /dev/null +++ b/research/problems/formal_conjectures/.skip-validation @@ -0,0 +1,3 @@ +Problems in this directory are auto-generated Lean proof tasks for open math +conjectures. Open conjectures cannot have a reference solution scoring > 0, +so CI reference validation is skipped (see scripts/detect_changed_problems.py). diff --git a/research/problems/formal_conjectures/_generator/ShapeCheck.lean b/research/problems/formal_conjectures/_generator/ShapeCheck.lean new file mode 100644 index 000000000..47e9e79af --- /dev/null +++ b/research/problems/formal_conjectures/_generator/ShapeCheck.lean @@ -0,0 +1,47 @@ +/- +Validation sweep for prove-or-disprove problems (run via shape_check.sh). + +Reads a file of lines " / " and checks, +in the prebuilt eval environment, that every target's compiled type has the +exact placeholder shape `True ↔ Q` required by CheckDriver.lean's +"prove_or_disprove" mode. Any target failing this would be a permanently-zero +problem (the driver fails closed) and must be excluded by the generator — +typically because the statement references section `variable`s, which prepend +∀ binders to the compiled type. + +Prints one "BAD : " line per failure and a final +"checked , bad " summary; exits non-zero iff any target is bad. +-/ +import Lean +open Lean + +def mkNameFromComponents (cs : List String) : Name := + cs.foldl .str .anonymous + +def main (args : List String) : IO UInt32 := do + initSearchPath (← findSysroot) + let lines ← IO.FS.lines ⟨args.head!⟩ + let entries := lines.filterMap fun l => + if l.isEmpty then none + else + match l.splitOn " / " with + | [m, t] => some (mkNameFromComponents (m.splitOn " "), + mkNameFromComponents (t.splitOn " ")) + | _ => none + let mods := entries.map (fun e => ({ module := e.1 } : Import)) + let env ← importModules mods {} + let mut bad := 0 + let mut total := 0 + for (_, name) in entries do + total := total + 1 + match env.find? name with + | none => IO.println s!"BAD missing: {name}"; bad := bad + 1 + | some ci => + if ci.type.hasSorry then + IO.println s!"BAD hasSorry: {name}"; bad := bad + 1 + else if !ci.type.isAppOfArity `Iff 2 then + IO.println s!"BAD not-iff: {name}"; bad := bad + 1 + else if !(ci.type.appFn!.appArg!.isConstOf `True) then + IO.println s!"BAD lhs-not-True: {name}"; bad := bad + 1 + IO.println s!"checked {total}, bad {bad}" + return if bad == 0 then 0 else 1 diff --git a/research/problems/formal_conjectures/_generator/generate.py b/research/problems/formal_conjectures/_generator/generate.py new file mode 100644 index 000000000..f5fee054c --- /dev/null +++ b/research/problems/formal_conjectures/_generator/generate.py @@ -0,0 +1,922 @@ +#!/usr/bin/env python3 +""" +Generate one Frontier-CS research problem per formal-conjectures statement, +directly from the third_party/formal-conjectures submodule sources. + +Each theorem tagged `@[category research open]` or `@[category research solved]` +becomes a problem directory: + + research/problems/formal_conjectures/// + config.yaml # identical for all problems + evaluate.sh # identical (in-container entrypoint) + check.sh # host-side wrapper: ./check.sh solution.lean scores locally + evaluator.py # thin shim importing ../../common/fc_evaluator.py + target.json # which module/theorem this problem targets + readme # statement, docstring, submission contract + +Generated directories are NOT committed (see ../.gitignore): the submodule is +the source of truth and generation is deterministic. Run this script once per +checkout (and after every submodule bump): + + python3 research/problems/formal_conjectures/_generator/generate.py --wipe + +"Fill-in-the-answer" conjectures — statements using `answer(sorry)` for an +unknown answer — get special treatment. Upstream's `answer()` elaborator +substitutes a placeholder (`True` for Props), so their elaborated type +misstates the question and the plain "prove this statement" contract would be +unsound. Statements of the exact shape `theorem n : answer(sorry) ↔ Q` become +mode "prove_or_disprove" problems instead (target.json `mode` field): the task +is to prove `Q` or `¬Q`, checked by the trusted driver against the compiled +`True ↔ Q` type. All other answer-style statements (value-style answers, +ambiguous shapes, statements referencing same-file sorry-defs) remain +excluded rather than misrepresented — there is no sound automatic check for +"is this value a genuine answer". + +The parser can be cross-checked against the upstream extractor (ground truth +from the built Lean environment): + + docker run --rm lake exe extract_names > /tmp/extract.json + python3 generate.py --check-against /tmp/extract.json +""" + +import argparse +import hashlib +import json +import re +import shutil +import subprocess +import sys +from dataclasses import dataclass +from pathlib import Path + +GENERATOR_DIR = Path(__file__).resolve().parent +PROBLEMS_ROOT = GENERATOR_DIR.parent # research/problems/formal_conjectures +REPO_ROOT = PROBLEMS_ROOT.parents[2] +SUBMODULE = REPO_ROOT / "third_party" / "formal-conjectures" +UPSTREAM = "https://github.com/google-deepmind/formal-conjectures" + +DEFAULT_CATEGORIES = ("research open", "research solved") +IMAGE = "shangyint/formal-conjectures-eval" + +CONFIG_YAML = """\ +tag: math +runtime: + language: lean + timeout_seconds: 1800 + environment: "Lean 4 + Mathlib + formal-conjectures ({ref}), prebuilt at /opt/formal-conjectures" + docker: + image: {image}:{ref} + resources: + cpus: "8" + memory: "32" +""" + +EVALUATE_SH = """\ +#!/usr/bin/env bash +set -euo pipefail +SCRIPT_DIR=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd) +cd "$SCRIPT_DIR" +# Default is the harness layout; override for standalone runs inside the eval +# image (or just use ./check.sh from the host, which sets this for you). +SOLUTION_PATH="${SOLUTION_PATH:-/work/execution_env/solution_env/solution.lean}" +python3 evaluator.py --solution-path "$SOLUTION_PATH" --target target.json +""" + +# Host-side scorer; @IMAGE_REF@ is substituted at generation time (the template +# is .replace()d, not .format()ted, because of the bash ${...} braces). +CHECK_SH = """\ +#!/usr/bin/env bash +# Score a candidate solution for this problem locally. Requires docker and the +# prebuilt eval image. Prints evaluator diagnostics on stderr; the last stdout +# line is the score (1.0 accepted / 0.0 rejected). Takes ~2 min (import loading). +# +# ./check.sh path/to/solution.lean +set -euo pipefail +if [ "$#" -ne 1 ] || [ ! -f "$1" ]; then + echo "usage: $0 path/to/solution.lean" >&2 + exit 2 +fi +SCRIPT_DIR=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd) +FC_ROOT=$(cd "$SCRIPT_DIR/../.." && pwd) +REL=${SCRIPT_DIR#"$FC_ROOT"/} +SOLUTION=$(cd "$(dirname "$1")" && pwd)/$(basename "$1") +exec docker run --rm \\ + -v "$FC_ROOT":/fcp:ro \\ + -v "$SOLUTION":/sol/solution.lean:ro \\ + -e SOLUTION_PATH=/sol/solution.lean \\ + @IMAGE_REF@ \\ + bash "/fcp/$REL/evaluate.sh" +""" + +EVALUATOR_PY = """\ +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "common")) + +from fc_evaluator import main + +if __name__ == "__main__": + main() +""" + +README = """\ +# {theorem} + +Formalized conjecture from [google-deepmind/formal-conjectures]({upstream}) at +`{ref}` — source: [`{source_file}`]({upstream}/blob/{ref}/{source_file}) +(vendored at `third_party/formal-conjectures`; Apache-2.0 / CC-BY). + +- Category: {category} +- AMS subjects: {subjects} + +## Statement +{docstring_section} +```lean +{statement} := by + sorry +``` +{namespace_note} +## Task + +Prove this statement. Submit **one Lean 4 file** that: + +1. Imports the module containing the statement (plus anything else you need + from Mathlib): + + ```lean + import {module_dotted} + ``` + +2. Declares a **top-level** theorem named `solution` whose statement is + *exactly* the statement above (you may `open` the relevant namespaces, or + restate it in any definitionally equal form): + + ```lean + theorem solution : := + ``` + +## Scoring + +Binary. Score 1.0 iff: + +- the file compiles against Lean {lean_version} + Mathlib + formal-conjectures + `{ref}` (the exact prebuilt environment is in the evaluation image), +- it contains no `sorry` / `admit`, +- the type of `solution` is definitionally equal to the statement of + `{theorem}`, and +- `solution` depends on no axioms beyond `propext`, `Classical.choice`, + `Quot.sound`. + +Anything else scores 0.0. Not allowed (rejected by lint): `axiom`, `macro`, +`elab`, `syntax`, `notation`, `initialize`, `run_cmd`, `implemented_by`, +`extern`, `unsafe`, `native_decide`, `set_option debug.*`. + +## Local verification + +With docker available, score a candidate from this problem directory: + + ./check.sh path/to/solution.lean + +This runs the official evaluator (lint + compile + trusted statement/axiom +check) inside `{image_ref}`; the last stdout line is the score. A run takes +~2 minutes, almost all of it Mathlib import loading — so while iterating, +prefer one compile-only pass over many small ones, batching experimental +lemmas into a single file: + + docker run --rm -v "$PWD":/sol {image_ref} \\ + bash -c 'cd /opt/formal-conjectures && lake env lean --root /sol /sol/solution.lean' + +Exit code 0 with no output means it compiles (`sorry` still compiles, with a +warning). Mathlib and formal-conjectures sources are browsable in the image +under `/opt/formal-conjectures`. +""" + + +README_POD = """\ +# {theorem} + +Formalized fill-in-the-answer conjecture from +[google-deepmind/formal-conjectures]({upstream}) at +`{ref}` — source: [`{source_file}`]({upstream}/blob/{ref}/{source_file}) +(vendored at `third_party/formal-conjectures`; Apache-2.0 / CC-BY). + +- Category: {category} +- AMS subjects: {subjects} +- Mode: prove or disprove + +## Statement +{docstring_section} +The upstream statement leaves its truth value open — `answer(sorry)` marks +the unknown answer: + +```lean +{statement} := by + sorry +``` + +The question, `Q`, is the right-hand side of the iff: + +```lean +Q := {question} +``` + +(In the prebuilt environment the `answer(sorry)` placeholder elaborates to +`True`, so the declared statement reads `True ↔ Q`. Do **not** prove that — +it misstates the question and scores 0.0.) +{namespace_note} +## Task + +Determine whether `Q` is true or false, and prove your answer. Submit **one +Lean 4 file** that: + +1. Imports the module containing the statement (plus anything else you need + from Mathlib): + + ```lean + import {module_dotted} + ``` + +2. Declares a **top-level** theorem named `solution` proving either `Q` or + `¬Q` (you may `open` the relevant namespaces, or use any definitionally + equal form): + + ```lean + theorem solution : := -- claiming the answer is yes + -- or + theorem solution : ¬() := -- claiming the answer is no + ``` + +## Scoring + +Binary. Score 1.0 iff: + +- the file compiles against Lean {lean_version} + Mathlib + formal-conjectures + `{ref}` (the exact prebuilt environment is in the evaluation image), +- it contains no `sorry` / `admit`, +- the type of `solution` is definitionally equal to `Q` or to `¬Q`, where the + trusted checker extracts `Q` from the compiled statement of `{theorem}`, and +- `solution` depends on no axioms beyond `propext`, `Classical.choice`, + `Quot.sound`. + +Anything else — including anything the trusted checker cannot positively +verify — scores 0.0. Not allowed (rejected by lint): `axiom`, `macro`, +`elab`, `syntax`, `notation`, `initialize`, `run_cmd`, `implemented_by`, +`extern`, `unsafe`, `native_decide`, `set_option debug.*`. + +## Local verification + +With docker available, score a candidate from this problem directory: + + ./check.sh path/to/solution.lean + +This runs the official evaluator (lint + compile + trusted statement/axiom +check) inside `{image_ref}`; the last stdout line is the score. A run takes +~2 minutes, almost all of it Mathlib import loading — so while iterating, +prefer one compile-only pass over many small ones, batching experimental +lemmas into a single file: + + docker run --rm -v "$PWD":/sol {image_ref} \\ + bash -c 'cd /opt/formal-conjectures && lake env lean --root /sol /sol/solution.lean' + +Exit code 0 with no output means it compiles (`sorry` still compiles, with a +warning). Mathlib and formal-conjectures sources are browsable in the image +under `/opt/formal-conjectures`. +""" + + +# -------------------------------------------------------------------------- +# Lean source parsing +# -------------------------------------------------------------------------- + +# Exact fill-in-the-answer shape rescuable as prove-or-disprove: the statement +# is a binder-free top-level `answer(sorry) ↔ Q`. (Trailing `Q ↔ answer(sorry)` +# is textually ambiguous with `∀ x, (P x ↔ answer(sorry))` and is not rescued.) +ANSWER_IFF_RE = re.compile( + r"(?s)\b(?:theorem|lemma)\s+[^\s:({\[⦃⟨]+\s*:\s*" + r"answer\(\s*sorry\s*\)\s*↔\s*(.+)$" +) + +DECL_RE = re.compile( + r"^(?:private\s+|protected\s+|noncomputable\s+)*(?:theorem|lemma)\s+" + r"([^\s:({\[⦃⟨]+)" +) +DEF_RE = re.compile( + r"^(?:private\s+|protected\s+|noncomputable\s+)*(?:def|abbrev)\s+" + r"([^\s:({\[⦃⟨]+)" +) +ANON_INSTANCE_RE = re.compile( + r"^(?:private\s+|protected\s+|noncomputable\s+)*instance\b" +) +NAMESPACE_RE = re.compile(r"^namespace\s+(\S+)") +SECTION_RE = re.compile(r"^(?:noncomputable\s+)?section\b") +END_RE = re.compile(r"^end\b") +VARIABLE_RE = re.compile(r"^variables?\b") +OPEN_BRACKETS = "([{⟨⦃" +CLOSE_BRACKETS = ")]}⟩⦄" + + +@dataclass +class Decl: + full_name_components: list + category: str + subjects: list + statement: str # attr line(s) + signature, proof stripped + docstring: str + module_components: list + source_file: str + skip_answer_style: bool + answer_taint: bool = False # statement references same-file sorry-defs + uses_section_vars: bool = False # statement references in-scope `variable`s + + @property + def full_name(self) -> str: + return ".".join(self.full_name_components) + + +def split_name(dotted: str) -> list: + """Split a Lean dotted name into components, honoring «...» quoting.""" + components, buf, depth = [], [], 0 + for ch in dotted: + if ch == "«": + depth += 1 + elif ch == "»": + depth -= 1 + elif ch == "." and depth == 0: + components.append("".join(buf)) + buf = [] + continue + else: + buf.append(ch) + components.append("".join(buf)) + return components + + +def is_internal(components: list) -> bool: + """Mirror upstream extract_names: names with `_`/`match_`/`proof_`-prefixed + components are auxiliary declarations, not benchmark statements.""" + return any(c.startswith(("_", "match_", "proof_")) for c in components) + + +def snake(name: str) -> str: + """CamelCase source dir -> snake_case problem dir (ErdosProblems -> erdos_problems).""" + s = re.sub(r"(?<=[a-z0-9])(?=[A-Z])|(?<=[A-Z])(?=[A-Z][a-z])", "_", name) + return s.lower() + + +def sanitize(component: str) -> str: + return re.sub(r"[^A-Za-z0-9_']", "_", component) + + +def consume_block_comment(s: str, depth: int): + """Consume a (nesting) block comment. Returns (remainder, new_depth).""" + pos = 0 + while depth > 0: + opener = s.find("/-", pos) + closer = s.find("-/", pos) + if opener != -1 and (closer == -1 or opener < closer): + depth += 1 + pos = opener + 2 + elif closer != -1: + depth -= 1 + pos = closer + 2 + else: + return "", depth + return s[pos:], 0 + + +class LineCleaner: + """Strips comments from source lines while capturing docstrings, across + lines. Feed raw lines; get back the code content of each line.""" + + def __init__(self): + self.comment_depth = 0 + self.docstring_open = None # accumulating /-- ... -/ lines + self.last_docstring = "" + + def feed(self, raw: str) -> str: + s = raw + if self.docstring_open is not None: + if "-/" not in s: + self.docstring_open.append(raw) + return "" + before, s = s.split("-/", 1) + self.docstring_open.append(before) + self.last_docstring = "\n".join(self.docstring_open).strip() + self.docstring_open = None + if self.comment_depth > 0: + s, self.comment_depth = consume_block_comment(s, self.comment_depth) + if self.comment_depth > 0: + return "" + + out = [] + j = 0 + while j < len(s): + if s[j : j + 2] == "--": + break + if s[j : j + 3] == "/--": + end = s.find("-/", j + 3) + if end == -1: + self.docstring_open = [s[j + 3 :]] + break + self.last_docstring = s[j + 3 : end].strip() + j = end + 2 + continue + if s[j : j + 2] == "/-": + rest, self.comment_depth = consume_block_comment(s[j + 2 :], 1) + if self.comment_depth > 0: + break + s = rest + j = 0 + continue + out.append(s[j]) + j += 1 + return "".join(out) + + +def clean_lines(text: str): + """Return (code_lines, docstring_before_line) for a Lean source text.""" + cleaner = LineCleaner() + code_lines, doc_map = [], [] + for raw in text.split("\n"): + doc_map.append(cleaner.last_docstring) + code_lines.append(cleaner.feed(raw)) + return code_lines, doc_map + + +def capture_statement(code_lines: list, start: int) -> str: + """Capture a declaration's signature from `code_lines[start]` up to + (excluding) the first `:=` at bracket depth 0. Note: `let x := e` inside a + statement type will truncate the capture early — acceptable, the capture is + for display only and the readme links to the full source.""" + captured, depth = [], 0 + for code in code_lines[start : start + 80]: + i = 0 + while i < len(code): + ch = code[i] + if ch in OPEN_BRACKETS: + depth += 1 + elif ch in CLOSE_BRACKETS: + depth -= 1 + elif ch == ":" and depth == 0 and code[i : i + 2] == ":=": + captured.append(code[:i].rstrip()) + return "\n".join(c for c in captured if c.strip()).rstrip() + i += 1 + captured.append(code.rstrip()) + return "\n".join(c for c in captured if c.strip()).rstrip() + + +def capture_decl_text(code_lines: list, start: int) -> str: + """Full text of a top-level declaration: from its first line until the next + column-0 code line (or EOF).""" + chunk = [code_lines[start]] + for code in code_lines[start + 1 :]: + if code and not code[0].isspace(): + break + chunk.append(code) + return "\n".join(chunk) + + +def parse_attr_list(attr_text: str) -> list: + """Split the inside of an @[...] block on top-level commas.""" + parts, buf, depth = [], [], 0 + for ch in attr_text: + if ch in OPEN_BRACKETS: + depth += 1 + elif ch in CLOSE_BRACKETS: + depth -= 1 + if ch == "," and depth == 0: + parts.append("".join(buf).strip()) + buf = [] + else: + buf.append(ch) + if buf: + parts.append("".join(buf).strip()) + return parts + + +def extract_binder_names(text: str) -> list: + """Names bound by a `variable ...` declaration: for each top-level binder + group, the identifiers before its `:`. Groups with no `:` (anonymous + instance binders like `[Fintype V]`) bind no names.""" + text = re.sub(r"^\s*variables?\b", "", text.strip()) + names, depth, buf = [], 0, None + for ch in text: + if ch in OPEN_BRACKETS: + depth += 1 + if depth == 1: + buf = [] + continue + elif ch in CLOSE_BRACKETS: + depth -= 1 + if depth == 0: + buf = None + continue + if depth == 1 and buf is not None: + if ch == ":": + names += "".join(buf).split() + buf = None + else: + buf.append(ch) + return [n for n in names if re.fullmatch(r"[^\W\d][\w']*", n)] + + +def find_tainted_defs(code_lines: list) -> set: + """Names of same-file `def`/`abbrev` declarations whose body contains + `answer(` or `sorry` — statements referencing them are fill-in-the-answer + style (their elaborated type embeds a placeholder).""" + tainted = set() + for idx, code in enumerate(code_lines): + stripped = code.strip() + m = DEF_RE.match(stripped) + if not m: + continue + body = capture_decl_text(code_lines, idx) + if re.search(r"\banswer\(|\bsorry\b", body): + tainted.add(split_name(m.group(1))[-1]) + return tainted + + +def parse_lean_file(path: Path, submodule: Path) -> list: + """Extract categorized theorem declarations from one Lean source file.""" + rel = path.relative_to(submodule) + module_components = list(rel.with_suffix("").parts) + source_file = str(rel) + text = path.read_text(encoding="utf-8") + code_lines, doc_map = clean_lines(text) + tainted = find_tainted_defs(code_lines) + + decls = [] + scope = [] # ("ns", [components]) | ("sec", None) + var_stack = [[]] # variable names bound per scope frame + pending_attrs = [] # accumulated @[...] attribute strings + pending_doc = "" + attr_buf = None # multi-line @[...] accumulator + + for idx, code_raw in enumerate(code_lines): + code = code_raw.strip() + if not code: + continue + + if attr_buf is not None: + attr_buf.append(code) + joined = " ".join(attr_buf) + if joined.count("[") == joined.count("]"): + pending_attrs.append(joined) + attr_buf = None + continue + if code.startswith("@["): + pending_doc = doc_map[idx] + if code.count("[") == code.count("]"): + pending_attrs.append(code) + after = code[code.rindex("]") + 1 :].strip() + if not after: + continue + code = after # attribute and declaration on one line + else: + attr_buf = [code] + continue + + m = NAMESPACE_RE.match(code) + if m: + scope.append(("ns", split_name(m.group(1)))) + var_stack.append([]) + pending_attrs = [] + continue + if SECTION_RE.match(code): + scope.append(("sec", None)) + var_stack.append([]) + pending_attrs = [] + continue + if END_RE.match(code): + if scope: + scope.pop() + if len(var_stack) > 1: + var_stack.pop() + pending_attrs = [] + continue + if VARIABLE_RE.match(code): + var_stack[-1].extend( + extract_binder_names(capture_decl_text(code_lines, idx))) + pending_attrs = [] + continue + + m = DECL_RE.match(code) + if m: + category, subjects, attr_display = None, [], [] + for attr in pending_attrs: + inner = attr.strip() + if inner.startswith("@[") and inner.endswith("]"): + inner = inner[2:-1] + for part in parse_attr_list(inner): + cm = re.match(r"category\s+(research\s+(?:open|solved)|test|API|textbook)", part) + if cm: + category = re.sub(r"\s+", " ", cm.group(1)) + attr_display.append(part) + am = re.match(r"AMS((?:\s+\d+)+)$", part) + if am: + subjects = am.group(1).split() + attr_display.append(part) + if category is not None: + ns_components = [c for kind, comps in scope if kind == "ns" for c in comps] + name_components = ns_components + split_name(m.group(1)) + if is_internal(name_components): + pending_attrs = [] + continue + statement_body = capture_statement(code_lines, idx) + decl_text = capture_decl_text(code_lines, idx) + taint = any( + re.search(rf"(? list: + decls = [] + for lean_file in sorted((submodule / "FormalConjectures").rglob("*.lean")): + decls.extend(parse_lean_file(lean_file, submodule)) + return decls + + +# -------------------------------------------------------------------------- +# Generation +# -------------------------------------------------------------------------- + +def answer_iff_question(decl: Decl): + """Textual `Q` for fill-in-the-answer statements of the exact rescuable + shape `theorem : answer(sorry) ↔ Q` — binder-free, exactly one + `answer()`/`sorry`, and no same-file sorry-def references. None otherwise. + + This gate is presentation-side only; the trusted checker independently + verifies the compiled statement has the `True ↔ Q` placeholder shape and + fails closed (0.0) on anything it cannot positively verify. + + Statements referencing section `variable`s are not rescuable: the compiled + type gains leading ∀ binders (`∀ vars, True ↔ Q`), which both breaks the + top-level-iff shape and makes prove-or-disprove semantically ambiguous + (the answer could differ per instantiation). Validate any change here with + _generator/shape_check.sh, which checks every generated prove-or-disprove + target's compiled type in the eval image. + """ + if decl.answer_taint or decl.uses_section_vars: + return None + if decl.statement.count("answer(") != 1: + return None + if len(re.findall(r"\bsorry\b", decl.statement)) != 1: + return None + m = ANSWER_IFF_RE.search(decl.statement) + if not m: + return None + return m.group(1).strip() + + +def generate(decls: list, out: Path, ref: str, lean_version: str, + categories: set, only: str) -> None: + generated, skipped_answer, by_category = [], [], {} + n_pod = 0 + seen_dirs = set() + + for decl in sorted(decls, key=lambda d: (d.source_file, d.full_name)): + if only: + if decl.full_name != only: + continue + elif decl.category not in categories: + continue + + question = None + if decl.skip_answer_style: + question = answer_iff_question(decl) + if question is None: + skipped_answer.append(decl.full_name) + continue + + source = snake(decl.module_components[1]) if len(decl.module_components) > 1 else "misc" + dir_name = ".".join(sanitize(c) for c in decl.full_name_components) + problem_dir = out / source / dir_name + + if str(problem_dir) in seen_dirs: + print(f"WARNING: duplicate problem dir {problem_dir}, skipping {decl.full_name}", + file=sys.stderr) + continue + seen_dirs.add(str(problem_dir)) + + module_dotted = ".".join( + c if re.fullmatch(r"[A-Za-z_][A-Za-z0-9_']*", c) else f"«{c}»" + for c in decl.module_components + ) + namespace_note = "" + if len(decl.full_name_components) > 1: + ns_prefix = decl.full_name_components[0] + namespace_note = ( + f"\nThe statement lives in namespace `{ns_prefix}` " + f"(fully-qualified name: `{decl.full_name}`); " + f"`open {ns_prefix} in` may be convenient.\n" + ) + + docstring_section = f"\n{decl.docstring}\n" if decl.docstring else "" + + problem_dir.mkdir(parents=True, exist_ok=True) + (problem_dir / "config.yaml").write_text( + CONFIG_YAML.format(ref=ref, image=IMAGE), encoding="utf-8") + (problem_dir / "evaluate.sh").write_text(EVALUATE_SH, encoding="utf-8") + (problem_dir / "check.sh").write_text( + CHECK_SH.replace("@IMAGE_REF@", f"{IMAGE}:{ref}"), encoding="utf-8") + (problem_dir / "evaluator.py").write_text(EVALUATOR_PY, encoding="utf-8") + target = { + "module": decl.module_components, + "theorem": decl.full_name_components, + "category": decl.category, + "subjects": decl.subjects, + "source_file": decl.source_file, + "ref": ref, + } + if question is not None: + target["mode"] = "prove_or_disprove" + (problem_dir / "target.json").write_text( + json.dumps(target, indent=2) + "\n", encoding="utf-8", + ) + readme_kwargs = dict( + theorem=decl.full_name, + upstream=UPSTREAM, + ref=ref, + source_file=decl.source_file, + category=decl.category, + subjects=", ".join(decl.subjects) or "-", + statement=decl.statement, + docstring_section=docstring_section, + namespace_note=namespace_note, + module_dotted=module_dotted, + lean_version=lean_version, + image_ref=f"{IMAGE}:{ref}", + ) + if question is None: + readme = README.format(**readme_kwargs) + else: + readme = README_POD.format(question=question, **readme_kwargs) + n_pod += 1 + (problem_dir / "readme").write_text(readme, encoding="utf-8") + (problem_dir / "evaluate.sh").chmod(0o755) + (problem_dir / "check.sh").chmod(0o755) + + generated.append(decl.full_name) + by_category[decl.category] = by_category.get(decl.category, 0) + 1 + + print(f"generated {len(generated)} problems into {out} " + f"({len(generated) - n_pod} prove, {n_pod} prove-or-disprove)") + for cat, n in sorted(by_category.items()): + print(f" {cat}: {n}") + print(f"skipped {len(skipped_answer)} answer-style statements with no sound " + "check mode (value-style, ambiguous shape, or sorry-def taint)") + + +def check_against(decls: list, extractor_json: Path, categories: set) -> int: + """Diff the parser's output against `lake exe extract_names` ground truth. + + Pass criteria: + - the (name, category) sets agree, except for warned anonymous instances + that appear only on the extractor side; + - every statement whose *elaborated type* contains sorry per the + extractor is also skipped by the parser (the parser intentionally + skips MORE: `answer(sorry)` Props elaborate to a `True` placeholder + that the extractor cannot distinguish from a real statement). + """ + data = json.loads(extractor_json.read_text(encoding="utf-8")) + entries = data["problems"] if isinstance(data, dict) else data + + def norm(name: str) -> str: + return ".".join(split_name(name)) + + truth = {norm(e["theorem"]): e["category"] for e in entries + if e["category"] in categories} + mine = {d.full_name: d.category for d in decls if d.category in categories} + + missing = sorted(set(truth) - set(mine)) + extra = sorted(set(mine) - set(truth)) + miscat = sorted(n for n in set(truth) & set(mine) if truth[n] != mine[n]) + + print(f"extractor: {len(truth)} parser: {len(mine)}") + for label, names in [("MISSING (in extractor, not parsed)", missing), + ("EXTRA (parsed, not in extractor)", extra), + ("CATEGORY MISMATCH", miscat)]: + print(f"{label}: {len(names)}") + for n in names[:20]: + print(f" - {n}") + + truth_sorry = {norm(e["theorem"]) for e in entries + if e["category"] in categories + and re.search(r"\bsorry(Ax)?\b", e.get("statement", ""))} + mine_sorry = {d.full_name for d in decls + if d.category in categories and d.skip_answer_style} + uncovered = sorted(truth_sorry - (mine_sorry | set(missing))) + print(f"type-contains-sorry (extractor): {len(truth_sorry)} " + f"answer-style skipped (parser): {len(mine_sorry)}") + print(f"UNCOVERED type-sorry statements (would become broken problems): " + f"{len(uncovered)} {uncovered[:10]}") + + instance_only_missing = all("inst" in n.split(".")[-1] for n in missing) + ok = (not extra and not miscat and not uncovered + and (not missing or instance_only_missing)) + print("CHECK:", "OK" if ok else "FAILED") + return 0 if ok else 1 + + +def generation_stamp(submodule_head: str) -> str: + """Stamp identifying what generated dirs were produced from. Must stay in + sync with the reimplementation in src/frontier_cs/lazy_problems.py.""" + ghash = hashlib.sha256(Path(__file__).read_bytes()).hexdigest()[:16] + return f"{submodule_head}+{ghash}" + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path, default=PROBLEMS_ROOT, + help="Problems root to generate into") + parser.add_argument("--ref", default=None, + help="formal-conjectures ref (default: submodule tag)") + parser.add_argument("--categories", default=",".join(DEFAULT_CATEGORIES), + help="Comma-separated categories to include") + parser.add_argument("--only", default=None, + help="Generate only this fully-qualified theorem (any category)") + parser.add_argument("--wipe", action="store_true", + help="Remove previously generated source dirs first") + parser.add_argument("--check-against", type=Path, default=None, + help="Diff parser output against extract_names JSON and exit") + args = parser.parse_args() + + if not (SUBMODULE / "FormalConjectures").is_dir(): + print("ERROR: submodule not initialized. Run: git submodule update --init", + file=sys.stderr) + return 1 + + decls = parse_all(SUBMODULE) + categories = {c.strip() for c in args.categories.split(",")} + + if args.check_against: + return check_against(decls, args.check_against, categories) + + if args.ref: + ref = args.ref + else: + ref = subprocess.run( + ["git", "-C", str(SUBMODULE), "describe", "--tags", "--exact-match"], + capture_output=True, text=True, check=True, + ).stdout.strip() + lean_version = (SUBMODULE / "lean-toolchain").read_text().strip().split(":")[-1] + + if args.wipe and not args.only: + for child in args.out.iterdir(): + if child.is_dir() and child.name not in ("common", "docker", "_generator"): + shutil.rmtree(child) + + generate(decls, args.out, ref, lean_version, categories, args.only) + + # Stamp submodule commit + generator hash so the framework's lazy + # materialization (src/frontier_cs/lazy_problems.py) regenerates when + # either the sources or the templates change. + if not args.only and args.out == PROBLEMS_ROOT: + head = subprocess.run( + ["git", "-C", str(SUBMODULE), "rev-parse", "HEAD"], + capture_output=True, text=True, + ) + if head.returncode == 0: + (GENERATOR_DIR / ".generated-ref").write_text( + generation_stamp(head.stdout.strip()) + "\n", encoding="utf-8") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/research/problems/formal_conjectures/_generator/shape_check.sh b/research/problems/formal_conjectures/_generator/shape_check.sh new file mode 100755 index 000000000..46617c975 --- /dev/null +++ b/research/problems/formal_conjectures/_generator/shape_check.sh @@ -0,0 +1,30 @@ +#!/usr/bin/env bash +# Validate every generated prove-or-disprove problem: its compiled statement +# must be exactly `True ↔ Q` (see ShapeCheck.lean). Requires docker and the +# prebuilt eval image. Run after (re)generation, especially on submodule bumps. +set -euo pipefail +SCRIPT_DIR=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd) +FC_ROOT=$(cd "$SCRIPT_DIR/.." && pwd) + +FIRST_CFG=$(find "$FC_ROOT" -mindepth 3 -maxdepth 3 -name config.yaml -print -quit) +if [ -z "$FIRST_CFG" ]; then + echo "no generated problems found (run generate.py first)" >&2 + exit 1 +fi +IMAGE=$(awk '/image:/ {print $2; exit}' "$FIRST_CFG") + +TMP=$(mktemp -d) +trap 'rm -rf "$TMP"' EXIT +python3 - "$FC_ROOT" > "$TMP/targets.txt" <<'EOF' +import json, pathlib, sys +root = pathlib.Path(sys.argv[1]) +for tj in sorted(root.glob("*/*/target.json")): + t = json.loads(tj.read_text(encoding="utf-8")) + if t.get("mode") == "prove_or_disprove": + print(" ".join(t["module"]) + " / " + " ".join(t["theorem"])) +EOF +echo "checking $(wc -l < "$TMP/targets.txt") prove-or-disprove targets against $IMAGE" +cp "$SCRIPT_DIR/ShapeCheck.lean" "$TMP/" +chmod -R a+rX "$TMP" +docker run --rm -v "$TMP":/sc:ro "$IMAGE" \ + bash -c 'cd /opt/formal-conjectures && lake env lean --root /sc --run /sc/ShapeCheck.lean /sc/targets.txt' diff --git a/research/problems/formal_conjectures/common/CheckDriver.lean b/research/problems/formal_conjectures/common/CheckDriver.lean new file mode 100644 index 000000000..8aa83bfb0 --- /dev/null +++ b/research/problems/formal_conjectures/common/CheckDriver.lean @@ -0,0 +1,104 @@ +/- +Trusted checker for formal_conjectures submissions. + +Run via `lake env lean --run CheckDriver.lean / [/ ]` from the formal-conjectures package root, with the +compiled submission (module `FCSolution`) on LEAN_PATH. + +This file only ever loads compiled .oleans via `importModules` — it never +elaborates submission *syntax*, so submission-defined macros/elaborators can +never influence the check. It verifies: + 1. the submission declares a constant `solution`, + 2. `solution` depends only on the standard axioms, and + 3. `solution`'s type matches the target, depending on : + - "prove" (default): definitionally equal to the target conjecture's + statement (the statement constant exists in the target module even + when its proof is `sorry`); + - "prove_or_disprove": the target is a fill-in-the-answer statement + whose `answer(sorry)` elaborated to a `True` placeholder, so its + compiled type must be literally `True ↔ Q`; the submission is accepted + iff `solution`'s type is definitionally equal to `Q` or to `¬Q`. + +Fail-closed: any shape the checker cannot positively verify (unexpected mode, +target not of the form `True ↔ Q`, type matching neither side) is an error, +which the evaluator scores 0.0. + +Prints FC_CHECK_OK and exits 0 iff the submission is accepted. +-/ +import Lean + +open Lean + +def allowedAxioms : List Name := [`propext, `Classical.choice, `Quot.sound] + +def mkNameFromComponents (cs : List String) : Name := + cs.foldl .str .anonymous + +def fail (msg : String) : IO UInt32 := do + IO.eprintln s!"[driver] {msg}" + return 1 + +def check (targetName : Name) (mode : String) : CoreM (Except String Unit) := do + let env ← getEnv + let some target := env.find? targetName + | return .error s!"target theorem {targetName} not found" + let some sol := env.find? `solution + | return .error "submission must declare a top-level `theorem solution : `" + if target.type.hasSorry then + return .error s!"target statement {targetName} contains sorry; problem is not checkable" + + -- Axiom audit: catches sorryAx, native_decide (ofReduceBool), custom axioms. + let axioms ← collectAxioms `solution + for ax in axioms do + unless allowedAxioms.contains ax do + return .error s!"solution depends on forbidden axiom: {ax}" + + unless target.levelParams.length == sol.levelParams.length do + return .error "universe parameter count differs from the conjecture statement" + let solType := sol.type.instantiateLevelParams sol.levelParams + (target.levelParams.map Level.param) + + match mode with + | "prove" => + -- `solution`'s type must be defeq to the conjecture's statement. + let ok ← Meta.MetaM.run' (Meta.isDefEq target.type solType) + unless ok do + return .error + s!"the type of `solution` does not match the statement of {targetName}" + return .ok () + | "prove_or_disprove" => + -- Target must have the exact placeholder shape `True ↔ Q` (no reduction: + -- anything else fails closed). Accept a proof of `Q` or of `¬Q`. + unless target.type.isAppOfArity `Iff 2 do + return .error s!"target {targetName} is not a top-level iff; not checkable" + let lhs := target.type.appFn!.appArg! + let q := target.type.appArg! + unless lhs.isConstOf `True do + return .error s!"target {targetName} placeholder is not `True`; not checkable" + if ← Meta.MetaM.run' (Meta.isDefEq q solType) then + return .ok () + if ← Meta.MetaM.run' (Meta.isDefEq (mkApp (mkConst `Not) q) solType) then + return .ok () + return .error + s!"the type of `solution` proves neither the question of {targetName} nor its negation" + | _ => return .error s!"unknown check mode: {mode}" + +def main (args : List String) : IO UInt32 := do + let (modComponents, rest) := args.span (· != "/") + let (thmComponents, rest2) := (rest.drop 1).span (· != "/") + let mode := (rest2.drop 1).headD "prove" + if modComponents.isEmpty || thmComponents.isEmpty then + return ← fail "usage: CheckDriver / [/ ]" + let targetMod := mkNameFromComponents modComponents + let targetName := mkNameFromComponents thmComponents + + initSearchPath (← findSysroot) + let env ← importModules #[{ module := targetMod }, { module := `FCSolution }] {} + + let coreCtx : Core.Context := { fileName := "", fileMap := default } + let (result, _) ← (check targetName mode).toIO coreCtx { env := env } + match result with + | .error msg => return ← fail msg + | .ok () => + IO.println "FC_CHECK_OK" + return 0 diff --git a/research/problems/formal_conjectures/common/fc_evaluator.py b/research/problems/formal_conjectures/common/fc_evaluator.py new file mode 100644 index 000000000..c6809b093 --- /dev/null +++ b/research/problems/formal_conjectures/common/fc_evaluator.py @@ -0,0 +1,146 @@ +""" +Shared evaluator for formal_conjectures problems. + +A submission is a single `solution.lean` file that must declare a top-level + + theorem solution : := + +The evaluator: + 1. Lints the source for constructs that could subvert checking. + 2. Compiles it against the prebuilt formal-conjectures + Mathlib package + baked into the Docker image at /opt/formal-conjectures. + 3. Runs the trusted CheckDriver.lean, which loads only compiled .oleans + (never elaborating submission syntax) and verifies that: + - `solution`'s type is definitionally equal to the conjecture's + statement (mode "prove", the default) — or, for fill-in-the-answer + problems (target.json mode "prove_or_disprove", statement compiled + as `True ↔ Q`), to `Q` or `¬Q`, and + - `solution` depends only on the standard axioms + (propext, Classical.choice, Quot.sound). + The driver fails closed: anything it cannot positively verify scores 0.0. + +Score contract (parsed by the framework from the last stdout line): + 1.0 proof accepted + 0.0 rejected (compile error / sorry / wrong statement / forbidden axiom) +An exception with no score line signals an infrastructure error. +""" + +import argparse +import json +import os +import re +import shlex +import subprocess +import sys +import tempfile +from pathlib import Path + +FC_ROOT = Path(os.environ.get("FC_ROOT", "/opt/formal-conjectures")) + +# Rejected outright. The trusted driver makes most of these unexploitable +# anyway (it never elaborates submission syntax); this is defense in depth, +# and none are needed for an honest proof. +FORBIDDEN_PATTERNS = [ + (r"\baxiom\b", "axiom declarations are not allowed"), + (r"\bsorryAx\b", "direct use of sorryAx is not allowed"), + (r"\bmacro\b|\bmacro_rules\b", "macro definitions are not allowed"), + (r"\belab\b|\belab_rules\b", "elaborator definitions are not allowed"), + (r"\bsyntax\b", "syntax definitions are not allowed"), + (r"\bnotation\b", "notation definitions are not allowed"), + (r"\binitialize\b", "initializers are not allowed"), + (r"\brun_cmd\b|\brun_elab\b", "compile-time command execution is not allowed"), + (r"\bimplemented_by\b|\bextern\b", "native overrides are not allowed"), + (r"\bnative_decide\b|\bofReduceBool\b|\bofReduceNat\b", + "native_decide and native reduction axioms are not allowed"), + (r"\bunsafe\b", "unsafe definitions are not allowed"), + (r"set_option\s+debug\.", "debug options are not allowed"), +] + + +def reject(reason: str, detail: str = "") -> None: + """Print diagnostics to stderr and the 0.0 score to stdout, then exit.""" + print(f"[fc] rejected: {reason}", file=sys.stderr) + if detail: + print(detail[-4000:], file=sys.stderr) + print("0.0") + sys.exit(0) + + +def run(cmd: list, cwd: Path) -> subprocess.CompletedProcess: + return subprocess.run(cmd, cwd=cwd, capture_output=True, text=True) + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--solution-path", required=True) + parser.add_argument("--target", required=True, help="Path to target.json") + args = parser.parse_args() + + target = json.loads(Path(args.target).read_text(encoding="utf-8")) + module = target["module"] # list of module name components + theorem = target["theorem"] # list of declaration name components + # "prove": solution's type must match the statement. "prove_or_disprove": + # fill-in-the-answer statement `answer(sorry) ↔ Q`; solution must prove Q + # or ¬Q. The trusted driver fails closed on anything else. + mode = target.get("mode", "prove") + + # Infrastructure sanity: the image must match the ref the problem was + # generated from, else statements could silently differ. Raise (no score + # line) so the framework reports ERROR instead of a misleading 0.0. + expected_ref = target.get("ref") + actual_ref = os.environ.get("FC_REF", "") + if not actual_ref: + proc = run(["git", "describe", "--tags", "--always"], cwd=FC_ROOT) + actual_ref = proc.stdout.strip() + if expected_ref and actual_ref and expected_ref != actual_ref: + raise RuntimeError( + f"image formal-conjectures ref {actual_ref!r} does not match " + f"problem ref {expected_ref!r}; rebuild the eval image" + ) + + solution_path = Path(args.solution_path) + if not solution_path.exists(): + raise FileNotFoundError(f"solution not found: {solution_path}") + src = solution_path.read_text(encoding="utf-8") + + for pattern, reason in FORBIDDEN_PATTERNS: + if re.search(pattern, src): + reject(reason) + + tmp = Path(tempfile.mkdtemp(prefix="fcsol_")) + (tmp / "FCSolution.lean").write_text(src, encoding="utf-8") + + print("[fc] compiling solution...", file=sys.stderr) + proc = run( + ["lake", "env", "lean", + "--root", str(tmp), + "-o", str(tmp / "FCSolution.olean"), + str(tmp / "FCSolution.lean")], + cwd=FC_ROOT, + ) + output = proc.stdout + "\n" + proc.stderr + if proc.returncode != 0: + reject("solution failed to compile", output) + if "declaration uses 'sorry'" in output: + reject("solution uses sorry", output) + + print("[fc] running trusted checker...", file=sys.stderr) + driver = Path(__file__).resolve().parent / "CheckDriver.lean" + driver_args = " ".join( + shlex.quote(c) for c in [*module, "/", *theorem, "/", mode]) + proc = run( + ["lake", "env", "bash", "-c", + f'export LEAN_PATH="$LEAN_PATH:{tmp}"; ' + f"exec lean --root {shlex.quote(str(driver.parent))} " + f"--run {shlex.quote(str(driver))} {driver_args}"], + cwd=FC_ROOT, + ) + if proc.returncode != 0 or "FC_CHECK_OK" not in proc.stdout: + reject("proof check failed", proc.stdout + "\n" + proc.stderr) + + print("[fc] proof accepted", file=sys.stderr) + print("1.0") + + +if __name__ == "__main__": + main() diff --git a/research/problems/formal_conjectures/docker/Dockerfile b/research/problems/formal_conjectures/docker/Dockerfile new file mode 100644 index 000000000..d18af24d8 --- /dev/null +++ b/research/problems/formal_conjectures/docker/Dockerfile @@ -0,0 +1,37 @@ +# Evaluation image for formal_conjectures problems. +# +# Contains Lean 4 (pinned by the formal-conjectures lean-toolchain), a fully +# built checkout of google-deepmind/formal-conjectures (including Mathlib via +# `lake exe cache get`), and python3 for the evaluator orchestrator. +# +# FC_REF must match the tag the third_party/formal-conjectures submodule is +# pinned to — build via build.sh, which derives it from the submodule. +FROM ubuntu:24.04 + +RUN apt-get update && apt-get install -y --no-install-recommends \ + git curl ca-certificates bash python3 \ + && rm -rf /var/lib/apt/lists/* + +RUN curl -sSf https://elan.lean-lang.org/elan-init.sh | sh -s -- -y --default-toolchain none +ENV PATH="/root/.elan/bin:${PATH}" + +ARG FC_REF=bench-v1-lean4.27.0 +RUN git clone --depth 1 --branch ${FC_REF} \ + https://github.com/google-deepmind/formal-conjectures /opt/formal-conjectures + +WORKDIR /opt/formal-conjectures + +# Mathlib olean cache, then compile the conjecture statements themselves. +# (lake 5.x has no jobs flag; parallelism follows available cores.) +RUN lake exe cache get +RUN lake build +# The upstream extractor exe, used once to generate the problem manifest. +RUN lake build extract_names + +# Smoke test: a trivial standalone theorem compiles against the built package. +RUN echo 'theorem solution : True := trivial' > /tmp/smoke.lean \ + && lake env lean /tmp/smoke.lean \ + && rm /tmp/smoke.lean + +# Stamp the pinned ref so the evaluator can verify image/problem consistency. +ENV FC_REF=${FC_REF} diff --git a/research/problems/formal_conjectures/docker/build.sh b/research/problems/formal_conjectures/docker/build.sh new file mode 100755 index 000000000..2fd815ea8 --- /dev/null +++ b/research/problems/formal_conjectures/docker/build.sh @@ -0,0 +1,27 @@ +#!/usr/bin/env bash +# Build (and optionally push) the formal_conjectures evaluation image. +# +# The image tag is derived from the third_party/formal-conjectures submodule +# pin so the image and the generated problems can never drift apart silently. +# +# Usage: ./build.sh [--push] +set -euo pipefail + +SCRIPT_DIR=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd) +REPO_ROOT=$(cd "$SCRIPT_DIR/../../../.." && pwd) +SUBMODULE="$REPO_ROOT/third_party/formal-conjectures" + +if [ ! -f "$SUBMODULE/lean-toolchain" ]; then + echo "ERROR: submodule not initialized. Run: git submodule update --init" >&2 + exit 1 +fi + +FC_REF=$(git -C "$SUBMODULE" describe --tags --exact-match) +IMAGE="${IMAGE:-shangyint/formal-conjectures-eval}" + +echo "Building $IMAGE:$FC_REF (formal-conjectures @ $FC_REF)" +docker build --build-arg "FC_REF=$FC_REF" -t "$IMAGE:$FC_REF" "$SCRIPT_DIR" + +if [ "${1:-}" = "--push" ]; then + docker push "$IMAGE:$FC_REF" +fi diff --git a/research/scripts/check_solutions.py b/research/scripts/check_solutions.py index e9f5aeeb1..fbc782acc 100755 --- a/research/scripts/check_solutions.py +++ b/research/scripts/check_solutions.py @@ -112,7 +112,9 @@ def info(text: str) -> str: # Directories to exclude when auto-discovering problems -EXCLUDE_DIRS = {"common", "resources", "__pycache__", ".venv"} +# formal_conjectures problems are auto-generated Lean proof tasks with no +# expected LLM solutions; keep them out of the solutions matrix and problems.txt. +EXCLUDE_DIRS = {"common", "resources", "__pycache__", ".venv", "formal_conjectures"} def discover_problems(problems_dir: Path) -> List[Tuple[str, Path]]: diff --git a/scripts/detect_changed_problems.py b/scripts/detect_changed_problems.py index 67659be15..afc1e298a 100644 --- a/scripts/detect_changed_problems.py +++ b/scripts/detect_changed_problems.py @@ -75,6 +75,13 @@ def detect_changed_problems(track: str, base_ref: str = "origin/main") -> list[s is_problem = (problem_dir / "evaluator.py").exists() if is_problem: + # Problem families marked with a `.skip-validation` file (in the + # problem dir or any ancestor) are excluded from CI validation. + # Used by research/problems/formal_conjectures/: open conjectures + # cannot have a reference solution scoring > 0 by design. + ancestors = [Path(prefix + "/".join(parts[:j])) for j in range(i + 1)] + if any((d / ".skip-validation").exists() for d in ancestors): + break problems.add(candidate) break diff --git a/scripts/update_problem_count.py b/scripts/update_problem_count.py index 18ea9d50b..bb7f2b78e 100644 --- a/scripts/update_problem_count.py +++ b/scripts/update_problem_count.py @@ -17,10 +17,11 @@ def count_research_problems(research_dir: Path) -> int: if poc_dir.exists(): count += 4 - # Count all evaluator.py files, excluding those in poc_generation + # Count all evaluator.py files, excluding those in poc_generation and + # formal_conjectures (auto-generated Lean problems, counted separately) for evaluator_file in research_dir.rglob('evaluator.py'): # Skip if it's under poc_generation directory - if 'poc_generation' not in str(evaluator_file): + if 'poc_generation' not in str(evaluator_file) and 'formal_conjectures' not in str(evaluator_file): count += 1 return count diff --git a/scripts/validate_problems.py b/scripts/validate_problems.py index 1c4921d54..9faacdeab 100644 --- a/scripts/validate_problems.py +++ b/scripts/validate_problems.py @@ -90,6 +90,16 @@ def validate_problem( print(f"Validating: {problem_id}") print("=" * 60) + # Problem families marked with `.skip-validation` (e.g. formal_conjectures) + # have no reference solution by design; treat as passing without running. + problem_dir = Path(f"{track}/problems/{problem_id}") + for d in [problem_dir, *problem_dir.parents]: + if (d / ".skip-validation").exists(): + print(" SKIP: .skip-validation marker (no reference solution by design)") + return True + if d == Path(f"{track}/problems"): + break + # Find reference solution ref_path = find_reference_solution(track, problem_id) if ref_path is None: diff --git a/src/frontier_cs/config.py b/src/frontier_cs/config.py index f4825d8f0..115d060f0 100644 --- a/src/frontier_cs/config.py +++ b/src/frontier_cs/config.py @@ -218,6 +218,11 @@ class LanguageConfig: extension="rs", code_block_tag="rust", ), + "lean": LanguageConfig( + name="lean", + extension="lean", + code_block_tag="lean", + ), } DEFAULT_LANGUAGE = "python" diff --git a/src/frontier_cs/lazy_problems.py b/src/frontier_cs/lazy_problems.py new file mode 100644 index 000000000..8ed3220f0 --- /dev/null +++ b/src/frontier_cs/lazy_problems.py @@ -0,0 +1,85 @@ +""" +Lazy materialization of generated problem directories. + +formal_conjectures problem dirs are generated from the +third_party/formal-conjectures submodule and are not committed (see +research/problems/formal_conjectures/.gitignore). This module regenerates them +transparently on first access: resolving a formal_conjectures problem id +(eval, show) or listing research problems triggers generation when the +directories are missing or were generated from a different submodule commit. +Afterwards everything is served directly from the files. +""" + +import hashlib +import subprocess +import sys +from pathlib import Path +from typing import Optional + +FC = "formal_conjectures" + +# problems_dirs verified current in this process; skip repeat git/stamp checks +_verified = set() + + +def _submodule_head(repo_root: Path) -> Optional[str]: + proc = subprocess.run( + ["git", "-C", str(repo_root / "third_party" / "formal-conjectures"), + "rev-parse", "HEAD"], + capture_output=True, text=True, + ) + return proc.stdout.strip() if proc.returncode == 0 else None + + +def ensure_formal_conjectures(problems_dir: Path, problem_id: Optional[str] = None) -> None: + """Generate formal_conjectures problem dirs if missing or stale. + + No-op when: this problems tree has no formal_conjectures generator, the + requested problem id is not a formal_conjectures one, or generation is + already up to date with the submodule commit and generator version + (stamped as "+" in + _generator/.generated-ref by the generator; must stay in sync with + generation_stamp() there). Failures are reported on stderr but never + raised — the caller then fails naturally with problem-not-found. + """ + if problems_dir in _verified: + return + if problem_id is not None and not str(problem_id).startswith(FC + "/"): + return + fc_root = problems_dir / FC + generator = fc_root / "_generator" / "generate.py" + if not generator.is_file(): + return + + repo_root = problems_dir.parents[1] + submodule = repo_root / "third_party" / "formal-conjectures" + if not (submodule / "FormalConjectures").is_dir(): + subprocess.run( + ["git", "submodule", "update", "--init", "third_party/formal-conjectures"], + cwd=repo_root, capture_output=True, + ) + if not (submodule / "FormalConjectures").is_dir(): + print(f"[{FC}] submodule not initialized and auto-init failed; " + "run: git submodule update --init", file=sys.stderr) + return + + head = _submodule_head(repo_root) + ghash = hashlib.sha256(generator.read_bytes()).hexdigest()[:16] + stamp_file = fc_root / "_generator" / ".generated-ref" + stamp = stamp_file.read_text(encoding="utf-8").strip() if stamp_file.is_file() else None + if head is not None and stamp == f"{head}+{ghash}": + _verified.add(problems_dir) + return # up to date; a missing problem id is genuinely unknown + + print(f"[{FC}] materializing problem directories from the submodule...", + file=sys.stderr) + proc = subprocess.run( + [sys.executable, str(generator), "--wipe"], + capture_output=True, text=True, + ) + if proc.returncode != 0: + print(f"[{FC}] generation failed:\n{proc.stderr}", file=sys.stderr) + return + summary = proc.stdout.splitlines()[0] if proc.stdout else "" + print(f"[{FC}] {summary}", file=sys.stderr) + _verified.add(problems_dir) diff --git a/src/frontier_cs/runner/base.py b/src/frontier_cs/runner/base.py index 8b0d4ea79..58fb98e13 100644 --- a/src/frontier_cs/runner/base.py +++ b/src/frontier_cs/runner/base.py @@ -128,7 +128,13 @@ def get_problem_path(self, problem_id: str) -> Path: With nested solution structure, problem_id is already the nested path (e.g., "cant_be_late/high_availability_loose_deadline_large_overhead"). + + formal_conjectures problems are generated from a submodule rather than + committed; materialize them on first access. """ + from ..lazy_problems import ensure_formal_conjectures + + ensure_formal_conjectures(self.problems_dir, problem_id) return self.problems_dir / problem_id def _get_problem_path_or_error( diff --git a/src/frontier_cs/single_evaluator.py b/src/frontier_cs/single_evaluator.py index 5bd7b0515..bf456156f 100644 --- a/src/frontier_cs/single_evaluator.py +++ b/src/frontier_cs/single_evaluator.py @@ -1,10 +1,10 @@ -""" -Unified evaluation API for Frontier-CS. - -Provides a single interface for evaluating both algorithmic and research problems, -with support for different backends (local Docker, SkyPilot cloud). -""" - +""" +Unified evaluation API for Frontier-CS. + +Provides a single interface for evaluating both algorithmic and research problems, +with support for different backends (local Docker, SkyPilot cloud). +""" + import atexit import signal from pathlib import Path @@ -14,67 +14,67 @@ from .runner.base import Runner from .runner.cluster_cleanup import ActiveClusterRegistry from .runner.research_skypilot import ResearchSkyPilotRunner - - + + TrackType = Literal["algorithmic", "research", "2.0"] BackendType = Literal["docker", "skypilot"] - - + + class SingleEvaluator: - """ - Unified evaluator for Frontier-CS problems. - - Example usage: + """ + Unified evaluator for Frontier-CS problems. + + Example usage: evaluator = SingleEvaluator() - - # Algorithmic problem (uses Docker by default) + + # Algorithmic problem (uses Docker by default) result = evaluator.evaluate("algorithmic", problem_id=1, code=cpp_code) - - # Research problem (uses SkyPilot by default) + + # Research problem (uses SkyPilot by default) result = evaluator.evaluate("research", problem_id="flash_attn", code=py_code) - - # Override backend + + # Override backend result = evaluator.evaluate("research", problem_id="flash_attn", code=py_code, backend="docker") - """ - + """ + def __init__( self, backend: Optional[BackendType] = None, base_dir: Optional[Path] = None, judge_url: str = "http://localhost:8081", - cloud: str = "gcp", - region: Optional[str] = None, - keep_cluster: bool = False, + cloud: str = "gcp", + region: Optional[str] = None, + keep_cluster: bool = False, idle_timeout: Optional[int] = 10, timeout: Optional[int] = None, register_cleanup: bool = True, ): - """ + """ Initialize SingleEvaluator. - - Args: - backend: Override default backend ("docker" or "skypilot"). - If None, auto-detects: research -> skypilot, algorithmic -> docker - base_dir: Base directory of Frontier-CS repo (auto-detected if None) - judge_url: URL of the algorithmic judge server - cloud: Cloud provider for SkyPilot ("gcp", "aws", "azure") - region: Cloud region for SkyPilot - keep_cluster: Keep SkyPilot cluster running after evaluation (disables autostop) - idle_timeout: Minutes of idleness before autostop (default: 10, None to disable) - timeout: Timeout per evaluation in seconds (default: None, uses runner default) - """ - self.default_backend = backend - self.base_dir = base_dir - self.judge_url = judge_url - self.cloud = cloud - self.region = region - self.keep_cluster = keep_cluster + + Args: + backend: Override default backend ("docker" or "skypilot"). + If None, auto-detects: research -> skypilot, algorithmic -> docker + base_dir: Base directory of Frontier-CS repo (auto-detected if None) + judge_url: URL of the algorithmic judge server + cloud: Cloud provider for SkyPilot ("gcp", "aws", "azure") + region: Cloud region for SkyPilot + keep_cluster: Keep SkyPilot cluster running after evaluation (disables autostop) + idle_timeout: Minutes of idleness before autostop (default: 10, None to disable) + timeout: Timeout per evaluation in seconds (default: None, uses runner default) + """ + self.default_backend = backend + self.base_dir = base_dir + self.judge_url = judge_url + self.cloud = cloud + self.region = region + self.keep_cluster = keep_cluster self.idle_timeout = idle_timeout self.timeout = timeout self._register_cleanup = register_cleanup - - # Lazy-initialized runners + + # Lazy-initialized runners self._algorithmic_runner: Optional[AlgorithmicLocalRunner] = None self._algorithmic_skypilot_runner: Optional[Runner] = None self._docker_runner: Optional[ResearchDockerRunner] = None @@ -110,52 +110,52 @@ def signal_handler(signum, frame): atexit.register(cleanup_on_exit) signal.signal(signal.SIGINT, signal_handler) - - @property + + @property def algorithmic_runner(self) -> AlgorithmicLocalRunner: - """Get or create the algorithmic runner.""" - if self._algorithmic_runner is None: + """Get or create the algorithmic runner.""" + if self._algorithmic_runner is None: self._algorithmic_runner = AlgorithmicLocalRunner( judge_url=self.judge_url, base_dir=self.base_dir, ) - return self._algorithmic_runner - - @property - def algorithmic_skypilot_runner(self) -> Runner: - """Get or create the algorithmic SkyPilot runner.""" - if self._algorithmic_skypilot_runner is None: - from .runner.algorithmic_skypilot import AlgorithmicSkyPilotRunner - self._algorithmic_skypilot_runner = AlgorithmicSkyPilotRunner( - base_dir=self.base_dir, - cloud=self.cloud, - region=self.region, - keep_cluster=self.keep_cluster, - idle_timeout=self.idle_timeout, - ) - return self._algorithmic_skypilot_runner - - @property + return self._algorithmic_runner + + @property + def algorithmic_skypilot_runner(self) -> Runner: + """Get or create the algorithmic SkyPilot runner.""" + if self._algorithmic_skypilot_runner is None: + from .runner.algorithmic_skypilot import AlgorithmicSkyPilotRunner + self._algorithmic_skypilot_runner = AlgorithmicSkyPilotRunner( + base_dir=self.base_dir, + cloud=self.cloud, + region=self.region, + keep_cluster=self.keep_cluster, + idle_timeout=self.idle_timeout, + ) + return self._algorithmic_skypilot_runner + + @property def docker_runner(self) -> ResearchDockerRunner: - """Get or create the Docker runner.""" - if self._docker_runner is None: + """Get or create the Docker runner.""" + if self._docker_runner is None: self._docker_runner = ResearchDockerRunner( base_dir=self.base_dir, timeout=self.timeout ) - return self._docker_runner - - @property + return self._docker_runner + + @property def skypilot_runner(self) -> Runner: """Get or create the SkyPilot runner.""" if self._skypilot_runner is None: from .runner.research_skypilot import ResearchSkyPilotRunner self._skypilot_runner = ResearchSkyPilotRunner( - base_dir=self.base_dir, - cloud=self.cloud, - region=self.region, - keep_cluster=self.keep_cluster, - idle_timeout=self.idle_timeout, - ) + base_dir=self.base_dir, + cloud=self.cloud, + region=self.region, + keep_cluster=self.keep_cluster, + idle_timeout=self.idle_timeout, + ) return self._skypilot_runner @property @@ -188,13 +188,13 @@ def benchmark20_skypilot_runner(self) -> Runner: return self._benchmark20_skypilot_runner def _get_runner(self, track: TrackType, backend: Optional[BackendType] = None) -> Runner: - """Get the appropriate runner for a track and backend.""" - # Priority: explicit backend > init backend > track default - if backend: - effective_backend = backend - elif self.default_backend: - effective_backend = self.default_backend - else: + """Get the appropriate runner for a track and backend.""" + # Priority: explicit backend > init backend > track default + if backend: + effective_backend = backend + elif self.default_backend: + effective_backend = self.default_backend + else: # Auto-detect: research -> skypilot, algorithmic/2.0 -> docker effective_backend = "skypilot" if track == "research" else "docker" @@ -211,84 +211,84 @@ def _get_runner(self, track: TrackType, backend: Optional[BackendType] = None) - if effective_backend == "skypilot": return self.skypilot_runner return self.docker_runner - - def evaluate( - self, - track: TrackType, - problem_id: Union[str, int], - code: str, - *, - backend: Optional[BackendType] = None, - ) -> EvaluationResult: - """ - Evaluate a solution for a single problem. - - Args: + + def evaluate( + self, + track: TrackType, + problem_id: Union[str, int], + code: str, + *, + backend: Optional[BackendType] = None, + ) -> EvaluationResult: + """ + Evaluate a solution for a single problem. + + Args: track: Problem track ("algorithmic", "research", or "2.0") problem_id: Problem identifier (int for algorithmic, str for research/2.0) code: Solution code (C++ for algorithmic, Python for research/2.0) - backend: Backend to use ("docker" or "skypilot"), defaults to init value - - Returns: - EvaluationResult with score and status - """ - runner = self._get_runner(track, backend) - return runner.evaluate(str(problem_id), code) - - def evaluate_file( - self, - track: TrackType, - problem_id: Union[str, int], - solution_path: Path, - *, - backend: Optional[BackendType] = None, - ) -> EvaluationResult: - """ - Evaluate a solution file for a single problem. - - Args: - track: Problem track - problem_id: Problem identifier - solution_path: Path to solution file - backend: Backend to use - - Returns: - EvaluationResult with score and status - """ - runner = self._get_runner(track, backend) - return runner.evaluate_file(str(problem_id), solution_path) - - def list_problems(self, track: TrackType) -> List[str]: - """ - List all available problems for a track. - - Args: - track: Problem track - - Returns: - List of problem identifiers - """ + backend: Backend to use ("docker" or "skypilot"), defaults to init value + + Returns: + EvaluationResult with score and status + """ + runner = self._get_runner(track, backend) + return runner.evaluate(str(problem_id), code) + + def evaluate_file( + self, + track: TrackType, + problem_id: Union[str, int], + solution_path: Path, + *, + backend: Optional[BackendType] = None, + ) -> EvaluationResult: + """ + Evaluate a solution file for a single problem. + + Args: + track: Problem track + problem_id: Problem identifier + solution_path: Path to solution file + backend: Backend to use + + Returns: + EvaluationResult with score and status + """ + runner = self._get_runner(track, backend) + return runner.evaluate_file(str(problem_id), solution_path) + + def list_problems(self, track: TrackType) -> List[str]: + """ + List all available problems for a track. + + Args: + track: Problem track + + Returns: + List of problem identifiers + """ if track == "algorithmic": # Read from local ./algorithmic/problems directory try: alg_base = self.docker_runner.base_dir / "algorithmic" / "problems" - except Exception: - return [] - - if not alg_base or not alg_base.exists(): - return [] - - problems = [] - for item in alg_base.iterdir(): - if item.is_dir() and not item.name.startswith("."): - problems.append(item.name) - - # Sort numerically if possible - def sort_key(name): - try: - return (0, int(name)) - except ValueError: - return (1, name) + except Exception: + return [] + + if not alg_base or not alg_base.exists(): + return [] + + problems = [] + for item in alg_base.iterdir(): + if item.is_dir() and not item.name.startswith("."): + problems.append(item.name) + + # Sort numerically if possible + def sort_key(name): + try: + return (0, int(name)) + except ValueError: + return (1, name) return sorted(problems, key=sort_key) @@ -304,57 +304,62 @@ def sort_key(name): # Research problems - count by evaluator.py files (matches update_problem_count.py logic) research_problems_dir = self.docker_runner.research_dir / "problems" - if not research_problems_dir.exists(): - return [] - - problems = [] - - # Special case: poc_generation has 4 subcategories - poc_dir = research_problems_dir / "poc_generation" - if poc_dir.exists(): - # List the 4 subcategories directly - problems.extend([ - "research/poc_generation/heap_buffer_overflow", - "research/poc_generation/heap_use_after_free", - "research/poc_generation/stack_buffer_overflow", - "research/poc_generation/uninitialized_value" - ]) - - # Find all evaluator.py files, excluding those in poc_generation - for evaluator_file in research_problems_dir.rglob("evaluator.py"): - # Skip if it's under poc_generation directory - if "poc_generation" not in str(evaluator_file): - # Get relative path from research_problems_dir - problem_path = evaluator_file.parent.relative_to(research_problems_dir) - problems.append("research/" + str(problem_path)) - - # Also include local algorithmic problems (from ./algorithmic/problems) - try: - alg_base = self.docker_runner.base_dir / "algorithmic" / "problems" - except Exception: - alg_base = None - - if alg_base and alg_base.exists(): - for item in sorted(alg_base.iterdir(), key=lambda p: p.name): - if item.is_dir() and not item.name.startswith("."): - problems.append(f"algorithmic/{item.name}") - - return sorted(problems) - - def get_problem_statement( - self, - track: TrackType, - problem_id: Union[str, int], - ) -> Optional[str]: - """ - Get the problem statement/readme for a problem. - - Args: - track: Problem track - problem_id: Problem identifier - - Returns: - Problem statement text, or None if not found + if not research_problems_dir.exists(): + return [] + + # formal_conjectures problems are generated from a submodule rather + # than committed; materialize them so they appear in the listing. + from .lazy_problems import ensure_formal_conjectures + ensure_formal_conjectures(research_problems_dir) + + problems = [] + + # Special case: poc_generation has 4 subcategories + poc_dir = research_problems_dir / "poc_generation" + if poc_dir.exists(): + # List the 4 subcategories directly + problems.extend([ + "research/poc_generation/heap_buffer_overflow", + "research/poc_generation/heap_use_after_free", + "research/poc_generation/stack_buffer_overflow", + "research/poc_generation/uninitialized_value" + ]) + + # Find all evaluator.py files, excluding those in poc_generation + for evaluator_file in research_problems_dir.rglob("evaluator.py"): + # Skip if it's under poc_generation directory + if "poc_generation" not in str(evaluator_file): + # Get relative path from research_problems_dir + problem_path = evaluator_file.parent.relative_to(research_problems_dir) + problems.append("research/" + str(problem_path)) + + # Also include local algorithmic problems (from ./algorithmic/problems) + try: + alg_base = self.docker_runner.base_dir / "algorithmic" / "problems" + except Exception: + alg_base = None + + if alg_base and alg_base.exists(): + for item in sorted(alg_base.iterdir(), key=lambda p: p.name): + if item.is_dir() and not item.name.startswith("."): + problems.append(f"algorithmic/{item.name}") + + return sorted(problems) + + def get_problem_statement( + self, + track: TrackType, + problem_id: Union[str, int], + ) -> Optional[str]: + """ + Get the problem statement/readme for a problem. + + Args: + track: Problem track + problem_id: Problem identifier + + Returns: + Problem statement text, or None if not found """ if track == "algorithmic": statement = self.algorithmic_runner.get_problem_statement(str(problem_id)) @@ -383,27 +388,27 @@ def get_problem_statement( # Research problem - read readme problem_path = self.docker_runner.get_problem_path(str(problem_id)) - readme = problem_path / "readme" - if readme.exists(): - return readme.read_text(encoding="utf-8") - return None - - -# Convenience function for quick evaluation -def evaluate( - track: TrackType, - problem_id: Union[str, int], - code: str, - *, - backend: BackendType = "docker", -) -> EvaluationResult: - """ - Quick evaluation function. - - Example: - from frontier_cs import evaluate - result = evaluate("research", "flash_attn", solution_code) - print(f"Score: {result.score}") - """ + readme = problem_path / "readme" + if readme.exists(): + return readme.read_text(encoding="utf-8") + return None + + +# Convenience function for quick evaluation +def evaluate( + track: TrackType, + problem_id: Union[str, int], + code: str, + *, + backend: BackendType = "docker", +) -> EvaluationResult: + """ + Quick evaluation function. + + Example: + from frontier_cs import evaluate + result = evaluate("research", "flash_attn", solution_code) + print(f"Score: {result.score}") + """ evaluator = SingleEvaluator(backend=backend) - return evaluator.evaluate(track, problem_id, code) + return evaluator.evaluate(track, problem_id, code) diff --git a/third_party/formal-conjectures b/third_party/formal-conjectures new file mode 160000 index 000000000..7a41db3d7 --- /dev/null +++ b/third_party/formal-conjectures @@ -0,0 +1 @@ +Subproject commit 7a41db3d761324599812d6ca6cb6a9f311046dc7