# Towards the Unseen: Iterative Text Recognition by Distilling from Errors

Ayan Kumar Bhunia1 Pinaki Nath Chowdhury1,2 Aneeshan Sain1,2 Yi-Zhe Song1,2
1SketchX, CVSSP, University of Surrey, United Kingdom.
2iFlyTek-Surrey Joint Research Centre on Artificial Intelligence.
{a.bhunia, p.chowdhury, a.sain<EMAIL_ADDRESS>
###### Abstract

Visual text recognition is undoubtedly one of the most extensively researched
topics in computer vision. Great progress have been made to date, with the
latest models starting to focus on the more practical “in-the-wild” setting.
However, a salient problem still hinders practical deployment – prior state-
of-arts mostly struggle with recognising unseen (or rarely seen) character
sequences. In this paper, we put forward a novel framework to specifically
tackle this “unseen” problem. Our framework is iterative in nature, in that it
utilises predicted knowledge of character sequences from a previous iteration,
to augment the main network in improving the next prediction. Key to our
success is a unique cross-modal variational autoencoder to act as a feedback
module, which is trained with the presence of textual error distribution data.
This module importantly translate a discrete predicted character space, to a
continuous affine transformation parameter space used to condition the visual
feature map at next iteration. Experiments on common datasets have shown
competitive performance over state-of-the-arts under the conventional setting.
Most importantly, under the new disjoint setup where train-test labels are
mutually exclusive, ours offers the best performance thus showcasing the
capability of generalising onto unseen words (Figure 1 offers a summary).

##  1 Introduction

Text recognition being a longstanding problem in computer vision plays a
pivotal role in a diverse set of applications, ranging from OCR systems [4,
42, 48, 54], navigation and guiding board recognition [10], to more recent
ones such as visual question answering [5]. With the advance of deep learning
[50, 62, 10, 43], recognition accuracy have notably increased over traditional
methods [36]. Research focus has thus shifted to the more practical “in-the-
wild” setting in an attempt towards ubiquity. Of these, irregular scene text
recognition [50, 10, 58, 60] has gained considerable attention, yet the focus
is placed on irregular-image rectification process [62, 58] other than the
core recognition problem itself.

Figure 1:  Figure shows how the performance of baseline model [50] is limited
under disjoint setup where testing words are not encountered during training.
Our method performs way better than the baseline in the disjoint setup,
reducing the performance gap with standard setup and showcasing its potential
onto rarely seen words. Nevertheless, improvement in standard setup can be
noticed over all datasets as well.

In this paper, we continue this push towards practicality, albeit with a
different perspective – we importantly focus on the understudied problem of
unseen (or rarely seen) word recognition, where no (or limited) word image of
a particular character sequence is present during training. Our motivation is
straightforward – humans can recognise a word image, even when it falls beyond
the scope of known vocabulary. In fact, robustness of a text recognition
framework largely depends on its performance on rarely or unseen words [52].
Note that unlike the conventional zero-shot [59] setting where the transfer
happens on class-level, here the combination of characters is “unseen”
although the characters individually have come up in training. The fact that
the sequences not being encountered during training is what makes this task
challenging. Our solution for this “unseen” problem is intuitive: (i) we
leverage an iterative framework with a feedback mechanism to give the model a
chance to re-visit its false predictions, and (ii) we explicitly ask such
feedback to encapsulate useful information that would help the model to
correct itself at the following iteration.

Our first contribution is therefore an iterative framework, where characters
predicted in the previous iteration provide clues through a feedback loop [17]
to enhance performance in the subsequent iterations. This is fundamentally
different to current state-of-the-arts [50, 10, 29], most of which adapt a
feed-forward framework consisting of three-components (feature-extracting
backbone, bidirectional-RNN encoder, and attention-based recurrent decoder).
Despite the attention mechanism, its single-pass nature still dictates wrong
predictions, thereby leaving no chance for the model to recover. To this end,
our iterative design enables the revision of incorrect intermediate
predictions in its subsequent steps, via a novel cross-modal (i.e., text
prediction to image feature-maps) feedback mechanism. The key to our success
lies with how feedback is progressed at each iteration. A naive solution might
be to apply an independent spelling correction network [13, 56] chained
serially to a basic text recognition model. Apart from not being end-to-end
trainable, this also ignores the intermediate visual features from the
recognition network, ultimately bisecting the feedback loop. We on the other
hand advocate that earlier word predictions (text labels) should be fed back
cross-modal to the main text recognition network and directly modulate the
visual feature maps at the next iteration. That is, the feedback module
triggers a mapping from the discrete predicated label space, to a continuous
space of affine transformation parameters (akin to [41]) which are
consequently used to condition visual features (hence closing the feedback
loop).

Simply knowing how feedback works is not enough – we still need to devise what
information should be fed back to give a model its best shot at rectifying
itself. For this, we resort to distilling knowledge from textual error
distributions collected from state-of-the-art text recognition models – this
is akin to humans who use prior experiences to help them to make corrections.
For example, ‘$hello$’ might be wrongly predicted as ‘$nello$’ or ‘$bello$’
due to partial structural similarity of ‘$h$’ with ‘$n$’ or ‘$b$’. By
distilling such error distributions into the feedback module (during training
only), the model will gain knowledge of correct character associations. Our
second contribution is therefore designing the feedback module via a
conditional variational auto-encoder (CVAE) [51] that learns from such error
distributions. More specifically, we augment the vanilla CVAE with an
_auxiliary decoder_ that tries to directly reconstruct the correct word, given
any incorrect prediction at each iteration. Note that deterministic
alternatives such as typical feedback networks [47, 17] or spelling correction
(prediction refining) networks, [13, 56] would not work well since they do not
model the uncertainty among multiple erroneous alternatives, dictating a
variational formulation like ours.

Our contributions are: [a] We for the first time propose an _iterative
approach_ to specifically tackle the “unseen” text recognition problem. [b] We
design a conditional variational autoencoder to act as a feedback module,
which works cross-modal to propagate predicted text labels from an earlier
iteration to condition the visual features from the main network. [c] Our
novel cross-modal feedback module is trained by distilling knowledge learned
from _textual error distributions_ that model multiple erroneous character
sequences to a given candidate word.

Experiments confirm our framework to be capable of adopting unseen words
better than state-of-the-art frameworks on various public scene-text
recognition and handwriting recognition datasets. Further ablative studies
demonstrate the superiority of our iterative framework over naive spell
checking [56, 13] and language model alternatives [22], and that the proposed
feedback module can be plug-and-play with more than one base network.

##  2 Related Works

Text Recognition: With the rising applicability of deep learning methods,
Jaderberg _et al_. [20] employed convolution neural network for text
recognition, but such methods were constrained to dictionary words. Although
this limitation was eliminated by Jaderberg _et al_. [18], it still needed
huge resources for character level localisation. Sequence discriminative
training using connectionist temporal classification (CTC) [11] coupled with
recurrent neural networks, dealt with the need for character level
localisation. This lead to an end-to-end trainable convolutional recurrent
neural network for reading texts [48]. This was further enhanced by
incorporating the idea of attention [3] for text recognition [26, 49]. Usually
a two-fold process is implemented [58, 49, 50, 62], where an irregular image
is first passed through a rectification network, and then followed by a text
recognition network. Ideas like 2D attention mechanism, focusing attention
network (FAN) [9] has been explored recently along-with the possibility of
enhancing text reading accuracy using synthetically generated large datasets
[63]. Despite such extensive research, reading irregular curved texts had not
been explored much in details until recently in [10], which describes how
arbitrarily oriented texts can be read by extracting four directional features
from the 2D input image. Baek _et al_. [2] has conducted a comparative study
where different popular text recognition architectures were trained in a
similar setting. Hence it can be observed that although recent works in text
reading have emphasised on designing a better rectification network [62, 58],
all such researches [31, 57] essentially used an off-the-shelf [48]
recognition module. On the other side, handwriting recognition poses a tougher
challenge owing to a free flow nature [4] of writing. Poznanski _et al_. [42]
employed a ConvNet to estimate an n-gram frequency profile along with a large
dictionary having true frequency profiles for recognition.

Feedback Mechanism:  Carreira _et al_. [7] augments input space based on a
corrective signal output manifold, improving on human pose estimation and
generalising to instance segmentation tasks [28]. While Wei _et al_. [55] used
a ConvNet followed by a similar module having a larger receptive field, Newell
_et al_. [37] developed an hour-glass network design, stacked together for
merging information across all input scales. Zamir _et al_. [61] proposed a
novel network architecture aligned with a feedback notion, functionally akin
to ResNet architecture. Others include instance segmentation [28], few-shot
learning [64], object detection [8], super resolution [35] and image
generation [47, 17]. However, we here introduce cross-modal iterative feedback
for text recognition with a conditional variational autoencoder that enables
modelling of a prior knowledge of linguistically correct character-sequences.

Error Correction: Earlier efforts to utilise this idea of refining character-
sequence prediction can be found in automatic speech recognition (ASR)
community. In works such as Rozovskaya _et al_. [46] and Hans _et al_. [15]
preposition errors were detected using classifiers. Grammatical error
correction was approached using statistical machine translation methods by Ng
_et al_. [38]. Recently,the idea of using recurrent encoder-decoder
architecture in conjunction with attention mechanism was presented by Xie _et
al_. [56] to address complex orthographic errors. Later this idea was adopted
by Guo _et al_. [13] for tasks related to ASR.

Figure 2: Training of the network consists of 2 steps: (i) Predicting Y (green
arrow); (ii) Refining Y to $Y^{\prime}$ using feedback mechanism. Feedback
module excluding $F_{\mathcal{P}}$ can be trained using additional text-only
data $\mathcal{G}$ (red). However, when trained using prediction $Y$, the
entire path is followed (red+blue). Inference in the model consists of
predicting $\mathrm{Y}^{t}$ using any arbitrary number of correction steps.

##  3 Methodology

Instead of generating results in a single feed forward pass [50, 30, 58, 65],
we propose an iterative approach towards text recognition. As our work solely
contributes to the text recognition part, we have refrained from detailing on
the initial rectification network. We have used an off-the-shelf rectification
network based on Spatial Transformer Network [21] and Thin Plate Splines [2]
from Shi _et al_. [50].

###  3.1 Text Recognition Module

The rectified image received from the rectification network [50] is fed into
this text recognition network $\mathbf{T}$ aiming to produce a character
sequence $\mathrm{Y}=\\{y_{1},y_{2},...,y_{K}\\}$, where $K$ denotes the
variable length of text. Given an image $\mathrm{I}\in\mathbb{R}^{H\times
W\times C}$, the convolutional feature extractor tries to learn rich visual
information and produce a feature map of size $\mathbb{R}^{H^{\prime}\times
W^{\prime}\times D}$, where $H^{\prime}$, $W^{\prime}$, and $D$ are the
height, width and number of channels in the output feature map respectively.
That output is reshaped into a sequence of feature vectors
$\mathrm{B}=[b_{1},b_{2},...,b_{L}]$, where $L=H^{\prime}\times W^{\prime}$,
and $b_{i}\in\mathbb{R}^{D}$. Every D dimensional feature vector $b_{i}$
encodes a particular local image region based on its receptive fields.
Thereafter a bidirectional-LSTM is employed to capture the long range
dependency in both the directions, thus alleviating the constraints of limited
receptive fields. It outputs an updated feature sequence of same length,
denoted by $\mathrm{H}\in[h_{1},h_{2},...,h_{L}]$. Following this $y_{k}$ is
decoded based on three factors viz; bidirectional-encoder output $\mathrm{H}$,
the previous internal state $s_{k-1}$, and the character $y_{k-1}$ predicted
in the last step. At time step $k$, a recurrent decoder network generates an
output vector $o_{k}$ and a new state vector $s_{k}$, defined as:
$\mathrm{(o_{k},s_{k})=RNN(s_{k-1},[g_{k},E(y_{k-1})])}$ where $g_{k}$ is the
glimpse vector [50] that encodes the information from specific relevant parts
of the encoded feature $\mathrm{H}$ to predict $y_{k}$; $\mathrm{E}$ is an
embedding layer, and $[\cdot]$ signifies a concatenation operation. Here,
$g_{k}$ is computed as:
$g_{k}=\sum_{i=0}^{L}\left(\frac{\exp(a_{k,i})}{\sum_{j=0}^{L}\exp(a_{k,j})}\right)h_{i}$
and, attention score
$\mathrm{a_{k,i}=v^{\top}tanh(W_{s}s_{k-1}+W_{h}h_{i}+b_{a})}$, where
$\mathrm{v},\mathrm{W_{s}},\mathrm{W_{h}},\mathrm{b_{a}}$ are the learnable
parameters. Finally the current step character $y_{k}$ is predicted by:
$\mathrm{p(y_{k})=softmax(W_{o}o_{k}+b_{o})}$ where $W_{o}$ and $b_{o}$ are
trainable parameters.

###  3.2 Cross-Modal Variational Feedback

Overview: Unlike previous attempts of devising mostly deterministic feedback
modules [17, 47, 61], we propose a Cross-Modal Variational Feedback network
instilling benefits of variational autoencoder (VAE) [25], a powerful class of
probabilistic models. Let us consider a text recognition network $\mathbf{T}$
that has been dissected into two parts, namely $\mathbf{T_{A}}$ and
$\mathbf{T_{B}}$ where the particular position of dissection is obtained
empirically as described in section 4.3. The prior knowledge from the
resultant discrete character space is modelled using a _Feedback Network_
$\mathbf{F}$ by predicting affine transformation parameters. Such parameters
modulate the output activation map of $\mathbf{T_{A}}$, as
$\mathrm{\Psi=T_{A}(I)}\in\mathbb{R}^{\hat{H}\times\hat{W}\times\hat{T}}$, via
a designed feedback conditioning layer $\mathrm{\Phi}$. In other words, for
iteration step t, the feedback network takes the preceding iteration’s output
$\mathrm{Y^{t-1}}$ as its input and predicts the transformation parameters
$\mathcal{P}^{t}$ as its output. As a result it learns the mapping:
$\mathrm{\mathbf{F}:Y\rightarrow\mathcal{P}}$, such that feedback conditioning
layer $\mathrm{\Phi}$ modulates $\mathrm{\Psi}$ based on $\mathcal{P}^{t}$.
This can be depicted as $\mathrm{\hat{\Psi^{t}}=\Phi(\Psi;\mathcal{P}^{t})}$
where $\mathrm{\hat{\Psi^{t}}}$ being fed to $\mathbf{T_{B}}$ predicts
$\mathrm{Y^{t}}$ with higher precision.

Feedback Conditioning Layer: The primary objective of this layer is the
propagation of prior knowledge from previous feed-forward pass prediction to
$\mathbf{T}$. This action couples the rich visual information extracted by
$\mathbf{T_{A}}$, with the prior feedback signal coming from earlier
prediction. A noteworthy mention in this context would be the work by Perez
_et al_. [41], where a general purpose conditioning layer FiLM has been
designed based on simple feature-wise affine transformation operation for
visual reasoning. Works involving visual-question-answering [41], image style
transfer [16] and semantic image synthesis [39] have been seen to endorse a
similar idea as well. Based on some prior or conditional information, the
intermediate activation map $\mathrm{\Psi}$ could be modulated as:
$\mathrm{\hat{\Psi}=\Psi\odot\gamma+\omega}$, where $\mathrm{\gamma}$,
$\mathrm{\omega}$ are global affine transformation parameters. They both have
dimensions $\mathbb{R}^{\hat{T}}$, and are usually predicted by a network
receiving the conditional information as input. In lieu of transforming each
channel globally, we allow local transformations [39] that attune each spatial
position of the activation map. Following earlier mathematical notations and
assumptions, the feedback conditioning layer can be formulated as:
$\mathrm{\hat{\Psi}=\Psi\odot\Gamma+\Omega}$ where
$\\{\Gamma,\Omega\\}\triangleq\mathcal{P}$ are the local transformation
parameters predicted by the feedback network having dimension of
$\mathbb{R}^{\hat{H}\times\hat{W}\times\hat{T}}$, similar to $\mathrm{\Psi}$.
This layer couples the prediction $Y$ with visual feature $\mathrm{\Psi}$ by
scaling, shifting and ReLU influenced selective thresholding, alternatively.
Compared to global tuning [41], such local harmonisation of features ensure a
better fine-grained control over the activations at each layer.

Feedback Network: Our goal is to model a conditional distribution
$p(\mathcal{P}|Y)$ from a discrete predicted character space $Y$ to the
transformation parameter space $\mathcal{P}$ of feedback conditioning layer
via a feedback network based on CVAE [51]. Sohn _et al_. [51] has shown that
the variational lower bound of this conditional distribution can be written
as:

$\mathrm{\mathcal{\widetilde{L}}(Y,\mathcal{P};\theta,\psi)=-KL(q_{\psi}(z|\mathcal{P},Y)||p_{\theta}(z|Y))+}\\\
\mathrm{\mathbb{E}_{q_{\psi}}[log\;p(\mathcal{P}|z,Y)]\leq
log\;p(\mathcal{P}|Y)}$ (1)

where $z$ is a latent variable assumed to follow a multivariate Gaussian
distribution with a diagonal covariance matrix. Due to intractability of true
posterior, we approximate the posterior distribution of $z$ through a
recognition neural network $q_{\psi}(z|\mathcal{P},Y)$. The prior distribution
of $z$ given $\mathrm{Y}$ is modelled through a prior network
$p_{\theta}(z|Y)$. For more details about CVAE, we refer to [51].

(i) Ideally speaking, $\mathcal{P}$ is supposed to adjust the activation map
$\mathrm{\Psi}$ in a way that predicts $\hat{Y}$ when passed through a fixed
$\mathbf{T_{B}}$. In other words, for time-step $t$, given $\mathcal{P}^{t}$
predicted by the feedback network with a conditioning on $Y^{t-1}$, the
modulated feature map $\noindent{\hat{\Psi^{t}}}$ is fed into $\mathbf{T_{B}}$
obtains the output of next iteration $\mathrm{Y^{\prime}}$. Therefore,
$\mathrm{Y^{\prime}=\mathbf{T_{B}}(\hat{\Psi^{t}})}$, where
$\mathrm{\hat{\Psi^{t}}=\Phi(\Psi;\mathcal{P}^{t})}$. Thus, minimizing the
cross-entropy loss between $Y^{\prime}$ and $\hat{Y}$ is equivalent to
maximizing the likelihood of $\mathcal{P}$.

(ii) We assume that posterior of $z$ depends on the actual ground-truth label
$\hat{Y}$ instead of $\mathcal{P}$, so $q_{\psi}(z|\mathcal{P},Y)\approx
q_{\psi}(z|\hat{Y},Y)$ which effectively makes the latent space $z$ aware of
exact ground-truth character sequence $\hat{Y}$.

(iii) Inspired by the auxiliary task approach towards improving primary task
objective [66], we aim to decode the ground truth character sequence $\hat{Y}$
directly from $z$ by using an auxiliary character sequence decoder. Firstly,
this approach tackles the problem of vanishing latent variable [6] and
provides better gradient to regularize the learning of feedback module.
Secondly, we discover a choice of training our feedback module (refer Figure
2) via relativistic information of prediction:ground-truth pairs (say
$\mathcal{G}$) generated from other state-of-the-arts, instead of depending on
$\mathbf{T}$ predicted $Y$ alone. This helps the module in learning an
associative relation between candidate correct words and closely related
erroneous instances. Loosely speaking ‘$hello$’ might be predicted as
‘$nello$’ or ‘$bello$’ due to a partial structural similarity of ‘$h$’ with
‘$n$’ or ‘$b$’. Learning this sense from _error distribution_ imparts the
model a semantic knowledge of required character association to form a valid
word. Additionally, using text-only data $\mathcal{G}$ alleviates the issue of
limited availability of image-paired datasets during training.

Hence, we adapt Eqn. 1 for our feedback network to generate a prior knowledge
$\mathcal{P}^{*}$, instead of transformation parameters only. This prior
knowledge has two components. One encapsulates relationship between $Y$ and
$\hat{Y}$, while the other generates $\mathcal{P}$ and injects $Y$ into
$\mathbf{T}$ for next prediction. Therefore adopting the aforementioned
variational lower bound expression (Eqn. 1), and assuming conditional
independence of those two knowledge components (given $z$ and $Y$) denoted by
$\mathrm{p(\mathcal{P}^{*}|z,Y)=p(\mathcal{P}|z,Y)p(\hat{Y}|z,Y)}$, we get a
modified lower bound as:

$\mathrm{\mathcal{\widetilde{L^{\prime}}}(Y,\mathcal{P}^{*};\theta,\psi)=-KL(q_{\psi}(z|\hat{Y},Y)||p_{\theta}(z|Y))+}\\\
\mathrm{\mathbb{E}_{q_{\psi}}[log\;p(\mathcal{P}|z,Y)]+\mathbb{E}_{q_{\psi}}[log\;p(\hat{Y}|z,Y)]}$
(2)

Network Components: Ignoring the time-step notation, let us consider any word
image $I$ having ground-truth $\hat{Y}$, that undergoes the first forward-pass
of $\mathbf{T}$ predicting $Y$ and $Y^{\prime}$ in current and successive
post-feedback iterations respectively. During training, we obtain an embedding
representation of both $\hat{Y}$ and $Y$ through a shared encoder network
$\mathbf{F}_{enc}$: $\hat{Y}_{enc}=\mathbf{F}_{enc}(\hat{Y})$ and
$Y_{enc}=\mathbf{F}_{enc}(Y)$. Moving on we have two independent branches: A
posterior network $\mathbf{F}_{post}$ to estimate parameters of posterior
distribution, and a prior network $\mathbf{F}_{prior}$ to do the same for
prior distribution. Following this, we get:
$\mathrm{\mu_{post},\sigma_{post}=\mathbf{F}_{post}([Y_{enc},\hat{Y}_{enc}])}$
and $\mathrm{\mu_{prior},\sigma_{prior}=\mathbf{F}_{prior}(Y_{enc})}$. A
latent variable $z$ is sampled from the posterior (or prior during testing)
distribution and merged with $Y_{enc}$ before feeding it to the auxiliary
ground-truth character sequence decoder $\mathbf{F}_{aux}$ and transformation
parameter prediction sub-module $\mathbf{F}_{\mathcal{P}}$. Therefore we have,
$\mathcal{P}=\mathbf{F}_{\mathcal{P}}([Y_{enc},z])$, and
$\bar{Y}=\mathbf{F}_{aux}([Y_{enc},z])$ where $\mathcal{P}$ encapsulates both
$\Gamma$ and $\Omega$, and $\mathbf{\bar{Y}}$ is output from the auxiliary
decoder ${F}_{aux}$. Thereafter, we evaluate the prediction of next iteration
as: $\mathrm{Y^{\prime}=\mathbf{T_{B}}(\hat{\Psi})}$, where
$\mathrm{\hat{\Psi}=\Phi(\Psi;\mathcal{P}})$. Please refer to Figure 2 for
clarity.

Learning Objectives: Our baseline text recognition network $\mathbf{T}$
(parameters $\mathrm{\mathbf{\theta_{T}}}$) is trained using Cross-Entropy
(ce) loss summed over the ground-truth output sequence $\mathrm{\hat{Y}}$

$\mathrm{L^{\mathbf{\theta_{T}}}=\mathrm{L_{ce}(Y,\hat{Y})=-\sum_{k=1}^{K}\hat{y_{k}}logP(y_{k}|I,\hat{y_{k-1}}})}\vspace{-0.3cm}$
(3)

Feedback module $\mathbf{F}$ is to be trained from two input sources: (a) by
using the prediction $Y$ obtained from $\mathbf{T}$. In cases where the
forward-pass prediction $Y$ is accurate the very first time, a diverged
prediction value in the next iteration is highly undesirable. Hence, along
with the lower bound (Eqn. 2), we impose a monotonically decreasing constraint
$L_{c}$. This enforces the loss value (Eqn. 3) related to the current
iteration $\\{Y^{\prime},\hat{Y}\\}$ to be lesser than its previous
$\\{Y,\hat{Y}\\}$, thus converging predictions to a higher precision. Hence,
we optimize all the parameters $\mathrm{\mathbf{\theta_{F}}}$ of feedback
module using:

$\mathrm{L^{\mathbf{\theta_{F}}}=\lambda_{1}L_{ce}(Y^{\prime},\hat{Y})+\lambda_{2}L_{ce}(\bar{Y},\hat{Y})+\lambda_{3}L_{KL}+\lambda_{4}L_{c}}\\\
\mathrm{where,L_{c}=max(0,L_{ce}(Y^{\prime},\hat{Y})-L_{ce}(Y,\hat{Y}))}$ (4)

(b) By using pre-collected text-only data $\mathcal{G}$ generated from
existing text-recognition methods [30, 10, 2, 50]. Doing so develops a
semantic sense of associative relation between candidate correct words and
erroneous alternatives. Keeping $F_{\mathcal{P}}$ fixed, rest of the feedback
module (parameters denoted by $\mathbf{\theta_{F^{\prime}}}$) is optimised
solely using auxiliary decoder reconstruction loss and KL divergence loss as:

$\mathrm{L^{\mathbf{\theta_{F^{\prime}}}}=\lambda_{2}L_{ce}(\bar{Y},\hat{Y})+\lambda_{3}L_{KL}}$
(5)

During testing we exclude both $\mathbf{F}_{aux}$ and $\mathbf{F}_{post}$,
where iterative prediction is done using the transformation parameter
predicted by $\mathbf{F}_{\mathcal{P}}$ (see Figure 2).

Comparative Discussions: While state-of-the-art text recognition frameworks
model a conditional distribution $\mathrm{p(Y|I)}$, our modelling objective is
$\mathrm{p(Y^{t}|Y^{t-1},I)}$. This could be decoupled into two marginal
distributions related via a transformation parameter space $\mathcal{P}^{t}$
(more strictly prior knowledge $\mathcal{P}^{*t}$). Assuming the obvious
conditional independence, we reformulate it as:
$\mathrm{p(Y^{t}|Y^{t-1},I)=p(Y^{t}|I,\mathcal{P}^{t})\times
p(\mathcal{P}^{t}|Y^{t-1})}$, where $\mathrm{p(Y^{t}|I,\mathcal{P}^{t})}$ is
our modified feed forward text recognition model and
$\mathrm{p(\mathcal{P}^{t}|Y^{t-1})}$ resembles our feedback network.

Algorithm 1 Training algorithm of the proposed framework

1:Input: Image and ground-truth pairs $\mathcal{D}$; prediction and ground-
truth pairs $\mathcal{G}$.

2:Initialise hyper params: $\alpha_{1}$, $\alpha_{2}$ be learning rate for
$\mathbf{T}$, $\mathbf{F}$ respectively.

3:Initialise model params: $\theta_{T}$, $\theta_{F}$
($\theta_{F^{\prime}}\subset\theta_{F}$ excluding $F_{\mathcal{P}}$)

4:while not done training do

5: Sample a mini-batch $\mathcal{D}_{i}$ from $\mathcal{D}$

6: Update
$\theta_{T}:=\theta_{T}-\alpha_{1}\nabla_{\theta_{T}}(L^{\mathbf{\theta_{T}}})$
$\triangleright$ Eqn. 3

7: Update
$\theta_{F}:=\theta_{F}-\alpha_{2}\nabla_{\theta_{F}}(L^{\mathbf{\theta_{F}}})$
$\triangleright$ Eqn. 4

8: Sample a mini-batch $\mathcal{G}_{i}$ from $\mathcal{G}$

9: Update
$\theta_{F^{\prime}}:=\theta_{F^{\prime}}-\alpha_{2}\nabla_{\theta_{F^{\prime}}}(L^{\mathbf{\theta_{F^{\prime}}}})$
$\triangleright$ Eqn. 5

10:end while

11:Output: $\theta_{T}$, $\theta_{F}$

##  4 Experiments

Table 1: Comparison of unconstrained WRA for novel words not encountered
during training. $t=0$ signifies no feedback.

Methods | IIIT5K | SVT | IC13 | IC15 | SVTP | CUTE80 | IAM | RIMES
---|---|---|---|---|---|---|---|---
$\left\\{\begin{array}[]{l}\text{Shi \emph{et al}.\hbox{} \cite[cite]{[\@@bibref{}{ShiBaiPAMI2019}{}{}]} (t=0) No-Feedback}\\\ \text{Baseline Seq-SCM}\\\ \text{Baseline Deterministic-Feedback}\\\ \text{Shi \emph{et al}.\hbox{} \cite[cite]{[\@@bibref{}{ShiBaiPAMI2019}{}{}]} {+ CVAE-Feedback} (t=1)}\\\ \text{Shi \emph{et al}.\hbox{} \cite[cite]{[\@@bibref{}{ShiBaiPAMI2019}{}{}]} {+ CVAE-Feedback} (t=2)}\\\ \text{Shi \emph{et al}.\hbox{} \cite[cite]{[\@@bibref{}{ShiBaiPAMI2019}{}{}]} {+ CVAE-Feedback} (t=3)}\\\ \end{array}\right.$ | 84.3 | 84.2 | 82.6 | 65.7 | 74.4 | 61.6 | 54.3 | 59.7
85.6 | 84.1 | 83.7 | 65.5 | 75.8 | 63.4 | 57.6 | 63.7
87.9 | 86.8 | 85.9 | 70.4 | 78.6 | 64.7 | 59.9 | 69.7
90.6 | 88.7 | 89.3 | 72.2 | 79.6 | 65.1 | 64.5 | 70.4
90.8 | 88.9 | 89.4 | 72.6 | 79.6 | 66.1 | 64.8 | 70.5
90.7 | 88.8 | 89.4 | 72.5 | 79.6 | 65.8 | 64.6 | 70.3
Relative Gain (t=0 vs t=2) | 6.5$\uparrow$ | 4.7$\uparrow$ | 6.8$\uparrow$ | 6.9$\uparrow$ | 5.2$\uparrow$ | 4.5$\uparrow$ | 10.5$\uparrow$ | 10.8 $\uparrow$
$\left\\{\begin{array}[]{l}\text{Show, Attend and Read \cite[cite]{[\@@bibref{}{li2019show}{}{}]} (t=0) No-Feedback}\\\ \text{Show, Attend and Read \cite[cite]{[\@@bibref{}{li2019show}{}{}]} {+ CVAE-Feedback} (t=2)}\\\ \end{array}\right.$ | 85.8 | 86.5 | 84.7 | 68.4 | 82.2 | 71.8 | 57.9 | 62.8
91.5 | 90.5 | 91.2 | 74.8 | 87.1 | 75.0 | 68.0 | 73.0
Relative Gain (t=0 vs t=2) | 5.7$\uparrow$ | 4.0$\uparrow$ | 6.5$\uparrow$ | 6.4$\uparrow$ | 4.9$\uparrow$ | 3.2$\uparrow$ | 10.1$\uparrow$ | 10.2 $\uparrow$
$\left\\{\begin{array}[]{l}\text{SCATTER \cite[cite]{[\@@bibref{}{litman2020scatter}{}{}]} (t=0) No-Feedback}\\\ \text{SCATTER \cite[cite]{[\@@bibref{}{litman2020scatter}{}{}]} {+ CVAE-Feedback} (t=2) }\\\ \end{array}\right.$ | 84.7 | 86.9 | 84.3 | 71.8 | 82.6 | 69.3 | 59.0 | 62.9
91.1 | 90.9 | 90.0 | 77.7 | 87.3 | 72.7 | 68.7 | 73.1
Relative Gain (t=0 vs t=2) | 6.4$\uparrow$ | 4.0$\uparrow$ | 6.6$\uparrow$ | 5.9$\uparrow$ | 4.7$\uparrow$ | 3.4$\uparrow$ | 9.7$\uparrow$ | 10.2 $\uparrow$
|  |  |  |  |  |  |  |

Datasets: We train our method using an approach similar to [62, 58, 2, 10, 50,
30], on synthetic datasets such as Synth90k [19] and SynthText [14] that hold
8 and 6 million images respectively. Evaluation is done on: IIIT5K-Words,
Street View Text (SVT), SVT-Perspective (SVT-P), ICDAR 2013 (IC13), ICDAR 2015
(IC15), and CUTE80. IIIT5K-Words [34] presents randomly picked 3000 cropped
word images. Street View Text [53] contains 647 images, mostly being blurred,
noisy or having low resolution. SVT-Perspective [44] offers 645 samples from
side-view angle snapshots having perspective distortion. ICDAR2013 [24]
presents 1015 words while ICDAR2015 [23] has 2077 images, 200 of which are
irregular. CUTE80 [45] distinguishes itself by presenting 288 cropped high
quality curved text images. Handwritten Text Recognition (HTR) and Scene-Text
Recognition (STR) both share a common objective in terms of recognition, which
is usually handled by similar network architecture. Hence, we validate our
results on two different public HTR datasets. The evaluation setup described
in [4] is employed on two large standard datasets viz, IAM [33] containing
1,15,320 words and RIMES having 66,982 words. For IAM we use the same
partition for training, validation and testing as provided. For RIMES, we
follow the partition released by ICDAR 2011 competition.

###  4.1 Implementation Details

Network Design: Keeping text rectification and recognition networks similar to
Shi _et al_. [50], we implement our framework using open sourced codes [2, 30]
in PyTorch [40]. A bi-directional LSTM of hidden size 256 is used in designing
$F_{enc}$ of our feedback module which accepts a one layer MLP embedded
128-dimensional representation of discrete character sequences. For both
posterior $F_{post}$ and prior $F_{prior}$ networks, we use 2 layer MLPs with
tanh non-linearity. The latent variable $z$ has a size of 256. The auxiliary
decoder $F_{aux}$ is a one layer LSTM decoder whose initial hidden state is
initialized by applying a FC-layer on the concatenated representation of
$Y_{enc}$ and sampled $z$. The parameter prediction network $F_{\mathcal{P}}$
is a convolutional decoder network inspired from [67]. The first layer is a
fully-connected layer implemented through a 1x1 convolution that maps to a
tensor of size equal to the last CNN layer of $\mathbf{T}$ via a reshaping
operation. Thereafter we introduce a sequence of residual decoder blocks which
upsamples feature maps to higher spatial dimensions in the reversed order of
down-sampling followed by $\mathbf{T}$. In other words, if a ResNet encoder
block in $\mathbf{T}$ halves the height of feature map, the corresponding
ResNet decoder block [67] in $\mathbf{F}_{\mathcal{P}}$ will double it. This
strategy essentially formulates intermediate feature maps of a decoder ResNet
block ($\mathbf{F}_{\mathcal{P}}$), whose spatial size is similar to the
corresponding layer in the encoder ResNet block ($\mathbf{T}$), thus
predicting required affine transformation parameters of similar dimensions as
well. Since we need to predict both $\Gamma$ and $\Omega$, we double the
number of convolutional filters in the last layer of
$\mathbf{F}_{\mathcal{P}}$ and split the output channel-wise to obtain
$\Gamma$ and $\Omega$ individually.

Training Details: It has been observed in practice, that warming up individual
components in the initial phase, followed by a joint training operation
provides better stability than training the entire framework at one go. Text
recognition network (T), along with rectification network, is trained using
ADADELTA optimizer having a learning rate of 1.0 and a batch size of 64.
Meanwhile Feedback module $\mathbf{F}$ is trained via Adam optimizer with a
learning rate 0.001, and gradient clipping at 5. In the warm-up phase,
firstly, text recognition and rectification networks are trained from a union
of MJSynth and SynthText datasets, for 600K iterations. The rectification
network is frozen thereafter. Then, to capture a linguistic prior from text-
data, the feedback module $\mathbf{F}$ is trained independently from
$\mathcal{G}$ for 300K iterations, thereby ignoring the $F_{\mathcal{P}}$ part
(Eqn. 5). Finally, keeping $\mathbf{T}$ fixed, we train the complete feedback
module using $Y$ (Eqn. 4), with the same training specifications for 300K
iterations. Now, for the joint training (see algorithm 1), after updating
$\mathbf{T}$, $\mathbf{F}$ is updated with the prediction $Y$ from
$\mathbf{T}$, as input. Thereafter, keeping $F_{\mathcal{P}}$ fixed,
$\mathbf{F}$ is updated using $\mathcal{G}$. During this training, we reduce
the learning rate of $\mathbf{T}$ to 0.01 which continues for 600K iterations.
Owing to corresponding data sizes in HTR, iterations for warm-up phases are
100K, 50K and 50K respectively, while for joint training it is 100K. For both
STR and HTR, we resize the image to 32x100 and train our model in a 11 GB
Nvidia RTX 2080-Ti GPU. $\lambda_{1}$, $\lambda_{2}$, $\lambda_{3}$ and
$\lambda_{4}$ has been assigned the values of 1, 1, 50 and 0.5 respectively
for the same purpose. In order to generate the text-only data $\mathcal{G}$,
we follow an approach similar to [68]. The entire training dataset is divided
into train-validation split in a cross validation setting, where top ten beam
search decoded hypotheses are collected from different state-of-the-art (SOTA)
models [30, 10, 2, 50], to harness (using open-source code) the error
information from closest possible erroneous alternatives. Such a collection
may consist of correctly or incorrectly predicted words. This requires the
feedback module to learn a language prior for fixing a wrongly predicted word,
as well as for a one-to-one character-sequence mapping for correctly predicted
words.

Figure 3: Unconstrained WRA on IAM dataset with varying _word length_ in (a)
CS, (b) DS setups. (c) Few samples which defeat single feed forward pass
mechanisms, but are acceptably recognised via our iterative framework in CS
setup.

###  4.2 Performance Analysis

Baselines: Aligned to our iterative approach we explore two alternatives as
baselines. Seq-SCN: Inspired from Automatic Speech Recognition community [56],
a naive baseline could be designed where we train an independent Spelling
Correction Module (SCM) based on sequence-to-sequence architecture from text-
only training data [13] consisting of paired model-hypothesis and
corresponding ground-truth. Deterministic-Feedback: Here, we simply replace
the CVAE based feedback module by a deterministic encoder(bi-LSTM)-decoder
(parameter prediction network) architecture along with Shi _et al_. [50].

New Evaluation Setup: Here we design a new disjoint train-test split (DS) in
addition to conventional train-test split (CS). While training we remove all
words from MJSynth and Synth90K whose truth-pairs appear in any of the
mentioned STR testing datasets. Additionally we ensure, $\mathcal{G}$ does not
contain any information from the testing set. Due to size constraint in HTR
datasets, we split it such that all word-image pairs corresponding to one
particular ground-truth character sequence must collectively fall in either
one of training or testing set, thus ensuring disjointedness. This evaluation
protocol grades our model’s recognition performance on word images whose
ground-truth character sequences never appeared in the training dataset. We
use it to verify generalising capability of our model for unseen or rarely
seen words. Furthermore, superiority of our model in this scenario confirms a
fair result on datasets having _less unique words_. As large datasets are
rarely available for text recognition (specifically handwriting) apart from
English, it is ideal to use a dataset created by collecting multiple instances
of a small set of unique words which thus need to be annotated just once per
unique word. To do so any model needs to learn character-specific fine-grained
details from a small available set of unique words, and generalise onto other
unseen character sequences. Please note that we re-train SOTA models [30, 10,
2, 50], used to collect the error distribution, by ensuring no words from
evaluation set appear in their training (ensuring no “leak” of information),
while collecting error distribution for DS setup.

Result Analysis: Along with the designed baselines, we incorporate our
iterative design on top of three popular state-of-the-art (SOTA) feed-forward
text recognition frameworks – a) Shi _et al_. [50], b) Show, Attend and Read
[27] c) SCATTER [29]. Show, Attend and Read [27] extends [50] by including 2D
attention and SCATTER [29] couples multiple BLSTM layers for richer context
modelling. We follow similar training protocol in [50, 27, 29] respectively.
Nevertheless, ours is a meta-framework and could be added on top of most SOTA
frameworks. Table 1 (highest scores are in red) depicts unconstrained word
recognition accuracy (WRA) on unseen words (DS setup). [i] Comparison with
Baselines: Seq-SCN performs inferior to our method as the rich visual feature
is not harnessed while refining the prediction. At times it fails to copy an
already accurate prediction, leading to a lower accuracy in certain datasets.
Deterministic-Feedback being an iterative framework, performs better than
other baselines at $t=2$, however, it lags behind our design since any
uncertainty handling potential is absent. [ii] Significant improvement under
DS setup: From Table 1, improvement due to our iterative pipeline is quite
evident in the DS scenario over three SOTA baselines [50, 27, 29] . Similarly,
in handwritten dataset (Table 1), the performance drop in DS setting is way
more severe than its STR counterpart. This signifies that HTR poses a greater
challenge due to its free-flow nature of writing. Improvement against Shi _et
al_. [50] reaches to 10.5% and 10.8%, without lexicon information
(unconstrained) in HTR dataset of IAM and RIMES respectively, while for STR
dataset of IC15 it secures a 6.9% rise in DS setup. [iii] Additional
Observations: Improvement at $t$=2 w.r.t $t$=0 is shown as relative gain where
our method outperforms fairly in CS setup, and largely in DS setup (Table 2).
In fact optimal WRA is seen at iteration $t=2$, which then diminishes.
Contrary to a possible impression, that our feedback module might remember the
erroneous pairings from $\mathcal{G}$, the improvement on “unseen” words
empirically validates against it. Figure 3 shows qualitative results.

Table 2: Comparison with SOTA results using standard setup [2].

Methods | IIIT5K | IC13 | IC15 | SVTP | CUTE80 | IAM
---|---|---|---|---|---|---
Yang _et al_. [58] | 94.4 | 93.9 | 78.7 | 80.8 | 87.5 | -
Luo _et al_. [30] | 91.2 | 92.4 | 68.8 | 76.1 | 77.4 | 82.1
Cheng _et al_. [10] | 87.0 | - | 68.2 | 73.0 | 76.8 | -
Zhang _et al_. [65] | 83.8 | - | - | - | - | -
Baek _et al_. [2] | 87.9 | 92.3 | 71.8 | 79.2 | 74.0 | -
Lyu _et al_. [32] | 94.0 | 92.7 | 76.3 | 82.3 | 86.8 | -
Zhan _et al_. [62] | 93.3 | - | 76.9 | 79.6 | 83.3 | -
Shi _et al_. [49] | 81.9 | - | - | - | - | 80.3
Cheng _et al_. [9] | 87.4 | 93.3 | 70.6 | - | - | -
$\circledast$ Shi _et al_. [50] | 93.4 | 91.8 | 76.1 | 78.5 | 79.5 | -
$\circledast$ Li _et al_. [27] | 95.0 | 94.0 | 78.8 | 86.4 | 89.6 | -
$\circledast$ Litman _et al_. [29] | 93.7 | 93.9 | 82.2 | 86.9 | 87.5 | -
Shi _et al_. [50] (t=0) | 93.2 | 91.6 | 75.9 | 78.2 | 79.3 | 82.3
Li _et al_. [27] (t=0) | 94.8 | 93.7 | 78.6 | 86.0 | 89.5 | 85.9
Litman _et al_. [29] (t=0) | 93.6 | 93.8 | 82.0 | 86.5 | 87.0 | 86.0
Baseline Seq-SCM | 93.4 | 91.8 | 75.8 | 78.5 | 79.9 | 82.9
Deterministic-Feed. | 93.5 | 92.7 | 77.1 | 79.6 | 80.5 | 85.6
[50]+CVAE-Feed. (t=2) | 94.9 | 93.7 | 78.8 | 80.9 | 82.9 | 87.5
[27] +CVAE-Feed.(t=2) | 96.3 | 95.4 | 81.4 | 88.5 | 91.0 | 89.7
[29] +CVAE-Feed.(t=2) | 95.2 | 95.7 | 84.6 | 88.9 | 89.7 | 90.3
|  |  |  |  |  |

###  4.3 Further Analysis and Insights

Ablation Study: We have done a thorough ablative study to justify the
contribution of every design choice on both IAM (HTR) and IC15 (STR) datasets
using Shi _et al_. [50] as baseline. [i] Significance of auxiliary decoder: On
removing this part along with its respective loss function from Eqn. 4 we see
a performance drop of 2.19%(1.98%) and 5.01%(2.94%) in the CS and DS setting
for IAM (IC15) dataset respectively, thus confirming its contribution. [ii]
Significance of monotonically decreasing constraint: Removing it, destabilizes
by 5.47% (3.87%) in DS setup, for IAM (IC15) datasets respectively, thus
confirming its importance. [iii] Significance of using error distribution:
Discarding data inclusion from $\mathcal{G}$(_error distribution_), leads to a
performance drop of 2.17% (1.87%) in conventional train-test split, and a
further drop of 4.9% (2.48%) in disjoint setup, for IAM (IC15) datasets.
Please refer to Table 4 for more analysis. [iv] Finding optimal block for
feedback: We evaluated the performance by providing a feedback signal into
every ResNet block of backbone feature extractor of $\mathbf{T}$ at a time.
Table 3 shows a complete analysis on both IAM and IC15 datasets in CS and DS
setups which shows the optimum result to be obtained by supplying feedback
signal to Block-3 of ResNet convolutional architecture. Moreover, local
transformation is seen to outperform the global one. [v] Performance with
varying text length It is often observed that any text recognition framework
struggles to recognize lengthy words. Owing to its iterative refining
approach, along with a modelled linguistic prior, our method shows a
considerably higher performance in comparison to no-feedback baseline on
increasing character sequence length, as shown in Figure 3. [vi] Computational
cost: Finally, we want to notify that benefit of any iterative pipeline [7, 8,
28] does incur extra computational expenses, be it text rectification [62] or
in our case text-recognition. A through study on complexity and speed analysis
(Intel(R) Xeon(R) W-2123 CPU @ 3.60GHz) in Table 5 reveals that $T_{B}$ takes
most time due to its sequential decoding operation, whereas $F$ adds minimal
burden. Please refer to _supplementary_ as well.

Table 3: WRA of using feedback after a specific ResNet Block (abbreviated as
‘Blk’) such as Block 1 $(16\times 50\times 64)$, Block 2 $(8\times 25\times
128)$, Block 3 $(4\times 25\times 256)$, Block 4 $(2\times 25\times 256)$,
Block 5 $(1\times 25\times 256)$ as described in ASTER [50].

Methods | Conventional Setup (CS) & Disjoint Setup (DS)
---|---
Blk_1 | Blk_2 | Blk_3 | Blk_4 | Blk_5
CS | DS | CS | DS | CS | DS | CS | DS | CS | DS
Global(IAM) | 84.7 | 59.9 | 85.5 | 60.8 | 86.7 | 61.9 | 86.2 | 60.8 | 84.5 | 58.5
Local(IAM) | 84.9 | 61.0 | 86.7 | 64.2 | 87.5 | 64.8 | 87.3 | 63.9 | 85.6 | 63.2
Global(IC15) | 78.5 | 68.6 | 76.6 | 70.2 | 78.6 | 71.4 | 78.5 | 70.4 | 78.4 | 69.6
Local(IC15) | 78.5 | 68.9 | 78.7 | 71.3 | 78.8 | 72.6 | 78.6 | 71.5 | 78.5 | 69.8

Table 4: Relative contribution (WRA) of three design choices behind training
Feedback Network for iterative prediction: (a) Regularisation constraint via
$L_{C}$ (Eqn. 4), (b) Modified variational lower bound for feedback network
accommodating $F_{aux}$, (c) Using $\mathcal{G}$ to capture the prior-
knowledge from error distribution.

Constraint | Auxiliary | Use Error | CS Setup | DS Setup
---|---|---|---|---
$L_{C}$ | Decoder $F_{aux}$ | Dist. $\mathcal{G}$ | IC15 | IAM | IC15 | IAM
✓ | - | - | 76.8 | 85.3 | 69.6 | 59.8
- | ✓ | ✓ | 76.6 | 84.5 | 68.7 | 59.3
✓ | ✓ | - | 76.9 | 85.3 | 70.1 | 59.9
✓ | ✓ | ✓ | 78.8 | 87.5 | 72.6 | 64.8

Feedback module vs Language Model: We could have substituted our iterative
approach towards refining text prediction with a Language model(LM). For
fairness, we use a state-of-the-art RNN-LM [13] trained from text corpus
(librispeech) at character level [1] that aims to predict the next likely
character. This could be fused with the text recognition decoder using two
state-of-the-art methods introduced in [12] via Shallow Fusion (weighted sum
of predicted scores) and Deep Fusion (fusing their hidden states). Our method
performs better in both CS and DS setups in comparison to these LM
integrations (Table 6). The limited performance of off-the-shelf LM [22] can
be attributed to: (i) LM is mostly used in speech recognition tasks, where
data is present at sentence-level which provides enough context. For distract
word recognition (our focus) however, LM cannot harness such extent of context
information. (ii) The LM corpus is significantly different from that used for
training word-image recognition system. This leads to a biased incorrectness
[13]. (iii) LM being an independent post processing step, not only ignores
rich visual features from the input image, but is also unaware of the error
distribution of the model. On the contrary, our model revisits the rich visual
features iteratively after every prediction, considering the error
distribution while training. Furthermore to align with the evaluation
standards for _unconstrained word recognition_ we cite all results in our work
using greedy decoding only – no LM based post-processing.

Table 5: Complexity and speed analysis against no. of parameters and flops
(Multiply-Add), for both individual component (left) and varying no, of
iterations (right), using CPU time during inference.

Network | Parameters | Multiply-Add | CPU |  | Iteration | CPU
---|---|---|---|---|---|---
$T_{A}$ | 5.4M | 1461M | 8.27ms |  | t=0 | 28.64ms
$T_{B}$ | 23.7M | 1428M | 12.82ms |  | t=1 | 43.69ms
F | 24.4M | 1897M | 2.19ms |  | t=2 | 58.66ms

Table 6: Comparison with different LM integration methods.

Methods | Conventional Setup & Disjoint Setup
---|---
IIIT5K | IC15 | CUTE80 | IAM | RIMES
CS | DS | CS | DS | CS | DS | CS | DS | CS | DS
Shi _et al_. [50] | 93.2 | 84.3 | 75.9 | 65.7 | 79.3 | 61.6 | 82.36 | 54.4 | 88.9 | 59.7
[50] \+ Shallow | 93.3 | 84.3 | 75.9 | 65.7 | 79.3 | 61.6 | 82.30 | 54.3 | 88.7 | 59.7
[50] \+ Deep | 93.5 | 85.6 | 76.5 | 67.4 | 81.2 | 62.9 | 83.67 | 57.5 | 89.9 | 63.6
[50] \+ CVAE-Feed. (t=2) | 94.9 | 90.8 | 78.8 | 72.6 | 82.9 | 66.1 | 87.5 | 64.8 | 92.7 | 70.5

##  5 Conclusion

Here we have proposed a novel _iterative approach_ towards text recognition.
Using a conditional variational autoencoder (CVAE) as a feedback module, the
knowledge of predicted character sequences is passed from the previous
iteration, into the main recognition network, improving subsequent
predictions. Our feedback network learns to use the _error distribution_ among
multiple character sequences that are closely related to a candidate word.
Experiments on various STR and HTR datasets show our network to outperform
others on the conventional setting, and more significantly on the more
practical disjoint (unseen) setting.

## References

  * [1] End-to-end automatic speech recognition systems - pytorch implementation.  https://github.com/Alexander-H-Liu/End-to-end-ASR-Pytorch.  Accessed on: 04-03-2021.
  * [2] Jeonghun Baek, Geewook Kim, Junyeop Lee, Sungrae Park, Dongyoon Han, Sangdoo Yun, Seong Joon Oh, and Hwalsuk Lee.  What is wrong with scene text recognition model comparisons? dataset and model analysis.  In ICCV, 2019.
  * [3] Dzmitry Bahdanau, Kyunghyun Cho, and Yoshua Bengio.  Neural machine translation by jointly learning to align and translate.  In ICLR, 2015.
  * [4] Ayan Kumar Bhunia, Abhirup Das, Ankan Kumar Bhunia, Perla Sai Raj Kishore, and Partha Pratim Roy.  Handwriting recognition in low-resource scripts using adversarial learning.  In CVPR, 2019.
  * [5] Ali Furkan Biten, Ruben Tito, Andres Mafla, Lluis Gomez, Marçal Rusiñol, Ernest Valveny, CV Jawahar, and Dimosthenis Karatzas.  Scene text visual question answering.  In CVPR, 2019.
  * [6] Samuel R. Bowman, Luke Vilnis, Oriol Vinyals, Andrew Dai, Rafal Jozefowicz, and Samy Bengio.  Generating sentences from a continuous space.  In CoNLL, 2016.
  * [7] João Carreira, Pulkit Agrawal, Katerina Fragkiadaki, and Jitendra Malik.  Human pose estimation with iterative error feedback.  In CVPR, 2016.
  * [8] Xinlei Chen, Li-Jia Li, Li Fei-Fei, and Abhinav Gupta.  Iterative visual reasoning beyond convolutions.  In CVPR, 2018.
  * [9] Zhanzhan Cheng, Fan Bai, Yunlu Xu, Gang Zheng, Shiliang Pu, and Shuigeng Zhou.  Focusing attention: Towards accurate text recognition in natural images.  In ICCV, 2017.
  * [10] Zhanzhan Cheng, Yangliu Xu, Fan Bai, Yi Niu, Shiliang Pu, and Shuigeng Zhou.  Aon: Towards arbitrarily-oriented text recognition.  In CVPR, 2018.
  * [11] Alex Graves, Santiago Fernández, Faustino Gomez, and Jürgen Schmidhuber.  Connectionist temporal classification: Labelling unsegmented sequence data with recurrent neural networks.  In ICML, 2006.
  * [12] Caglar Gulcehre, Orhan Firat, Kelvin Xu, Kyunghyun Cho, Loic Barrault, Huei-Chi Lin, Fethi Bougares, Holger Schwenk, and Yoshua Bengio.  On using monolingual corpora in neural machine translation.  arXiv preprint arXiv:1503.03535, 2015.
  * [13] Jinxi Guo, Tara N Sainath, and Ron J Weiss.  A spelling correction model for end-to-end speech recognition.  In ICASSP, 2019.
  * [14] Ankush Gupta, Andrea Vedaldi, and Andrew Zisserman.  Synthetic data for text localisation in natural images.  In CVPR, 2016.
  * [15] Na-Rae Han, Martin Chodorow, and Claudia Leakcock.  Detecting errors in english article usage by non-native speakers.  Natural Language Engineering, 2006.
  * [16] Xun Huang and Serge Belongie.  Arbitrary style transfer in real-time with adaptive instance normalization.  In ICCV, 2017.
  * [17] Minyoung Huh, Shao-Hua Sun, and Ning Zhang.  Feedback adversarial learning: Spatial feedback for improving generative adversarial networks.  In CVPR, 2019.
  * [18] Max Jaderberg, Andrea Simonyan, Karen Vidaldi, and Andrew Zisserman.  Deep structured output learning for unconstrained text recognition.  In ICLR, 2015.
  * [19] Max Jaderberg, Karen Simonyan, Andrea Vedaldi, and Andrew Zisserman.  Synthetic data and artificial neural networks for natural scene text recognition.  In NeurIPS Deep Learning Workshop, 2014.
  * [20] Max Jaderberg, Karen Simonyan, Andrea Vedaldi, and Andrew Zisserman.  Reading text in the wild with convolutional neuralnetworks.  IJCV, 2016.
  * [21] Max Jaderberg, Karen Simonyan, Andrew Zisserman, and koray kavukcuoglu.  Spatial transformer networks.  In NeurIPS, 2015.
  * [22] Lei Kang, Pau Riba, Mauricio Villegas, Alicia Fornés, and Marçal Rusiñol.  Candidate fusion: Integrating language modelling into a sequence-to-sequence handwritten word recognition architecture.  arXiv preprint arXiv:1912.10308, 2019.
  * [23] Dimosthenis Karatzas, Lluis Gomez-Bigorda, Anguelos Nicolaou, Suman Ghosh, Andrew Bagdanov, Masakazu Iwamura, Jiri Matas, Lukas Neumann, Vijay Ramaseshan Chandrasekhar, Shijian Lu, et al.  Icdar 2015 competition on robust reading.  In ICDAR, 2015.
  * [24] Dimosthenis Karatzas, Faisal Shafait, Seiichi Uchida, Masakazu Iwamura, Lluis Gomez i Bigorda, Sergi Robles Mestre, Joan Mas, David Fernandez Mota, Jon Almazan Almazan, and Lluis Pere De Las Heras.  Icdar 2013 robust reading competition.  In ICDAR, 2013.
  * [25] Diederik P. Kingma and Max Welling.  Auto-encoding variational bayes.  In ICLR, 2014.
  * [26] Chen-Yu Lee and Simon Osindero.  Recursive recurrent nets with attention modeling for OCR in the wild.  In CVPR, 2016.
  * [27] Hui Li, Peng Wang, Chunhua Shen, and Guyu Zhang.  Show, attend and read: A simple and strong baseline for irregular text recognition.  In AAAI, 2019.
  * [28] Ke Li, Bharath Hariharan, and Jitendra Malik.  Iterative instance segmentation.  In CVPR, 2016.
  * [29] Ron Litman, Oron Anschel, Shahar Tsiper, Roee Litman, Shai Mazor, and R Manmatha.  Scatter: selective context attentional scene text recognizer.  In CVPR, 2020.
  * [30] Canjie Luo, Lianwen Jin, and Zenghui Sun.  Moran: A multi-object rectified attention network for scene text recognition.  Pattern Recognition, 90, 2019.
  * [31] Canjie Luo, Yuanzhi Zhu, Lianwen Jin, and Yongpan Wang.  Learn to augment: Joint data augmentation and network optimization for text recognition.  In CVPR, 2020.
  * [32] Pengyuan Lyu, Zhicheng Yang, Xinhang Leng, Xiaojun Wu, Ruiyu Li, and Xiaoyong Shen.  2d attentional irregular scene text recognizer.  arXiv preprint arXiv:1906.05708, 2019.
  * [33] U-V Marti and Horst Bunke.  The iam-database: an english sentence database for offline handwriting recognition.  IJDAR, 2002.
  * [34] Anand Mishra, Karteek Alahari, and C. V. Jawahar.  Scene text recognition using higher order language priors.  In BMVC, 2012.
  * [35] Norimichi Ukita Muhammad Haris, Greg Shakhnarovich.  Deep back-projection networks for super-resolution.  In CVPR, 2018.
  * [36] Lukáš Neumann and Jiří Matas.  Real-time scene text localization and recognition.  In CVPR, 2012.
  * [37] Alejandro Newell, Kaiyu Yang, and Jia Deng.  Stacked hourglass networks for human pose estimation.  In ECCV, 2016.
  * [38] Hwee Tou Ng, Siew Mei Wu, Ted Briscoe, Christian Hadiwinoto, Raymond Hendy Susanto, and Christopher Bryant.  The CoNLL-2014 shared task on grammatical error correction.  In CoNLL, 2014.
  * [39] Taesung Park, Ming-Yu Liu, Ting-Chun Wang, and Jun-Yan Zhu.  Semantic image synthesis with spatially-adaptive normalization.  In CVPR, 2019.
  * [40] Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary DeVito, Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer.  Automatic differentiation in PyTorch.  In NeurIPS Autodiff Workshop, 2017.
  * [41] Ethan Perez, Florian Strub, Harm De Vries, Vincent Dumoulin, and Aaron Courville.  Film: Visual reasoning with a general conditioning layer.  In AAAI, 2018.
  * [42] Arik Poznanski and Lior Wolf.  Cnn-n-gram for handwritingword recognition.  In CVPR, 2016.
  * [43] Zhi Qiao, Yu Zhou, Dongbao Yang, Yucan Zhou, and Weiping Wang.  Seed: Semantics enhanced encoder-decoder framework for scene text recognition.  In CVPR, 2020.
  * [44] Trung Quy Phan, Palaiahnakote Shivakumara, Shangxuan Tian, and Chew Lim Tan.  Recognizing text with perspective distortion in natural scenes.  In ICCV, 2013.
  * [45] Anhar Risnumawan, Palaiahankote Shivakumara, Chee Seng Chan, and Chew Lim Tan.  A robust arbitrary text detection system for natural scene images.  Expert Systems with Applications, 2014.
  * [46] Alla Rozovskaya and Dan Roth.  Generating confusion sets for context-sensitive error correction.  In EMNLP, 2010.
  * [47] Firas Shama, Roey Mechrez, Alon Shoshan, and Lihi Zelnik-Manor.  Adversarial feedback loop.  In ICCV, 2019.
  * [48] Baoguang Shi, Xiang Bai, and Cong Yao.  An end-to-end trainable neural network for image-based sequence recognition and its application to scene text recognition.  IEEE T-PAMI, 2017.
  * [49] Baoguang Shi, Xinggang Wang, Pengyuan Lyu, Cong Yao, and Xiang Bai.  Robust scene text recognition with automatic rectification.  In CVPR, 2016.
  * [50] Baoguang Shi, Mingkun Yang, Xinggang Wang, Pengyuan Lyu, Cong Yao, and Xiang Bai.  Aster: An attentional scene text recognizer with flexible rectification.  IEEE T-PAMI, 2018.
  * [51] Kihyuk Sohn, Honglak Lee, and Xinchen Yan.  Learning structured output representation using deep conditional generative models.  In NeurIPS, 2015.
  * [52] Zhaoyi Wan, Jielei Zhang, Liang Zhang, Jiebo Luo, and Cong Yao.  On vocabulary reliance in scene text recognition.  In CVPR, 2020.
  * [53] Kai Wang, Boris Babenko, and Serge Belongie.  End-to-end scene text recognition.  In ICCV, 2011.
  * [54] Wenjia Wang, Enze Xie, Xuebo Liu, Wenhai Wang, Ding Liang, Chunhua Shen, and Xiang Bai.  Scene text image super-resolution in the wild.  In ECCV, 2020.
  * [55] Shih-En Wei, Varun Ramakrishna, Takeo Kanade, and Yaser Sheikh.  Convolutional pose machines.  In CVPR, 2016.
  * [56] Ziang Xie, Anand Avati, Naveen Arivazhagan, Dan Jurafsky, and Andrew Y Ng.  Neural language correction with character-based attention.  arXiv preprint arXiv:1603.09727, 2016.
  * [57] Xing Xu, Jiefu Chen, Jinhui Xiao, Lianli Gao, Fumin Shen, and Heng Tao Shen.  What machines see is not what they get: Fooling scene text recognition models with adversarial text images.  In CVPR, 2020.
  * [58] MingKun Yang, Yushuo Guan, Minghui Liao, Xin He, Kaigui Bian, Song Bai, Cong Yao, and Xiang Bai.  Symmetry-constrained rectification network for scene text recognition.  In ICCV.
  * [59] Meng Ye and Yuhong Guo.  Zero-shot classification with discriminative semantic representation learning.  In CVPR, 2017.
  * [60] Xiaoyu Yue, Zhanghui Kuang, Chenhao Lin, Hongbin Sun, and Wayne Zhang.  Robustscanner: Dynamically enhancing positional clues for robust text recognition.  In ECCV, 2020.
  * [61] Amir Roshan Zamir, Te-Lin Wu, Lin Sun, William B. Shen, Jitendra Malik, and Silvio Savarese.  Feedback networks.  In CVPR, 2017.
  * [62] Fangneng Zhan and Shijian Lu.  Esir: End-to-end scene text recognition via iterative image rectification.  In CVPR, 2019.
  * [63] Fangneng Zhan, Shijian Lu, and Chuhui Xue.  Verisimilar image synthesis for accurate detection and recognition of texts in scenes.  In ECCV, 2018.
  * [64] Chi Zhang, Guosheng Lin, Fayao Liu, Rui Yao, and Chunhua Shen.  Canet: Class-agnostic segmentation networks with iterative refinement and attentive few-shot learning.  In CVPR, 2019.
  * [65] Yaping Zhang, Shuai Nie, Wenju Liu, Xing Xu, Dongxiang Zhang, and Heng Tao Shen.  Sequence-to-sequence domain adaptation network for robust text image recognition1.  In CVPR, 2019.
  * [66] Tiancheng Zhao, Ran Zhao, and Maxine Eskénazi.  Learning discourse-level diversity for neural dialog models using conditional variational autoencoders.  In ACL, 2017.
  * [67] Chuanxia Zheng, Tat-Jen Cham, and Jianfei Cai.  Pluralistic image completion.  In CVPR, 2019.
  * [68] Quanlong Zheng, Xiaotian Qiao, Ying Cao, and Rynson WH Lau.  Distraction-aware shadow detection.  In CVPR, 2019.


# The Sequent Calculus Trainer – Helping Students to Correctly Construct
Proofs

Arno Ehle  School of Electrical Engineering and Computer Science
University of Kassel, Germany  Norbert Hundeshagen  School of Electrical
Engineering and Computer Science
University of Kassel, Germany  Martin Lange  School of Electrical Engineering
and Computer Science
University of Kassel, Germany

###### Abstract

We present the Sequent Calculus Trainer, a tool that supports students in
learning how to correctly construct proofs in the sequent calculus for first-
order logic with equality. It is a proof assistant fostering the understanding
of all the syntactic principles that need to be obeyed in constructing correct
proofs. It does not provide any help in finding good proof strategies. Instead
it aims at understanding the sequent calculus on a lower syntactic level that
needs to be mastered before one can consider proof strategies. Its main
feature is a proper feedback system embedded in a graphical user interface.

We also report on some empirical findings that indicate how the Sequent
Calculus Trainer can improve the students’ success in learning sequent
calculus for full first-order logic.

Arno Ehle and Norbert Hundeshagen and Martin Lange

logo_ttlM. Antonia Huertas, João Marcos, María Manzano, Sophie Pinchinat,
François Schwarzentruber54th International Conference on Tools for Teaching
Logic1135TTL2015

##  1 Introduction

Many courses in theoretical computer science suffer from high failure rates
and it is common among students to alienate themselves from such courses, c.f.
[9, 11]. The reasons are manifold and vary from the way mathematics is taught
in school, to lack of general problem solving competences, and not least, to a
diversity in skills for adapting new knowledge.

The BSc computer science curriculum at the University of Kassel contains a
2nd-year mandatory course on logic in computer science, as it can be found in
typical computer science university programs. This course has been re-
organised in recent years with the aim of improving learning outcomes and
therefore reducing failure rates. A central point of this re-organisation is
the use of constructivistic learning theory, in particular the inverted-
classroom model (c.f. [8]). This model focuses on learning, literally, as a
self-organised activity; consequently, the logic course should engage students
with methods and tools to assist and self-assess the use of formal logic and
the calculi taught with them. One of these tools, developed for such purposes,
is the _Sequent Calculus Trainer_ whose design and use will be described in
this paper.

We start by explaining typical problems that students encounter when being
faced with a standard exercise in learning Gentzen’s sequent calculus [5]: to
find a proof for a given sequent, formally expressing that some formula is a
logical consequence of a set of formulas. We assume the reader to be entirely
familiar with first-order logic with equality [3] and proof calculi in
general. Familiarity with sequent calculus in particular is not strictly
necessary to follow those explanations; the principles should become clear
from the examples we use. We give a brief description of the Sequent Calculus
Trainer and explain its aims. At last we provide some empirical data that
supports the claim that the Sequent Calculus Trainer can effectively aid the
learning of the sequent calculus for first-order logic.

##  2 The Sequent Calculus

###  2.1 The Proof Rules

The sequent calculus is a system of proof rules that operate on _sequents_
which are pairs of multi-sets of formulas, written
$\Gamma\Longrightarrow\Delta$. The intended meaning of such a sequent is that
the conjunction over $\Gamma$ logically implies the disjunction over $\Delta$.
The rules listed in Figure 1 operate on formulas in the antecedent $\Gamma$ or
succedent $\Delta$ of the rule’s conclusion below the line, possibly producing
new premisses shown above the line. A proof for a sequent
$\Gamma\Longrightarrow\Delta$ is, as usual, a finite tree of sequents formed
from $\Gamma\Longrightarrow\Delta$ at its root by successively applying these
rules. Each branch must end in an instance of an axiom, i.e. a rule with no
premisses.

In the rules for quantified formulas, $c$ must always be a fresh constant –
called Skolem constant – that does not occur in the conclusion of this rule
already; $t$ must be a ground term over the symbols that occur in the
conclusion.

$\begin{array}[]{c}\Gamma,\varphi,\psi\Longrightarrow\Delta\\\
\hline\cr\Gamma,\varphi\wedge\psi\Longrightarrow\Delta\end{array}\qquad\begin{array}[]{c}\Gamma\Longrightarrow\varphi,\Delta\qquad\Gamma\Longrightarrow\psi,\Delta\\\
\hline\cr\Gamma\Longrightarrow\varphi\wedge\psi,\Delta\end{array}\qquad\begin{array}[]{c}\Gamma,\varphi\Longrightarrow\Delta\\\
\hline\cr\Gamma\Longrightarrow\neg\varphi,\Delta\end{array}\qquad\begin{array}[]{c}\Gamma\Longrightarrow\varphi,\Delta\\\
\hline\cr\Gamma,\neg\varphi\Longrightarrow\Delta\end{array}$

$\begin{array}[]{c}\Gamma,\varphi\Longrightarrow\Delta\qquad\Gamma,\psi\Longrightarrow\Delta\\\
\hline\cr\Gamma,\varphi\vee\psi\Longrightarrow\Delta\end{array}\qquad\begin{array}[]{c}\Gamma\Longrightarrow\varphi,\psi,\Delta\\\
\hline\cr\Gamma\Longrightarrow\varphi\vee\psi,\Delta\end{array}\qquad\begin{array}[]{c}\Gamma\Longrightarrow\varphi,\varphi,\Delta\\\
\hline\cr\Gamma\Longrightarrow\varphi,\Delta\end{array}\qquad\begin{array}[]{c}\Gamma,\varphi,\varphi\Longrightarrow\Delta\\\
\hline\cr\Gamma,\varphi\Longrightarrow\Delta\end{array}$

$\begin{array}[]{c}\Gamma,\psi\Longrightarrow\Delta\qquad\Gamma\Longrightarrow\varphi,\Delta\\\
\hline\cr\Gamma,\varphi\to\psi\Longrightarrow\Delta\end{array}\quad\enspace\begin{array}[]{c}\Gamma,\varphi\Longrightarrow\psi,\Delta\\\
\hline\cr\Gamma\Longrightarrow\varphi\to\psi,\Delta\end{array}\quad\enspace\begin{array}[]{c}\\\
\hline\cr\Gamma,\varphi\Longrightarrow\varphi,\Delta\end{array}\quad\enspace\begin{array}[]{c}\\\
\hline\cr\Gamma\Longrightarrow s=s,\Delta\end{array}$

$\begin{array}[]{c}\Gamma,\varphi[c/x]\Longrightarrow\Delta\\\
\hline\cr\Gamma,\exists
x\;\varphi\Longrightarrow\Delta\end{array}\qquad\begin{array}[]{c}\Gamma\Longrightarrow\varphi[t/x],\Delta\\\
\hline\cr\Gamma\Longrightarrow\exists
x\;\varphi,\Delta\end{array}\qquad\begin{array}[]{c}\Gamma,\varphi[t/x]\Longrightarrow\Delta\\\
\hline\cr\Gamma,\forall
x\;\varphi\Longrightarrow\Delta\end{array}\qquad\begin{array}[]{c}\Gamma\Longrightarrow\varphi[c/x],\Delta\\\
\hline\cr\Gamma\Longrightarrow\exists x\;\varphi,\Delta\end{array}$

$\begin{array}[]{c}\Gamma,s=s\Longrightarrow\Delta\\\
\hline\cr\Gamma\Longrightarrow\Delta\end{array}\qquad\begin{array}[]{c}\Gamma,\varphi[s^{\prime}/x]\Longrightarrow\Delta\\\
\hline\cr\Gamma,s=s^{\prime},\varphi[s/x]\Longrightarrow\Delta\end{array}\qquad\begin{array}[]{c}\Gamma\Longrightarrow\varphi[s^{\prime}/x],\Delta\\\
\hline\cr\Gamma,s=s^{\prime}\Longrightarrow\varphi[s/x],\Delta\end{array}$

Figure 1: The proof rules of the sequent calculus.

###  2.2 A Didactic Perspective

A standard exercise in sequent calculus asks for a proof of a given sequent,
e.g. $\mathcal{S}_{0}:=$

$\forall x\forall y.\;E(x,y)\rightarrow x=f(y)\leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ \forall x\forall y\forall z.\;E(x,z)\wedge
E(y,z)\rightarrow x=y\ .$

Difficulties and mistakes can generally be put into two categories.

(1) The first one is about _constructing a correct proof_ : many students are
not able to handle formalisms well; often they can barely parse sequents and
apply rules correctly. In this example, one has to introduce new names for the
universally quantified variables $x,y,z$ in this order and then decompose the
Boolean operators on the right side, yielding $\mathcal{S}_{1}:=$

$\forall x\forall y.\;E(x,y)\rightarrow
x=f(y),E(a,c),E(b,c)\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\
a=b\ .$

Typical mistakes at this syntactic level are concerned with wrong rule
applications and include

  * •

_confusing_ rules, for instance applying the rule for conjunctions to a
disjunction;

  * •

_misplacing_ rules, usually by applying a rule to a genuine subformula rather
than a formula in the sequent; in other words not understanding the structure
of a sequent;

  * •

_wrong first-order instantiations_ , for instance not choosing a fresh Skolem
constant when needed;

  * •

_wrong rule instantiations_ , for instance by adding the symbols $\Gamma$ and
$\Delta$ to the sequent at hand;

and so on.

(2) There are other ways of applying rules in a syntactically correct way in
this example, for instance by operating on the formulas in the premiss
instead. This, however, is unwise for _finding the right proof_. For this one
must proceed as described above and then have the inspiration to double one of
the formulas in the premiss and instantiate both copies differently yielding

$E(a,c)\rightarrow a=f(c),E(b,c)\rightarrow
b=f(c),E(a,c),E(b,c)\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\
a=b\ .$

The rest of this proof task is relatively easy using Boolean elimination rules
and very simple reasoning about equalities.

There is a clear dependency between these two challenges: the ones described
in (1) need to be met before those in (2) can be met; it is impossible to find
a proof unless one is able to construct correct proofs at all. The latter is
clearly a very difficult task for students who already struggle with
uncertainties like “am I allowed to apply this rule here?”, “was the
application correct?”, “should I introduce a new name or instantiate with an
already existing term?”, etc.

This gap between syntactical and semantical understanding has been addressed
in many fields like teaching programming or simply mathematics (e.g. in [10]).
This phenomenon is accurately described in [4] as the ability to “write rather
rigorously a simple C program”, while they cannot “rigorously write down a
mathematical proof of the kind needed in graph theory, formal logic, […]”
There is a hidden hint in this observation on how to tackle the problem of
teaching proof calculi. Students seem to easily understand syntactic
principles as long as there is a mechanism – like a compiler – which allows
them to learn the formalism in a trial-and-error way.

This is where the Sequent Calculus Trainer comes into play. It is supposed to
aid the constructing of correct proofs but does not help at all in finding the
right proofs. From a logical point of view it is merely a proof assistant, not
a theorem prover. From a didactic point of view, its use is supposed to
address the students’ rote memory such that they become able to reach this gap
between syntax and semantics, thus enabling them to start understanding the
underlying logical concepts. The Sequent Calculus Trainer therefore adheres to
two design principles: it is an easy-to-use and simple assistant for building
proof trees in sequent calculus. Moreover, it comes with a compiler-like
feedback system, which is known for its benefits in tutorial teaching
environments [1].

###  2.3 Related Tools

There are other high quality interactive proof systems that can be used to
train the construction of correct proofs in the sequent calculus. The tool
that meets the prerequisites laid out here best is
LOGITEXT111http://logitext.mit.edu; others worth mentioning are JAPE [2] and
PANDA [4]. None of these treats first-order logic _with_ equality, though.
This is a major drawback since equality is – possibly together with
quantification – one of the most difficult concepts for constructing and
finding proofs. Yet equality reasoning is ubiquitous in computer science;
hence, it should not be ignored in teaching contexts. Furthermore, JAPE is
lacking a feedback system, and PANDA’s proof calculus is natural deduction
which differs from the sequent calculus.

In a setting where we measure success through the understanding of syntactic
concepts, it is essential that the proof calculus used in classroom must be
the same as that used by a supporting tool. None of those existing tools is
general enough to serve the purposes described above – to act as a tool
supporting the learning of proof construction in the sequent calculus for
first-order logic with equality. One also should not underestimate the effort
that would be needed in order to extend or amend an existing software tool
created by others. Hence, having many tools with slightly differing features
in this area should be considered advantageous.

Figure 2: The user-interface.

##  3 The Sequent Calculus Trainer

Figure 3: The feedback system.

We provide the Sequent Calculus Trainer as an open source application under
the BSD-3 license and the source code as well as the binaries are publicly
available222http://www.uni-kassel.de/eecs/fachgebiete/fmv/projects/sequent-
calculus-trainer.html. Figure 2 shows the graphical user interface which is
kept fairly simple. The trainer is shipped with two main views, one for
propositional logic and one for first-order logic. They both differ only in
the number of applicable rules shown on the right side of the windows, and in
the treatment of atomic propositions, which are interpreted as 0-ary
predicates in the first-order logic view. Sequents can be input either through
a simple text file or in the text fields at the bottom, where the syntax
specification for the input is given, too. Furthermore, it is possible to save
and load proof trees in an internal format as well as export them in PNG
format.

###  3.1 Key Features

Figure 4: The substitution rule.

We briefly introduce the two key features of the Sequent Calculus Trainer.

  * •

Nearly every user action leads to a response by the program. Figure 3
exemplarily illustrates such on-screen messages. Each rule button is equipped
with a short message, which occurs on mouse-over. These messages usually
contain the formal definition of a rule as well as some appropriate high-level
explanations of the rule’s meaning and, if suitable, why it is a valid logical
principle.

If the user has chosen a rule and tries to apply it to a formula by selecting
a logical operator, the formula represented by this operator “responds” by
telling the user whether or not the rule is applicable there. This happens in
two ways: the part of the formula that is in scope of the selected operator or
symbol is highlighted. This helps to understand precedence rules and the
structure of sequents and formulas. When a wrong operator or symbol is chosen,
the user is provided with an error message which includes a hint on the
mistake. For instance, the reason why a current leaf in the prooftree is an
axiom has to be identified via clicking on the part of the formula that causes
the application of an axiom rule.

  * •

The second notable feature is the handling of sequents that include
equalities. Figure 4 shows how the substitution rule works. After the rule for
substitution on the left-hand or right-hand side of the sequent has been
chosen, the program expects an atomic formula with an equality predicate to be
selected. In the last step, the term that should be substituted needs to be
clicked on.

A final point worth mentioning is that the user is able to undo all steps in
the proof up to a certain sequent at any time by just applying a different
rule to that particular sequent.

###  3.2 The Backend

The Sequent Calculus Trainer is meant to be used by a broad range of students;
hence, it platform independency provided by an implementation in Java is a key
design principle. It uses the GUI framework JavaFX, which is integrated in the
Java Standard Library since the emerging of Oracle’s Java 8. This mainly
allows the program to have only one dependency in ControlsFX that is a small
extension library for JavaFX, designed to give even more UI controls and
simple dialogs. The result is a clear and comprehensive feedback system which
was another key design principle.

The Sequent Calculus Trainer is designed according to the principles provided
in the model-view-controller-patterns (MVC). Thus, it consists of three parts;
the data model which contains the data and algorithms as a standalone part of
the program, the controllers which contain the logic for the GUI, and finally
the GUI itself which is build with JavaFX while mainly using the XML based
notation for GUI elements called FXML. The program is equipped with the
possibility to simply add new languages in form of language sets in simple
text files and new country flags for the frontend. Currently German and
English are available.

##  4 Experiences in Teaching the Sequent Calculus

The computer science BSc curriculum at the University of Kassel contains a
mandatory 2nd-year course on logic which teaches, amongst others, the sequent
calculus for first-order logic with equality. In order to pass the course
students need to take a written exam. We report on the results achieved in
three successive years. Group 1 took the exam in winter term 2012/13. The
Sequent Calculus Trainer was developed afterwards, so it was not available to
them at the time of preparation for the exam. Group 2 took the exam in winter
term 2013/14, and they were greatly encouraged to solve corresponding
exercises using the Sequent Calculus Trainer. Group 3 took the exam in winter
term 2014/15. The Sequent Calculus Trainer was made available, but in
comparison to group 2 the trainer had been advertised less. The preconditions
are comparable in the sense that before the exam, all groups had to pass two
graded exercises on sequent calculus, they were provided with the same number
of additional voluntary tasks on this topic, and they were allowed to prepare
a handwritten note for the exam which contained the sequent calculus rules in
many cases.

The three exams under consideration featured a question each, asking for a
proof of a given sequent. The three sequents differed, with the ones used for
group 2 and 3 being seemingly more difficult to prove with regards to both
aspects of constructing and finding a proof.

group 1: | $\forall x\exists y.\;x=v(y)\wedge\forall x\;F(v(x))\enspace\Longrightarrow\enspace\forall x\;F(x)$
---|---
group 2: | $\forall x\forall y.\;E(x,y)\rightarrow x=f(y)\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \forall x\forall y\forall z.\;E(x,z)\wedge E(y,z)\rightarrow x=y$
group 3: | $\forall x\forall z.\;P(x,c)\wedge Q(z,g(x,z))\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \exists y\forall x\;P(x,y)\wedge\forall z\exists u\;Q(z,u)$

While the sequents for groups 2 and 3 need some insight into the properties
expressed by its formulas, the sequent for group 1 can be proved using almost
syntactic considerations only. Surprisingly, out of 70 students in group 1,
more than 50% (46 in total) were not able to apply such a simple strategy of
applying all possible rules in the correct order. Moreover, when adding the 10
students that did not even try to execute the exercise, we may conclude that
80% of group 1 did not succeed in this exercise because of problems with the
correct application of rules. The mistakes most frequently made were
_misplacing_ of rules and _wrong first-order instantiations_ according to the
classification listed in Section 2.2. Some examples of typical mistakes are
shown in Figure 5.

Figure 5: Examples of frequently made mistakes with wrong rule applications.

Group 2 shows a totally different picture. Out of 51 students only 12 already
failed in simple rule applications, where 1 student did not execute the
exercise, which leads to 25% in total. Thus, nearly 75% of the students where
at least able to handle the syntactic formalism resulting in correct rule
applications before a deeper understanding would be needed.

The most recent data is taken from group 3. Out of 46 students 19 failed to
achieve the mentioned goal and 2 did not execute the exercise which is 46% in
total.

If we summarize the results of the latter two groups we get a rate of 34
students out of 97 which failed for reasons of wrong application of rules.
Thus, nearly 65% of the students where at least able to handle the syntactic
formalism resulting in correct rule applications. We believe that this is due
to the availability of the Sequent Calculus Trainer.

This conclusion seems to be in contrast to two other – seemingly odd –
observations. First of all, group 2 did not achieve significantly more points
than group 1. Both exercises were graded with 4 points in total where group 1
reached an average of 1.2 points and group 2 an average of 1.5 points. As
mentioned above, from a semantical perspective the sequent for group 2 is
harder to proof and, therefore, needs a more involved strategy. This is the
main reason for the only slight improvement in the average grade; a
syntactically correct but unsuccessful proof attempt is not graded with more
than 2 out of 4 points. Hence, the introduction of the Sequent Calculus
Trainer into the process of learning how to correctly apply rules resulted in
a 25%-gain in points between these two groups. The still low absolute average
value achieved by group 2 points out the lack of “understanding” of the
underlying theory which is not addressed by the use of the Sequent Calculus
Trainer.

Secondly, the results of group 3 seem to worsen in comparison to group 2.
Again, the exercise on sequent calculus of group 3 was graded under the same
constraints with 4 points in total. The effort needed to prove this sequent is
comparable to the effort for the sequent of group 2, as both need a similar
strategy of replacing the quantified variables in the correct order. However,
the outcome is different. In group 3 more students made mistakes in rule
applications although they were also provided with the Sequent Calculus
Trainer. They reached an average of 2.7 points. One explanation of this
observation can be found when comparing the mistakes made in rule
applications. Out of 19 students who tried to solve the exercise and failed in
rule applications 7 made the same single mistake of misreading the precedence
of the conjunction in the succedent, exemplarily shown in Figure 6. Such
“near” solutions were graded with 3 out of 4 points.

Figure 6: Example of the most frequent mistake in group 3.

##  5 Discussion and Future Work

The improvement in the exam results of the logic course at the University of
Kassel in winter term 2013/14 and 2014/15 compared against those achieved in
winter term 2012/13 correlate to the availability and encouragement to
actively make use of the Sequent Calculus Trainer. Clearly, the improvement of
results in one particular course can be caused by various reasons; it is well
known that the teaching staff has the greatest impact on learning outcomes
(cf. [7]). In our setting the lectures for all groups were given by the same
lecturer and the main part of the exercises was given by the same teaching
assistant. The role of the group’s composition and the educational background
of the students is of course not to be underestimated. However, the
significance of the measured effect was too great to be caused solely by the
aforementioned reasons. This is strongly emphasised by the fact that the
differences in the total outcome of the exams are marginal. Nevertheless, it
would obviously be interesting to support this further by a broader empirical
evaluation, in particular by considering its effects on students at different
universities.

When regarding the effect more deeply, a software for teaching sequent
calculus used as an interactive compiler for the language of proof trees
perfectly meets the requirements given in Section 2.2 for closing the
syntactic gap that may be present in students’ minds when introducing a new
formal concept. From a different point of view such a piece of software offers
a suitable alternative in addressing the rote memory to replace just the right
amount of pen and paper exercises, needed to understand the formalism. In
addition, it directly forbids mistakes that would be possible to make with pen
and paper and would have to be manually marked by human teaching assistants.

Clearly, the goal in teaching a calculus for propositional or first-order
logic is not just about the simple manipulation of strings. Instead students
need to learn to fluently understand the properties being expressed by logical
formulas, to visualise the classes of structures that are being represented by
them, etc. In other words, students also need to understand the semantics of
logical languages and calculi. The Sequent Calculus Trainer is not meant to
address possible deficits in understanding semantics, nor does it do it
automatically as the considerations at the end of Section 4 show. We do
believe, though, that similar improvement in learning success could be
achieved for such semantical aspects by complementing the Sequent Calculus
Trainer with a tool that trains the understanding of semantics, for instance
using model checking games for first-order logic [6].

## Acknowledgements

We would like to thank Angelika Hoffman-Hesse for doing the statistical
evaluation of which mistakes were made by how many students as reported above,
and Florian Bruse for acting as a linguistic consultant in the development of
the Sequent Calculus Trainer. The work has been financially supported by the
_Service Center Lehre_ of the University of Kassel under an _Innovation-in-
Teaching_ grant.

## References

  * [1] J. R. Anderson, A. T. Corbett, K. R. Koedinger, and R. Pelletier.  Cognitive tutors: Lessons learned.  J. of the Learning Sciences, 4(2):167–207, 1995.
  * [2] R. Bornat and B. Sufrin.  Animating formal proof at the surface: The jape proof calculator.  Comput. J., 42(3):177–192, 1999.
  * [3] H.-D. Ebbinghaus, J. Flum, and W. Thomas.  Mathematical Logic.  Undergraduate Texts in Mathematics. Springer, Berlin, 2nd edition, 1994\.
  * [4] O. Gasquet, F. Schwarzentruber, and M. Strecker.  Panda: A proof assistant in natural deduction for all. A Gentzen style proof assistant for undergraduate students.  In Proc. 3rd Int. Congress on Tools for Teaching Logic, TICTTL 2011, volume 6680 of LNCS, pages 85–92. Springer, 2011.
  * [5] G. Gentzen.  Untersuchungen über das Logische Schliessen.  Mathematische Zeitschrift, 39:176–210, 405–431, 1935.
  * [6] E. Grädel, P. G. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Y. Vardi, Y. Venema, and S. Weinstein.  Finite Model Theory and Its Applications (Texts in Theoretical Computer Science. An EATCS Series).  Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2005.
  * [7] J. Hattie.  Visible Learning: A Synthesis of Over 800 Meta-Analyses Relating to Achievement.  Taylor & Francis, 2008.
  * [8] M. J. Lage, G. J. Platt, and M. Treglia.  Inverting the classroom: A gateway to creating an inclusive learning environment.  J. of Economic Education, 31(1):pp. 30–43, 2000.
  * [9] Gabriel Robins.  Teaching theoretical computer science at the undergraduate level: Experiences, observations, and proposals to improve the status quo.  Technical report, Computer Science Department, UCLA, 1988.
  * [10] B. Shneiderman and R. E. Mayer.  Syntactic/semantic interactions in programmer behavior: A model and experimental results.  Int. J. of Parallel Programming, 8(3):219–238, 1979.
  * [11] David R. Surma.  Rolling the dice on theory: One department’s decision to strengthen the theoretical computing aspect of their curriculum.  J. Comput. Sci. Coll., 28(1):74–80, 2012.