We propose a new perspective on deep ReLU networks, namely as circuit
counterparts of Lukasiewicz infinite-valued logic -- a many-valued (MV)
generalization of Boolean logic. An algorithm for extracting formulae in MV
logic from deep ReLU networks is presented. As the algorithm applies to
networks with general, in particular also real-valued, weights, it can be used
to extract logical formulae from deep ReLU networks trained on data.

提出了一种关于深层 ReLU 网络的新方法，将其视为 Lukasiewicz 无限值逻辑的电路对应物。介绍了一种从深层 ReLU 网络中提取多值逻辑公式的算法，适用于具有一般权重，包括实值权重的网络，可用于从数据上训练的深层 ReLU 网络中提取逻辑公式。

从深度神经网络中提取多值逻辑公式

Extracting Formulae in Many-Valued Logic from Deep Neural Networks

Recent advances in the integration of deep learning with automated theorem
proving have centered around the representation of logical formulae as inputs
to deep learning systems. In particular, there has been a growing interest in
adapting structure-aware neural methods to work with the underlying graph
representations of logical expressions. While more effective than character and
token-level approaches, graph-based methods have often made representational
trade-offs that limited their ability to capture key structural properties of
their inputs. In this work we propose a novel approach for embedding logical
formulae that is designed to overcome the representational limitations of prior
approaches. Our architecture works for logics of different expressivity; e.g.,
first-order and higher-order logic. We evaluate our approach on two standard
datasets and show that the proposed architecture achieves state-of-the-art
performance on both premise selection and proof step classification.

本研究通过开发一种新型的嵌入逻辑公式的结构感知神经网络架构，成功地解决了图形化方法在逻辑公式表示时的局限性，并在两个标准数据集上进行了实证研究，取得了最先进的性能，为深度学习与自动定理证明的融合提供了新的思路。