SlimONNX: A Story of Optimizing Neural Networks for Verification

Introduction

Two graph fragments can express the same calculation without being interchangeable everywhere they occur. A matrix multiplication followed by an addition suggests an obvious fusion. But the intermediate value may also feed another branch, or the target operator may require a shape the program has not established. An algebraic identity is only the beginning of a graph rewrite.

SlimONNX makes these decisions explicit for ONNX models used in verification workflows. Constant folding, redundant-operation removal and operator fusion offer different opportunities. The useful question is not simply how many nodes disappear, but which replacement the available information allows.

A rewrite needs the right context. Connectivity tells us who consumes an intermediate value; graph outputs tell us whether it remains externally observable; shapes and operator attributes determine whether the proposed replacement represents the same operation. Shape inference contributes to that decision, but it is not a substitute for the other checks.

When a required fact is unavailable, leaving the graph unchanged is a legitimate outcome. The optimizer has missed an opportunity, not thereby changed the function. A historical implementation path that is not algebraically equivalent is a different issue and should be documented as an implementation limitation, rather than explained away by the conservative policy used elsewhere.

What “exact” has to mean for a graph rewrite

Here’s the challenge: You train a beautiful neural network in PyTorch or TensorFlow. Everything works perfectly. Then you export it to ONNX for verification, and you’re working with a computational graph that, while semantically correct, contains patterns that verification tools find difficult to analyze: redundant operations, unfused layer pairs, and operators that could be combined for clearer mathematical structure. The model computes the same outputs, but the representation isn’t optimized for formal analysis.

Existing tools like ONNX Simplifier are excellent at what they’re designed for: inference deployment. They reduce runtime overhead, simplify graphs for faster execution, and optimize memory usage. For verification workflows, we have different priorities. This doesn’t make one tool better than the other—they serve different communities with different needs. We don’t just need faster models; we need analyzable models with explicit layer structure, deterministic behavior, and mathematical properties that formal verification tools can reason about.

That gap motivated SlimONNX: a pure Python toolkit for optimizing ONNX models specifically for verification workflows. Against the VNN-COMP model suite it keeps the same function under ONNXRuntime, with three recorded models where it does not. Not “make it run faster,” but “make it verifiable while preserving correctness.”

We’ll cover:

• Why verification needs different optimizations than inference
• The architecture and design philosophy behind SlimONNX
• Deep technical dives into operator fusion, shape inference, and version compatibility
• Real-world validation on 100+ models from VNN-COMP 2024
• The cost of the guarantee on the rewrites that lack one

If you work in neural network verification, ML safety, or just wonder how to make AI systems easier to analyze and validate, this is for you.

Why exported graphs accumulate rewritable structure

Let’s start with fundamentals. ONNX (Open Neural Network Exchange) was designed with a clear goal: enable interoperability between ML frameworks. Train in PyTorch, deploy with TensorFlow Lite. Train in TensorFlow, optimize with NVIDIA TensorRT. The promise is beautiful—write once, run anywhere.

ONNX prioritizes portability and semantic fidelity as its primary design goals. When you export a model to ONNX, the framework faithfully translates your high-level operations into ONNX operators, preserving the computational semantics exactly. This is exactly what cross-framework compatibility requires—correct computation matters more than optimal representation.

ONNX Design Goals vs. Verification Needs

ONNX’s priorities:

1. Cross-framework compatibility: Every framework’s quirks must map to ONNX operators
2. Semantic fidelity: The exported model must compute exactly the same outputs
3. Broad hardware support: Models should run on CPUs, GPUs, NPUs, edge devices

These are all good goals! But they create specific patterns in exported models:

• Redundant operations: Operations like Add(x, 0) or Mul(x, 1) appear frequently
• Unfused layers: MatMul followed by Add instead of a single Gemm operation
• Identity transformations: Reshape nodes that don’t actually change tensor shape
• Complex graph structure: Topological ordering may not be canonical, making comparison difficult

The gap is real but it is not the shape of the graph. Verification does not want a different shape — it wants the same function expressed in a form whose algebra is written down somewhere, so that a bound can be derived from it rather than guessed at. And the tool’s own README frames the value the same modest way, naming three techniques rather than a philosophy: operator fusion, constant folding, and redundant-operation removal.

Node count is not the objective, and the two reasons a pass deletes a node are not the same reason. Constant folding and redundant-operation removal delete work nothing downstream needs. Conv followed by BatchNormalization is fused for a different one: in inference mode a BatchNormalization is a per-channel affine map — scale / sqrt(var + epsilon) and bias - mean * bn_weight, both constants of the trained graph — so composing it with a convolution yields another affine map, and the pair collapses into one operator’s weight and bias. Which fusions a graph admits is therefore decided by its structure, not by how small it could get. In presets.py, 12 of the benchmark presets enable nothing but constant folding, and cgan_2023 turns three Conv/BN fusions on while turning two others off with the note that padding breaks them.

But “the algebra is the same” is a claim about an idealised graph. The shipped code carries three further conditions before it will do any of this, and they are where exactness is actually decided:

• Adjacency and a single consumer. The helper every linear fusion calls first is _is_only_next_node, and its comment names the failure: a fusion that rewrites its predecessor “otherwise silently drops a forward edge from the computation graph”. That is graph-correctness, not analysis.
• Representability. MatMul+Add becomes Gemm only for rank-2 inputs, checked against the shape map, because Gemm requires it. A constant-left MatMul keeps its operand order instead.
• Observability. An internal tensor that is also a graph output blocks the rewrite. The legacy-Softmax pass will only rewrite a scaffold whose intermediate values are single-consumer and non-observable, and leaves “every other graph … unchanged”.

None of those three is about verification. They are the price of doing a rewrite at all, and they are why the exactness question below is harder than it looks: adjacency and single-consumer checks are graph structure, representability is a shape condition, and observability is about what the graph exposes externally.

Example: A Simple PyTorch Network

Let’s make this concrete. Here’s a trivial neural network in PyTorch:

import torch
import torch.nn as nn
import torch.nn.functional as F

class SimpleNet(nn.Module):
    def __init__(self):
        super().__init__()
        self.fc1 = nn.Linear(10, 20)
        self.fc2 = nn.Linear(20, 10)

    def forward(self, x):
        x = F.relu(self.fc1(x))
        return self.fc2(x)

# Export to ONNX
model = SimpleNet()
dummy_input = torch.randn(1, 10)
torch.onnx.export(model, dummy_input, "simple.onnx", opset_version=17)

What you expect: Three operations (Linear → ReLU → Linear).

What you get in ONNX (This is not a very good example and it maybe unrealistic, but for illustration; the real case maybe some programmers uses matrix multiplication and addition to implement linear layers):

Input → MatMul → Add → Relu → MatMul → Add → Output

Still pretty clean, right? But even here, there are optimization opportunities:

1. MatMul + Add can fuse to Gemm (General Matrix Multiplication with bias)
2. Node ordering might not be topological (depending on export version)
3. Names like “/fc1/MatMul_output_0” obscure structure (what layer is this?)

Now scale this to ResNet-50, ViT, or a custom architecture with batch normalization, skip connections, and complex data flow. Suddenly you’re looking at thousands of nodes with patterns like:

Conv → Reshape → BatchNormalization → Reshape → Relu

When this could be:

Conv → Relu  (with BN folded into Conv weights)

Existing Tools and Their Design Goals

ONNX Simplifier (onnxsim) is a widely used tool for ONNX optimization, and it’s excellent at what it’s designed for—inference deployment:

• Constant folding (evaluate constant expressions at compile time)
• Shape inference (determine tensor shapes statically)
• Basic redundancy removal (eliminate identity operations)
• Fast optimization (seconds even for large models)

These optimizations prioritize runtime speed and memory efficiency, which is exactly right for deploying models to production. For verification workflows, the priorities are different—not better or worse, just different.

The repository states its value proposition in one sentence — operator fusion, constant folding, and redundant operation removal — and the code divides that into three commitments:

A canonical form, whether or not a flag asks for one. Four transforms always run: Constant nodes become initializers, Mul(x, x) becomes Pow(x, 2), Gemm attributes are absorbed into static inputs when possible, and the node list is put in strict topological order. Two exporters of the same network disagree about all four, and each disagreement is two spellings of one function.

Operators a downstream consumer can match. Mul(x, x) left as a generic binary multiply hides operand identity from whatever reads it and forces it onto a weaker bilinear surface; rewriting it to Pow(x, 2) removes no nodes at all, and it is one of the four unconditional transforms. ONNX’s own version conversion is the larger version of the same problem: a last-axis Softmax comes back as Shape(X); Flatten(X); Softmax; Reshape(..., Shape(X)), four nodes for a function the graph already had a one-node spelling for.

Semantics preserved rather than assumed. A rewrite is checked against the original instead of trusted: outputs are compared with np.allclose(rtol=1e-5, atol=1e-6) across sampled inputs, and a mismatch raises rather than warns. What makes that hold is a guard on each rewrite — the Softmax scaffold is replaced only when it has a single consumer and no graph output names it; a fusion that reuses an intermediate output name for a different value has to invalidate that value’s provenance; and fused parameters are cast back to the convolution’s own dtype before they are written.

The verification gap: none of the three is recorded in the ONNX model, so the caller has to state which spelling it wants rather than the tool inferring it. Two of them are selections rather than commitments, and they are booleans on OptimizationConfig; the first is not, because a canonical form is a property of the pipeline and not something a caller opts out of. OptimizationConfig has twenty boolean fields and two of them default to True: remove_dropout and has_batch_dim. Worth knowing that the class’s own docstring says otherwise — it claims the exceptions are simplify_node_name and has_batch_dim, and simplify_node_name is in fact False. Quoting the docstring here would have been quoting a bug, and it is a nice illustration of why a note about a tool should cite the fields rather than the prose above them.

SlimONNX fills this gap by prioritizing verifiability over raw performance. It’s not about making models run faster—it’s about making them analyzable.

Real-World Impact

When preparing models for VNN-COMP 2024 (the International Verification of Neural Networks Competition), I encountered:

• Models with redundant nodes (operations that could be eliminated)
• Fusible MatMul+Add patterns (opportunities to reduce node count)
• Inconsistent Conv+BatchNorm representations (some fused, some not)
• Non-canonical graph orderings (same model exports to different graphs)

After SlimONNX optimization:

• Cleaner structure: Explicit layer boundaries for manual inspection
• Less to consume: Fewer nodes = less work for whatever consumes the graph
• Reproducible results: Same model always optimizes to same graph
• Tool compatibility: Simplified graphs work better with verification tools (alpha,beta-CROWN, ERAN, etc.)

Note: For verification workflows, the structure of the computation graph matters as much as the numerical outputs. A model that’s mathematically equivalent but structurally different can have dramatically different verification complexity.

Design philosophy, and the mathematics it rests on

Before diving into implementation details, let’s establish the theoretical foundations. SlimONNX isn’t just about removing nodes—it’s about preserving mathematical equivalence while optimizing for analyzability.

Design Principles

1. Semantic Equivalence as Invariant

Every transformation must preserve the mathematical function computed by the model. The intent, for any optimization $\mathcal{O}$, is

for every $x$ in the input domain, with $f$ the model’s function. That intent is what the closed forms below are written to satisfy, and it is a property of the algebra rather than of the test suite. What the suite actually establishes is narrower and is worth stating separately: outputs are compared with np.allclose(rtol=1e-5, atol=1e-6) across sampled inputs, so equivalence is checked numerically on a sample, not proved pointwise and not bit-exact. A rewrite whose closed form is correct can still fail the sampled comparison, which is a bug in the derivation; one that passes it has not thereby been proved.

2. Transparency Over Opacity

Optimization should make the model’s structure clearer, not more obscure. When we fuse Conv → BatchNorm into a single Conv, we’re not hiding complexity—we’re revealing that these two layers are mathematically equivalent to a single affine transformation.

3. Functional Composition

The optimization pipeline is built as a composition of pure functions:

from dataclasses import dataclass
from functools import reduce
from typing import Callable
from onnx import ModelProto

@dataclass(frozen=True)
class OptimizationPipeline:
    """
    Functional composition of graph transformations.

    Each transform is a pure function: ModelProto → ModelProto
    The pipeline composes them: T_n ∘ T_{n-1} ∘ ... ∘ T_1
    """
    transforms: list[Callable[[ModelProto], ModelProto]]

    def apply(self, model: ModelProto) -> ModelProto:
        """Apply all transformations in sequence."""
        return reduce(lambda m, t: t(m), self.transforms, model)

This makes the pipeline:

• Testable: Each transform can be unit tested independently
• Composable: New optimizations can be added without modifying existing ones
• Deterministic: Same input always produces same output (no hidden state)

4. Verification-Aware Trade-offs

Some optimizations improve inference speed but hurt verification:

• Aggressive constant folding: Can eliminate nodes verification tools use as landmarks
• Operator fusion: Might hide layer boundaries needed for bound propagation
• Graph reordering: Can change the canonical form verification tools expect

SlimONNX makes different choices:

• Conservative fusion: Only fuse when it clarifies structure (Conv+BN) or is mathematically trivial (MatMul+Add→Gemm)
• Preserve structure: Keep explicit layer boundaries
• Canonical ordering: Ensure deterministic topological sort

Mathematical Correctness Framework

Let’s formalize what “correct optimization” means. Consider a neural network as a composition of layers:

An optimization transforms this to $g(x) = g_m \circ ... \circ g_1(x)$ where $m \leq n$ (fewer layers). For correctness, we need:

Property 1: Functional Equivalence

This is the property the closed form is derived to satisfy. It is not discharged by the test suite, which compares sampled outputs at a tolerance.

Property 2: Numerical Stability

The transformation should not significantly affect numerical precision. The analysis target for floating-point arithmetic is

Where $\epsilon_{\text{mach}}$ is machine epsilon and $C$ accumulates over the fused operations. The suite does not measure $C$ and does not check this bound; it checks the coarser and much weaker condition that sampled outputs agree to rtol=1e-5, atol=1e-6. That gap is deliberate — the tolerance is loose enough to tolerate reassociation, which is the whole point of fusing — but it does mean a numerically worse rewrite can pass.

Property 3: Verification Compatibility

The intent is that the optimized model $g$ is no harder for a verifier than the original $f$, with verification complexity including:

• Number of nodes (less work for whatever consumes the graph)
• Operator types (some are easier to analyze than others)
• Graph structure (DAG with clear layers vs complex dependencies)

This is a design goal, not a measured result, and it is not safe to assume: fewer nodes does not entail a cheaper bound, because what a propagator costs per node depends on the operator it is handed. MatMul followed by Add and a single Gemm are not obviously equal work for a bound propagator, and this note does not measure them.

Software Engineering Principles

Immutability: All configuration objects are frozen dataclasses. State changes happen explicitly through transformations, never through mutation. OptimizationConfig is the one every other piece of state is derived from, and it appears once only, under Architecture — a second, shorter transcription of the same class is a place for the defaults to disagree, and one did. The block there is adapted rather than verbatim: its docstring line is the repository’s own, and it is wrong in the way described above, so read the fields under it rather than the sentence.

Separation of Concerns: The codebase is organized into distinct modules:

• configs.py: Configuration (what to optimize)
• optimize_onnx/: Transformations (how to optimize)
• validate/: Correctness checking (did optimization preserve semantics?)
• analyze/: Graph analysis (understanding model structure)

Fail-Fast Validation: Every transformation validates its inputs and outputs. If an optimization produces an invalid model, we error immediately with a clear message, not silently continue.

Testing Strategy:

• Unit tests: Each transformation tested in isolation
• Property-based tests: Random models tested for semantic equivalence
• Integration tests: End-to-end on VNN-COMP benchmarks
• Numerical tests: Verify outputs match to machine precision

This foundation ensures that when we fuse operators or eliminate nodes, we’re not just making the graph smaller—we’re making it mathematically cleaner while preserving correctness.

Architecture, as the code actually has it

Building a code optimizer is one thing. Building one for verification required some unconventional choices. Let me walk through the key architectural decisions and why they matter.

Pure Python: Accessibility Over Speed

Decision: SlimONNX is pure Python—no C++ extensions, no Cython, no compiled components.

Why?

1. Accessibility: Researchers can read the code, understand the optimizations, and trust what’s happening
2. Debuggability: When optimization goes wrong, you can step through the code in a debugger
3. Maintainability: No build toolchain, no cross-platform compilation issues
4. Simplicity: pip install onnx onnxruntime numpy and you’re done

Trade-off: Pure Python is slower than C++ implementations. For large models (thousands of nodes), optimization might take seconds instead of milliseconds.

Verdict: Worth it. Verification workflows are not latency-critical. Spending 5 seconds to optimize a model that then takes hours to verify is fine. The clarity and trustworthiness of pure Python matter more.

Immutable Configuration: Preventing Accidental Bugs

Decision: All configurations are frozen dataclasses. Once created, they cannot be modified.

From slimonnx/configs.py (source):

@dataclass(frozen=True)
class OptimizationConfig:
    """Immutable optimization configuration.

    Defines which optimizations to apply during ONNX model slimming.
    All flags default to False except simplify_node_name and has_batch_dim.
    """

    # Fusion optimizations
    fuse_matmul_add: bool = False
    fuse_conv_bn: bool = False
    fuse_bn_conv: bool = False
    fuse_gemm_reshape_bn: bool = False
    # 20 boolean fields in total: 13 fusions, 2 simplifications, and the rest

    # Model properties
    has_batch_dim: bool = True

Why frozen?

Consider this bug-prone code:

config = OptimizationConfig(fuse_conv_bn=True)

# Somewhere deep in the optimization pipeline...
def some_helper(config):
    config.fuse_conv_bn = False  # Accidentally disable fusion
    # ... rest of the code

some_helper(config)  # Oops! Config is now modified

With frozen=True, this code raises an error immediately. Configurations are immutable. If you need a modified config, you create a new one:

from dataclasses import replace

new_config = replace(config, fuse_conv_bn=False)

Benefits:

• No hidden mutations: Configurations can’t change under your feet
• Clear dependencies: Each optimization declares exactly what it needs
• Debugging: You can inspect config state at any point and trust it hasn’t changed

Pure Functional Pipeline: Composability and Testability

Decision: Every optimization is a pure function: (model, config) → optimized_model. No side effects, no global state.

The optimization pipeline from slimonnx/slimonnx.py (source):

def slim(self, onnx_path: str, target_path: str | None = None, config: OptimizationConfig | None = None):
    """Optimize ONNX model through functional pipeline."""

    # Load model (pure function)
    model = onnx.load(onnx_path)

    # Preprocessing (pure functions)
    model = preprocess.convert_version(model, target_opset=OPSET_RUNTIME)
    # slim() passes infer_shapes=False, so ONNX's own inference is not run at
    # the head of the pipeline. Shape inference happens later, per pass.
    model = preprocess.cleanup(model)

    # Optimization passes (all pure functions)
    model = optimize.constant_to_initializer(model)
    if config.remove_dropout:
        model = optimize.remove_dropout(model)
    if config.constant_folding:
        model = optimize.constant_folding(model)
    if config.fuse_matmul_add:
        model = optimize.fuse_matmul_add(model)
    # ... more optimizations

    # Always-applied transformations (pure functions)
    model = optimize.simplify_gemm(model)
    model = optimize.topological_sort(model)

    # Save result
    onnx.save(model, target_path)

Every function takes an ONNX model (protobuf structure) and returns a modified copy. No function modifies global state, file system (except save), or depends on order of execution beyond explicit data dependencies.

Benefits:

1. Testable: Each optimization can be tested in isolation
2. Composable: Enable/disable optimizations without side effects
3. Predictable: Same input always produces same output (deterministic)
4. Debuggable: Inspect model state between any two passes

Example: Testing fusion in isolation:

def test_conv_bn_fusion():
    model_before = load_test_model("conv_bn_pattern.onnx")
    model_after = optimize.fuse_conv_bn(model_before)

    assert count_nodes(model_after, "BatchNormalization") == 0
    assert count_nodes(model_after, "Conv") == count_nodes(model_before, "Conv")
    assert_numerically_equivalent(model_before, model_after)

This would be much harder with stateful, imperative code.

Composition via Configuration Flags

Decision: Optimizations are controlled by boolean flags in the config, not inheritance or plugins.

Alternative approaches considered:

1. Plugin system: Register optimizations dynamically
2. Inheritance: Subclass optimizers for different strategies
3. Builder pattern: Chain optimization methods

Why simple flags won?

• Clarity: config.fuse_conv_bn = True is immediately obvious
• Preset compatibility: Easy to create preset configurations for benchmarks
• Debugging: You can print the config and see exactly what’s enabled
• Performance: No dynamic dispatch overhead

The Preset System: Benchmark-Specific Configurations

Different neural network architectures have different optimization opportunities. A convolutional network with batch normalization benefits from Conv+BN fusion. A transformer with feedforward layers benefits from MatMul+Add fusion. A GAN with transposed convolutions has specific padding constraints.

Rather than make users figure out the right flags, SlimONNX provides presets for common benchmarks from VNN-COMP 2024.

From slimonnx/presets.py (source):

ACAS_XU_2023_CONFIG = OptimizationConfig(
    fuse_matmul_add=True,
    fuse_gemm_gemm=True,
    remove_redundant_operations=True,
    constant_folding=True,
    simplify_node_name=True,
    has_batch_dim=False,  # ACAS-Xu has no batch dimension
)

VIT_2023_CONFIG = OptimizationConfig(
    fuse_matmul_add=True,
    fuse_gemm_reshape_bn=True,
    fuse_bn_reshape_gemm=True,
    remove_redundant_operations=True,
    constant_folding=True,
    simplify_node_name=True,
    has_batch_dim=True,  # ViT uses batch processing
)

CGAN_2023_CONFIG = OptimizationConfig(
    fuse_conv_bn=True,
    fuse_bn_conv=True,
    fuse_conv_transpose_bn=True,
    fuse_gemm_reshape_bn=False,  # Disabled: padding issues with cGAN structure
    fuse_bn_reshape_gemm=False,  # Disabled: padding issues with cGAN structure
    constant_folding=True,
    remove_redundant_operations=True,
    has_batch_dim=True,
)

Notice what the cGAN preset’s own comments say. The two flags it marks disabled are the Gemm/Reshape-plus-BN pair, not the Conv/BN pair — fuse_bn_conv is on. And both disabled flags are already False in the class defaults, so naming them records an intent the code cannot execute. That combination is worth sitting with: a reader of this block would conclude the preset skips BN-to-Conv fusion for padding reasons, when what it does is leave two already-off flags off.

Usage:

from slimonnx import SlimONNX, get_preset

slimonnx = SlimONNX()
config = get_preset("vit_2023")
slimonnx.slim("vit_model.onnx", "vit_optimized.onnx", config=config)

SlimONNX ships 34 preset names, of which six alias others and one is a synthetic all-optimisations preset, leaving 27 distinct benchmark configurations. They are named for the families they were tuned against, which are mostly VNN-COMP 2022 and 2023 rather than 2024 — the 2024 suffix appears on five.

Tip: If you’re optimizing models from a specific domain (e.g., all your models are CNNs with batch normalization), create a custom preset. It’s just a frozen dataclass—trivial to define and share.

Operator fusion: writing the algebra down

Now for the hard part. Operator fusion sounds simple: “combine two operations into one.” In practice, it’s a minefield of numerical correctness issues, shape constraints, and ONNX operator semantics.

The Mathematical Equivalence Problem

The core challenge: Prove that the fused operation computes exactly the same function as the original two operations.

This isn’t just “the outputs should be close.” For verification, we need bitwise equivalence (or at least equivalence within floating-point precision). If fusion changes the output by even 1e-10, downstream verification results could be invalid.

Why is this hard?

1. Floating-point arithmetic is not associative: (a + b) + c != a + (b + c) in general
2. Operator semantics vary by ONNX version: BatchNorm epsilon handling changed between opset 16 and 17
3. Broadcasting rules are complex: What happens when bias shape doesn’t match MatMul output?
4. Dtype mismatches cause silent failures: Mixing float32 and float64 produces wrong results

Let’s walk through three case studies, from simple to complex.

Case Study 1: MatMul + Add → Gemm

Pattern: Matrix multiplication followed by bias addition.

ONNX graph before:

Input (shape: [N, K]) → MatMul (weight: [K, M]) → Output1 (shape: [N, M])
                                                     ↓
Bias (shape: [M]) ──────────────────→ Add ─────→ Output2 (shape: [N, M])

ONNX graph after:

Input (shape: [N, K]) → Gemm (weight: [K, M], bias: [M]) → Output2 (shape: [N, M])

Mathematical equivalence:

This seems trivial, but there are constraints:

1. Shape constraint: MatMul output must be rank-2 (2D tensor) for Gemm. If it’s rank-3 or higher, fusion is illegal.
2. Bias broadcasting: The bias shape must broadcast correctly to the MatMul output.
3. Attribute compatibility: Gemm has alpha, beta, transA, transB attributes that affect computation.

From slimonnx/optimize_onnx/_mm_add.py (simplified):

def _fuse_matmul_add(nodes, initializers):
    for i in range(len(nodes) - 1):
        matmul_node = nodes[i]
        add_node = nodes[i + 1]

        if matmul_node.op_type != "MatMul" or add_node.op_type != "Add":
            continue

        # Check: MatMul output feeds into Add input
        if matmul_node.output[0] != add_node.input[0]:
            continue

        # Check: MatMul output is rank-2 (Gemm requires this)
        output_shape = get_tensor_shape(matmul_node.output[0])
        if len(output_shape) != 2:
            continue  # Skip fusion

        # Extract weight and bias
        weight = initializers[matmul_node.input[1]]
        bias = initializers[add_node.input[1]]

        # Create Gemm node
        gemm_node = onnx.helper.make_node(
            "Gemm",
            inputs=[matmul_node.input[0], matmul_node.input[1], add_node.input[1]],
            outputs=[add_node.output[0]],
            alpha=1.0,
            beta=1.0,
            transA=0,
            transB=0,
        )

        # Replace MatMul+Add with Gemm
        return replace_nodes(nodes, i, 2, gemm_node)

Key insight: Shape checking is mandatory. If the MatMul output is rank-3 (e.g., batched matrix multiply), Gemm fusion is illegal because Gemm only supports rank-2 inputs.

Case Study 2: Conv + BatchNormalization

Pattern: Convolution followed by batch normalization. Extremely common in CNNs (ResNet, VGG, etc.).

Mathematical equivalence:

Batch normalization computes:

Where $\mu, \sigma^2$ are the running mean and variance (computed during training), $\gamma, \beta$ are learned scale and shift parameters, and $\epsilon$ is a small constant for numerical stability.

Formal Equivalence Theorem: For a convolution $y = W * x + b$ followed by batch normalization in inference mode (fixed $\mu, \sigma^2$), the composition $\text{BN}(\text{Conv}(x))$ is mathematically equivalent to a single convolution with modified parameters.

Proof sketch: For a Conv output $y = W * x + b$ (where $*$ is convolution), we have:

Rearranging:

This is equivalent to a new Conv with:

Implementation from slimonnx/optimize_onnx/_bn_conv.py (source):

def _fuse_conv_bn_or_bn_conv(nodes, initializers, is_conv_bn=True):
    # ... pattern matching code ...

    # Extract parameters
    epsilon, scale, bn_bias, mean, var = _get_batchnorm_params(bn_node, initializers)
    weight, bias, attrs = _get_conv_params(conv_node, initializers)

    # CRITICAL: Preserve dtype to avoid float32/float64 mismatch
    target_dtype = weight.dtype
    bn_weight, bn_bias = compute_batchnorm_fusion_params(
        epsilon, scale, bn_bias, mean, var, target_dtype
    )

    # Fuse parameters
    if is_conv_bn:
        # Conv → BN: scale is applied per output channel
        new_weight = (weight * bn_weight.reshape(-1, 1, 1, 1)).astype(target_dtype, copy=False)
        new_bias = (bias * bn_weight + bn_bias).astype(target_dtype, copy=False)
    else:
        # BN → Conv: scale is applied per input channel
        new_weight = (weight * bn_weight.reshape(1, -1, 1, 1)).astype(target_dtype, copy=False)
        new_bias = (bias + np.sum(weight * bn_bias.reshape(1, -1, 1, 1), axis=(1, 2, 3))).astype(target_dtype, copy=False)

    # Create new Conv node with fused weights
    # ... node creation code ...

Numerical Correctness: The Dtype Gotcha

Notice the line: target_dtype = weight.dtype. This is critical. Here’s why:

ONNX models can mix float32 and float64 tensors. If Conv weights are float32 but BatchNorm parameters are float64 (or vice versa), naive fusion would compute:

# WRONG: dtype mismatch
new_weight = weight * bn_weight.reshape(-1, 1, 1, 1)
# weight is float32, bn_weight is float64 → result is float64
# But Conv expects float32 input!

This produces silent numerical differences. The model runs, outputs look reasonable, but verification fails because the outputs don’t match.

Fix: Always cast back to the original weight dtype:

# CORRECT: preserve dtype
new_weight = (weight * bn_weight.reshape(-1, 1, 1, 1)).astype(target_dtype, copy=False)

This took me days to debug during VNN-COMP 2024 prep. Models that should have verified were failing with tiny numerical differences (1e-8). The root cause: dtype mismatches in fusion.

Warning: Dtype preservation is mandatory for numerical correctness. Always cast fused parameters back to the original dtype. Mixing float32 and float64 causes subtle verification failures.

Case Study 3: Gemm-Reshape-BatchNormalization

Pattern: Gemm (fully connected layer), Reshape, then BatchNormalization. Common in Vision Transformers and MLPs.

ONNX graph:

Input (shape: [N, K]) → Gemm → Output1 (shape: [N, M])
                          ↓
                      Reshape → Output2 (shape: [N, C, H, W])
                          ↓
                   BatchNormalization → Output3 (shape: [N, C, H, W])

Why this is hard: The weights need to be reshaped across dimensions to account for the Reshape node between Gemm and BatchNorm.

Mathematical derivation:

Reshape to $[N, C, H, W]$ where $M = C \times H \times W$:

BatchNorm computes per-channel:

After reshaping back, the fused Gemm should compute:

Where scale, mu, and beta are broadcast according to the reshape dimensions.

Implementation complexity: The fusion code must:

1. Validate that Reshape dimensions are compatible with BatchNorm channels
2. Broadcast BatchNorm parameters according to reshape layout
3. Preserve dtype across three operations
4. Handle edge cases (e.g., Reshape that doesn’t actually change shape)

This is why SlimONNX has separate optimizations for fuse_gemm_reshape_bn and fuse_bn_reshape_gemm—the math is different depending on order.

Pattern Matching in Arbitrary Graphs

A final challenge: Graphs are not always linear. Nodes may have multiple inputs (skip connections), multiple outputs (branches), or complex topological orderings.

Example: In ResNet, you have:

Input → Conv1 → BN1 → ReLU1 ─┬→ Conv2 → BN2 → ReLU2 → Add → Output
                               │                            ↑
                               └────────────────────────────┘
                                   (skip connection)

If you’re fusing Conv2+BN2, you need to check that:

1. BN2’s input comes only from Conv2 (not shared with other nodes)
2. Conv2’s output goes only to BN2 (not used elsewhere)
3. The pattern is topologically sequential (no interleaved operations)

From slimonnx/optimize_onnx/_utils.py:

def _is_only_next_node(pre_node, node, all_nodes):
    """Check if `node` is the only consumer of `pre_node`'s output."""
    pre_output = pre_node.output[0]

    # Count how many nodes use pre_output as input
    consumers = sum(1 for n in all_nodes if pre_output in n.input)

    # Fusion is only safe if exactly one consumer
    return consumers == 1

Without this check, you could accidentally fuse operations that are part of different branches, producing incorrect results.

Note: Operator fusion is correct by construction when you validate:

1. Pattern matches expected operator sequence
2. Shapes are compatible
3. Data flow is exclusive (no shared inputs/outputs)
4. Dtype is preserved
5. Mathematical equivalence is proven

The two rewrites that are not exact

Both of these are in the shipped code, both are described accurately in its own comments, and both are load-bearing for a test suite. The third fact is the one that gets over-read. A test written against a behaviour is a regression guard: it records what the code did, and it is precisely the kind of test that fails when the behaviour is corrected — which is what distinguishes it from an argument that the behaviour is right. So “tests pin it” explains why the rewrite is still there and says nothing about whether it should be.

Depthwise BatchNormalization: a formula that is right and still not the closed form

For an ordinary convolution, folding BatchNormalization in means recomputing the convolution’s bias, because the normalisation scales every input channel and the bias has to absorb the part of that scale that falls outside the receptive field where the padding put zeros. In the general case the sum runs over the receptive field, and the helper’s comment calls the result “the math-correct closed form when the receptive field does no implicit padding”.

For a depthwise convolution the arithmetic collapses — every output channel is produced from a single input channel by its own (1, kH, kW) filter — and the helper uses a per-channel scalar, bias + bn_bias. Its docstring is explicit about the status of that scalar:

def _depthwise_simplified_bias(...):
    """Return the simplified depthwise BN->Conv bias: ``bias + bn_bias``.
    ... (legacy historical formula -- not the mathematically exact closed
    form in general).
    """

Exact when the depthwise structure makes it so, approximate in general, and documented in the place a reader would look. The alternative — refusing the fusion — is available and is not what the code does.

ConvTranspose: an unguarded direction

The same helper guards the padded convolution in the forward direction and the comment explains why: the bias would be applied outside the receptive field, where the padding supplies zeros. ConvTranspose has no such guard, and says so:

“There is no padding-skip on ConvTranspose: legacy behaviour did not guard the bn_to_op direction and tests pin it.”

That sentence records two facts and argues for neither. The behaviour predates the guard, and tests were written against it — which is why changing either alone would break something else, and why the comment exists at all. What it does not do is establish that the behaviour is correct. The reasonable reading is therefore that this is recorded debt rather than a settled decision, and the comment is what keeps it debt instead of a surprise.

What the two have in common, and what exactness depends on

Neither is a case of somebody skipping the algebra. In both, the algebra was done once, correctly, and the approximation is what survived contact with an existing expectation.

Which points at the part of the tool that is harder to be honest about. The guards do not all ask the same question. Adjacency, single-consumer structure and observability come from the graph itself; rank-2 representability and some operator-specific cases require shape information. That shape map is not computed from first principles here: SlimONNX delegates to shapeonnx, a separate optional package, and treats failure as normal:

    """Run shapeonnx inference, returning None on any tolerated failure.

    Shape inference is best-effort: shapeonnx is optional and tolerates partial
    coverage. ...
    :return: Shape map keyed by tensor name, or ``None`` on failure.
    """

The failure mode is chosen, and it is chosen for throughput: a warning is emitted, None is returned, and CONVENTIONS.md §9.5 records that the shape-dependent detectors “silently skip when data_shapes is None — this degradation path is intentional”. A model whose shapes cannot be inferred gets fewer rewrites, not an error.

Worth separating that from the other thing this section is easy to leave out. A missing shape map costs coverage, not trust. The detectors that need shapes do not run, so the graph comes back with fewer rewrites than the same graph would get on a model whose shapes were inferable — but every rewrite that did run ran against a map the tool had, and passed the same guards as always. Nothing here shows that an executed rewrite is less reliable because a different one was skipped.

What follows for a reader is about what they get rather than what they can rely on, and it is why the configuration is a table of dozens of benchmark-keyed presets rather than one flag: which rewrites are available depends on the graph in front of you, and the honest response to that is to be explicit about which model you are looking at. The rewrites that are simply not algebraically exact are a different argument, made further down, and they do not belong on this ladder.

Shape inference: what the exactness claims rest on

Many optimizations (constant folding, redundancy removal, fusion validation) require knowing tensor shapes at compile time. But ONNX models don’t always include shape information.

Why Shape Information Matters

Use cases for shapes:

1. Constant folding: If a tensor has shape [1, 1] and you add a scalar, you can pre-compute the result
2. Redundancy detection: A Reshape from [N, 256] to [N, 256] is identity and can be removed
3. Fusion validation: MatMul+Add fusion requires rank-2 output (you need shapes to check this)
4. Pattern matching: Some patterns only make sense with specific shapes (e.g., depthwise Conv)

The problem: Exported ONNX models may have:

• Dynamic shapes ([batch, channels, height, width] where batch is unknown)
• Missing shape annotations (older ONNX versions)
• Incomplete shape inference (some operators don’t propagate shapes)

Integration with ShapeONNX

SlimONNX uses ShapeONNX (github.com/ZhongkuiMa/shapeonnx), a companion library for advanced shape inference.

Why not use ONNX’s built-in shape inference?

ONNX’s onnx.shape_inference.infer_shapes() is fast but limited:

• Fails on models with dynamic dimensions
• Doesn’t handle all operators (especially custom ops)
• Can’t infer shapes through control flow (If, Loop nodes)

ShapeONNX provides more aggressive inference:

• A single topological pass: one walk of the graph in dependency order, rather than a fixed iteration count
• Concrete shape values: explicit_shapes carries actual integers for the shape tensors, with dynamic dimensions collapsed to -1 before the walk begins. Dynamic batch dimensions are therefore handled by being bounded, not by being propagated as symbolic terms
• Pattern-based inference: Uses common architecture patterns to infer unknown shapes

Usage in SlimONNX:

from slimonnx.preprocess import infer_shapes

def slim(model, config):
    # Attempt shape inference
    model = infer_shapes(model)

    # Check if shapes are available
    if has_shape_info(model):
        # Enable shape-dependent optimizations
        if config.constant_folding:
            model = constant_folding(model)
        if config.remove_redundant_operations:
            model = remove_redundant_reshapes(model)

    # Shape-independent optimizations (always possible)
    model = topological_sort(model)
    return model

Lazy evaluation: slim() passes infer_shapes=False, so ONNX’s own inference is not run at the head of the pipeline. Shape inference runs later, per pass, and the result is cached between passes behind a None sentinel that any mutation to the node list or the initialisers clears — so it is a memo rather than a run-once, and a pass that mutates forces a recompute before the next pass that needs shapes. Two details are worth being precise about. There is no flag that suppresses it: with every optimisation disabled the shape-based passes still call it, because two of the always-on transforms need a shape map. And the gating is over individual passes, not over whether inference happens at all.

ONNX Opset Compatibility

Different ONNX opsets (operator specification versions) have different shape inference rules.

SlimONNX works over opset 17 to 21. The floor and the ceiling are MIN_TESTED_OPSET and MAX_TESTED_OPSET in version_converter.py, and they are sourced from two constants in constants.py rather than chosen freely: OPSET_RUNTIME = 17, commented “Opset version for ONNX Runtime compatibility”, and OPSET_SHAPEONNX = 21, commented “Opset version for shapeonnx shape inference compatibility”. A target outside that range produces a warning naming the range, and a conversion that raises leaves the model’s own opset in place instead of substituting one that was never tested. Within the range, 20 is the recommended target; the slim pipeline converts to 17.

Why version pinning matters: the exact versions are not written in prose, they are dependencies, so installing the package gives the same ONNX the fusions were developed against.

From pyproject.toml:

# Exact versions required
pip install onnx==1.16.0 onnxruntime==1.22.0 numpy==1.26.4

Using higher versions may cause opset incompatibilities.

Performance Consideration

Shape inference is the most expensive operation in the optimization pipeline. For large models, shape inference can dominate the total optimization time.

How often it runs: once per pass that needs it, and not otherwise. It is memoised behind a None sentinel, and every pass that mutates the node list or the initialisers clears that memo, so the next shape-dependent pass rebuilds it. A pipeline that rewrites a lot early and reads a lot late therefore re-infers more than one that does the reverse, and there is no configuration that turns the whole thing off — with every optimisation disabled the shape-based passes still call it, because two of the always-on transforms need a map. What the memo saves is the work a pass would otherwise repeat within itself, not the work of the passes between them.

Tip: Complete annotations on the input — an export with do_constant_folding=True, say — are worth having, because they make each cached shape map cheap to rebuild. They do not let you skip inference: no configuration flag suppresses it.

Version compatibility

ONNX is a moving target. Operator semantics change between versions, sometimes in subtle ways that break optimization correctness.

What Numerical Comparisons Establish

The useful lesson is about evidence, not about a preferred diagnosis. A numerical comparison tests agreement on the chosen inputs. A mismatch can expose a problem with the rewrite, the reference computation, or their execution assumptions. Agreement on those inputs does not prove equivalence everywhere. Its size alone does not tell us whether the cause is floating-point evaluation, an operator assumption, or a different calculation. The method should make those questions easier to separate, not choose the answer from a tolerance threshold.

Version pinning still matters because the same formula can be evaluated under different operator semantics or arithmetic implementations. It is a way to make the execution environment reproducible, not proof that every observed mismatch has been explained.

ONNXRuntime Pinning

SlimONNX pins onnxruntime==1.22.0, and separately names the opset it targets for the runtime. That number is OPSET_RUNTIME = 17, commented in constants.py as “Opset version for ONNX Runtime compatibility” and passed as slim’s conversion target — so the opset a rewritten graph is written against is a fixed quantity rather than whatever the input happened to export.

What happens with version mismatches?

# This might fail
import onnx  # version 1.18.0 (hypothetical future version)
import onnxruntime as ort  # version 1.22.0

# Model optimized with onnx 1.16, loaded with onnxruntime 1.22
session = ort.InferenceSession("optimized.onnx")  # May fail to load!

ONNXRuntime validates that model opset matches its supported range. If you optimize with a newer ONNX version that uses opset 22, ONNXRuntime 1.22 will refuse to load the model.

Conservative Optimization Philosophy

When in doubt, skip the fusion.

Example from the CGAN preset:

CGAN_2023_CONFIG = OptimizationConfig(
    fuse_conv_bn=True,
    fuse_bn_conv=True,
    fuse_conv_transpose_bn=True,
    fuse_gemm_reshape_bn=False,  # Disabled: padding issues with cGAN structure
    fuse_bn_reshape_gemm=False,  # Disabled: padding issues with cGAN structure
    constant_folding=True,
    remove_redundant_operations=True,
)

For cGAN models, which use ConvTranspose for upsampling, the preset leaves the Gemm/Reshape-plus-BN fusions off and keeps the Conv/BN pair on. Padding is the reason recorded in the comments — and it is the same reason the guarded BN-to-Conv direction is skipped on padded convolutions elsewhere — but the flags named here are the other two, and both default to off already. The conservative behaviour is real.

Philosophy: Verification requires correctness above all else. A missed optimization opportunity (slightly larger graph) is acceptable. An incorrect fusion (wrong outputs) is catastrophic.

Warning: When building verification tools, conservative correctness beats aggressive optimization. A 10% slower verification is fine. A 0.0001% error rate is not.

What the tool does to real benchmark models

SlimONNX ships recorded baselines for 22 benchmark directories and 135 models. The benchmark suite is opt-in: its corpus is a symlink to a clone that has to be fetched separately, so these are the numbers the repository carries rather than a claim about every VNN-COMP benchmark.

VNN-COMP 2024: The Ultimate Stress Test

The International Verification of Neural Networks Competition (vnn2024) includes:

• Feedforward networks: ACAS-Xu (collision avoidance), Collins RUL (predictive maintenance)
• Convolutional networks: CIFAR-100, TinyImageNet, YOLO (object detection)
• Transformers: ViT (Vision Transformer)
• Graph neural networks: CORA, ML4ACOPF (power systems)
• GANs: cGAN with transposed convolutions

Each benchmark has unique architectural patterns, making it a comprehensive test suite.

Three-Tier Validation Methodology

For each model, SlimONNX validates:

Tier 1: Structural Validity

import onnx

model_optimized = onnx.load("model_optimized.onnx")
onnx.checker.check_model(model_optimized)  # Ensures valid ONNX protobuf

Tier 2: Runtime Compatibility

import onnxruntime as ort

session = ort.InferenceSession("model_optimized.onnx")
# If this succeeds, model is loadable and executable

Tier 3: Numerical Equivalence

import numpy as np

# Load both models
session_orig = ort.InferenceSession("model_original.onnx")
session_opt = ort.InferenceSession("model_optimized.onnx")

# Generate random inputs
for _ in range(10):
    inputs = generate_random_input(model.input_shapes)

    # Run both models
    output_orig = session_orig.run(None, inputs)[0]
    output_opt = session_opt.run(None, inputs)[0]

    # Check numerical equivalence
    np.testing.assert_allclose(output_orig, output_opt, rtol=1e-5, atol=1e-6)

Success Metrics

These are the repository’s own baselines rather than a summary line, which matters because the two figures a summary line would imply — 100% optimization success and 100% ONNXRuntime compatibility — appear nowhere in the tool’s documentation or tests, and the shipped baselines do not support them: 132 of the 135 recorded models pass, and three do not. The benchmark suite is also opt-in and its corpus is a symlink to a directory that has to be cloned separately, so “over 100 models” is the most the repository can be said to have exercised, and only by someone who cloned it.

Known Limitations

It is worth stating the scope before the list, because “conservative” is the claim these limitations support and it needs a number behind it: of the 135 models in the shipped baselines, 132 pass, and the three that do not are all one benchmark. What follows are design choices about correctness, not failures of ambition — but the three recorded failures are failures, and a list introduced by a 100% figure would have hidden them.

SlimONNX is not a silver bullet. Here are known limitations:

1. Dynamic shapes limit optimization: Models with fully dynamic batch dimensions (no shape info) can’t use constant folding or redundancy removal

2. BatchNorm fusion assumes inference mode: If BatchNorm is in training mode (updating running stats), fusion is incorrect

3. Some graph patterns too complex: Graphs with extensive control flow (Loop, If nodes) may not optimize well

4. Shape inference can fail: Models with very complex shapes or custom operators may not infer successfully

Design decision: These limitations are acceptable for verification workflows. Most verification benchmarks use:

• Fixed input shapes (or batch dimension only)
• Inference mode (no training)
• Feedforward architectures (minimal control flow)

For models outside this scope, SlimONNX falls back gracefully—it skips optimizations that can’t be validated rather than producing incorrect results.

Tip: If SlimONNX skips optimizations you expect, check:

1. Are tensor shapes available? (Run shape inference explicitly)
2. Is BatchNorm in inference mode? (Set training=False before export)
3. Are you using a supported opset? (17-21 tested; 20 is the recommended target)

Optimization Performance

Single-Pass Optimization

SlimONNX achieves efficiency through single-pass processing:

What the shipped baselines record

Baseline directories: 22
Recorded models:      135
├─ passed:             132
├─ failed:               3   (all three in collins_rul_cnn_2023)
└─ criterion:         max_diff < 1e-5 and mean_diff < 1e-6

A separate shipped figure is the unit-test suite: 239 tests, 0.27 seconds. That is a different measurement from model inference and the two should not be added together — and the same document lists performance regression testing and automated benchmarking as future work, which is the clearest statement available about what is not measured.

Why Single-Pass Matters

Multi-pass optimization (as used by some tools) requires multiple graph traversals:

• Pass 1: Constant folding
• Pass 2: Operator fusion
• Pass 3: Dead code elimination

SlimONNX combines these into a single traversal, reducing optimization overhead while maintaining correctness. Skipping when uncertain is what keeps the shipped baselines at 132 of 135 rather than lower — a coverage number, not a measure of how much rewriting survived on any one model.

Design Trade-off: SlimONNX prioritizes correctness over maximum optimization. When facing ambiguous patterns, it skips optimization rather than risk introducing errors. That preference is not free, and the shipped baselines are where its cost is visible: three models record passed: false, all in collins_rul_cnn_2023.

Three things that were not design preferences

Three constraints decided most of what the tool does and does not do. None of them is “verification wants a different kind of graph”, and that framing explains less than it seems to.

A rewrite has to be exact for the pattern at hand, or it is skipped

A transformation whose validity cannot be established for the specific shape in front of it is not attempted. That is why the guards read as a conjunction rather than a checklist — adjacency and a single consumer and rank-2 representability and non-observability — and why the unsupported cases raise rather than guess: NotImplementedError for a node type or operator with no handler, rather than a rewrite and a warning.

The padded convolution is the case worth naming, because the answer is directional and less tidy than a rule. BatchNormalization in front of a padded convolution is skipped, since the bias it would introduce falls outside the receptive field where the padding supplies zeros. The same fusion in the other direction is guarded by a flag rather than refused. And ConvTranspose is not guarded at all, for the reason given earlier: the behaviour predates the guard and tests depend on it.

A tool that skipped everything it could not prove would be small and easy to defend. This one is not small, and the two places where it is not exact are written down instead.

The oracle is best-effort, and the degradation is silent on purpose

Every exactness claim above is a claim about shapes, and the shapes come from a separate optional package whose failure is tolerated rather than raised. The consequence is that a graph whose shapes cannot be inferred gets fewer rewrites — not an error.

That is a deliberate choice, recorded as one: skipping is cheaper than failing, and a tool that refused to run on a partially-inferable graph would be a tool people stopped running. What a reader should take from it concerns what they get rather than what they can trust: a graph without shapes comes back less rewritten, and everything in it that was rewritten was rewritten on shapes the tool had.

The pair of rewrites that are not algebraically exact is a separate argument, and stacking it underneath this one turns two different facts into a single false inference. “The shapes may never have been inferred” cannot weaken a rewrite that never consults the shape map, and those two do not.

Output has to be a deterministic function of the graph

Verify a model, get SAFE, re-optimise the same model, and the answer must not change — so the optimiser has to be a function of the graph and nothing else.

The natural implementation breaks this. Python dictionaries have been insertion-ordered since 3.7, which makes it easy to believe that iterating a structure is deterministic, and for a dict built the same way twice it usually is. ONNX protobuf maps are not guaranteed to iterate in a consistent order, so an optimiser that iterates one produces a different graph on different runs. The outputs agree numerically and the graph is not identical, which is the worst case: nothing fails, and a verification result is quietly not reproducible.

The fix is to make every iteration order explicit — topologically for nodes, by name for initialisers — so the same input always produces the same output graph.

Conclusion

The guarantee worth understanding is local. A rewrite is exact when the algebra and the graph context establish that it is: BatchNormalization folded into a convolution, MatMul+Add collapsed into a Gemm, or an identity operation removed because its shape and value prove it does nothing. Where a case is not covered, the code should refuse or skip rather than guess.

Whether a rewrite is available at all depends on the graph, and some guards read a shape map that may not exist. That is a statement about coverage, not a weaker form of exactness. The historical depthwise formula and unguarded ConvTranspose direction are separate implementation limitations; the conservative skip path does not prove either one correct.

The preset table makes that boundary explicit. Which rewrites are available depends on the graph in front of you, so naming configurations per benchmark is more honest than pretending one global setting can make the decision for every model.

Repository: https://github.com/ZhongkuiMa/slimonnx

Related projects:

• ShapeONNX: shape inference, for the static shapes several of these optimisations require
• TorchONNX: ONNX-to-PyTorch conversion, which produces the program a verifier actually analyses
• PropDAG: graph traversal for bound propagation