Repository navigation
Land sathandlers with sound Pow, matrix and function guards - #9
Open
tilorc-bot wants to merge 31 commits into
Open
tilorc-bot wants to merge 31 commits into
tilorc-bot wants to merge 31 commits into
Conversation
Combine agent/2a-add-mul-pow (Add/Mul/Pow closure, sign, parity and related facts) with agent/2b-elementary-functions (sin/cos/exp/log/Abs/re/im/factorial and inverse-trig facts). The only conflict was an import collision in sathandlers.py. Also restrict the generic Pow real rule for imaginary exponents to non-E bases, where the function facts handle E**z exactly; without that guard the two fact sets derived positive and not-real for E**(I*pi*x) with even x.
The real implication in _sin_cos_facts fed exact sign facts for unevaluated numeric values such as cos(2)**2 + sin(2)**2, which then combined with the Add imaginary closure to decide negative(-I + I*(cos(2)**2 + sin(2)**2)) and its positive sibling as False. Numeric arguments now only get the complex and finite facts; symbolic arguments keep the real implication the function tests rely on.
- 0**negative (concrete odd-denominator exponent) is complex infinity, so Pow(x, -1, evaluate=False) is not real when x is zero (test_real_pow). - Positive rational base with an integer multiple of I*pi as exponent is not real, so it cannot be nonzero (test_nonzero). - Scope both rules narrowly to avoid over-deriving for symbolic negative exponents (test_positive) and negative even-denominator rationals. - Update unit tests that encoded the old conservative results and add regression coverage for the new facts.
SymPy's handler-local FiniteHandler_Mul returns None for finite(x*y*z) given ~finite(z) and extended-nonzero factors, but a sound global fact base cannot: extended_nonzero splits into positive/negative (finite and nonzero) or the two infinities, so every model satisfies one of the earlier explicit-finiteness patterns that must stay False. Pin all four patterns; no rule changes. Unit 96 passed/1 xfailed; mypy clean; checker 0; validation 60/34/4/6.
Symbols created with old-assumption keywords carry facts that the clean fact base never sees. reasoning.symbolfacts asks upstream sympy.assumptions.ask.ask for the scalar old-assumption vocabulary with an empty context, caches the answers per Symbol object, and the adapter asserts True results as local premises and False results as their negations. Explicit assumptions about the same applied predicate win, so the default commutative fact stays overridable. MatrixSymbol is skipped: upstream answers for it are type-derived rather than declared, and matrix knowledge lives in matrixfacts. test_check_old_assumption now passes; the bridge also supplies Q.integer(e)/Q.negative(e) for test_field_assumptions, whose remaining failure at line 261 needs a negative-integer MatPow rule owned by the matrix track.
# Conflicts: # reasoning/sympy_adapter.py
The complex and algebraic closure rules treated every complex (or algebraic) base raised to a complex (or rational) exponent as closed, but 0**negative is complex infinity. The same missing precondition leaked into the finite, hermitian, antihermitian, and real rules, and into the factorial integer rule at negative integers. Add a _pow_regular guard (nonzero base or real nonnegative exponent, which keeps 0**0 = 1) to those rules, require a nonzero exponent for the realness rules that are decided by the exponent, and update the tests that encoded the unguarded answers.
_pow_closure_facts (complex) and _pow_algebraic_facts (algebraic) close over a possibly-zero base with a negative exponent, where 0**-1 is zoo and neither complex nor algebraic. The new tests fail on the unfixed tip and pass with the OR(NOT(zero(base)), NOT(negative(exp))) guard the neighboring rules use. The report traces the miss to handler-vs-core-evaluator transcription, the absence of a singularity test matrix, upstream tests asserting the unsound closure, and the soundness fuzzer not being a CI gate.
Pin twenty unsound satask answers found by fuzzing and targeted probing: Add imaginary cancellation consequences, acos positivity at 1, factorial for negative integers, finite function values at infinities, infinite-base negative-exponent powers, several spurious inconsistencies (function facts at infinities, Pow with zero exponent, declared zero symbols, unevaluated Pow), and concrete-matrix counterexamples for ZeroMatrix, MatPow, MatMul, MatAdd, HadamardProduct and MatrixSlice. Nineteen of the twenty still fail with the two proposed Pow guards applied; the report records the fuzzer invocations, models and blind spots.
The adversarial suite documents fifteen definite satask answers that a concrete model contradicts and the Pow domain guards do not fix yet: Add imaginary closure on cancelling sums, function facts with unbounded arguments, Pow zero/infinite-base edge cases, and matrixfacts element predicates, slices and ZeroMatrix shape. Strict xfail keeps CI green and turns each entry into a failure once the underlying fact is fixed, so the marker must be removed with the fix.
Six adversarial tests exposed definite matrix answers contradicted by concrete models. Fix the handlers and drop their strict xfail entries: - ZeroMatrix only reports the square-dependent predicates when the shape is actually square. - MatPow keeps integer_elements only for nonnegative integer exponents (an inverse can introduce fractions). - MatAdd, MatMul and HadamardProduct close the element predicates only in the positive direction; the negative direction fails when terms cancel. - A proper principal submatrix no longer inherits fullrank, invertible, unitary or orthogonal: [[0]] is the leading slice of the full-rank, invertible, orthogonal [[0, 1], [1, 0]]. The invertible transfer also re-derived fullrank through the known-fact table. A slice covering the whole parent still keeps all of them. test_matrixfacts_soundness.py pins each guard next to the sound direction it must keep. The pinned upstream test_MatrixSlice asserts the removed invertible/orthogonal transfers, so validation moves from 76/18 to 75/19 with that single new failure.
Nine adversarial regressions pinned by test_soundness_adversarial.py were root causes in the Add, Mul, Pow, and elementary-function facts: * Add imaginary: a sum of imaginary terms can cancel to zero (x = I, y = -I), so the closed-group inference `imaginary(args) -> imaginary(sum)` was dropped; the sound antihermitian closure already covers it. The exactly-one-real direction now requires that real argument to be nonzero (x = 0 leaves x + I imaginary). * acos positivity excluded the upper endpoint: `acos(1) == 0` is not positive, so the interval is `nonnegative(arg + 1) & negative(arg - 1)`. * exp/E**x, Abs, re, and im asserted complex/real values unconditionally, but exp(oo) == oo, exp(-oo) == 0, Abs(oo) == oo, re(oo) == oo and im(zoo) == nan. Their value predicates are now gated on finite arguments (Abs additionally keeps the sound extended-nonnegative fact). * Pow zero: `zero(base**exp) <-> zero(base) & positive(exp)` ignored `oo**-1 == 0`, `0**oo == 0` and `(1/2)**oo == 0`; it is now split into the sound forward directions (`zero(base) & positive(exp)`, `infinite(base) & negative(exp)`, `zero(exp) -> ~zero(expr)`) plus guarded converses (`zero(expr) & positive(exp) & finite(exp) -> zero(base)`, and `finite` nonzero base with finite exponent -> nonzero). `_pow_rational_facts` needs a finite base for the rational-iff-zero-exponent rule, and the complex closed-group arm now needs a positive integer exponent so `oo**0 == 1` and `oo**-1 == 0` stay complex. * Mul zero: a zero factor only makes the product zero when the other factors are finite (oo*0 == nan); a zero factor still refutes a nonzero product. * Pow antihermitian parity and `antihermitian(x**2)` were already sound through existing nonzero-base guards; the new guard tests pin them. The nine fixed tests lose their strict xfail markers (the six matrixfacts entries stay), and test_soundness_scalar_guards.py pins each new guard together with the inference it must keep. Existing unit tests that encoded the unsound answers were updated to the sound ones. Validation/test_query flips: test_issue_7246 and test_real_functions now fail because upstream expects positive(acos(x)) on the closed interval and real(re(x))/real(im(x)) without finiteness; test_issue_27662_xfail now XPASSes because finite(x*y) under ~finite(x) & zero(y) is None.
tilorc-bot
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
This lands the
feature/sathandlerswork on top of currentmain(including the ask-oracle CI gate from #7 and the soundness fuzzer from #8) and makes the added fact families sound.main+feature/sathandlers(a4f6e44).d0731ee):_pow_regular(base nonzero or exponent real nonnegative, preserving0**0 = 1) on the complex/algebraic/finite/hermitian Pow closures; nonzero-exponent guards on the imaginary-exponent realness andI*pirules; zero-base guards on the antihermitian rules;factorialrequires a nonnegative argument. Fixes ~15 wrong-answer repros, e.g.satask(Q.zero(x), ~Q.complex(1/x))returnedFalsewith modelx = 0(1/0 = zoois not complex).69da8ad):agent-reports/2026-09-22-sathandlers-soundness-root-cause.md+test_soundness_singularities.py. Cause:3840c36transcribed SymPy's zero-blind assumption handlers instead of its guarded core evaluators; the same commit guardedextended_real/finite/realbut notcomplex/algebraic, and no test exercised base-zero singularities.0dd5d45):agent-reports/2026-09-22-sathandlers-adversarial-fuzz.md+test_soundness_adversarial.py(20 tests). The 15 open regressions were first pinned as strict xfail (924c4a9), then fixed:b069723): ZeroMatrix shape, MatPow negative-exponent element transfer, MatMul/MatAdd/Hadamard negation closure, MatrixSlice fullrank/invertible/orthogonal transfer.7aa514c): Add imaginary closure on cancelling sums,acos(1) = 0, function facts with unbounded arguments (exp/Abs/re/im),oo**0 = 1/oo**-1 = 0/0**oo = 0,0*oo = nan, and the Pow zero/rational equivalences.test_matrixfacts_soundness.py(10 tests) andtest_soundness_scalar_guards.py(11 tests).Verification
tools/check_soundness.py(PYTHONPATH at this branch): 0 findings, 0 upstream-shared in default,--engine random --cases 300, and--strictruns (extra random seeds 1–5 × 500 cases also clean).pytest reasoning/tests: 257 passed, 1 xfailed.mypy: clean (56 files);regen_known_facts --check: up to date.benchmarks.compare_satask --oracle --include-early-return: 122 agree, 3 stronger, 4 weaker, 3 inconsistent, 2 oracle-error, 0 failing (only definite contradictions withaskor unexpected exceptions fail).validation/test_query.py+test_matrices.py: 73 passed / 21 failed / 1 xfailed / 9 xpassed (was 79/15 on the unguarded branch). The six flipped tests —test_complex,test_algebraic,test_nonzero,test_issue_7246,test_real_functions,test_MatrixSlice— assert upstreamask's zero-blind or slice-transfer answers; soundness wins, and these divergences are deliberate.Follow-ups
agent-reports/2026-09-21-sathandlers-validation-triage.md, whose 79/104 figures and "landed on main" status are stale.