Complete Identification of Deep ReLU Neural Networks by Many-Valued Logic

TL;DR

The paper tackles the complete identification problem for deep ReLU networks by mapping network realizations to Łukasiewicz logic formulae and applying MV-algebraic axioms to generate all functionally equivalent architectures and parameters. A three-step extraction pipeline converts a ReLU network into a Łukasiewicz formula via ρ-to-σ conversion, per-neuron formula extraction, and layer-wise substitution, while a graphical normal form preserves architectural information. It then demonstrates a constructive two-step procedure to rebuild networks from a given MV formula, ensuring the network realizes the same function, and proves that MV axioms provide a complete set of symmetries for the identification task via Chang’s completeness theorem. The framework is extended to finite, rational, and real weight settings using corresponding valued logics and algebras, enabling complete identification across a broad range of practical weight regimes. This synthesis of many-valued logic with neural network identifiability offers a principled basis for understanding nonuniqueness and for systematic network synthesis and analysis.

Abstract

Deep ReLU neural networks admit nontrivial functional symmetries: vastly different architectures and parameters (weights and biases) can realize the same function. We address the complete identification problem -- given a function f, deriving the architecture and parameters of all feedforward ReLU networks giving rise to f. We translate ReLU networks into Lukasiewicz logic formulae, and effect functional equivalent network transformations through algebraic rewrites governed by the logic axioms. A compositional norm form is proposed to facilitate the mapping from Lukasiewicz logic formulae back to ReLU networks. Using Chang's completeness theorem, we show that for every functional equivalence class, all ReLU networks in that class are connected by a finite set of symmetries corresponding to the finite set of axioms of Lukasiewicz logic. This idea is reminiscent of Shannon's seminal work on switching circuit design, where the circuits are translated into Boolean formulae, and synthesis is effected by algebraic rewriting governed by Boolean logic axioms.

Figures (23)

• Figure 1: The ReLU networks ${\mathcal{N}}$ and three other ReLU networks ${\mathcal{N}}_1,{\mathcal{N}}_2,{\mathcal{N}}_3$, which are modifed from ${\mathcal{N}}$ by permutation, scaling, and affine symmetry, repsectively. The labels on the edges represent the weights, and the labels in the nodes represent the biases and the activation functions. Edges with zero-weights are erased from the illustration for the sake of clearness.
• Figure 2: The networks ${\mathcal{N}}'$ and ${\mathcal{N}}"$ realize the same function, but ${\mathcal{N}}'$ cannot be modified into ${\mathcal{N}}"$ by affine or scaling symmetries.
• Figure 3: A ReLU networks ${\mathcal{N}}^*$ and a zero-output network ${\mathcal{N}}^{**}$, which is derived from ${\mathcal{N}}^*$ by manipulating its associated formula. Edges with zero-weights are erased from the illustration for cleanness.
• Figure 4: A neural network. The labels on the edges denote the weights, and those in the nodes denote the biases and/or the associated activation functions.
• Figure 5: The function on domain $[0,1]^2$ realized by the network in \ref{['fig:dag']}.

Theorems & Definitions (92)

• Definition 1
• Proposition 1: nnaffid2020
• Proposition 2: grigsbyFunctionalDimensionFeedforward2022
• Definition 2
• Definition 3
• Definition 4
• Definition 5
• Theorem 1.1: McNaughton Theorem mcnaughtonTheoremInfiniteValuedSentential1951
• Theorem 1.2: changAlgebraicAnalysisMany1958chang1959new
• Theorem 1.3