Deep neural networks are revolutionizing the way complex systems are developed. However, these automatically-generated networks are opaque to humans, making it difficult to reason about them and guarantee their correctness. Here, we propose a novel approach for verifying properties of a widespread variant of neural networks, called recurrent neural networks. Recurrent neural networks play a key role in, e.g., natural language processing, and their verification is crucial for guaranteeing the reliability of many critical systems. Our approach is based on the inference of invariants, which allow us to reduce the complex problem of verifying recurrent networks into simpler, non-recurrent problems. Experiments with a proof-of-concept implementation of our approach demonstrate that it performs orders-of-magnitude better than the state of the art.
Czech Institute of Informatics, Robotics and Cybernetics（捷克信息学、机器人与控制论研究所）；Faculty of Mathematics, Informatics and Mechanics, University of Warsaw（华沙大学数学、信息学与力学学院）
We present a dataset and experiments on applying recurrent neural networks (RNNs) for guiding clause selection in the connection tableau proof calculus. The RNN encodes a sequence of literals from the current branch of the partial proof tree to a hidden vector state; using it, the system selects a clause for extending the proof tree. The training data and learning setup are described, and the results are discussed and compared with state of the art using gradient boosted trees. Additionally, we perform a conjecturing experiment in which the RNN does not just select an existing clause, but comp…
LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay（巴黎萨克雷高等师范学院、巴黎萨克雷大学、法国国家科学研究中心、验证与安全实验室）；Inria（法国国家信息与自动化研究所）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；Université Paris-Est Créteil（巴黎东大克雷泰伊校区）；Universität zu Lübeck（吕贝克大学）；CentraleSupélec（中央理工-高等电力学院）；Institut Universitaire de France（法国大学研究院）
This paper presents a property-directed approach to verifying recurrent neural networks (RNNs). To this end, we learn a deterministic finite automaton as a surrogate model from a given RNN using active automata learning. This model may then be analyzed using model checking as verification technique. The term property-directed reflects the idea that our procedure is guided and controlled by the given property rather than performing the two steps separately. We show that this not only allows us to discover small counterexamples fast, but also to generalize them by pumping towards faulty flows hi…
Okinawa Institute of Science and Technology（冲绳科学技术大学院大学）
It is crucial to ask how agents can achieve goals by generating action plans using only partial models of the world acquired through habituated sensory-motor experiences. Although many existing robotics studies use a forward model framework, there are generalization issues with high degrees of freedom. The current study shows that the predictive coding (PC) and active inference (AIF) frameworks, which employ a generative model, can develop better generalization by learning a prior distribution in a low dimensional latent state space representing probabilistic structures extracted from well hab…
Deep learning models have achieved remarkable success in natural language inference (NLI) tasks. While these models are widely explored, they are hard to interpret and it is often unclear how and why they actually work. In this paper, we take a step toward explaining such deep learning based models through a case study on a popular neural model for NLI. In particular, we propose to interpret the intermediate layers of NLI models by visualizing the saliency of attention and LSTM gating signals. We present several examples for which our methods are able to reveal interesting insights and identif…
The Chinese University of Hong Kong（香港中文大学）；Tencent Inc.（腾讯公司）
We propose a new framework for abstractive text summarization based on a sequence-to-sequence oriented encoder-decoder model equipped with a deep recurrent generative decoder (DRGN). Latent structure information implied in the target summaries is learned based on a recurrent latent random model for improving the summarization quality. Neural variational inference is employed to address the intractable posterior inference for the recurrent latent variables. Abstractive summaries are generated based on both the generative latent variables and the discriminative deterministic states. Extensive ex…
University of Manchester（曼彻斯特大学）；University of Amazonas（亚马逊大学）
QNNVerifier is the first open-source tool for verifying implementations of neural networks that takes into account the finite word-length (i.e. quantization) of their operands. The novel support for quantization is achieved by employing state-of-the-art software model checking (SMC) techniques. It translates the implementation of neural networks to a decidable fragment of first-order logic based on satisfiability modulo theories (SMT). The effects of fixed- and floating-point operations are represented through direct implementations given a hardware-determined precision. Furthermore, QNNVerifi…
University of Manchester（曼彻斯特大学）；Idiap Research Institute（IDIAP研究所）
An emerging line of research in Explainable NLP is the creation of datasets enriched with human-annotated explanations and rationales, used to build and evaluate models with step-wise inference and explanation generation capabilities. While human-annotated explanations are used as ground-truth for the inference, there is a lack of systematic assessment of their consistency and rigour. In an attempt to provide a critical quality assessment of Explanation Gold Standards (XGSs) for NLI, we propose a systematic annotation methodology, named Explanation Entailment Verification (EEV), to quantify th…
We propose a recurrent extension of the Ladder networks whose structure is motivated by the inference required in hierarchical latent variable models. We demonstrate that the recurrent Ladder is able to handle a wide variety of complex learning tasks that benefit from iterative inference and temporal modeling. The architecture shows close-to-optimal results on temporal modeling of video data, competitive results on music modeling, and improved perceptual grouping based on higher order abstractions, such as stochastic textures and motion cues. We present results for fully supervised, semi-super…
When Quantization Breaks Memory: Recurrent-State Write-Back in Low-Precision Temporal Inference
Rensselaer Polytechnic Institute（伦斯勒理工学院）；Center for Modeling, Simulation, and Imaging in Medicine（医学建模、仿真与成像中心）；Department of Biomedical Engineering（生物医学工程系）
University of Southern California（南加利福尼亚大学）；MILA - Quebec AI Institute（魁北克人工智能研究所）；University of Montréal（蒙特利尔大学）
Knowledge graph reasoning is a critical task in natural language processing. The task becomes more challenging on temporal knowledge graphs, where each fact is associated with a timestamp. Most existing methods focus on reasoning at past timestamps and they are not able to predict facts happening in the future. This paper proposes Recurrent Event Network (RE-NET), a novel autoregressive architecture for predicting future interactions. The occurrence of a fact (event) is modeled as a probability distribution conditioned on temporal sequences of past knowledge graphs. Specifically, our RE-NET em…
Universidad de Murcia（穆尔西亚大学）；Universidad de Granada（格拉纳达大学）
Valuation based systems verifying an idempotent property are studied. A partial order is defined between the valuations giving them a lattice structure. Then, two different strategies are introduced to represent valuations: as infimum of the most informative valuations or as supremum of the least informative ones. It is studied how to carry out computations with both representations in an efficient way. The particular cases of finite sets and convex polytopes are considered.
Transformers have recently been popular for learning and inference in the spatial-temporal domain. However, their performance relies on storing and applying attention to the feature tensor of each frame in video. Hence, their space and time complexity increase linearly as the length of video grows, which could be very costly for long videos. We propose a novel visual memory network architecture for the learning and inference problem in the spatial-temporal domain. We maintain a fixed set of memory slots in our memory network and propose an algorithm based on Gumbel-Softmax to learn an adaptive…
GLINT-RU: Gated Lightweight Intelligent Recurrent Units for Sequential Recommender Systems
City University of Hong Kong（香港城市大学）；High Magnetic Field Laboratory, Chinese Academy of Sciences（中国科学院强磁场科学中心）；Southern University of Science and Technology（南方科技大学）；Jinan University（暨南大学）；University of Science and Technology of China（中国科学技术大学）
Toward a mechanistic understanding of inference in visual cortex and diffusion models
Dept. of Electrical Engineering and Computer Science, UC Berkeley（加州大学伯克利分校电气工程与计算机科学系）；Helen Wills Neuroscience Institute, UC Berkeley（加州大学伯克利分校海伦·威尔斯神经科学研究所）；Herbert Wertheim School of Optometry and Vision Science, UC Berkeley（加州大学伯克利分校赫伯特·韦特海姆视觉科学学院）；Redwood Center for Theoretical Neuroscience, UC Berkeley（加州大学伯克利分校红木理论神经科学中心）；Flatiron Institute（Flatiron研究所）；Dept. of Electrical and Computer Engineering, UC Davis（加州大学戴维斯分校电气与计算机工程系）
University of Sussex（萨塞克斯大学）；VERSES Research Lab（VERSES研究实验室）；University of Oxford（牛津大学）
Predictive coding is an influential model of cortical neural activity. It proposes that perceptual beliefs are furnished by sequentially minimising "prediction errors" - the differences between predicted and observed data. Implicit in this proposal is the idea that perception requires multiple cycles of neural activity. This is at odds with evidence that several aspects of visual perception - including complex forms of object recognition - arise from an initial "feedforward sweep" that occurs on fast timescales which preclude substantial recurrent activity. Here, we propose that the feedforwar…
