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

TL;DR

This paper presents a method to fully identify and characterize all ReLU neural networks that produce the same function by translating them into Lukasiewicz logic and applying algebraic rewrites based on logic axioms.

Contribution

It introduces a novel approach translating ReLU networks into Lukasiewicz logic to achieve complete identification and characterization of all equivalent networks.

Findings

All networks in a functional equivalence class are connected by finite symmetries.

The method leverages logic axioms to perform algebraic rewrites of network representations.

A compositional norm form facilitates mapping from logic formulae back to networks.

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.