Repository navigation
Add solver result interfaces - #123
Open
guanqin-123 wants to merge 11 commits into
Open
guanqin-123 wants to merge 11 commits into
guanqin-123 wants to merge 11 commits into
Conversation
Expose shared result interfaces to BaB and branching while retaining concrete dual results for CLIMB replay.
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## main #123 +/- ##
==========================================
+ Coverage 77.61% 82.03% +4.41%
==========================================
Files 95 100 +5
Lines 23007 24842 +1835
==========================================
+ Hits 17858 20380 +2522
+ Misses 5149 4462 -687
Flags with carried forward coverage won't be shown. Click here to find out more.
... and 6 files with indirect coverage changes Continue to review full report in Codecov by Harness.
🚀 New features to boost your workflow:
|
Canonicalize shared norms, scalar or per-sample radii, and token selections while preserving creator-facing indices. Check actual finite-p membership and share the INPUT_SPEC parameter layout between validation and emission. Emit the existing embedding-width metadata and declare it in the schema so current dual bounds retain independent token-ball geometry after flattening.
Add C2 projection, Conv1d, division and square paths with compact token-wise dense bounds. Preserve symbolic smooth and bilinear composition, optimize MATMUL alpha state, and align reconstruction semantics.
Align native and selected ONNX tensor operations with verifier lanes and fixed model shapes. Preserve ordered graph operands and recursive JSON metadata with v2 compatibility. Extend the existing smoke checks for conversion, LP witnesses, and serialization.
Unify instance loading, disjunct aggregation, and exact-Net export across CLI and runner. Add strict compact checkpoints, equivalent conversion routes, and indexed text queries. Centralize creator construction and use module smoke checks instead of inline CI fixtures. Add BaB budget and CLIMB controls while preserving search time and certificate replay.
Install the existing Transformers dependency in BaB CI and keep workflow and local dependency declarations on Transformers 4. Preserve the compact tokenizer and numerical smoke assertions.
…erge Share one strict closed-unsafe boundary across interval, dual, BaB and replay checks; LINEAR_LE and RANGE keep legal equality. The dual CLI cascade now runs UNSAFE_LINEAR properties instead of skipping them. Add bound_refresh as the single interval and linear refresh owner, using original input geometry and an interval fallback for unsupported graphs. CLIMB accepts split_refresh and split_refresh_linear by replaying retained cores from the required split-free reference with raw backward proofs. Add exact packed core operations. Frontier merging with cold rebound, one-shot complement bounding, score-only steering and the pre-split propagation gate are explicit flags; existing preset defaults are unchanged. Extend the existing BaB and backend CLI smoke checks.
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.
In #14f31 (14f31de), previous constraint-export work focused on constraint expressions.
This change exposes shared result interfaces to BaB and branching while retaining concrete dual results for CLIMB replay and tracing.
In #96056 (9605645), front-end support full actual per-token with finite-p membership. This change normalises radii and perturbation masks across wrappers and conversion.
In #7271e (7271ebe), finite-p bounds support for backend and BaB splits preserve the original input geometry. This change adds prefix caching and optional early stopping while separating forward proofs from backward certificates used for CLIMB replay.
In #b1e8b0b0 (b1e8b0b) CLIMB supports differential activation bounding constraint refinements.
In #75a8a99 (75a8a99) Fix multi-head attention bounding and \nu bounding in dual approach.
In #39b8feb (39b8feb) CLIMB now supports a full encoder-only model with multi-head attention components that includes CV and NLP models.
In #8d9d1 (8d9d128) CLIMB optimizes NLP task.
In #e2c88 (e2c88d3) Extend CLIMB with split-dependent refresh, core lifting/replay and frontier merge