From 903bed15379db1db2dab9b45f45775f18013b962 Mon Sep 17 00:00:00 2001 From: tilorc-bot <309221022+tilorc-bot@users.noreply.github.com> Date: Tue, 22 Sep 2026 05:02:15 +0000 Subject: [PATCH] Compare satask answers against the ask oracle in CI Upstream satask parity rejects intentional improvements: the sathandlers work raises the validation pass rate from 40/104 to 79/104 by matching full ask, yet introduces six divergences from upstream satask (including three ValueError answers for inconsistent assumptions), so the comparison gate goes red. Add an --oracle mode to benchmarks.compare_satask that uses pinned SymPy's ask as the correctness reference. Being stronger or weaker than ask is reported but accepted, and ValueError for inconsistent assumptions is accepted; only a definite answer contradicting ask, or an unexpected exception, fails the run. CI switches to this mode; the baseline satask comparison remains available via the existing options. --- .github/workflows/ci.yml | 4 +- README.md | 7 ++ benchmarks/__init__.py | 0 benchmarks/compare_satask.py | 120 +++++++++++++++++++++---- reasoning/tests/test_compare_satask.py | 55 ++++++++++++ 5 files changed, 168 insertions(+), 18 deletions(-) create mode 100644 benchmarks/__init__.py create mode 100644 reasoning/tests/test_compare_satask.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 39c0674..10d4a8e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -54,8 +54,8 @@ jobs: cache: pip - name: Install the package with pinned SymPy and dev tools run: python -m pip install -e '.[sympy,dev]' - - name: Compare satask results against pinned SymPy - run: python -m benchmarks.compare_satask --include-early-return + - name: Compare satask answers against the SymPy ask oracle + run: python -m benchmarks.compare_satask --oracle --include-early-return - name: Run the satask timing benchmark run: python -m benchmarks.satask --repeat 25 | tee benchmark.json - name: Add the timing benchmark to the job summary diff --git a/README.md b/README.md index 588425c..5baa8b3 100644 --- a/README.md +++ b/README.md @@ -77,6 +77,13 @@ To compare answers against the pinned SymPy `satask`, run `python -m benchmarks.compare_satask --include-early-return`. Saved original modules remain supported with `--baseline-satask` and `--baseline-handlers`. +CI instead checks answers against SymPy's full `ask` as the correctness oracle +with `python -m benchmarks.compare_satask --oracle --include-early-return`. +Being stronger than `ask` (a definite answer where `ask` is unsure) or weaker +is reported, and `ValueError` for inconsistent assumptions is accepted; only a +definite answer that contradicts `ask`, or an unexpected exception, fails the +run. + CI (`.github/workflows/ci.yml`) runs the unit tests, mypy, and the vendored known-facts check on Python 3.10 and 3.14, plus the commands above, for every pull request. Timing results and the validation progress comparison appear in diff --git a/benchmarks/__init__.py b/benchmarks/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/benchmarks/compare_satask.py b/benchmarks/compare_satask.py index 00068ca..d61700f 100644 --- a/benchmarks/compare_satask.py +++ b/benchmarks/compare_satask.py @@ -1,4 +1,4 @@ -"""Compare this checkout's ``satask`` against a baseline ``satask``. +"""Compare this checkout's ``satask`` against a baseline or an oracle. By default the baseline is the pinned SymPy ``satask`` from the installed ``sympy`` package. Saved baseline modules can be supplied instead:: @@ -10,6 +10,13 @@ The saved files are loaded only in memory. In particular, the baseline ``satask`` sees the supplied baseline handler registry even when this checkout has already migrated its handlers to lightweight formulas. + +With ``--oracle`` the pinned SymPy ``ask`` is the correctness reference +instead of the upstream ``satask`` parity check. A definite answer that full +``ask`` cannot give (``stronger``), a missing answer (``weaker``), and a +``ValueError`` for inconsistent assumptions are all acceptable; only a +definite answer that contradicts ``ask``, or an unexpected exception, fails +the run. """ from __future__ import annotations @@ -17,16 +24,23 @@ import importlib.util import random import sys +from collections import Counter from pathlib import Path -from typing import Any, Callable, cast +from typing import Any, Callable, TypeAlias, cast -from sympy import I, Q, pi, symbols +from sympy import I, Q, ask, pi, symbols from sympy.logic.boolalg import And, Equivalent, Implies, Not, Or, Xor from sympy.matrices.expressions import MatrixSymbol from reasoning.satask import satask as current_satask from reasoning.sympy_types import SymPyExpr +Outcome: TypeAlias = tuple[str, Any] + +VERDICT_ORDER = ("agree", "stronger", "weaker", "inconsistent", + "oracle-error", "mismatch", "current-error") +FAILING_VERDICTS = ("mismatch", "current-error") + def _load_module(name: str, path: Path) -> Any: spec = importlib.util.spec_from_file_location(name, path) @@ -61,13 +75,45 @@ def load_baseline(satask_path: Path, handlers_path: Path) -> Callable[..., Any]: def evaluate(function: Callable[..., Any], proposition: SymPyExpr, assumptions: SymPyExpr, - early_return: bool = False) -> tuple[str, Any]: + early_return: bool = False) -> Outcome: try: return "value", function(proposition, assumptions, early_return=early_return) except Exception as error: # Baselines can differ in their exception type. return "error", type(error).__name__ +def evaluate_oracle(oracle: Callable[..., Any], proposition: SymPyExpr, + assumptions: SymPyExpr) -> Outcome: + """Evaluate a case with SymPy's full ``ask`` as the correctness oracle.""" + try: + return "value", oracle(proposition, assumptions) + except Exception as error: + return "error", type(error).__name__ + + +def classify(current: Outcome, oracle: Outcome) -> str: + """Classify a current/ask outcome pair. + + ``mismatch`` (two definite, different answers) and ``current-error`` (an + unexpected exception) are the only failing verdicts. Being stronger or + weaker than ``ask`` is reported, not penalised, and ``ValueError`` is the + documented outcome for inconsistent assumptions. + """ + current_kind, current_value = current + oracle_kind, oracle_value = oracle + if oracle_kind == "error": + if current_kind == "error": + return "agree" if current_value == oracle_value else "oracle-error" + return "oracle-error" + if current_kind == "error": + return "inconsistent" if current_value == "ValueError" else "current-error" + if oracle_value is None: + return "stronger" if current_value is not None else "agree" + if current_value is None: + return "weaker" + return "agree" if current_value == oracle_value else "mismatch" + + def cases(seed: int, random_cases: int) -> list[tuple[SymPyExpr, SymPyExpr]]: x, y, z = symbols("x y z") subjects = [x, y, x + y, x*y, x*y*z, x**2, x**3, x**y, @@ -127,33 +173,75 @@ def compare(baseline: Callable[..., Any], seed: int, random_cases: int, return len(all_cases), mismatches +def compare_with_oracle(seed: int, random_cases: int, + early_return: bool = False, + current: Callable[..., Any] = current_satask, + oracle: Callable[..., Any] = ask) -> tuple[ + int, Counter[str], + list[tuple[int, SymPyExpr, SymPyExpr, Outcome, Outcome, str]], + ]: + """Compare current answers against the ``ask`` oracle verdict by verdict.""" + verdicts: Counter[str] = Counter() + failures = [] + all_cases = cases(seed, random_cases) + for index, (proposition, assumptions) in enumerate(all_cases): + current_outcome = evaluate(current, proposition, assumptions, early_return) + oracle_outcome = evaluate_oracle(oracle, proposition, assumptions) + verdict = classify(current_outcome, oracle_outcome) + verdicts[verdict] += 1 + if verdict in FAILING_VERDICTS: + failures.append((index, proposition, assumptions, + current_outcome, oracle_outcome, verdict)) + return len(all_cases), verdicts, failures + + def main() -> None: parser = argparse.ArgumentParser(description=__doc__) parser.add_argument("--baseline-satask", type=Path, help="a saved baseline satask.py file") parser.add_argument("--baseline-handlers", type=Path, help="the saved sathandlers.py matching --baseline-satask") + parser.add_argument("--oracle", action="store_true", + help="benchmark against SymPy's ask as the correctness " + "oracle instead of upstream satask parity") parser.add_argument("--seed", type=int, default=62819) parser.add_argument("--random-cases", type=int, default=120) parser.add_argument("--include-early-return", action="store_true") args = parser.parse_args() + if args.oracle and args.baseline_satask is not None: + parser.error("--oracle cannot be combined with a saved baseline") if (args.baseline_satask is None) != (args.baseline_handlers is None): parser.error("--baseline-satask and --baseline-handlers are required together") - if args.baseline_satask is None: - baseline = load_installed_baseline() - else: - baseline = load_baseline(args.baseline_satask, args.baseline_handlers) modes = [False] + ([True] if args.include_early_return else []) failed = False - for early_return in modes: - count, mismatches = compare(baseline, args.seed, args.random_cases, early_return) - mode = "early_return" if early_return else "full SAT" - print(f"{mode}: {count} cases, {len(mismatches)} mismatches") - for index, proposition, assumptions, old, new in mismatches: - print(f" case {index}: {proposition!s} under {assumptions!s}") - print(f" baseline={old}; current={new}") - failed |= bool(mismatches) + if args.oracle: + for early_return in modes: + count, verdicts, failures = compare_with_oracle( + args.seed, args.random_cases, early_return) + mode = "early_return" if early_return else "full SAT" + summary = ", ".join(f"{verdicts[verdict]} {verdict}" + for verdict in VERDICT_ORDER if verdicts[verdict]) + print(f"{mode}: {count} cases: {summary}") + for index, proposition, assumptions, current, oracle, verdict in failures: + print(f" {verdict} case {index}: {proposition!s} " + f"under {assumptions!s}") + print(f" current={current}; ask oracle={oracle}") + failed |= bool(failures) + else: + if args.baseline_satask is None: + baseline = load_installed_baseline() + else: + baseline = load_baseline(args.baseline_satask, args.baseline_handlers) + for early_return in modes: + count, mismatches = compare(baseline, args.seed, + args.random_cases, early_return) + mode = "early_return" if early_return else "full SAT" + print(f"{mode}: {count} cases, {len(mismatches)} mismatches") + for index, proposition, assumptions, old, new in mismatches: + print(f" case {index}: {proposition!s} under {assumptions!s}") + print(f" baseline={old}; current={new}") + failed |= bool(mismatches) raise SystemExit(1 if failed else 0) diff --git a/reasoning/tests/test_compare_satask.py b/reasoning/tests/test_compare_satask.py new file mode 100644 index 0000000..bd48563 --- /dev/null +++ b/reasoning/tests/test_compare_satask.py @@ -0,0 +1,55 @@ +from __future__ import annotations + +from typing import Any + +from benchmarks.compare_satask import classify, compare_with_oracle + + +def test_classify_agreement() -> None: + assert classify(("value", True), ("value", True)) == "agree" + assert classify(("value", False), ("value", False)) == "agree" + assert classify(("value", None), ("value", None)) == "agree" + + +def test_classify_definite_disagreement_fails() -> None: + assert classify(("value", True), ("value", False)) == "mismatch" + assert classify(("value", False), ("value", True)) == "mismatch" + + +def test_classify_stronger_than_oracle_is_allowed() -> None: + assert classify(("value", True), ("value", None)) == "stronger" + assert classify(("value", False), ("value", None)) == "stronger" + + +def test_classify_weaker_than_oracle_is_reported() -> None: + assert classify(("value", None), ("value", True)) == "weaker" + assert classify(("value", None), ("value", False)) == "weaker" + + +def test_classify_inconsistent_assumptions_are_allowed() -> None: + assert classify(("error", "ValueError"), ("value", None)) == "inconsistent" + assert classify(("error", "ValueError"), ("value", False)) == "inconsistent" + + +def test_classify_unexpected_exception_fails() -> None: + assert classify(("error", "TypeError"), ("value", True)) == "current-error" + assert classify(("error", "TypeError"), ("value", None)) == "current-error" + + +def test_classify_oracle_error_is_unjudged() -> None: + assert classify(("value", True), ("error", "TypeError")) == "oracle-error" + assert classify(("error", "ValueError"), ("error", "ValueError")) == "agree" + + +def test_compare_with_oracle_counts_verdicts() -> None: + def current(proposition: Any, assumptions: Any, + early_return: bool = False) -> bool: + return True + + def oracle(proposition: Any, assumptions: Any) -> None: + return None + + count, verdicts, failures = compare_with_oracle( + 0, 2, current=current, oracle=oracle) + assert failures == [] + assert verdicts["stronger"] == count