Compare satask answers against the ask oracle in CI

.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

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

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,23 +10,37 @@
 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
 
 import argparse
 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)
 
 

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