Research map / Learning theory and algorithms / Combinatorial and search optimization

Taming Binarized Neural Networks and Mixed-Integer Programs

AAAI 2024 · Learning theory and algorithms › Combinatorial and search optimization · approach: Semidefinite relaxations for verification · 6 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Shows that training binarized neural networks can be reformulated via the subadditive dual of a conic mixed-integer program into a tame (o-minimal-definable) problem, enabling implicit differentiation and chain-rule backpropagation.

Problem

Backpropagation and the straight-through estimator give weight updates that are not subgradients of the forward pass for binarized neural networks (BNNs), so standard autodiff training is unreliable.

Approach

Reformulate BNN training as a MILP, then as the subadditive dual of a conic MIP; for "nice" MIPs this dual is locally Lipschitz and tame (o-minimal definable), so the Bolte et al. conservative-field chain rule applies and backpropagation yields valid subgradient-like updates.

Key results

• Proves that for a 'nice' conic MIP (feasible, dual-feasible continuous relaxation, finitely many non-differentiable points in objective graph), the subadditive dual is definable in an o-minimal structure.
• Shows the subadditive dual is locally Lipschitz, which together with the Bolte et al. framework yields a chain rule and implicit differentiation for training BNNs.
• Illustrates on a three-layer toy BNN example with a two-segment piecewise-linear approximation of the subadditive dual; no empirical benchmark numbers reported.

Surprising findings

• Non-decreasing subadditive functions are not tame in general (Cantor staircase counterexample), so a constraint qualification is needed.

Limitations

• No empirical training experiments on real BNNs; main evidence is theoretical and a toy example.
• Efficiency of algorithms for constructing the subadditive dual is not well understood.
• Constraint qualification needed since general subadditive duals need not be tame.

Experimental setup

Baselines: Straight-Through Estimator Saturated STE Expectation BackPropagation Quantized BackPropagation

Builds on: Bolte et al. conservative fields / nonsmooth implicit differentiation Straight-Through Estimator Johnson-Kiefer-style subadditive duality for conic MIPs (Thm 3 of cited work) Wilkie's o-minimality of Rexp

Closest papers by meaning

• Understanding Neural Network Binarization with Forward and Backward Proximal Quantizers (NeurIPS 2023 · similarity 0.87)
• Training Binary Neural Networks through Learning with Noisy Supervision (ICML 2020 · similarity 0.86)
• Training Binary Neural Networks via Gaussian Variational Inference and Low-Rank Semidefinite Programming (NeurIPS 2024 · similarity 0.86)
• Learning to Add, Multiply, and Execute Algorithmic Instructions Exactly with Neural Networks (NeurIPS 2025 · similarity 0.85)
• BIPNN: Learning to Solve Binary Integer Programming via Hypergraph Neural Networks (NeurIPS 2025 · similarity 0.84)
• Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations (ICML 2025 · similarity 0.84)