Recursive querying of neural networks via weighted structures

TL;DR

This paper develops a logical framework for querying neural networks using recursive, weighted structures, enabling verification and interpretation while analyzing computational complexity of various query types.

Contribution

It introduces a Datalog-like fixpoint logic for weighted structures, extending existing formalisms to include recursion and weight overwriting, with polynomial-time expressiveness results.

Findings

Proposes a scalar fixpoint logic with PTIME data complexity.

Shows PTIME model-agnostic queries are expressible in the logic.

Demonstrates simple queries can be NP-complete.

Abstract

Expressive querying of machine learning models - viewed as a form of intentional data - enables their verification and interpretation using declarative languages, thereby making learned representations of data more accessible. Motivated by the querying of feedforward neural networks, we investigate logics for weighted structures. In the absence of a bound on neural network depth, such logics must incorporate recursion; thereto we revisit the functional fixpoint mechanism proposed by Gr\"adel and Gurevich. We adopt it in a Datalog-like syntax; we extend normal forms for fixpoint logics to weighted structures; and show an equivalent "loose" fixpoint mechanism that allows values of inductively defined weight functions to be overwritten. We propose a "scalar" restriction of functional fixpoint logic, of polynomial-time data complexity, and show it can express all PTIME model-agnostic queries over reduced networks with polynomially bounded weights. In contrast, we show that very simple model-agnostic queries are already NP-complete. Finally, we consider transformations of weighted structures by iterated transductions.