# XLAVS-R: Cross-Lingual Audio-Visual Speech Representation Learning
for Noise-Robust Speech Perception

HyoJung Han1 Mohamed Anwar11footnotemark: 1 Juan Pino2 Wei-Ning Hsu2
Marine Carpuat1 Bowen Shi2 Changhan Wang2
1University of Maryland, USA 2 Meta AI, USA
<EMAIL_ADDRESS><EMAIL_ADDRESS>
Work done at Meta AI

###### Abstract

Speech recognition and translation systems perform poorly on noisy inputs,
which are frequent in realistic environments. Augmenting these systems with
visual signals has the potential to improve robustness to noise. However,
audio-visual (AV) data is only available in limited amounts and for fewer
languages than audio-only resources. To address this gap, we present XLAVS-R,
a cross-lingual audio-visual speech representation model for noise-robust
speech recognition and translation in over 100 languages. It is designed to
maximize the benefits of limited multilingual AV pre-training data, by
building on top of audio-only multilingual pre-training and simplifying
existing pre-training schemes. Extensive evaluation on the MuAViC benchmark
shows the strength of XLAVS-R on downstream audio-visual speech recognition
and translation tasks, where it outperforms the previous state of the art by
up to 18.5% WER and 4.7 BLEU given noisy AV inputs, and enables strong zero-
shot audio-visual ability with audio-only fine-tuning.

XLAVS-R: Cross-Lingual Audio-Visual Speech Representation Learning
for Noise-Robust Speech Perception

HyoJung Han1††thanks:  Work done at Meta AI Mohamed Anwar11footnotemark: 1
Juan Pino2 Wei-Ning Hsu2 Marine Carpuat1 Bowen Shi2 Changhan Wang2 1University
of Maryland, USA 2 Meta AI, USA<EMAIL_ADDRESS><EMAIL_ADDRESS>

##  1 Introduction

Speech recognition and speech-to-text translation, two core speech perception
tasks, have witnessed rapid developments in the past two years. Still, the
performance of state-of-the-art (SOTA) models such as Whisper Radford et al.
(2023) and SeamlessM4T Communication (2023b) degrades sharply in noisy
environments Anwar et al. (2023); Communication (2023a). Audio-only approaches
to make such systems more robust (Ng et al., 2023; Zhu et al., 2023) remain
challenged by frequent noise types such as intense babble noise and overlapped
speech Shi et al. (2022b).

| Hours | Languages
---|---|---
| A | AV | A | AV
Audio-Only Pre-Training Data
AVFormer Seo et al. (2023) | 60K | 0 | 1⋆ | 0
FAVA May et al. (2023) | 2.8K | 0 |  $>$100† | 0
Audio-Visual Pre-Training Data
AV-HuBERT Shi et al. (2022a) | 0 | 1.8K | 0 | 1⋆
AV-data2vec Lian et al. (2024) | 0 | 1.8K | 0 | 1⋆
AV2AV Choi et al. (2023) | 0 | 7K | 0 |  $>$100
Audio-Only & Audio-Visual Pre-Training Data
u-HuBERT Hsu and Shi (2022) | 0.5K | 1.8K | 1⋆ | 1⋆
VATLM Zhu et al. (2024) | 4.3K | 1.8K | 1⋆ | 1⋆
XLAVS-R (this work) | 436K | 1.2K | 128 | 9
Table 1: Pre-training data type, amount and language coverage in audio-visual
speech perception models (A: audio, AV: audio-visual). Compared to prior work,
XLAVS-R exploits audio-only speech data for efficient data scaling and
language coverage expansion. ⋆ English-only.

Complementing audio inputs with visual signals such as video frames of
speaker’s lips offers an alternative approach (Sumby and Pollack, 1954;
Potamianos et al., 2004; Mroueh et al., 2015; Chung et al., 2017), with
promising results in audio-visual speech recognition (AVSR) and audio-visual
speech-to-text translation (AVS2TT) tasks Afouras et al. (2022); Ma et al.
(2021); Shi et al. (2022b); Anwar et al. (2023). Yet, as summarized in Table
1, prior works are either restricted to English (Hsu and Shi, 2022; Zhu et
al., 2024; Seo et al., 2023) or to a limited amount of audio-visual data Shi
et al. (2022a); Choi et al. (2023); Lian et al. (2024), limiting language
coverage and performance on downstream tasks.

To bridge this gap, we present XLAVS-R, a cross-lingual audio-visual speech
representation learning model for noise-robust speech perception across over
100 languages. Its training strategy is designed to maximize the efficiency of
multilingual AV pre-training by injecting audio-visual (AV) signals (§3.2)
after pre-training on audio-only (A-only) data that is easier to scale in size
and language coverage (§3.1). We improve AV-HuBERT (Shi et al., 2022a) with
simplified training protocol and updated model architecture, and scale model
size up to 2B parameters for performance in the multilingual setting.

We conduct extensive evaluations on the MuAViC benchmark (Anwar et al., 2023).
XLAVS-R yields SOTA performance on speech recognition in 9 languages and
speech-to-text translation in 6 X-to-English pairs (§5.1, §5.2), notably
improving their robustness to noisy inputs. Furthermore, XLAVS-R enables zero-
shot audio-visual ability in downstream tasks with audio-only fine-tuning
(FT): fine-tuning our XLAVS-R 2B model without supervised AV downstream data
achieves the best audio-visual performances in noisy settings even compared to
the corresponding audio-visual supervised fine-tuned model (§5.4). This
confirms the benefits of our pre-training strategy and relaxes the data
requirements for downstream tasks, making it possible to tackle AVSR and AVSTT
tasks without labeled—transcribed or translated—audio-visual data.

##  2 Related Work

Self-supervised audio-only speech representation. Self-supervised learning
(SSL) for speech aims to establish a general speech representation with
unlabeled speech data applicable to various downstream applications, including
speech recognition and spoken language understanding tasks wen Yang et al.
(2021). Many of today’s successful SSL approaches Baevski et al. (2020); Hsu
et al. (2021); Baevski et al. (2022); Chiu et al. (2022) are based on masked
span prediction. Specifically, wav2vec 2.0 Baevski et al. (2020) applies a
contrastive predictive coding-like van den Oord et al. (2018) loss on masked
speech utterances. HuBERT Hsu et al. (2021) utilizes masked speech features to
predict hidden units derived from layerwise features. Instead of using
discrete units, Data2vec Baevski et al. (2022) directly regresses dense
features from an exponential moving average (EMA) teacher.

SSL approaches notably reduce the need for labeled speech data. In ASR
benchmarks Panayotov et al. (2015), they yield performance on par with or
better than fully supervised models with far fewer transcriptions. This has
motivated sustained efforts toward multilingual SSL models such as XLSR-53
Conneau et al. (2021), XLS-R Babu et al. (2022), and MMS Pratap et al. (2023),
which particularly excel in low-resource language scenarios.

Self-supervised audio-visual speech representation. Audio-visual SSL
approaches draw heavy inspiration from their audio-only counterparts. AV-
HuBERT Shi et al. (2022a) extends HuBERT Hsu et al. (2021) to the audio-visual
setting by taking the masked audio-visual stream as input and predicting the
hidden units initialized with MFCC clusters, iteratively refining them with
layerwise features. This framework has proven effective for multiple
downstream tasks, including lip reading Shi et al. (2022a), audio-visual
speech recognition and translation Shi et al. (2022b); Anwar et al. (2023). In
AV2AV (Choi et al., 2023) and our work of XLAVS-R, it has been extended to a
multilingual setting. RAVEn Haliassos et al. (2023) leverages modality-
specific EMA teachers to generate targets for masked prediction, thus avoiding
an iterative refinement process. Similarly, AV-data2vec Lian et al. (2024) is
based on data2vec Baevski et al. (2022) and regresses multimodal features with
an audio-visual EMA teacher. AV2vec Zhang et al. (2023) further combines AV-
data2vec with the masked prediction objective in AV-HuBERT. Some prior works
also investigated the use of unpaired unimodal data, notably audio, to improve
multimodal representation. u-HuBERT Hsu and Shi (2022) augments AV-HuBERT with
audio-only speech during pre-training, resulting in improved audio-visual
speech recognition performance. VATLM Zhu et al. (2024) further added text-
only data and trained the model on an arbitrary modality stream. Our work
builds on the insights of AV/u-HuBERT with adaptations for continual SSL
training with visual modality injection to A-only model and for the
multilingual setting.

Audio-visual adaptation of audio-only speech models. Recent work has begun to
explore the adaptation of audio-only speech models into audio-visual models.
MixSpeech Cheng et al. (2023) develops a visual speech translation model based
on a pre-trained audio-only speech translation model by minimizing the
discrepancy between the probabilities from audio-only and multi-modal streams.
AVFormer Seo et al. (2023) incorporates lightweight modules into an audio-only
speech recognizer to adapt it into visually grounded speech recognition
through two-stage fine-tuning. FAVA May et al. (2023) directly fine-tunes a
pre-trained BEST-RQ Chiu et al. (2022) encoder for audio-visual speech
recognition with a randomly initialized visual encoder. FAVA connects to our
work by applying this technique to a multilingual audio-only model. However,
its evaluation focuses on English with labeled AV speech data for supervised
fine-tuning, while our approach focuses on AV SSL to achieve competitive zero-
shot results without AV labeled data as well as state-of-the-art supervised
multilingual performance.

Figure 1: Overview of XLAVS-R. From the audio-only SSL model, we generate unit
targets for audio-visual SSL pre-training (left box). We inject visual
modality into the first stage model (blue blocks) and fuse visual modality
with audio one (pink blocks) to continue training with audio-visual SSL pre-
training. In AV SSL, noises are added randomly to clean audio, and masked
prediction objectives (right top) are applied to the union set of masked
frames of audio and visual stream (bottom gray).

##  3 XLAVS-R

Our approach (Figure 1) requires first training an audio-only SSL model, which
is used to generate unit targets for audio-visual SSL pre-training. We inject
visual modality into the resulting model to continue training with audio-
visual SSL pre-training. Through this process, XLAVS-R introduces three key
improvements over baseline approaches. First, we leverage the abundant
availability of audio-only speech data to enhance overall performances and
achieve greater robustness on domain shift (§3.1), and inject visual modality
to build an audio-visual pre-training model on top of audio-only pre-training
model (§3.2). Second, we use a learnable audio feature extractor to better
capture the various phonetic information of multilingual audios (§3.3). Third,
we improve the training efficiency of the audio-visual pre-training stage by
single-round training with unit targets from audio-only contextualized
representation (§3.4).

###  3.1 Audio-Only Pre-Training

Instead of training an audio-visual model in one step with the mix of audio-
only data and audio-visual data, we first train an audio-only speech model and
adapt it to an audio-visual one via self-supervised continual pre-training
with audio-visual data. This is motivated by the facts that audio-only data is
much more plentiful than audio-visual data, particularly for low-resource
languages, and that audio-only models are much more computationally efficient
than audio-visual models with similar architecture and size because of the
cost of visual feature extraction and bi-modal feature fusion. We concentrate
our computational resources on the first stage of A-only SSL since audio-only
data has greater volume and the audio modality naturally contains richer
semantic information than the visual modality. We refer to the outcome model
of this audio-only self-supervised learning as XLS-R, as we follow the XLS-R
training settings (Babu et al., 2022) and adopt its wav2vec 2.0 architecture
(Baevski et al., 2020).

###  3.2 Continued Audio-Visual Pre-Training with Visual Modality Injection

After obtaining XLS-R through A-only pre-training, we add a ResNet-based
visual feature extractor (VFE) and a linear projection-based feature fusion
module to build up an audio-visual model and continue AV pre-training.

For audio-visual self-supervised learning, we follow Shi et al. (2022a, b)
using AV-HuBERT pre-training loss. Given temporally aligned audio input
$I_{a}\in\mathbb{R}^{T_{a}\times C_{a}}$ and video speech input
$I_{v}\in\mathbb{R}^{T_{v}\times C_{v}\times W\times H}$, each modality
feature extractor encode inputs into same length feature sequences
$f_{a},f_{v}\in\mathbb{R}^{T\times D}$. Here, audio and visual frames are
masked independently by separate masking probabilities. Frame-wisely fused
audio-visual features $Fusion(f_{a},f_{v})\in\mathbb{R}^{T\times D^{\prime}}$
are processed by the Transformer (Vaswani et al., 2017) to generate
contextualized audio-visual representation. Target units
$z\in\\{1,\ldots,K\\}^{T}$ for each frame are assigned by an unsupervised
clustering method. Given the output probability $p$ from the fused
representation and the target units $z$, the model is trained with the
following loss:

$L=-\sum_{t\in M}\log p_{t}(z_{t})-\alpha\sum_{t\notin M}\log p_{t}(z_{t}),$
(1)

where $M$ is a union set of masked frames for the audio and visuals stream and
$\alpha$ is weighing factor for the unmasked regions.

As in AV/u-HuBERT, we apply modality dropout to encourage the fusion of audio
and visual representation space. In the modality fusion, either sequence of
$f_{a}$ or $f_{v}$ can be dropped out by the modality dropout probability
$p_{m}$ and filled with zero. In the case of dropping out one of the
modalities, $f_{a}$ is selected with an audio dropout probability $p_{a}$ to
have $Fusion(0,f_{v})$.

With the masked prediction objective on audio-only targets, the continued
training of audio-visual SSL aligns audio-visual and visual-only
representations to corresponding audio-only representation, which is
established in the previous A-only SSL.

Besides the audio-to-visual representation alignment, clean-to-noisy audio
representation is also aligned during the continued AV SSL training phase by
using potentially noised audio as audio inputs. This is implemented by
randomly adding noises to clean speech audio during the training.

After self-supervised learning, we fine-tune with sequence-to-sequence cross-
entropy loss for downstream tasks.

###  3.3 Learnable Audio Feature Extractor

XLAVS-R has the same model architecture as AV/u-HuBERT except for the nature
of the audio features provided as inputs to the Transformer encoder. We
jointly train a convolutional audio feature extractor (AFE) as that in wav2vec
2.0 Baevski et al. (2020) for high-dimensional audio inputs. This differs from
AV/u-HuBERT which uses lower-dimensional filterbank features. Our approach
provides more capacity for multilingual models and their cross-lingual
inferences.

###  3.4 Single-Round AV Training with Self-Supervised Audio-Only Targets

AV-HuBERT Shi et al. (2022a, b) and u-HuBERT (Hsu and Shi, 2022) require
multiple pre-training rounds, with training targets switching from quantized
audio-only local features to quantized audio-visual contextualized
representation. In each round, the AV model is re-trained from scratch. Hence,
the model quality gains across training rounds come from the updated training
targets. While these iterative rounds help the model encode more advanced
contextual and bi-modal information in the later stage, the resulting training
process is complex and computationally expensive.

To improve training efficiency, we propose to create first-round training
targets from a contextualized audio-only representation instead of local
features that have noisier, lower-level information. This accelerates the
masked prediction learning of high-level semantic information in the first
round and reduces the necessity for additional training rounds. We obtain
audio-only contextualized representation from a self-supervised multilingual
speech model described in Section 3.1.

Model | Test Mode | OOD | In-Domain
---|---|---|---
Avg | En | Ar | De | El | Es | Fr | It | Pt | Ru | Avg
Clean environment, Test WER (%) $\downarrow$
AV-HuBERT (Shi et al., 2022b) | A | 41.8 | 2.0 | 89.6 | 53.5 | 47.2 | 18.2 | 20.7 | 21.2 | 22.9 | 46.0 | 35.7
AV | - | 1.7 | 89.4 | 52.0 | 46.2 | 17.4 | 20.3 | 20.8 | 22.1 | 44.7 | 35.0
u-HuBERT (Hsu and Shi, 2022) | A | 41.4 | 1.9 | 89.3 | 53.3 | 47.2 | 17.9 | 20.7 | 21.6 | 22.5 | 45.8 | 35.6
AV | - | 1.9 | 89.3 | 52.1 | 46.4 | 17.3 | 20.5 | 21.2 | 21.9 | 44.4 | 35.0
XLAVS-R |  |  |  |  |  |  |  |  |  |  |  |
XLAVS-R 300M | A | 32.5 | 2.5 | 82.4 | 45.6 | 24.2 | 11.3 | 14.6 | 12.9 | 13.7 | 33.0 | 26.7
AV | - | 2.4 | 81.7 | 44.7 | 24.3 | 10.9 | 14.4 | 12.8 | 13.2 | 32.7 | 26.3
XLAVS-R 2B | A | 34.2 | 1.9 | 80.3 | 45.5 | 19.5 | 9.4 | 12.5 | 10.9 | 11.6 | 26.0 | 24.2
AV | - | 1.7 | 79.3 | 44.4 | 19.0 | 9.1 | 12.3 | 10.6 | 11.2 | 25.0 | 23.6
Noise environment, Test WER (%) $\downarrow$
AV-HuBERT (Shi et al., 2022b) | A | 89.3 | 39.3 | 111.2 | 87.0 | 85.2 | 65.6 | 58.1 | 69.5 | 69.9 | 75.9 | 73.5
AV | - | 6.4 | 104.7 | 74.2 | 70.4 | 43.1 | 43.0 | 48.2 | 47.5 | 67.4 | 56.1
u-HuBERT (Hsu and Shi, 2022) | A | 87.5 | 31.8 | 109.4 | 84.7 | 83.1 | 62.7 | 56.6 | 67.8 | 68.2 | 74.4 | 71.0
AV | - | 6.6 | 102.3 | 73.2 | 69.7 | 43.7 | 43.2 | 48.5 | 47.6 | 67.0 | 55.8
XLAVS-R |  |  |  |  |  |  |  |  |  |  |  |
XLAVS-R 300M | A | 79.8 | 42.4 | 100.1 | 69.4 | 56.2 | 39.9 | 33.4 | 40.5 | 45.4 | 53.0 | 53.4
AV | - | 5.8 | 95.8 | 61.4 | 44.7 | 28.0 | 27.2 | 29.4 | 30.6 | 47.8 | 41.2
XLAVS-R 2B | A | 74.0 | 49.5 | 98.9 | 66.3 | 50.6 | 36.0 | 30.0 | 36.8 | 40.6 | 48.3 | 50.8
AV | - | 5.9 | 93.5 | 58.5 | 38.6 | 23.9 | 23.5 | 24.6 | 26.1 | 41.0 | 37.3
Table 2: Results of audio-visual speech recognition (AVSR) on in-domain
(MuAViC) and out-of-domain (OOD, FLEURS) evaluation in test mode of audio-only
(A) and audio-video (AV). Our XLAVS-R model outperforms the two English-only
baselines of AV-HuBERT and u-HuBERT (both 300M sized) by up to 18% WER of in-
domain average in noisy AV mode.

##  4 Experiments

#### Data.

For AV pre-training, we leverage a total 1.2K hours of data in 9 languages:
English (En), Arabic (Ar), German (De), Greek (El), Spanish (Es), French (Fr),
Italian (It), Portuguese (Pt) and Russian (Ru). For A-only pre-training, we
follow Babu et al. (2022) for training on 436K-hour data in 128 languages.

For all the pre-trained models, we perform multilingual fine-tuning on MuAViC
labeled data for audio-visual speech recognition (AVSR) in all 9 languages and
audio-visual speech-to-text translation (AVS2TT) in 6 language pairs into
English—El, Es, Fr, It, Pt, Ru.

We use MuAViC for in-domain evaluation on both audio-only and audio-visual
test modes. We use FLEURS Conneau et al. (2023) for audio-only out-of-domain
(OOD) evaluation. We report an average of all 9 languages for AVSR and 6 X-to-
English language pairs for AVS2TT in both in-domain and out-of-domain
evaluation.

We remove extremely short utterances (less than 0.2 seconds) and long
utterances (more than 20 seconds) for better training stability.

Model | Test Mode | OOD | In-Domain
---|---|---|---
Avg | El-En | Es-En | Fr-En | It-En | Pt-En | Ru-En | Avg
Clean environment, Test BLEU $\uparrow$ |
AV-HuBERT (Shi et al., 2022b) | A | 12.7 | 13.9 | 22.3 | 28.1 | 23.5 | 26.1 | 10.7 | 20.8
AV | - | 14.3 | 22.9 | 28.3 | 23.9 | 26.5 | 11.2 | 21.2
u-HuBERT (Hsu and Shi, 2022) | A | 12.8 | 14.4 | 23.0 | 28.6 | 23.4 | 26.6 | 11.3 | 21.2
AV | - | 14.5 | 23.1 | 28.6 | 23.7 | 27.0 | 11.4 | 21.4
XLAVS-R |  |  |  |  |  |  |  |  |
XLAVS-R 300M | A | 14.0 | 18.9 | 23.7 | 29.7 | 24.9 | 28.5 | 12.6 | 23.0
AV | - | 19.1 | 23.8 | 29.8 | 25.0 | 28.8 | 13.0 | 23.2
XLAVS-R 2B | A | 16.0 | 21.7 | 25.0 | 30.6 | 26.5 | 30.2 | 13.9 | 24.7
AV | - | 21.6 | 25.1 | 30.6 | 26.6 | 29.9 | 13.9 | 24.6
Noisy environment, Test BLEU $\uparrow$ |
AV-HuBERT (Shi et al., 2022b) | A | 3.2 | 4.4 | 9.1 | 13.1 | 8.3 | 8.8 | 4.8 | 8.1
AV | - | 8.8 | 15.6 | 19.2 | 15.0 | 17.6 | 7.2 | 13.9
u-HuBERT (Hsu and Shi, 2022) | A | 3.4 | 4.7 | 9.8 | 13.8 | 8.7 | 10.3 | 5.3 | 8.8
AV | - | 8.2 | 15.6 | 19.7 | 14.6 | 18.3 | 7.3 | 14.0
XLAVS-R |  |  |  |  |  |  |  |  |
XLAVS-R 300M | A | 4.3 | 8.3 | 13.9 | 20.4 | 15.2 | 15.1 | 8.2 | 13.5
AV | - | 13.2 | 17.4 | 23.8 | 18.7 | 21.8 | 9.4 | 17.4
XLAVS-R 2B | A | 6.4 | 11.0 | 15.1 | 20.9 | 16.2 | 16.0 | 9.0 | 14.7
AV | - | 15.7 | 19.2 | 24.6 | 20.1 | 22.3 | 10.4 | 18.7
Table 3: Results of audio-visual speech-to-text translation (AVS2TT) on in-
domain (MuAViC) and out-of-domain (OOD, FLEURS) evaluation in test mode of
audio-only (A) and audio-video (AV). Our XLAVS-R model outperforms the two
English-only baselines of AV-HuBERT and u-HuBERT (both 300M sized) for all
language pairs in any mode and by up to 4.8 BLEU of in-domain average in noisy
AV mode.

#### Modeling.

We build XLS-R (§3.1) and XLAVS-R (§3) models in two model sizes: 300M and 2B.
The number of encoder layers/embedding dimension/feed forward dimension are
24/1024/4096 and 48/1920/7680 respectively. For audio-visual training targets
of XLAVS-R, we extract audio-only speech representation from the 36th layer of
XLS-R 2B and quantize it with 2000 k-means clusters. For fine-tuning AVSR and
AVS2TT models, we follow Anwar et al. (2023) to add a Transformer decoder that
has 6 layers, an embedding dimension of 768, and feed forward network
dimension of 3072. The visual feature extractor of our model is modified
ResNet-18 as in AV-HuBERT and prior lipreading works (Stafylakis and
Tzimiropoulos, 2017; Martinez et al., 2020; Ma et al., 2021). For XLAVS-R, we
set both $p_{m}$ and $p_{a}$ to 0.5 for pre-training which is the same with
AV/u-HuBERT. For fine-tuning all pre-trained models, we set $p_{m}$ and
$p_{a}$ to 0.5 and 0, where the models use 50% AV modality and 50% A-only
modality.

#### Noise Augmentation.

Following Shi et al. (2022b) and Anwar et al. (2023), we randomly augment the
input samples with additive noises at 0dB of signal-to-noise ratio. Noise
audio clips are sampled from the MUSAN dataset Snyder et al. (2015) as well as
drawn from MuAViC train set (for babble type of noises). We augment 25% of the
input in pre-training and 50% in fine-tuning with noises.

#### Evaluation.

We evaluate AVSR and AVS2TT in audio-only (“A”) and audio-visual (“AV”) test
modes, where the former leverages only audio modality in inference while the
latter leverages both audio and visual modalities. We select the best
checkpoint by validation accuracy for inference. We use beam search with
default hyper-parameters and beam size of 5. For AVSR, we apply Whisper text
normalizer Radford et al. (2023) before calculating WER (word error rate). For
AVS2TT, we compute BLEU Papineni et al. (2002) using SacreBLEU Post (2018)
with default options and the built-in 13a tokenizer. For the simulation of
noisy test environment, we add babble type of noises drawn from MuAViC test
set.

Figure 2: Effectiveness of each component towards XLAVS-R and multilingual
pre-training data starting from AV-HuBERT model pre-trained only on MuAViC-En.
All the components of XLAVS-R are shown to be effective. Each ablated pre-
trained models are fine-tuned and evaluated on multilingual audio-visual
speech recognition with identical training and test settings (A: audio, AV:
audio+video). The numbers of the plots are in Appendix, Table 7.

##  5 Results

###  5.1 Multilingual Speech Recognition

We compare our XLAVS-R representations against the AV-HuBERT and u-HUBERT
English-only representations when fine-tuned for multilingual speech
recognition in Table 2, reporting WER on both clean and noisy inputs in the
upper and lower half of the Table respectively.

In the clean setup, the XLAVS-R models perform on par or better than the
baselines in both audio-only and audio-visual test modes. The XLAVS-R 300M
model outperforms the AV-HuBERT and u-HuBERT, English-only AV pre-trained
models of similar size, by up to 9% WER and 8.7% WER respectively for average
audio-only and audio-visual test modes. Our larger XLAVS-R 2B outperforms the
English-only baseline by an average 11.5% WER and the average of 11.4% WER
respectively for the two modes. XLAVS-R 300M and 2B both outperform the
baselines by large margins in every non-English language. English WER slightly
increased in XLAVS-R 300M model compared to the English-only pre-trained
baseline by 0.5% WER. We attribute this effect to inter-language competition
(Conneau et al., 2020; Chang et al., 2023), since XLAVS-R 300M covers 128
languages with the same capacity as the English-only baselines (Table 1).
Increasing the XLAVS-R model capacity to 2B achieves the lowest WER of all
models in both A and AV modes. The OOD results on FLEURS confirm that our
models also maintain reasonable Audio-only performance on other existing
benchmarks.

In the noisy setup, where we add multilingual babble noises to clean speech
inputs, the XLAVS-R models improve performance across the board, in all
languages and in both modes. In the AV mode, the average WER for XLAVS-R 2B
drops significantly to 37.3%, which remarkably approaches that of the
AV/u-HuBERT baseline in clean settings.

Overall, XLAVS-R models outperform the two baselines by a large margin on
average in clean and noisy settings, while remaining competitive with English-
only pre-trained models in English. Results of experiments with additional AV
data for domain and language coverage during AV pre-training are available in
Appendix A and Table 5.

(a) In-domain test average of 300M sized model

(b) In-domain test average of 2B sized model

Figure 3:  XLAVS-R shows greater zero-shot ability on audio-visual test mode
with audio-only fine-tuned (FT, striped) model compared to that of AV-HuBERT.
Without fine-tuned on the labeled audio-visual set, the A-only FT model from
XLAVS-R shows 5% WER improvement on AV test mode compared to A test mode
(purple), while that of AV-HuBERT shows only 3% WER (orange) in a noisy
environment. The bigger the XLAVS-R model size, the greater the zero-shot
ability—the gap of 9.8% WER between A and AV test mode of A-only FT 2B model
in a noisy environment). Values of individual languages are in Appendix, Table
8.

###  5.2 Multilingual Speech-To-Text Translation

Next, we evaluate models fine-tuned for the X-En AVS2TT tasks (Table 3),
reporting BLEU scores in clean (top) vs. noisy settings (bottom).

In the clean setup, XLAVS-R 300M outperforms the English-only pre-trained
AV/u-HuBERT by up to 2.2 and 2 BLEU average scores for audio-only and audio-
visual modes. It consistently outperforms the baseline by large margins in all
directions and test modalities, suggesting that multilingual pre-training is
essential for cross-lingual ability in the downstream tasks. Our best model,
XLAVS-R 2B outperforms the English-only baselines by even wider margins (up to
3.9 and 3.4 BLEU average scores respectively for the two modes).

In the noisy setup, we simulate noisy environments as in AVSR tasks by adding
multilingual babble noises to clean speech sources. XLAVS-R 300M outperforms
the English-only baselines of similar size largely by up to 5.4/3.5 average
BLEU improvement on A/AV, and 6.6/4.8 average BLEU for 2B model.

Overall, these results show that our XLAVS-R models outperform two baselines
by a large margin in all translation directions for both clean and noisy
settings, both A-only and AV test modes, and both in-domain and OOD. Results
of experiments with additional AV data for domain and language coverage during
AV pre-training are available in Appendix A and Table 6.

###  5.3 Ablation Experiments of XLAVS-R

In Figure 2111Appendix Table 7 contains the exact numbers plotted., we
validate the effectiveness of the key changes from AV-HuBERT to XLAVS-R, step-
by-step starting from AV-HuBERT pre-trained on MuAViC-En. First, simplifying
the training process – single-round AV-HuBERT training with self-supervised
contextualized audio-only units from XLS-R (\+ Single-round w/SSL units)
instead of the original 5 training rounds – actually yields moderate
improvements. Second, switching to a learnable audio feature extractor (\+
Learnable AFE) shows the biggest improvements in both clean and noisy
settings, especially in the low-resource languages (El and Ru). Third,
augmenting AV pre-training with multilingual data (\+ MuAViC non-English) is
the second-highest improvement indicating that multilingual audio-visual
representation learning is critical in the self-supervised pre-training stage.
Last, the introduction of the audio-only pre-training stage and multilingual
audio-only resources (\+ A-only pre-training (XLAVS-R)) further improves both
A and AV performance in the in-domain evaluations. It yields even higher
improvements in OOD evaluations, suggesting that audio-only pretraining may
enhance robustness against domain shift.

In sum, all of the design contributions of XLAVS-R are shown to be effective.

###  5.4 Zero-shot Audio-Visual Inference

We compare the performance of A-only fine-tuning vs. AV fine-tuning: this
matters when labels for a given language in downstream task are not available
for AV fine-tuning, and thus we need to rely on the zero-shot audio-visual
ability from the pre-trained AV representation. In A-only FT, we exclude any
visual modalities for all languages.

For 300M models (Figure 3(a)), XLAVS-R shows only a mild performance
degradation in the noisy AV mode from AV FT to zero-shot A-only FT (41.2 WER
to 48.2 WER, 17% increase rate) and almost none in clean. By contrast, the AV-
HuBERT baseline shows severe degradation even in the clean setting—56.1 to
79.8, 42.25% in noisy, and 27.7% in the clean setting. The XLAVS-R model thus
effectively transfers knowledge from the pre-trained AV representation and
leverages it for downstream tasks, even though there is no visual modality
involved at all during the supervised fine-tuning.

For 2B models (Figure 3(b)), although AV FT has better recognition performance
in a clean setting (23.6 vs 25.0 WER in AV mode), A-only FT model has even
better performances over AV FT mode in noisy settings tested on AV mode (37.2
vs 37.3 WER), showing that the increased model capacity improves its zero-shot
ability. The result of the scaled-up model suggests that XLAVS-R relaxes the
need for labeled AV datasets of downstream tasks to have noise robustness.

##  6 Conclusion

We introduced XLAVS-R, a cross-lingual audio-visual speech representation for
noise-robust speech perception in over 100 languages. Since audio-visual data
is harder to come by than audio-only data, we injected the visual modality by
continuing training an audio-only pre-trained model. We also design a simpler
yet more effective training scheme and improved architecture compared to
previous state-of-the-art models. Extensive evaluation on the MuAViC benchmark
shows XLAVS-R achieves SOTA performance on both audio-visual speech
recognition and translation tasks, yielding particularly large improvements in
noisy settings. We also show that XLAVS-R effectively leverages unlabeled
audio-only multilingual speech data and audio-visual data in self-supervised
learning to show enhanced zero-shot audio-visual ability for downstream tasks.

## Limitations

Our findings are inherently limited by the settings of our empirical
evaluation. For instance, we simulate noisy environments only with the
“babble” sound in testing experimental setup (§4), and it remains to be seen
how other types of noise might impact our model. In addition, while we include
a diverse set of languages with varying amounts of resources in our
evaluation, we did not evaluate translation out-of-English and between non-
English languages.

## References

  * Afouras et al. (2022) Triantafyllos Afouras, Joon Son Chung, Andrew Senior, Oriol Vinyals, and Andrew Zisserman. 2022.  Deep audio-visual speech recognition.  _IEEE Transactions on Pattern Analysis and Machine Intelligence_ , 44(12):8717–8727.
  * Anwar et al. (2023) Mohamed Anwar, Bowen Shi, Vedanuj Goswami, Wei-Ning Hsu, Juan Pino, and Changhan Wang. 2023.  MuAViC: A Multilingual Audio-Visual Corpus for Robust Speech Recognition and Robust Speech-to-Text Translation.  In _Proc. INTERSPEECH 2023_ , pages 4064–4068.
  * Babu et al. (2022) Arun Babu, Changhan Wang, Andros Tjandra, Kushal Lakhotia, Qiantong Xu, Naman Goyal, Kritika Singh, Patrick von Platen, Yatharth Saraf, Juan Pino, Alexei Baevski, Alexis Conneau, and Michael Auli. 2022.  XLS-R: Self-supervised Cross-lingual Speech Representation Learning at Scale.  In _Proc. Interspeech 2022_ , pages 2278–2282.
  * Baevski et al. (2022) Alexei Baevski, Wei-Ning Hsu, Qiantong Xu, Arun Babu, Jiatao Gu, and Michael Auli. 2022.  data2vec: A general framework for self-supervised learning in speech, vision and language.  In _Proceedings of the 39th International Conference on Machine Learning_ , volume 162 of _Proceedings of Machine Learning Research_ , pages 1298–1312. PMLR.
  * Baevski et al. (2020) Alexei Baevski, Yuhao Zhou, Abdelrahman Mohamed, and Michael Auli. 2020.  wav2vec 2.0: A framework for self-supervised learning of speech representations.  In _Advances in Neural Information Processing Systems_ , volume 33, pages 12449–12460. Curran Associates, Inc.
  * Chang et al. (2023) Tyler A. Chang, Catherine Arnett, Zhuowen Tu, and Benjamin K. Bergen. 2023.  When is multilinguality a curse? language modeling for 250 high- and low-resource languages.
  * Cheng et al. (2023) X. Cheng, T. Jin, R. Huang, L. Li, W. Lin, Z. Wang, Y. Wang, H. Liu, A. Yin, and Z. Zhao. 2023.  Mixspeech: Cross-modality self-learning with audio-visual stream mixup for visual speech translation and recognition.  In _2023 IEEE/CVF International Conference on Computer Vision (ICCV)_ , pages 15689–15699, Los Alamitos, CA, USA. IEEE Computer Society.
  * Chiu et al. (2022) Chung-Cheng Chiu, James Qin, Yu Zhang, Jiahui Yu, and Yonghui Wu. 2022.  Self-supervised learning with random-projection quantizer for speech recognition.  In _Proceedings of the 39th International Conference on Machine Learning_ , volume 162 of _Proceedings of Machine Learning Research_ , pages 3915–3924. PMLR.
  * Choi et al. (2023) Jeongsoo Choi, Se Jin Park, Minsu Kim, and Yong Man Ro. 2023.  Av2av: Direct audio-visual speech to audio-visual speech translation with unified audio-visual speech representation.
  * Chung et al. (2017) Joon Son Chung, Andrew Senior, Oriol Vinyals, and Andrew Zisserman. 2017.  Lip reading sentences in the wild.  In _2017 IEEE Conference on Computer Vision and Pattern Recognition (CVPR)_. IEEE.
  * Communication (2023a) Seamless Communication. 2023a.  Seamless: Multilingual expressive and streaming speech translation.
  * Communication (2023b) Seamless Communication. 2023b.  Seamlessm4t: Massively multilingual & multimodal machine translation.
  * Conneau et al. (2021) Alexis Conneau, Alexei Baevski, Ronan Collobert, Abdelrahman Mohamed, and Michael Auli. 2021.  Unsupervised Cross-Lingual Representation Learning for Speech Recognition.  In _Proc. Interspeech 2021_ , pages 2426–2430.
  * Conneau et al. (2020) Alexis Conneau, Kartikay Khandelwal, Naman Goyal, Vishrav Chaudhary, Guillaume Wenzek, Francisco Guzmán, Edouard Grave, Myle Ott, Luke Zettlemoyer, and Veselin Stoyanov. 2020.  Unsupervised cross-lingual representation learning at scale.  In _Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics_ , pages 8440–8451, Online. Association for Computational Linguistics.
  * Conneau et al. (2023) Alexis Conneau, Min Ma, Simran Khanuja, Yu Zhang, Vera Axelrod, Siddharth Dalmia, Jason Riesa, Clara Rivera, and Ankur Bapna. 2023.  Fleurs: Few-shot learning evaluation of universal representations of speech.  In _2022 IEEE Spoken Language Technology Workshop (SLT)_ , pages 798–805.
  * Haliassos et al. (2023) Alexandros Haliassos, Pingchuan Ma, Rodrigo Mira, Stavros Petridis, and Maja Pantic. 2023.  Jointly learning visual and auditory speech representations from raw data.  In _The Eleventh International Conference on Learning Representations_.
  * Hsu et al. (2021) Wei-Ning Hsu, Benjamin Bolte, Yao-Hung Hubert Tsai, Kushal Lakhotia, Ruslan Salakhutdinov, and Abdelrahman Mohamed. 2021.  Hubert: Self-supervised speech representation learning by masked prediction of hidden units.  _IEEE/ACM Trans. Audio, Speech and Lang. Proc._ , 29:3451–3460.
  * Hsu and Shi (2022) Wei-Ning Hsu and Bowen Shi. 2022.  u-huBERT: Unified mixed-modal speech pretraining and zero-shot transfer to unlabeled modality.  In _Advances in Neural Information Processing Systems_.
  * Lian et al. (2024) Jiachen Lian, Alexei Baevski, Wei-Ning Hsu, and Michael Auli. 2024.  Av-data2vec: Self-supervised learning of audio-visual speech representations with contextualized target representations.
  * Ma et al. (2021) Pingchuan Ma, Stavros Petridis, and Maja Pantic. 2021.  End-to-end audio-visual speech recognition with conformers.  In _ICASSP 2021 - 2021 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_ , pages 7613–7617.
  * Martinez et al. (2020) Brais Martinez, Pingchuan Ma, Stavros Petridis, and Maja Pantic. 2020.  Lipreading using temporal convolutional networks.  In _ICASSP 2020 - 2020 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_ , pages 6319–6323.
  * May et al. (2023) Avner May, Dmitriy Serdyuk, Ankit Parag Shah, Otavio Braga, and Olivier Siohan. 2023.  Audio-visual fine-tuning of audio-only asr models.
  * Mroueh et al. (2015) Youssef Mroueh, Etienne Marcheret, and Vaibhava Goel. 2015.  Deep multimodal learning for audio-visual speech recognition.  In _2015 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_ , pages 2130–2134.
  * Ng et al. (2023) Dianwen Ng, Ruixiong Zhang, Jia Qi Yip, Zhao Yang, Jinjie Ni, Chong Zhang, Yukun Ma, Chongjia Ni, Eng Siong Chng, and Binchao Ma. 2023.  De’hubert: Disentangling noise in a self-supervised model for robust speech recognition.  _ICASSP 2023 - 2023 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_ , pages 1–5.
  * Panayotov et al. (2015) Vassil Panayotov, Guoguo Chen, Daniel Povey, and Sanjeev Khudanpur. 2015.  Librispeech: An asr corpus based on public domain audio books.  In _2015 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_ , pages 5206–5210.
  * Papineni et al. (2002) Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. 2002.  Bleu: a method for automatic evaluation of machine translation.  In _Proceedings of the 40th Annual Meeting of the Association for Computational Linguistics_ , pages 311–318, Philadelphia, Pennsylvania, USA. Association for Computational Linguistics.
  * Post (2018) Matt Post. 2018.  A call for clarity in reporting BLEU scores.  In _Proceedings of the Third Conference on Machine Translation: Research Papers_ , pages 186–191.
  * Potamianos et al. (2004) Gerasimos Potamianos, Chalapathy Neti, Juergen Luettin, and Iain Matthews. 2004.  Audio-visual automatic speech recognition: An overview.  _Issues in visual and audio-visual speech processing_ , 22:23.
  * Pratap et al. (2023) Vineel Pratap, Andros Tjandra, Bowen Shi, Paden Tomasello, Arun Babu, Sayani Kundu, Ali Elkahky, Zhaoheng Ni, Apoorv Vyas, Maryam Fazel-Zarandi, Alexei Baevski, Yossi Adi, Xiaohui Zhang, Wei-Ning Hsu, Alexis Conneau, and Michael Auli. 2023.  Scaling speech technology to 1,000+ languages.
  * Radford et al. (2023) Alec Radford, Jong Wook Kim, Tao Xu, Greg Brockman, Christine McLeavey, and Ilya Sutskever. 2023.  Robust speech recognition via large-scale weak supervision.  In _Proceedings of the 40th International Conference on Machine Learning_ , ICML’23. JMLR.org.
  * Seo et al. (2023) Paul Hongsuck Seo, Arsha Nagrani, and Cordelia Schmid. 2023.  Avformer: Injecting vision into frozen speech models for zero-shot av-asr.  In _Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition_ , pages 22922–22931.
  * Shi et al. (2022a) Bowen Shi, Wei-Ning Hsu, Kushal Lakhotia, and Abdelrahman Mohamed. 2022a.  Learning audio-visual speech representation by masked multimodal cluster prediction.  In _International Conference on Learning Representations_.
  * Shi et al. (2022b) Bowen Shi, Wei-Ning Hsu, and Abdelrahman Mohamed. 2022b.  Robust Self-Supervised Audio-Visual Speech Recognition.  In _Proc. Interspeech 2022_ , pages 2118–2122.
  * Snyder et al. (2015) David Snyder, Guoguo Chen, and Daniel Povey. 2015.  Musan: A music, speech, and noise corpus.
  * Stafylakis and Tzimiropoulos (2017) Themos Stafylakis and Georgios Tzimiropoulos. 2017.  Combining residual networks with lstms for lipreading.
  * Sumby and Pollack (1954) William H Sumby and Irwin Pollack. 1954.  Visual contribution to speech intelligibility in noise.  _The journal of the acoustical society of america_ , 26(2):212–215.
  * van den Oord et al. (2018) Aäron van den Oord, Yazhe Li, and Oriol Vinyals. 2018.  Representation learning with contrastive predictive coding.  _ArXiv_ , abs/1807.03748.
  * Vaswani et al. (2017) Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Ł ukasz Kaiser, and Illia Polosukhin. 2017.  Attention is all you need.  In _Advances in Neural Information Processing Systems_ , volume 30. Curran Associates, Inc.
  * wen Yang et al. (2021) Shu wen Yang, Po-Han Chi, Yung-Sung Chuang, Cheng-I Lai, Kushal Lakhotia, Yist Y. Lin, Andy T. Liu, Jiatong Shi, Xuankai Chang, Guan-Ting Lin, Tzu hsien Huang, Wei-Cheng Tseng, Ko tik Lee, Da-Rong Liu, Zili Huang, Shuyan Dong, Shang-Wen Li, Shinji Watanabe, Abdel rahman Mohamed, and Hung yi Lee. 2021.  Superb: Speech processing universal performance benchmark.  In _Interspeech_.
  * Zhang et al. (2023) Jing-Xuan Zhang, Genshun Wan, Zhen-Hua Ling, Jia Pan, Jianqing Gao, and Cong Liu. 2023.  Self-supervised audio-visual speech representations learning by multimodal self-distillation.  In _ICASSP 2023 - 2023 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_ , pages 1–5.
  * Zhu et al. (2023) Qiu-Shi Zhu, Long Zhou, Jie Zhang, Shu-Jie Liu, Yu-Chen Hu, and Li-Rong Dai. 2023.  Robust data2vec: Noise-robust speech representation learning for asr by combining regression and improved contrastive learning.  In _ICASSP 2023 - 2023 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_ , pages 1–5.
  * Zhu et al. (2024) Qiushi Zhu, Long Zhou, Ziqiang Zhang, Shujie Liu, Binxing Jiao, Jie Zhang, Lirong Dai, Daxin Jiang, Jinyu Li, and Furu Wei. 2024.  Vatlm: Visual-audio-text pre-training with unified masked prediction for speech representation learning.  _IEEE Transactions on Multimedia_ , page 1–11.

##  Appendix A Results with Additional Training Data

We also experiment with additional data for domain and language coverage
during the audio-visual self-supervised learning phase. On top of the existing
1.2K-hour data, we add 7.1K hours of in-house AV data in 100+ languages and
train XLAVS-R with a total of 8.3K hours in 100+ languages, as summarized in
the last row of Table 4. We show the AVSR and AVS2TT results comparing the
XLAVS-R 300M models trained on different sizes and numbers of the language of
the training dataset.

Table 5 shows AVSR performances of 9 languages on OOD and in-domain test sets.
On the in-domain test set, the model pre-trained on a scaled-up AV training
set shows improved AV average performances of 0.2% WER for both clean and
noisy environments. In contrast to the slight improvement or even the
degradation for noisy A-only mode in the in-domain, the 8.3K model shows
significant improvements in OOD for both clean and noisy settings by up to
6.1% WER on average.

Table 6 shows AVS2TT performances of 6 X-to-English pairs on OOD and in-domain
test sets, where the trend of the prominent improvement in OOD is similar to
that of AVSR comparison. Additional AV SSL dataset improves the average
performance of in-domain noisy setting by 0.7 BLEU for A-only test mode and
0.4 BLEU for AV test mode, while slightly degrades in clean settings by 0.1
BLEU in A-only test mode and 0.2 in AV test mode on average. In out-of-domain
evaluation, augmented data in AV SSL enhances the translation quality by up to
1.5 BLEU on average in noisy environments.

Overall, scaling up audio-visual pre-training data enhances robustness against
domain shift while also remains effective for noisy robustness with audio-
visual input in the in-domain.

| Hours | Languages
---|---|---
| A | AV | A | AV
Audio-Only Pre-Training Data
AVFormer Seo et al. (2023) | 60K | 0 | 1⋆ | 0
FAVA May et al. (2023) | 2.8K | 0 |  $>$100† | 0
Audio-Visual Pre-Training Data
AV-HuBERT Shi et al. (2022a) | 0 | 1.8K | 0 | 1⋆
AV-data2vec Lian et al. (2024) | 0 | 1.8K | 0 | 1⋆
AV2AV Choi et al. (2023) | 0 | 7K | 0 |  $>$100†
Audio-Only & Audio-Visual Pre-Training Data
u-HuBERT Hsu and Shi (2022) | 0.5K | 1.8K | 1⋆ | 1⋆
VATLM Zhu et al. (2024) | 4.3K | 1.8K | 1⋆ | 1⋆
XLAVS-R (w/ basic AV data) | 436K | 1.2K | 128 | 9
XLAVS-R (w/ extended AV data) | 436K | 8.3K | 128 | 100+†
Table 4: Pre-training data type, amount and language coverage in audio-visual speech perception models (A: audio, AV: audio-visual). Compared to prior work, XLAVS-R exploits audio-only speech data for efficient data scaling and language coverage expansion. ⋆ English-only. † Estimated by a speech language identification model.  Model | Test Mode | OOD | In-Domain
---|---|---|---
Avg | En | Ar | De | El | Es | Fr | It | Pt | Ru | Avg
Clean environment, Test WER (%) $\downarrow$
XLAVS-R 300M |  |  |  |  |  |  |  |  |  |  |  |
Basic AV data: 1.2K hours | A | 32.5 | 2.5 | 82.4 | 45.6 | 24.2 | 11.3 | 14.6 | 12.9 | 13.7 | 33.0 | 26.7
in 9 languages | AV | - | 2.4 | 81.7 | 44.7 | 24.3 | 10.9 | 14.4 | 12.8 | 13.2 | 32.7 | 26.3
Extended AV data: 8.3K hours | A | 28.3 | 2.2 | 80.2 | 38.7 | 28.7 | 11.9 | 15.5 | 14.1 | 14.9 | 32.1 | 26.5
in 100+ languages | AV | - | 2.1 | 80.0 | 38.0 | 28.1 | 11.7 | 15.3 | 13.8 | 14.4 | 31.2 | 26.1
Noise environment, Test WER (%) $\downarrow$
XLAVS-R 300M |  |  |  |  |  |  |  |  |  |  |  |
Basic AV data: 1.2K hours | A | 79.8 | 42.4 | 100.1 | 69.4 | 56.2 | 39.9 | 33.4 | 40.5 | 45.4 | 53.0 | 53.4
in 9 languages | AV | - | 5.8 | 95.8 | 61.4 | 44.7 | 28.0 | 27.2 | 29.4 | 30.6 | 47.8 | 41.2
Extended AV data: 8.3K hours | A | 73.7 | 44.0 | 97.2 | 62.4 | 60.7 | 41.0 | 36.2 | 44.5 | 48.0 | 51.0 | 53.9
in 100+ languages | AV | - | 5.3 | 91.9 | 53.5 | 49.6 | 28.8 | 29.3 | 32.2 | 32.5 | 46.1 | 41.0
Table 5: Comparison of XLAVS-R 300M models trained on different sizes of the audio-visual pre-training dataset. Results show the performance of audio-visual speech recognition (AVSR) on in-domain (MuAViC) and out-of-domain (OOD, FLEURS) evaluation in test mode of audio-only (A) and audio-video (AV).  Model | Test Mode | OOD | In-Domain
---|---|---|---
Avg | El-En | Es-En | Fr-En | It-En | Pt-En | Ru-En | Avg
Clean environment, Test BLEU $\uparrow$ |
XLAVS-R 300M |  |  |  |  |  |  |  |  |
Basic AV data: 1.2K hours | A | 14.0 | 18.9 | 23.7 | 29.7 | 24.9 | 28.5 | 12.6 | 23.0
in 9 languages | AV | - | 19.1 | 23.8 | 29.8 | 25.0 | 28.8 | 13.0 | 23.2
Extended AV data: 8.3K hours | A | 14.4 | 18.5 | 23.6 | 29.6 | 25.1 | 28.6 | 12.0 | 22.9
in 100+ languages | AV | - | 18.3 | 23.9 | 29.8 | 25.1 | 28.9 | 12.1 | 23.0
Noisy environment, Test BLEU $\uparrow$ |
XLAVS-R 300M |  |  |  |  |  |  |  |  |
Basic AV data: 1.2K hours | A | 4.3 | 8.3 | 13.9 | 20.4 | 15.2 | 15.1 | 8.2 | 13.5
in 9 languages | AV | - | 13.2 | 17.4 | 23.8 | 18.7 | 21.8 | 9.4 | 17.4
Extended AV data: 8.3K hours | A | 5.8 | 11.1 | 14.8 | 20.0 | 15.4 | 15.4 | 8.5 | 14.2
in 100+ languages | AV | - | 13.8 | 18.4 | 23.7 | 19.6 | 21.7 | 9.8 | 17.8
Table 6: Comparison of XLAVS-R 300M models trained on different sizes of the audio-visual pre-training dataset. Results show the performance of audio-visual speech-to-text translation (AVS2TT) on in-domain (MuAViC) and out-of-domain (OOD, FLEURS) evaluation in test mode of audio-only (A) and audio-video (AV).  Model | Test Mode | OOD | In-Domain
---|---|---|---
Avg | En | Ar | De | El | Es | Fr | It | Pt | Ru | Avg
Clean environment, Test WER (%) $\downarrow$
AV-HuBERT (MuAViC-En) | A | 45.5 | 4.3 | 92.3 | 56.4 | 48.9 | 19.4 | 22.2 | 23.5 | 25.0 | 48.3 | 37.8
AV | - | 2.2 | 91.1 | 54.7 | 47.7 | 18.6 | 21.6 | 22.6 | 23.8 | 46.5 | 36.5
\+ Single-round w/ SSL units | A | 44.6 | 3.9 | 89.7 | 56.4 | 48.7 | 20.1 | 23.0 | 24.4 | 25.9 | 48.3 | 37.8
AV | - | 2.6 | 89.3 | 54.4 | 47.5 | 18.7 | 22.5 | 23.7 | 24.6 | 46.3 | 36.6
\+ Learned AFE | A | 36.5 | 4.6 | 90.8 | 52.4 | 31.6 | 15.7 | 18.2 | 18.5 | 18.8 | 41.7 | 32.5
AV | - | 2.3 | 84.4 | 48.1 | 29.7 | 13.7 | 16.6 | 16.5 | 17.1 | 36.6 | 29.4
\+ MuAViC non-English | A | 35.1 | 3.1 | 83.7 | 50.0 | 28.1 | 12.7 | 16.9 | 15.9 | 16.6 | 37.1 | 29.3
AV | - | 2.8 | 82.2 | 48.4 | 27.0 | 12.1 | 16.6 | 15.2 | 15.6 | 35.1 | 28.3
\+ A-only pre-training (XLAVS-R) | A | 32.5 | 2.5 | 82.4 | 45.6 | 24.2 | 11.3 | 14.6 | 12.9 | 13.7 | 33.0 | 26.7
AV | - | 2.4 | 81.7 | 44.7 | 24.3 | 10.9 | 14.4 | 12.8 | 13.2 | 32.7 | 26.3
Noisy environment, Test WER (%) $\downarrow$
AV-HuBERT (MuAViC-En) | A | 100.2 | 85.3 | 113.9 | 95.0 | 89.9 | 74.8 | 67.1 | 78.5 | 79.2 | 82.3 | 85.1
AV | - | 9.5 | 107.3 | 79.5 | 74.3 | 49.4 | 48.0 | 54.1 | 52.5 | 71.5 | 60.7
\+ Single-round w/ SSL units | A | 93.8 | 67.1 | 109.1 | 90.3 | 86.1 | 68.4 | 63.6 | 74.3 | 73.7 | 79.1 | 79.1
AV | - | 9.0 | 102.2 | 76.0 | 71.5 | 46.5 | 46.6 | 51.9 | 50.8 | 69.7 | 58.2
\+ Learned AFE | A | 102.4 | 183.6 | 119.5 | 85.2 | 77.4 | 58.1 | 51.1 | 63.2 | 63.5 | 76.9 | 86.5
AV | - | 6.5 | 99.5 | 66.8 | 54.6 | 36.1 | 34.7 | 39.7 | 40.2 | 56.6 | 48.3
\+ MuAViC non-English | A | 88.4 | 100.7 | 104.3 | 76.2 | 63.6 | 46.9 | 41.3 | 50.3 | 56.5 | 60.7 | 66.7
AV | - | 6.3 | 94.3 | 63.7 | 46.3 | 28.3 | 29.4 | 31.0 | 32.9 | 50.3 | 42.5
\+ A-only pre-training (XLAVS-R) | A | 79.8 | 2.4 | 100.1 | 69.4 | 56.2 | 39.9 | 33.4 | 40.5 | 45.4 | 53.0 | 53.4
AV | - | 5.8 | 95.8 | 61.4 | 44.7 | 28.0 | 27.2 | 29.4 | 30.6 | 47.8 | 41.2
Table 7:  This is a table containing all the values of the plots in Section 5.3, Figure 2. Effectiveness of each component towards XLAVS-R and multilingual pre-training data starting from AV-HuBERT model pre-trained only on MuAViC-En. All the components of XLAVS-R are shown to be effective. Each ablated pre-trained models are fine-tuned and evaluated on multilingual audio-visual speech recognition with identical training and test settings (A: audio, AV: audio+video).  Model | Test Mode | OOD | In-Domain
---|---|---|---
Avg | En | Ar | De | El | Es | Fr | It | Pt | Ru | Avg
Clean environment, Test WER (%) $\downarrow$
300M model |  |  |  |  |  |  |  |  |  |  |  |
XLAVS-R | A | 30.3 | 2.2 | 81.7 | 45.6 | 23.6 | 11.2 | 14.8 | 12.7 | 13.5 | 32.9 | 26.5
(A-only fine-tuning) | AV | - | 2.2 | 82.1 | 45.2 | 23.6 | 11.0 | 14.7 | 12.8 | 13.5 | 33.0 | 26.5
XLAVS-R | A | 32.5 | 2.5 | 82.4 | 45.6 | 24.2 | 11.3 | 14.6 | 12.9 | 13.7 | 33.0 | 26.7
(AV fine-tuning) | AV | - | 2.4 | 81.7 | 44.7 | 24.3 | 10.9 | 14.4 | 12.8 | 13.2 | 32.7 | 26.3
2B model |  |  |  |  |  |  |  |  |  |  |  |
XLAVS-R | A | 35.5 | 2.2 | 83.3 | 49.0 | 22.3 | 9.6 | 13.2 | 10.5 | 11.2 | 26.6 | 25.3
(A-only fine-tuning) | AV | - | 2.0 | 83.7 | 48.2 | 21.6 | 9.4 | 13.2 | 10.4 | 10.9 | 26.0 | 25.0
XLAVS-R | A | 34.2 | 1.9 | 80.3 | 45.5 | 19.5 | 9.4 | 12.5 | 10.9 | 11.6 | 26.0 | 24.2
(AV fine-tuning) | AV | - | 1.7 | 79.3 | 44.4 | 19.0 | 9.1 | 12.3 | 10.6 | 11.2 | 25.0 | 23.6
Noisy environment, Test WER (%) $\downarrow$
300M model |  |  |  |  |  |  |  |  |  |  |  |
XLAVS-R | A | 78.1 | 45.1 | 102.2 | 68.1 | 55.1 | 39.2 | 33.2 | 39.9 | 44.9 | 52.3 | 53.3
(A-only fine-tuning) | AV | - | 13.8 | 101.4 | 66.5 | 52.7 | 37.1 | 31.5 | 38.3 | 40.9 | 51.9 | 48.2
XLAVS-R | A | 79.8 | 42.4 | 100.1 | 69.4 | 56.2 | 39.9 | 33.4 | 40.5 | 45.4 | 53.0 | 53.4
(AV fine-tuning) | AV | - | 5.8 | 95.8 | 61.4 | 44.7 | 28.0 | 27.2 | 29.4 | 30.6 | 47.8 | 41.2
2B model |  |  |  |  |  |  |  |  |  |  |  |
XLAVS-R | A | 74.3 | 34.2 | 100.9 | 65.1 | 52.6 | 31.8 | 26.7 | 31.7 | 35.4 | 44.8 | 47.0
(A-only fine-tuning) | AV | - | 4.3 | 96.3 | 60.3 | 41.6 | 23.0 | 22.1 | 22.9 | 24.7 | 39.3 | 37.2
XLAVS-R | A | 74.0 | 49.5 | 98.9 | 66.3 | 50.6 | 36.0 | 30.0 | 36.8 | 40.6 | 48.3 | 50.8
(AV fine-tuning) | AV | - | 5.9 | 93.5 | 58.5 | 38.6 | 23.9 | 23.5 | 24.6 | 26.1 | 41.0 | 37.3
Table 8:  This is a table containing all the values of the summarized plots in
Section 5.4, Figure 3. XLAVS-R shows greater zero-shot ability on audio-visual
test mode with audio-only fine-tuned (FT) model compared to that of AV-HuBERT.
Without fine-tuned on the labeled audio-visual set, the A-only FT model from
XLAVS-R shows 5% WER improvement on AV test mode compared to A test mode
(purple), while that of AV-HuBERT show only 3% WER (orange) in noisy
environment. The bigger the XLAVS-R model size, the greater the zero-shot
ability—the gap of 9.8% WER between A and AV test mode of A-only FT 2B model
in a noisy environment).


# Hybrid dynamical type theories for navigation ††thanks: This work has been
submitted to the IEEE for possible publication. Copyright may be transferred
without notice, after which this version may no longer be accessible.

Paul Gustafson<EMAIL_ADDRESS>School of Engineering and Applied Science,
University of Pennsylvania, Philadelphia, PA 19104, USA  Jared Culbertson
<EMAIL_ADDRESS>Autonomous Capabilities Team (ACT3), Air
Force Research Laboratory, Dayton, OH 45433, USA  Daniel Koditschek
<EMAIL_ADDRESS>School of Engineering and Applied Science, University of
Pennsylvania, Philadelphia, PA 19104, USA

###### Abstract

We present a hybrid dynamical type theory equipped with useful primitives for
organizing and proving safety of navigational control algorithms. This type
theory combines the framework of Fu–Kishida–Selinger for constructing linear
dependent type theories from state-parameter fibrations with previous work on
categories of hybrid systems under sequential composition. We also define a
conjectural embedding of a fragment of linear-time temporal logic within our
type theory, with the goal of obtaining interoperability with existing state-
of-the-art tools for automatic controller synthesis from formal task
specifications. As a case study, we use the type theory to organize and prove
safety properties for an obstacle-avoiding navigation algorithm of
Arslan–Koditschek as implemented by Vasilopoulos. Finally, we speculate on
extensions of the type theory to deal with conjugacies between model and
physical spaces, as well as hierarchical template-anchor relationships.

##  I Introduction

The problem of composing complex systems from simpler subcomponents is common
to all branches of engineering. A general approach is to specify interfaces
between components – both logical and physical. For logical interfaces,
arguably the most advanced specification language is dependent type theory, a
formal system capable of expressing the entirety of constructive mathematics
[29]. On the other hand, physical interfaces must deal with finite resources,
leading naturally to linear logic, a simultaneous refinement of intuitionistic
and classical logic that emphasizes the role of formulas as resources [18].
Combining linear logic with dependent types is still an active research area,
but much progress has been made in recent years [10, 36, 25, 30, 27]. We are
particularly interested in the categorical framework of [16], in which the
nonlinear dependent types can only depend on the “shape” of a linear term.
Roughly speaking, this means that type dependency lives on the parameter level
and cannot inspect state-level information of linear terms.

For applications to robotics, we desire a type system capable of encoding
sequential and parallel compositions, as well as safety constraints. The
former two forms of composition fit naturally within the framework of linear
logic, particularly via its incarnation as the internal language of symmetric
monoidal categories. Indeed, a weak version of such a category of directed
hybrid systems compatible with sequential and independent parallel composition
has been defined in [13]. On the other hand, safety constraints have a natural
formulation in the internal language of presheaves over an agent’s sensorium,
a setting particularly well-suited to formulating local conditions in the
presence of uncertainty.

As we note below, both of these categories—directed hybrid systems and
presheaves over the sensorium—can be connected via a state-parameter
fibration, the primary input to the linear dependent type theory construction
of [16]. Although that paper focuses primarily on a symmetric monoidal
category of quantum circuits and a corresponding state-parameter fibration
from a formal completion of the circuit category to the category of sets,
their construction applies equally well to state-parameter fibrations from
other symmetric monoidal categories to other locally cartesian closed
categories. In our setting, we replace quantum circuits with directed hybrid
systems and the base category $\mathbf{Set}$ with
$\operatorname{\mathbf{PSh}}(\Sigma)$, the category of presheaves over a
sensorium $\Sigma$.

With a state-parameter fibration and its corresponding linear dependent type
in hand, we are ready to give types to hybrid controllers used by real
engineers. We first provide a conjectural translation from a fragment of
linear-time temporal logic (LTL) into the type theory with the goal of
interfacing with existing state-of-the-art methods for controller synthesis
from formal task specifications [22, 34]. Then as a case study, we type
various components of a navigational controller designed by Arslan–Koditschek
[2] and implemented by Vasilopolous [37].

##  II Related work

The closest related work within robotics is the body of literature on
controller synthesis from temporal logic specifications. In 1977, Amir Pnueli
first proposed linear-time temporal logic as a specification language for
formal verification of computer programs [32]. In 1996, Antoniotti and Mishra
used computation tree logic, a branching-time temporal logic developed by
Clarke and Emerson to analyze concurrent programs [14], to generate a
supervisory controller for a walking robot [1]. In the mid 2000s, Kress-Gazit,
Fainekos, and Pappas developed a procedure for automatic controller synthesis
from an robot model, class of admissible environments, and LTL task
specification [22]. Subsequently as the field of robotics has grown in
importance, temporal logic-based specification has remained the dominant
paradigm for formal verification of controllers [28].

The main difference between our type-theoretic formalization and temporal
logic-based approaches is ease of composition. Whereas temporal logics are
close to natural human language [23], their basic connectives (e.g., “and,”
“or,” and classical implication) are a less convenient setting for sequential
and parallel composition of dynamical-system-based controllers than the linear
logic corresponding to the symmetric monoidal category of directed systems
[13].

On the other hand, the relative simplicity of LTL allows for automatic
controller synthesis once one restricts to a computationally tractable class
of formulas [8]. Thus, the strengths of the type-theoretic and temporal logic
approaches are in fact complementary. We provide a conjectural translation
between the two logical systems below.

On the type theory side, many have worked on integrating linear logic with
non-linear intuitionistic logic in general, and dependent type theory in
particular. The idea of using a linear-nonlinear adjunction, i.e. a pair of
symmetric monoidal functors between a symmetric monoidal closed category and a
cartesian closed category, to relate a linear type theory to the simply typed
lambda calculus originates with Benton [7]. Adding dependent types is
significantly harder since it is not immediately clear what it means for a
type to depend on a linear term. In particular, if $u:L$ is a linear term and
$T_{x}$ is a type family depending on $L$, then both terms $x_{u}$ of type
$T_{u}$ and the type $T_{u}$ itself generally reference the term $u$—a
violation of linearity, the axiom that linear terms must be used exactly once.

One approach to resolving this contradiction is to have two separate
contexts—one for linear data, and one for intuitionistic data—and prescribe
how types are allowed to depend on linear terms. This is the approach taken by
Cervesato and Pfenning in their Linear Logical Framework combining linear
logic with $LF$ [10]. In their system, types may not depend on linear terms at
all, only intuitionistic terms.

A significant further advance was McBride’s use of indices
$k\in\\{0,1,\omega\\}$ to decorate the typing annotations $x:_{k}A$ to denote
the number of times the variable $x$ is used. When $k=\omega$, his dependent
types corresponds to those of Cervesato and Pfenning. The index $k=0$
corresponds to terms that occur in types, and $k=1$ corresponds to terms
evaluated at runtime. This allowed much more granular control over variable
usage, enabling non-trivial type dependence on linear terms.

Recently, Licata, Shulman, and Riley vastly generalized this work in their
fibrational framework for substructural and modal logics [27], parameterizing
a type theory by an underlying mode theory. Categorically, their framework
corresponds to a functor between 2-dimensional cartesian multicategories, a
powerful but very abstract setting.

In the current paper, we employ the framework of Fu–Kishida–Selinger [16] for
constructing linear dependent type theories from state-parameter fibrations.
Their approach uses McBride’s approach to variable count indexing, but also
shares the fibrational approach to categorical semantics of
Licata–Shulman–Riley in a less abstract setting (monoidal category theory,
rather than higher category theory).

##  III A state-parameter fibration

The primary datum required in the construction of the linear dependent type
theory defined in [16] is a state-parameter fibration, a categorical fibration
from a symmetric monoidal closed category (a setting for linear logic) to a
locally cartesian closed category (a setting for dependent type theory)
satisfying some additional compatibility axioms.

To construct such a fibration, we start with a symmetric monoidal category of
“generalized circuits,” in our case directed hybrid systems as defined in
[13]. In brief (using the notation of [13], where full details can also be
found), a hybrid system $H$ consists of a directed graph $G(H)$, whose
vertices index a set of continuous modes $\\{I_{v}\\}_{v\in G(H)}$ and whose
edges index a set of reset maps $\\{r_{e}\\}_{e\in G(H)}$ between these modes.
We can then define a hybrid semiconjugacy $\alpha:H\to K$ of hybrid systems to
be a graph morphism on the underlying graphs together with a collection of
smooth maps $\alpha_{v}:I_{v}(H)\to I_{\alpha(v)}(K)$ restricting to classical
smooth semiconjugacies of the continuous flows and respecting the discrete
jumps in the sense that the squares

$I_{v}(H)$$I_{u}(H)$$I_{\alpha(v)}(K)$$I_{\alpha(u)}(K)$$r_{e}$$\alpha_{v}$$\alpha_{u}$$r_{\alpha(e)}$

commute for each reset map $r_{e}:I_{v}\to I_{u}$. These basic constructions
then allow us to define a directed hybrid system to be a cospan of hybrid
semiconjugacies

$H_{i}\to H\leftarrow H_{f}$

such that (i) both legs are embeddings, (ii) each component map of the right
leg is a diffeomorphism, (iii) the image of the graph $G(H_{f})$ in $G(H)$ is
a sink, and (iv) for every $\epsilon,T>0$ and state $x\in I(H)=\sqcup_{v\in
G(H)}I_{v}(H)$, there exists an $(\epsilon,T)$-chain from $x$ to the image of
$H_{f}$ in $H$. Roughly speaking, such a system forms the ambient substrate
for a “funnel” leading its initial subsystem $H_{i}$ into its final subsystem
$H_{f}$.

Sequential composition corresponds to the usual notion of composition of
cospans via pushouts: the directed system $H^{\prime}\odot H$ obtained by
composing the systems $H:H_{i}\to K$ and $H^{\prime}:K\to H^{\prime}_{f}$ is
given by

$K$$H^{\prime}$$H$$H^{\prime}\odot H$ ,$K\to H^{\prime}$$K\to H$

an operation defined only up to isomorphism [6, 19]. Thus, in order to get a
strict category, we will consider directed systems up to conjugacy; that is,
up to isomorphisms with respect to hybrid semiconjugacy. Using the categorical
product with respect to semiconjugacy defined in [13] as the monoidal product,
we then have a symmetric monoidal category $\mathbf{DH}$ of directed systems
up to conjugacy under sequential composition.

Following the recipe of [16], our first step towards constructing a
corresponding linear dependent type theory is to embed $\mathbf{DH}$ into a
symmetric monoidal closed category with products $\mathbf{\overline{DH}}$ by
taking the Yoneda embedding. This procedure formally extends the category with
exponential objects and categorical products for a more ergonomic type theory.

The second step is to form a category $\mathbf{\overline{\overline{DH}}}$ of
parametrized circuits. In their case, the spaces of parameters are sets; in
ours, presheaves over a topological space $\Sigma$, which we call the
sensorium. An object $A$ of this category consists of a pair
$(\underline{A},(A_{x})_{x\in A})$ where $\underline{A}$ is a presheaf over
the sensorium $\Sigma$, and $(A_{x})$ is an indexed family of objects of
$\mathbf{\overline{DH}}$, one for each element of $A$ (here, an element of a
presheaf is a morphism $*\to A$, i.e. a choice of set-element over every open
set of $\Sigma$). An arrow $f:A\to B$ consists of a pair
$(\underline{f},(f_{x})_{x\in A})$ where
$\underline{f}:\underline{A}\to\underline{B}$ is a map of presheaves, and
$(f_{x}:A_{x}\to B_{\underline{f}(x)})$ is an indexed family of morphisms of
$\mathbf{\overline{DH}}$.

One can check, following the proof of Fact 2.4 in [16], that the functor
$\mathbf{\overline{\overline{DH}}}\to\operatorname{\mathbf{PSh}}(\Sigma)$
given by projecting to the first component forms a state-parameter fibration.

##  IV Type system

For the purposes of our navigational case study, we focus on three families of
simple types: $See(n)_{n\in\mathbb{N}}$, $At(x)_{x\in X}$ where $X$ is a two-
dimensional manifold (the “workspace”), and $Safe(c)$ where $c$ is any term.
Figure 1 provides their semantics as objects in
$\mathbf{\overline{\overline{DH}}}$, fixing the sensorium
$\Sigma:=C(S^{1},\overline{\mathbb{R}_{\geq 0}})$ corresponding to distance
measurements from a limited range line-of-sight sensor. For example, the
hybrid system associated to $See(n)$ consists of $n$ object centers and radii
with a $0$ vector field, while its presheaf consists of a proof that for every
sensor measurement $f$ in an open set of uncertainty $U$, there exist $n$
connected components of distance readings less than a maximum range $M$.

Type | Hybrid System | Presheaf (evaluated at $U\subset\Sigma$)
---|---|---
$See(n)$ | $(X^{n}\times\mathbb{R}^{n},0)$ | $|\pi_{0}(f^{-1}([0,M])|=n\quad\forall f\in U$
$At(g)$ | $(X,-\nabla\|x-g\|^{2})$ | $\sup_{f\in U}d(x_{f},g_{f})<\epsilon$
$Safe(c)$ | $Unit$ | $\sup_{f\in U}\min_{\theta}f(\theta)>R$
Figure 1: Semantics of simple types with sensorium
$\Sigma:=C(S^{1},\overline{\mathbb{R}_{\geq 0}}$). In the presheaf associated
to $\operatorname{At}(g)$, the symbols $x_{f}$ and $g_{f}$ correspond to the
robot’s inferred position and goal locations based on a sensor reading $f$.

With the exception of the simple types, the syntax of the corresponding type
theory shown in Figure 2 is identical to [16], which we refer to for the
corresponding inference rules. The most interesting types are the linear
dependent sum and linear dependent function. Just as with regular dependent
types, a term of a linear dependent sum $(x:A)\otimes B[x]$ is a pair
$(x,b_{x})$ of types $A$ and $B[x]$, respectively, and a term of a linear
dependent function $(x:A)\multimap B[x]$ is a function that returns a term of
type $B[x]$ for every term $x:A$. However, linear (i.e. state-level) variables
can only be used at most once with one exception—their “shape” can be used
arbitrarily many times in parameter types. Roughly speaking, the shape of
state-level data corresponds to replacing every simple type in its definition
by the $Unit$ parameter type.

In the formal type theory, variable usage is encoded by the index $k$ in
$x:_{k}A$, and the inference rules enforce state-parameter usage constraints.
The “!”, $\operatorname{lift}$, and $\operatorname{force}(^{\prime})$
operations move types and terms from the state-level to the parameter level
and vice versa, while ensuring that parameters can only depend on the shape of
linear terms.

  * _Simple types_ $S::=See(n)\mid At(x)\mid Safe(M)$

  * _Types_ $A,B::=S\mid Unit\mid!A\mid(x:A)\multimap B[x]\mid(x:A)\otimes B[x]\mid(x:P_{1})\to P_{2}[x]$

  * _Parameter types_ $P::=Unit\mid!A\mid(x:P_{1})\otimes P_{2}[x]\mid(x:P_{1})\to P_{2}[x]$

  * _Terms_ $M,N,L::=unit\mid x\mid\lambda x.M\mid MN\mid\operatorname{force}M\mid\operatorname{force}^{\prime}R$
$\mid\operatorname{lift}M\mid(M,N)\mid\operatorname{let}(x,y)=N\operatorname{in}M\mid\lambda^{\prime}x.R\mid
R_{1}@R_{2}$

  * _Parameter terms_ $R::=unit\mid x\mid\lambda^{\prime}x.R\mid R_{1}@R_{2}\mid\operatorname{force}^{\prime}R$
$\mid\operatorname{lift}M\mid(R_{1},R_{2})\mid\operatorname{let}(x,y)=R_{1}\operatorname{in}R_{2}$

  * _Values_ $V::=unit\mid x\mid\lambda x.M\mid\lambda^{\prime}x.R\mid\operatorname{lift}M$

  * _Indices_ $k::=0\mid 1\mid\omega$

  * _Contexts_ $\Gamma::=\cdot\mid x:_{k}A,\Gamma$

  * _Parameter contexts_ $\Phi::=\cdot\mid x:_{k}A,\Phi$, where $k=1$ only if $A$ is a parameter type.

Figure 2: Syntax of navigational type theory

We also have a conjectural embedding of a fragment of linear temporal logic
(LTL) [32] into the type theory shown in Figure 3. We translate the atomic
propositions directly into hybrid dynamical types whose presheaves enforce the
invariant; for example, inhabitation in a partition element corresponds to a
presheaf only supported on that element. We translate “or” as the disjoint
union of hybrid systems, and “and” as the parallel composition. The
“Eventually” diamond corresponds to a directed system with codomain
corresponding to the argument of the diamond operator. We simply translate the
“Always” box operator as a directed system whose corresponding presheaf always
validates the argument proposition.

LTL Proposition $p$ | Hybrid dynamical type $T(p)$
---|---
$p\vee q$ | $T(p)\oplus T(q)$
$p\wedge q$ | $T(p)\otimes T(q)$
$\Diamond p$ | $\operatorname{Unit}\multimap T(p)$
$\Box p$ | $T(p)$
Figure 3: Conjectural embedding of a fragment of LTL

##  V Navigation example

Figure 4: Voronoi-based navigation using a limited range line-of-sight sensor
(Image source: [2])

As a case study, we formulate the navigation algorithm of [2] as a composition
of typed hybrid systems and proofs of correctness. Under an assumption on the
curvature of the obstacle boundaries (satisfied by circles, for example), the
main theorem of the paper is essentially

$(d(O_{i},O_{j})>2R\,\wedge\,d(x_{0},O_{i})>2R)\to\Box\forall_{i}d(O_{i})>R\,\wedge\,\Diamond(At(g)),$

where $x_{0}$ is the initial position of the robot, $R$ is a safety radius.
Rearranging things slightly, we want

$\displaystyle d(x_{0},O_{i})>2R)$
$\displaystyle\to\exists_{i,j}(d(O_{i},O_{j})\geq 2R$
$\displaystyle\vee\,(\Diamond(At(g))\,\wedge\,\Box\forall_{i}d(O_{i})>R).$

Under the translation shown in Figure 3, our task is to construct a controller
of type

$\displaystyle(d(x_{0},$ $\displaystyle
O_{i})>R)\to(O_{i},O_{j}:Obstacle)\otimes(d(O_{i},O_{j})\geq 2R)$
$\displaystyle\oplus(c:(Unit\multimap At(g)\oplus\,d(O_{i},O_{j})\leq
2R))\otimes Safe(c).$

That is, if the initial position of the robot is safe, then we have a safe
controller that reaches the goal unless the obstacle-separation assumption is
violated.

$\displaystyle Obstacle$
$\displaystyle=(center:X)\times(radius:\mathbb{R}_{\geq 0})$ $\displaystyle
SeparationViolation$ $\displaystyle=(O_{i},O_{j}:Obstacle)\to
d(O_{i},O_{j})\leq 2R$ $\displaystyle go$
$\displaystyle:(g:X,n:\mathbb{N})\to(c:(s:See(n))\multimap(At(g)\otimes
See(n))\oplus Interrupt(s))$ $\displaystyle Interrupt$
$\displaystyle:See(n)\multimap NewObs(See(n+1))\oplus LoseObs(See(n-1))$
$\displaystyle\oplus SV((O_{1},O_{2}:Obstacle)\otimes
SeparationViolation(o1,o2))$ $\displaystyle detect$
$\displaystyle:See(n)\multimap See(n-1)\oplus See(n)\oplus See(n+1)$
$\displaystyle visibleObs$ $\displaystyle:\,!See(n)\to List(Obstacle)$
$\displaystyle projGoal$ $\displaystyle:ConvHull(n)\to X\to X$ $\displaystyle
voronoi$ $\displaystyle:\,!See(n)\to ConvHull$ $\displaystyle ConvHull$
$\displaystyle=List(X)$ $\displaystyle startSensing$
$\displaystyle:Unit\multimap(n:\mathbb{N})\otimes See(n)$ $\displaystyle
stopSensing$ $\displaystyle:(n:\mathbb{N})\to See(n)\multimap Unit$
$\displaystyle controller$ $\displaystyle:(g:X)\to d(x,nearestObs(s))>R)$
$\displaystyle\to(f:Free\multimap At(g)\oplus(O_{i},O_{j}:Obstacle)\otimes
SeparationViolation(O_{i},O_{j}))\otimes Safe(f)$ Figure 5: Types for
navigation functions

    controller g p = (f, safetyProof f ) where
      f = stopSensing . c . startSensing
      c s = case mpg g p s of
        Left (localGoal, s)) ->
          if localGoal == g
          then (sp, d)
          else mpg g f s
        Right (NewObs s’)  -> inl (mpg g f s’)
        Right (LoseObs s’) -> inl (mpg g f s’)
        Right (SeparationViolation o1 o2) -> inr (SeparationViolation o1 o2)
      mpg g p s = go(projGoal(voronoi(lift(s)), g), f, s))
      safetyProof f = <Euclidean geometry formalization of Arslan-Koditschek proof>

Figure 6: Navigation controller pseudocode

The types shown in Figure 5 provide some Haskell-style typing declarations for
the functions involved in such a controller. For example, the “go” function’s
typing declaration in Figure 5 has the following meaning—for every natural
number $n$ and goal location $g$, given the data of a $Free$ navigational
state and $n$ visible objects, this controller will either end up at the goal
while still seeing $n$ objects or it will be interrupted. The $Interrupt$ type
says that the only interrupts correspond to seeing a new object, forgetting an
object, or noting that the object separation axiom is violated.

The “controller” function (Figure 6) is defined by looping over the MPG (move-
to-projected-goal) function as follows. The result of one application of the
MPG function is either arriving at the projected goal or an interrupt. If you
have arrived at the projected goal, check to see if it is the final goal
point, in which case you are done. Otherwise, check to see if you have
detected an obstacle separation violation. If so, pass the violation along and
stop. In all other cases, perform MPG again with your current location and
sensor readings. In addition, one would like a proof of safety — i.e. a term
of the $Safe$ type taking the controller definition as an argument. This
corresponds to formalizing Proposition 3 of [2], which states that the robot’s
free space is positively invariant.

##  VI Future work

This paper has outlined a type theory useful for organizing and proving safety
properties for navigational tasks – a baby step towards our broader goal of a
functional programming language for physical work. On the practical side, the
next step is to integrate some form of type checking with physical robot
platforms. There are two parts to this task – (i) integrating the Robot
Operating System (ROS) [33] with better support for functional programming in
general and linear dependent types in particular, and (ii) completing the
formalization of the algorithm in Figure 6. For the first task, one approach
would be to use ideas from RosHask [12] to call ROS from Haskell [21], and
either embed a linear dependent language in Haskell or follow Agda’s approach
to foreign function interface to Haskell [31]. For the second task, the main
obstacle is the reliance of the proof of safety on basic Euclidean geometry
which requires some effort to formalize. Fortunately, it may be possible to
leverage GeoCoq [9], a dependently typed formalization Tarski’s axiomatic
system [35] in the Coq proof assistant [11, 4], previously used to formalize
the first book of Euclid’s Elements [5, 20].

More theoretically, the type theory still leaves much to be desired. Perhaps
most urgent is the inclusion of template-anchor relationships, a form of
controller hierarchy integral to much of robotic programming [17]. A first
step towards this goal would be to extend the type theory to deal with hybrid
semiconjugacies, the vertical morphisms in the double category of hybrid
systems defined in [13], potentially leveraging work of New and Licata on
double categorical semantics of gradual typing [26].

Another important direction is the exploration of more expressive categories
of “funnel-like” systems closed under sequential composition. For example,
since our category of directed systems is not monoidal closed, we need to use
the Yoneda embedding to formally adjoin exponential objects. These formal
exponentials are not hybrid systems, but rather spaces of recipes for
producing hybrid systems. However, just as it is often useful to use the fact
that the collection of functions between two finite sets is itself a set, or
the collection of linear maps between two vector spaces is a vector space, we
believe that putting dynamical structures on the space of “funnels” between
two systems will prove useful. However, fundamental obstructions exist when
considering even classical dynamical systems, and finding a convenient
category in this setting requires considering alternative generalizations of
manifolds such as Chen spaces, diffeological spaces, or Frölicher spaces [3,
15]. Thus, a more natural setting for exploring exponentials in categories of
hybrid systems might be to consider more topological perspectives such as
locally preordered spaces [24]. Additionally, we might imagine a refinement
procedure that takes a crude plan (“funnel”) to get from an initial system to
a final system, and iteratively improves the plan, incorporating a
hierarchical notion of dynamics.

##  VII Acknowledgment

This work was supported in part by ONR N000141612817, a Vannevar Bush Faculty
Fellowship held by Koditschek and by UATL 10601110D8Z, a LUCI Fel-lowship held
by Culbertson, both granted by the Basic Research Office of the US
Undersecretary of Defense for Research and Engineering.

## References

  * [1] Marco Antoniotti and Bud Mishra  “Discrete event models+ temporal logic= supervisory controller: Automatic synthesis of locomotion controllers”  In _Proceedings of 1995 IEEE International Conference on Robotics and Automation_ 2, 1995, pp. 1441–1446  IEEE
  * [2] Omur Arslan and Daniel E Koditschek  “Sensor-based reactive navigation in unknown convex sphere worlds”  In _The International Journal of Robotics Research_ 38.2-3 SAGE Publications Sage UK: London, England, 2019, pp. 196–223
  * [3] John Baez and Alexander Hoffnung  “Convenient categories of smooth spaces”  In _Transactions of the American Mathematical Society_ 363.11, 2011, pp. 5789–5825
  * [4] Bruno Barras et al.  “The Coq proof assistant reference manual: Version 6.1”, 1997
  * [5] Michael Beeson, Julien Narboux and Freek Wiedijk  “Proof-checking Euclid”  In _Annals of Mathematics and Artificial Intelligence_ Springer Verlag, 2019, pp. 53  DOI: 10.1007/s10472-018-9606-x
  * [6] Jean Bénabou  “Introduction to bicategories”  In _Reports of the midwest category seminar_ , 1967, pp. 1–77  Springer
  * [7] P Nick Benton  “A mixed linear and non-linear logic: Proofs, terms and models”  In _International Workshop on Computer Science Logic_ , 1994, pp. 121–135  Springer
  * [8] Roderick Bloem et al.  “Synthesis of reactive (1) designs”  In _Journal of Computer and System Sciences_ 78.3 Elsevier, 2012, pp. 911–938
  * [9] Pierre Boutry, Gabriel Braun and Julien Narboux  “Formalization of the Arithmetization of Euclidean Plane Geometry and Applications”  In _Journal of Symbolic Computation_ 90, Special Issue on Symbolic Computation in Software Science  Elsevier, 2019, pp. 149–168  DOI: 10.1016/j.jsc.2018.04.007
  * [10] Iliano Cervesato and Frank Pfenning  “A linear logical framework”  In _Information and Computation_ 179.1 Elsevier, 2002, pp. 19–75
  * [11] Thierry Coquand and Gérard Huet  “The calculus of constructions”, 1986
  * [12] Anthony Cowley and Camillo J Taylor  “Stream-oriented robotics programming: The design of roshask”  In _2011 IEEE/RSJ International Conference on Intelligent Robots and Systems_ , 2011, pp. 1048–1054  IEEE
  * [13] Jared Culbertson, Paul Gustafson, Daniel E Koditschek and Peter F Stiller  “Formal composition of hybrid systems”  In _Theory and Applications of Categories_ 35.45, 2020, pp. 1634–1682
  * [14] E Allen Emerson and Edmund M Clarke  “Using branching time temporal logic to synthesize synchronization skeletons”  In _Science of Computer programming_ 2.3 Elsevier, 1982, pp. 241–266
  * [15] Alfred Frölicher  “Categories cartésiennement fermées engendrées par des monoides”  In _Cahiers de topologie et géométrie différentielle catégoriques_ 21.4, 1980, pp. 367–375
  * [16] Peng Fu, Kohei Kishida and Peter Selinger  “Linear dependent type theory for quantum programming languages”  In _Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science_ , 2020, pp. 440–453
  * [17] Robert J Full and Daniel E Koditschek  “Templates and anchors: neuromechanical hypotheses of legged locomotion on land”  In _Journal of experimental biology_ 202.23 Company of Biologists The Company of Biologists, Bidder Building, 140 Cowley …, 1999, pp. 3325–3332
  * [18] Jean-Yves Girard  “Linear logic”  In _Theoretical computer science_ 50.1 Elsevier, 1987, pp. 1–101
  * [19] Marco Grandis and Robert Paré  “Limits in double categories”  In _Cahiers de topologie et géométrie différentielle catégoriques_ 40.3, 1999, pp. 162–220
  * [20] Thomas Little Heath  “The thirteen books of Euclid’s Elements”  Courier Corporation, 1956
  * [21] Simon Peyton Jones  “Haskell 98 language and libraries: the revised report”  Cambridge University Press, 2003
  * [22] Hadas Kress-Gazit, Georgios E Fainekos and George J Pappas  “Temporal-logic-based reactive mission and motion planning”  In _IEEE transactions on robotics_ 25.6 IEEE, 2009, pp. 1370–1381
  * [23] Hadas Kress-Gazit, Georgios E Fainekos and George J Pappas  “Translating structured english to robot controllers”  In _Advanced Robotics_ 22.12 Taylor & Francis, 2008, pp. 1343–1359
  * [24] Sanjeevi Krishnan  “A convenient category of locally preordered spaces”  In _Applied Categorical Structures_ 17.5 Springer, 2009, pp. 445–466
  * [25] Neelakantan R Krishnaswami, Pierre Pradic and Nick Benton  “Integrating linear and dependent types”  In _ACM SIGPLAN Notices_ 50.1 ACM New York, NY, USA, 2015, pp. 17–30
  * [26] Daniel R Licata and Max S New  “Call-by-name Gradual Type Theory”  In _Logical Methods in Computer Science_ 16 Episciences. org, 2020
  * [27] Daniel R Licata, Michael Shulman and Mitchell Riley  “A fibrational framework for substructural and modal logics”  In _2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)_ , 2017  Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik
  * [28] Matt Luckcuck et al.  “Formal specification and verification of autonomous robotic systems: A survey”  In _ACM Computing Surveys (CSUR)_ 52.5 ACM New York, NY, USA, 2019, pp. 1–41
  * [29] Per Martin-Löf  “Constructive mathematics and computer programming”  In _Studies in Logic and the Foundations of Mathematics_ 104 Elsevier, 1982, pp. 153–175
  * [30] Conor McBride  “I got plenty o’nuttin”’  In _A List of Successes That Can Change the World_ Springer, 2016, pp. 207–233
  * [31] Ulf Norell  “Dependently typed programming in Agda”  In _International school on advanced functional programming_ , 2008, pp. 230–266  Springer
  * [32] Amir Pnueli  “The temporal logic of programs”  In _18th Annual Symposium on Foundations of Computer Science (sfcs 1977)_ , 1977, pp. 46–57  IEEE
  * [33] Morgan Quigley et al.  “ROS: an open-source Robot Operating System”  In _ICRA workshop on open source software_ 3.3.2, 2009, pp. 5  Kobe, Japan
  * [34] Indranil Saha et al.  “Automated composition of motion primitives for multi-robot systems from safe LTL specifications”  In _2014 IEEE/RSJ International Conference on Intelligent Robots and Systems_ , 2014, pp. 1525–1532  IEEE
  * [35] Alfred Tarski and Steven Givant  “Tarski’s system of geometry”  In _Bulletin of Symbolic Logic_ 5.2 Cambridge University Press, 1999, pp. 175–214
  * [36] Matthijs Vákár  “Syntax and semantics of linear dependent types”  In _arXiv preprint arXiv:1405.0033_ , 2014
  * [37] Vasileios Vasilopoulos et al.  “Reactive semantic planning in unexplored semantic environments using deep perceptual feedback”  In _IEEE Robotics and Automation Letters_ 5.3 IEEE, 2020, pp. 4455–4462