Mathematical knowledge¶
This folder collects the mathematical knowledge needed to understand NCET's
bound propagation and exact optimization encoding. The notes describe the
formulations and their connection to the current implementation; broader
frontend and GraphIR design details are documented elsewhere under docs/.
Recommended reading order¶
- Interval Bound Propagation explains how NCET obtains finite tensor bounds throughout a graph.
- Exact Encoding explains how a bounded GraphIR becomes an LP- or MILP-compatible CVXPY constraint system.
- The operator notes derive the sparse matrices or exact formulations used by the backend:
- Conv2d
- BatchNorm
- AdaptiveAvgPool2d
- ReduceMean
- AvgPool2d
- MaxPool2d
Scope of each note¶
| Note | Main topic |
|---|---|
| Interval Bound Propagation | Bound rules for affine, monotone, arithmetic, and structural operators |
| Exact Encoding | Graph-wide LP/MILP variables, constraints, and exactness |
| Conv2d | Sparse affine matrix for convolution |
| BatchNorm | Inference-mode per-channel affine map |
| AdaptiveAvgPool2d | Adaptive windows and sparse averaging matrix |
| ReduceMean | Mean reduction, dimension handling, and linear equality |
| AvgPool2d | Sparse averaging matrix and pooling divisor |
| MaxPool2d | Full one-hot exact maximum formulation |