[WIP – ignore until reviewed by @ChrisRackauckas] Add islinear/isquadratic: polynomial-degree certification by tracer types#66
Draft
ChrisRackauckas-Claude wants to merge 1 commit into
Conversation
…ypes Implements the islinear/isquadratic proofs requested in SciML#1, using the tracer-type abstract-interpretation approach of the referenced Sparsity Programming paper, applied to polynomial degree instead of sparsity. `islinear(f, x...; wrt = 1)` and `isquadratic(f, x...; wrt = 1)` attempt to PROVE that `f` is a polynomial of degree <= 1 (affine) or <= 2 in the tracked arguments, holding the others fixed. `true` is a certificate under real arithmetic; `false` only means "not proven" -- the safe polarity for choosing an LP/QP path. Deciding this for arbitrary programs is impossible (Rice's theorem), so the design gives one-sided reliability: - The tracked arguments are seeded with `PolyDegree` tracer numbers and `f` is executed on them: `+`/`-` take the max degree, `*` adds, division by a constant and integer powers scale, and any non-polynomial operation on a non-constant poisons the result. Conservative by construction: the bound does not model cancellation (`x^2 - x^2 + x` is not certified). - Every predicate or conversion that would need the traced VALUE (comparisons, `isnan`, rounding, conversion) throws, aborting the trace -- this catches value-dependent branching dynamically even inside Base broadcast machinery, where `hasbranching`'s library-leaf policy is blind (`max.(u, 0)` is correctly rejected). - `hasbranching` is additionally required, proving statically that the traced path is the only path. The two guards cover each other's blind spots; a branch on an UNTRACKED argument also withholds the certificate (conservative, documented). The `wrt` selection gives the semantics SciML needs: an ODE right-hand side `(u, p, t) -> p[1]*u[1]` is certified linear in `u` for fixed `p`, while tracking everything (`wrt = :`) correctly refuses. Generic matrix code certifies: `u -> A*u` proves linear through the generic matmul. In-place right-hand sides work through a closure, shown in the tests. Tests include a ground-truth cross-validation: every issued linear certificate must have exactly vanishing second finite differences over exact Rational{BigInt} arithmetic at random points -- soundness is checked against real arithmetic, not against the tracer's own rules. The source is split by concern: `src/hasbranching.jl` holds the branch analysis, `src/polydegree.jl` the degree tracer and certificates, and the module file only exports and includes. Suites 70/70 on 1.10.11 and 72/72 on 1.12.6 and 1.13.0-rc1 (the tracer is pure dispatch, fully functional on lts); QA 18/18 (constructor disambiguators added for Base's cross-family Number constructors); docs build clean; Runic and typos clean. Additive on the 1.0.0 release: 1.0.0 -> 1.1.0. Co-Authored-By: Chris Rackauckas <accounts@chrisrackauckas.com>
ChrisRackauckas-Claude
force-pushed
the
islinear-isquadratic
branch
from
f215716 to
0799363
Compare
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
2 participants
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.
Is it possible to reliably know if a function is linear or quadratic?
Not unconditionally: linearity is a non-trivial semantic property of programs, so Rice's theorem rules out a total decision procedure. What is achievable — and what solver dispatch actually needs — is one-sided reliability:
trueis a proof,falseis only "not proven." That is the contract implemented here, mirroringhasbranching's conservatism.API
islinear(f, x...; wrt = 1)/isquadratic(f, x...; wrt = 1)— prove polynomial degree ≤ 1 (affine) / ≤ 2 in the arguments selected bywrt(index, indices, or:), holding the others fixed. Both exported, docstring'd, and on the API docs page.Mechanism — the tracer approach of the issue's reference, applied to degrees
Per the linked Sparsity Programming paper's methodology (abstract interpretation via tracer number types), a
PolyDegree <: Realtracer propagates a sound upper bound on real-arithmetic polynomial degree:+/-→ max,*→ sum,/constand integer^scale, transcendentals on non-constants poison. Three design points give the certificate its teeth:isnan, rounding, conversions on a tracer abort the trace — so value-dependent branching is caught dynamically even inside Base broadcast machinery, where thehasbranchinglibrary-leaf policy is blind:u -> max.(u, 0.0)is correctly rejected.hasbranchingis also required, statically proving the traced path is the only path. The two guards cover each other's blind spots. A branch on an untracked argument also (conservatively) withholds the certificate — documented with a test.wrtgives the SciML semantics:(u,p,t) -> p[1]*u[1]is certified linear inufor fixedp; withwrt = :it correctly refuses (bilinear).u -> A*ucertifies through the generic matmul. In-place RHS via a closure (tested).Conservatism is explicit: no cancellation modeling (
x^2 - x^2 + xis genuinely linear but not certified —falsemeans fall back, never "proven nonlinear").Ground-truth validation
Every issued linear certificate is cross-checked in the tests against exactly vanishing second finite differences over
Rational{BigInt}arithmetic at random points — an independent real-arithmetic soundness oracle. A known-nonlinear corpus is asserted never-certified.Code organization
Split by concern:
src/hasbranching.jl(branch analysis),src/polydegree.jl(degree tracer + certificates), module file only includes/exports.Verification
Numberconstructors resolved with explicit disambiguators; one allow-list entry,TwicePrecision, exists solely for that disambiguation and is documented).