Knowing When to Stop: Evaluation and Verification of Conformity to Output-size Specifications

TL;DR

This paper introduces methods to evaluate and verify neural models' output length, addressing the risk of undesirable output sizes in applications like translation and captioning.

Contribution

It proposes a differentiable proxy for output-lengthening and a formal verification approach to ensure output size constraints are met.

Findings

Output-lengthening can produce outputs 50 times longer than inputs.

Verification can prove output length bounds within a given input domain.

Methods improve understanding and control of model output sizes.

Abstract

Models such as Sequence-to-Sequence and Image-to-Sequence are widely used in real world applications. While the ability of these neural architectures to produce variable-length outputs makes them extremely effective for problems like Machine Translation and Image Captioning, it also leaves them vulnerable to failures of the form where the model produces outputs of undesirable length. This behavior can have severe consequences such as usage of increased computation and induce faults in downstream modules that expect outputs of a certain length. Motivated by the need to have a better understanding of the failures of these models, this paper proposes and studies the novel output-size modulation problem and makes two key technical contributions. First, to evaluate model robustness, we develop an easy-to-compute differentiable proxy objective that can be used with gradient-based algorithms to find output-lengthening inputs. Second and more importantly, we develop a verification approach that can formally verify whether a network always produces outputs within a certain length. Experimental results on Machine Translation and Image Captioning show that our output-lengthening approach can produce outputs that are 50 times longer than the input, while our verification approach can, given a model and input domain, prove that the output length is below a certain size.