# On Code Safety for Quantum Intermediate Representations

Junjie Luo Kyushu University<EMAIL_ADDRESS>Kyushu University
Jianjun Zhao Kyushu University<EMAIL_ADDRESS>
# Formalization of Quantum Intermediate Representations
for Code Safety

Junjie Luo Kyushu University<EMAIL_ADDRESS>Kyushu University
Jianjun Zhao Kyushu University<EMAIL_ADDRESS>
###### Abstract

Quantum Intermediate Representation (QIR) is a Microsoft-developed, LLVM-based
intermediate representation for quantum program compilers. QIR aims to provide
a general solution for quantum program compilers independent of front-end
languages and back-end hardware, thus avoiding duplicate development of
intermediate representations and compilers. Since it is still under
development, QIR is described in natural language and lacks a formal
definition, leading to ambiguity in its interpretation and a lack of rigor in
implementing quantum functions. In this paper, we provide formal definitions
for the data types and instruction sets of QIR, aiming to provide correctness
and safety guarantees for operations and intermediate code conversions in QIR.
To validate our design, we show some samples of unsafe QIR code where errors
can be detected by our formal approach.

##  1 Introduction

Developing a Noisy Intermediate-Scale Quantum Computer (NISQ) [22] offers new
opportunities for research and development of quantum software. With the
increasing development of quantum hardware, quantum program processors (QPUs)
are expected to complement further and accelerate existing classical
scientific computation workflows, called heterogeneous quantum-classical
computation. Various programming languages such as Qiskit [2], Cirq [28], Q#
[27], Quipper [9], and ProjectQ [29] have been developed to implement such a
computational model. Like classical programs, compiled quantum programming
languages, such as Q#, require their quantum programs to be compiled by a
compiler into an intermediate representation (IR), which is subsequently
optimized and transformed for efficient execution on a designated platform.
Since IR has platform-independent features, its optimizer and executable
generator can be reused under multiple source languages and generate the
corresponding executable code according to the target execution platform. It
is often necessary to develop new IRs or extend existing ones to adapt the
intermediate representation to quantum properties. Some of the intermediate
representations used in quantum programming languages include MLIR [12, 15],
SQIR [10], and OpenQASM [6].

Quantum Intermediate Representation (QIR) [8] is a new intermediate
representation of quantum programs developed by Microsoft, based on the
popular open-source LLVM intermediate language [11]. QIR enables the
representation of quantum computing workflows and tasks by specifying a set of
rules for representing quantum structures in LLVM without any extensions or
modifications. Its goal is to provide a unified and common interface to
multiple quantum programming languages and quantum computing platforms, thus
facilitating the development of general quantum compilation tools that can be
reused in the compiler mechanism.

Figure 1: The QIR compiler architecture.

The QIR-based compiler processes the high-level source quantum language by
converting it to QIR and handing it over to the target backend for execution
(see Figure 1). Since QIR is designed and implemented based on LLVM, applying
the classical LLVM optimization methods to transform and optimize QIR code is
possible. However, since QIR is still in the early stage of development, it
lacks clear formal semantics. Thus, its execution and the correctness of the
optimization and conversion are difficult to rigorously proven, making it
difficult to guarantee the correct operations of quantum programs. In our
work, we hope to design a formal method for QIR and develop a framework for
verification based on this method so that QIR code can be tested for safety by
this verification framework before it actually executed.

In our work, we focus on the core functions of QIR, which play a crucial role
in the correct operation of QIR programs. Therefore, in this paper, we
prioritize formalizing the syntax and semantics of these core functions so
that we can detect possible errors in the execution of QIR’s core functions
and guarantee that QIR’s essential functions can be executed properly. Our
contributions can be summarized as follows:

  * •

We formalize the syntax of QIR based on the work of Zhao et al. [30].
Specifically, we have adapted its abstract syntax to remove LLVM directives
and types not used in QIR and augment QIR-specific data types.

  * •

We design the semantics of important instructions in QIR, such as allocation
and release qubits, gate operations, and measurement. These operations
constitute the implementation of the most basic quantum program functions, and
formalization based on them can allow us to capture unsafe parts of the code.

  * •

We design a management model for qubits through which, together with our
formal methods, the unsafe parts of the QIR code can be captured (e.g., qubits
cloning and the use of released qubits).

  * •

We validate the effectiveness of our formal approach by applying it to real
cases of unsafe QIR code.

The rest of the paper is organized as follows. We introduce the background
information of LLVM Intermediate Representation (LLVM IR) and QIR in Section
2. We present our formalization of the syntax and semantics of QIR in Section
3. The validation of our formal method with real-world examples is presented
in Section 4. We discuss related work in Sections 5, and the conclusion is
given in Section 6.

##  2 Background

This section briefly introduces LLVM IR, the basis of QIR, and QIR itself.

###  2.1 Basic Concepts

Unlike classical programs that use classical bits to store information, in
quantum programs, quantum bits (”qubits”) are used as the medium for storing
data. As compared to a classical bit that can only be in either $0$ or $1$
state, a qubit can be in both $0$ and $1$ states, and it is called a quantum
superposition state. The superposition state of a qubit can be represented by
$\ket{\psi}=\alpha\ket{0}+\beta\ket{1}$, where $\ket{}$ is called the Dirac
symbol, and $|\alpha|^{2}+|\beta|^{2}=1$. We cannot directly observe the state
of a qubit, which is in the superposition state; instead, we must measure it
and obtain a $0$-state with probability $|\alpha|^{2}$ or a $1$-state with
probability $|\beta|^{2}$.

In quantum computing, we usually use quantum logic gates to control the state
of the qubits. Some basic gate operations include:

  * •

X gate (NOT gate): When a quantum undergoes the X-gate operation, its state
changes from $\ket{\psi}=\alpha\ket{0}+\beta\ket{1}$ to
$\ket{\psi}=\beta\ket{0}+\alpha\ket{1}$. We can use the matrix to represent
this operation:

$X=\left[\begin{array}[]{ll}0&1\\\ 1&0\end{array}\right]$ (1)

  * •

Y gate and Z gate: Similarly, for the Y and Z gates have the following
expressions:

$Y=\left[\begin{array}[]{ll}0&-1i\\\ 1i&0\end{array}\right]\quad\&\quad
Z=\left[\begin{array}[]{ll}1&0\\\ 0&-1\end{array}\right]$ (2)

  * •

Hadamard gate (H gate): Hadamard gate can turn a $\ket{0}$ state or a
$\ket{1}$ state into a superposition of $\ket{0}$ and $\ket{1}$ with equal
probability:

$H=\frac{1}{\sqrt{2}}\left[\begin{array}[]{cc}1&1\\\ 1&-1\end{array}\right]$
(3)

  * •

Controlled gate: Unlike the single-qubit gate that can only accept one qubit
as input, as described above, the controlled gate can accept multiple qubits
as input. Specifically, for qubits input to the controlled gate, there are
control qubits and target qubits, and the state of the target qubit is changed
only when the states of both control qubits are $\ket{1}$. For example, for
the CNOT gate (Controlled NOT gate), the logical expression is:

$\ket{A,B}\rightarrow\ket{A,B\oplus A}$ (4)

Similarly, the Toffoli gate, also known as the CCNOT gate, possesses two
control qubits that together control the flip of the target qubit with the
expression:

$\ket{A,B,C}\rightarrow\ket{A,B,C\oplus AB}$ (5)

All the above quantum logic gates are reversible, so no information loss
occurs during quantum computing. By applying gate operations to qubits,
quantum circuits can be composed, and thus quantum algorithms can be
implemented. It is the model widely used by quantum programs nowadays. One
other important operation is measurement. A classical bit in a 0 or 1 state
can be obtained by performing a measurement operation on a single qubit. More
content related to quantum computing can be found in the book by Nielsen and
Chuang [21].

###  2.2 LLVM IR

The LLVM IR [11] is a high-level static single assignment form (SSA) language
used by the LLVM compiler infrastructure as the intermediate representation
for source code. It is a representation of the source code that is independent
of the source languages and target platforms. It is currently widely used and
there are many conversion and optimization methods available around it.
Compilers can perform various optimizations on the code of a program based on
this, including common subexpression elimination, dead code elimination, and
loop unrolling. These optimizations can improve the performance of the
generated machine code, making it run faster and more efficiently.

LLVM IR is a strongly typed language, meaning each value has a specific type,
such as an integer or floating point value. Such a design helps prevent type
errors and allows the compiler to generate more efficient code. Similar to
RISC instructions, LLVM IR is designed as a triple-address form. Combined with
its strong typing, it allows for both compilation and optimization based on
individual compilation units and precise global optimization performed at link
time using type information. LLVM IR also includes support for control flow,
loops, and other common language constructs, which makes it possible to
represent a wide range of programs.

###  2.3 Quantum Intermediate Representation (QIR)

Microsoft has developed a new quantum intermediate representation called
Quantum Intermediate Representation (QIR), which is based on the widely used
open-source LLVM IR. To promote QIR and provide solutions for efficient use of
different quantum processors, Microsoft has established the QIR Alliance [3].
QIR avoids the need for creating new compilers for different quantum
programming languages by leveraging the existing classical infrastructure of
LLVM IR, enabling support for the necessary functions of quantum programs
without requiring additional extensions or modifications. Specifically, QIR
preserves the LLVM primitives such as call, bitcast, getelementptr, and other
classical data types such as integer i$sz$ and double Double. In order to
implement quantum operations, QIR adds two data types to LLVM IR, %Qubit and
%Result, which represent quantum registers and the results of measurements,
respectively. There are also two data structures, %Array and %Tuple, which
represent arrays of the same type of data and user-defined structures composed
of arrays of multiple types, respectively. All the above four data types are
opaque to QIR. To make it easier to express the operations of qubits, QIR adds
new data types, such as %Pauli, which refers to the four Pauli matrices in
quantum mechanics.

In addition to the data types, QIR also declares quantum-related runtime
functions and functions that operate on qubits (e.g., quantum gate operations
and measurement operations). These functions are not implemented in the QIR
and need to be defined and implemented externally. Such a design facilitates
the adaptation of the QIR to different hardware backends, thus making the QIR
independent of the hardware backend. QIR’s official documentation [16]
contains definitions for its instructions, and we will provide a brief
explanation of the QIR instructions used in our work. Since the instructions
for qubits declared in QIR have the same prefix _@__quantum__rt___ or
_@__quantum__qis___ , in our work, we have adopted an omitted notation for
them to save space (e.g., the _@__quantum__rt__qubit_allocate_ is omitted and
noted as qubit_allocate, the @__quantum__qis__gateop__body is omitted and
noted as gateop__body).

Figure 2 shows a sample QIR code, which briefly describes the design of QIR.
Lines 1 to 3 of the code mark the opaque data types. In lines 5 through 12,
the code implements the function of allocating a qubit register and measuring
it after executing the H gate. In line 7, the qubit_allocate function is
called, which allocates a qubit register. The functions that perform
operations on the $Qubit$ are all declared as gateop__body, where gateop is
the specific operation to be performed, e.g., h in line 8 refers to the H
gate. After executing the H gate operation in line 8, the measurement
operation in line 9 is explicitly defined in lines 14 through 32. After
completing the measurement, the qubit is released with qubit_release in line
10, and the measurement result is returned in line 11.

    1   %Result = type opaque
    2   %Qubit = type opaque
    3   %Array = type opaque
    4
    5   define internal %Result* @Sample__SampleQ__body() {
    6   entry:
    7     %q = call %Qubit* @__quantum__rt__qubit_allocate()
    8     call void @__quantum__qis__h__body(%Qubit* %q)
    9     %0 = call %Result* @Microsoft__Quantum__Intrinsic__M__body(%Qubit* %q)
    10    call void @__quantum__rt__qubit_release(%Qubit* %q)
    11    ret %Result* %0
    12  }
    13
    14  define internal %Result* @Microsoft__Quantum__Intrinsic__M__body(%Qubit* %qubit) {
    15  entry:

        ...
    31    ret %Result* %4
    32  }
    33
    34    declare %Qubit* @__quantum__rt__qubit_allocate()
    35    declare void @__quantum__rt__qubit_release(%Qubit*)
    36    declare void @__quantum__qis__h__body(%Qubit*)
    37    declare void @__quantum__rt__array_update_alias_count(%Array*, i32)
    38    declare %Array* @__quantum__rt__array_create_1d(i32, i64)
    39    declare i8* @__quantum__rt__array_get_element_ptr_1d(%Array*, i64)
    40    declare %Result* @__quantum__qis__measure__body(%Array*, %Array*)
    41    declare void @__quantum__rt__array_update_reference_count(%Array*, i32)

Figure 2: Example of QIR.

##  3 Methodology

In this section, we formalize the syntax and semantics of QIR to support the
verification of unsafe code. Since QIR is designed based on LLVM IR, this
paper does not consider the formalization of the classical LLVM IR part, which
can be done using methods [30, 13]. Our formalization of QIP is based on
version 0.1 of QIR.

###  3.1 Syntax of QIR

We first present our formalization of the syntax of QIR in Figure 3. Our
abstract syntax extends on the work of Zhou et al. [30], which provides a
relatively complete formalization of LLVM IR. We mainly add to it data types
that are specific to QIR, such as %Qubit, %Result, %Array, etc. Since the QIR
instruction is called with LLVM’s call instruction, its abstract semantics can
be attributed to $id$, so instructions about quantum gate operations,
measurement operations, etc., cannot be reflected in the abstract syntax.

$\small\begin{array}[]{l}\text{Types\quad\quad\ $typ$ ::= {i}{sz} $|$ {double}
$|$ {typ}* $|$ [$sz\times typ$] $|$ $typ$ $\overline{typ_{j}}^{j}$ $|$
\\{$\overline{typ_{j}}^{j}$\\} $|$ {id} $|$
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\%Pauli}}
$|$
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\%Range}}
$|$
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\%Result}}
}\\\ \text{\quad\quad\quad\quad\quad\quad\ \ \ $|$
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\%Qubit}}
$|$
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\%Array}}
$|$
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\%Tuple}}}\\\
\text{Products\ \ {prod} ::= {define} $typ$ $id$ ($\overline{arg}$)
\\{$\overline{b}$\\} $|$ {declare} $typ$ $id$ ($\overline{arg}$)}\\\
\text{Values\quad\ \ \ \ $val$ ::= $id$ $|$ $cnst$}\\\ \text{Constants {cnst}
::= {i}{sz} {Int} $|$ {double} {Double} $|$ {void} $|$ $typ^{*}id$ $|$ $typ$
[$\overline{cnst_{j}}^{j}$] $|$ \\{$\overline{cnst_{j}}^{j}$\\} $|$
{extractvalue} $cnst$ $\overline{cnst_{j}}^{j}$ }\\\
\text{\quad\quad\quad\quad\quad\quad\ \ $|$ {getelementptr} $cnst$
$\overline{cnst_{j}}^{j}$ $|$ {bitcast} {cnst} {to} {typ} $|$
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\%Range}
{Int} {Int} {Int}} $|$
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\%Pauli}
$Int$}}\\\ \text{Blocks\ \ \quad\quad b ::=
$l\overline{\phi}\overline{c}tmn$}\\\ \text{Tmns \quad\ \ \ $tmn$ ::= {ret}
$typ$ $val$ $|$ {ret void} $|$ {br} $val$ $l_{1}$ $l_{2}$ $|$ {br} $l$ }\\\
\text{Commands \ \ {c} ::= {id} = {bitcast} $typ_{1}val$ {to} $typ_{2}$ $|$
{store} {typ} $val_{1}$ $val_{2}$ {align} $|$ {option id} = {call} $typ_{0}$
$val_{0}$ $\overline{param}$ }\\\ \text{\quad\quad\quad\quad\quad\quad\ \ $|$
\ {id} = {getelementptr} ($typ*$) $val$ $\overline{val_{j}}^{j}$ $|$ {id} =
{load} ($typ*$) $val_{1}$ $align$}\\\ \text{\quad\quad\quad\quad\quad\quad\ \
$|$ \ $id$ = {icmp} $cond$ $typ$ $val_{1}$ $val_{2}$ $|$ $id$ = {alloca} $typ$
$val$ $align$}\\\ \end{array}$

Figure 3: The abstract syntax of QIR. The red font shows what is added to the
abstract semantics of QIR compared to LLVM IR.

###  3.2 Semantics of QIR

We next present our formalization of the semantics of QIR. Since QIR is
designed to treat instructions as declarations of quantum runtime functions,
the type is explicitly specified for each instruction input and output. Such a
design avoids the nondeterministic semantics found in classical LLVM IR, thus
liberating our efforts from cumbersome type checking and allowing us to focus
the formalization on checking the correctness of quantum operations. Since the
back-end hardware is responsible for implementing quantum operations in QIR,
formalizing this process in QIR is not necessary. The guarantee of correct
quantum operations should lie with the back-end hardware. Therefore, we can
assume that the quantum operations are correct and further improve the
security of the QIR code.

####  3.2.1 Allocating and Releasing Qubits

QIR manipulates the corresponding qubits in the back-end registers by feeding
$\textbf{\%Qubit}^{*}$ or $\textbf{\%Array}^{*}$ composed of them to the
corresponding functions, without having direct access to %Qubit or %Array
information (since they are opaque to QIR as well as LLVM). It makes it
difficult for QIR to manage the state of qubits, and the compiler cannot know
whether they have been released, thus raising a potential security risk. In
this section, we formalize the semantics from the creation of a single qubit
as well as an array of qubits and propose a set of management schemes for
qubits and qubit arrays so that the possible problems of qubits cloning and
the use of released qubits in QIR can be effectively captured.

##### Static creation.

In QIR, the allocation of qubits includes both static and dynamic methods. For
qubits whose identifiers are already determinable at compile time, static
qubit values can be generated using LLVM’s inttoptr instruction. The following
example is given in the specification document of QIR:

%qubit3 = inttoptr i32 3 to $\textbf{\%Qubit}^{*}$

This code refers to a qubit3 device in the real equipment (or simulator) by
converting the 3 of the i32 data type to the $\textbf{\%Qubit}^{*}$ type.
Since the instructions for static creation of qubits use only the classical
LLVM IR, the formal semantics are not elaborated in our work.

Figure 4: A management model for qubits and qubits arrays in QIR.

##### Dynamic management.

Dynamic qubits are allocated and released by the quantum runtime method. To
store the allocated qubits and qubit arrays in the QIR code, we introduce two
data structures in the framework, a one-dimensional array Q and a two-
dimensional array QA, respectively. Our management model is presented in
Figure 4, where Q stores the $\textbf{\%Qubit}^{*}$ pointers for each
allocated qubit. The first column of QA stores the $\textbf{\%Array}^{*}$
pointer for the qubit array, while the corresponding row stores the pointer
$\textbf{\%Qubit}^{*}$ for each qubit in the array. Some of the methods used
to manage these two data structures are listed in Table 1.

Table 1: Some of the methods used to manage qubits and qubit arrays in our validation framework Method |  Description
---|---
appqlist(Q, $q$) | Append $q$ to Q.
appqarrlist(QA, $qarray$) | Append $qarray$ to QA.
checkq(Q, $q$) | Check if $q$ is in Q. If true, return 1; otherwise, return 0.
checkqarrlist(QA, $qarray$) | Check if $qarray$ is in QA. If true, return 1; otherwise, return 0.
delq(Q, $q$) | Remove $q$ from Q.
delqarr(QA, $qarray$) | Remove the row of $qarray$ from QA.
appqarr(QA, $qarray$, $q$) | Append $q$ to $qarray$ in QA. Skip if $q$ already exists in $qarray$.
checkqarr(QA, $qarray$, $q$) | Check if $q$ is in $qarray$. If true, return 1; otherwise, return 0.
findqarr(QA, $q$) | Returns the array where $q$ is located, or 0 if the array does not exist.

Our formal method is concerned with two possible safety issues in QIR code:
the cloning operation of qubits and the usage of released qubits. These two
kinds of unsafe codes can be effectively captured using our proposed
management model. Equations 6 to 9 show the operational semantics of
allocation and release of qubits and qubit arrays, respectively, where
$qubit\\_allocate$, $qubit\\_allocate\\_array$, $qubit\\_release$, and
$qubit\\_release\\_array$ are the instructions provided in QIR. Specifically,
after performing the allocation of qubits and qubit arrays, their return
values ($\textbf{\%Qubit}^{*}$ and $\textbf{\%Array}^{*}$) are stored in Q and
QA (See Figure 4). After releasing the qubit and qubit arrays, the
corresponding values are removed from Q and QA. To avoid using released qubits
and qubit arrays, we add the process of checking whether the qubits and qubit
arrays are in Q and QA (use checkq and checkqarrlist) in all the rules in
addition to Q_ALLOC and QARR_ALLOC.

In particular, when releasing a single qubit (rule Q_DEALLOC), we have added
the process of checking whether the qubit belongs to a qubit array (with
findqarr) because releasing a single qubit in a qubit array directly can lead
to errors when releasing the qubit array later.

$\displaystyle\frac{\begin{aligned} q=qubit\\_allocate()\
\textbf{appqlist}(\textbf{{Q}},q)=\textbf{{Q}}^{\prime}\end{aligned}}{\textbf{{Q}}\vdash\textbf{{Q}},id=\textbf{call
\%Qubit}^{*}qubit\\_allocate()\Rightarrow\textbf{{Q}}^{\prime},id\leftarrow
q}\ \text{Q\\_ALLOC}$ (6)

$\displaystyle\frac{\begin{aligned} qarray=qubit\\_allocate\\_array(n)\
\textbf{appqarrlist}(\textbf{{QA}},qarray)=\textbf{{QA}}^{\prime}\end{aligned}}{\textbf{{QA}},n\vdash\textbf{{QA}},id=\textbf{call
\%Array}^{*}qubit\\_allocate\\_array(n)\Rightarrow\textbf{{QA}}^{\prime},n,id\leftarrow
qarray}\ \text{QARR\\_ALLOC}$ (7)

$\displaystyle\frac{\begin{aligned} &\text{if not}\
qarray=\textbf{findqarr}(\textbf{{QA}},q)\ \text{and}\
\textbf{checkq}(\textbf{{Q}},q)\ \text{then}\ qubit\\_release(q)\
\textbf{delq}(\textbf{{Q}},q)=\textbf{{Q}}^{\prime}\ \text{else}\
abort\end{aligned}}{\textbf{{Q}},\textbf{{QA}},q\vdash\textbf{{Q}},\textbf{{QA}},\textbf{call
void}\ qubit\\_release(q)\Rightarrow\textbf{{Q}}^{\prime},\textbf{{QA}},q}\
\text{Q\\_DEALLOC}$ (8)

$\displaystyle\frac{\begin{aligned} &\text{if}\
\textbf{checkqarrlist}(\textbf{{QA}},qarray)\ \text{then}\
qubit\\_release\\_array(qarray)\
\textbf{delqarr}(\textbf{{QA}},qarray)=\textbf{{QA}}^{\prime}\ \text{else}\
abort\end{aligned}}{\textbf{{QA}},qarray\vdash\textbf{{QA}},\textbf{call
void}\
qubit\\_release\\_array(qarray)\Rightarrow\textbf{{QA}}^{\prime},qarray}\
\text{QARR\\_DEALLOC}$ (9)

####  3.2.2 Manipulating Qubits in Qubit Arrays and Forming Qubit Arrays with
Allocated Qubits

In addition to directly allocating qubits and qubit arrays with the methods of
QIR, it is possible to load a single qubit from a qubit array or combine
multiple allocated qubits into a new qubit array. We summarize these two
operations in the functions $load\\_qubit$ and $create\\_qubit\\_array$,
respectively:

$\small\begin{aligned} (id=load\\_qubit(qarray,n))=\\{&id_{1}=\textbf{call
i}sz^{*}\ array\\_get\\_element\\_ptr\\_1d(qarray,n);\\\
&id_{2}=\textbf{bitcast i}sz^{*}\ id_{1}\ \textbf{to}\
\textbf{\%Qubit}^{**};\\\ &id=(id_{3}=\textbf{load
\%Qubit}^{*},\textbf{\%Qubit}^{**}\ id_{2},align)\\}\end{aligned}$

$\small\begin{aligned}
(id=&create\\_qubit\\_array(q_{1},q_{2},...,q_{n}))=\\{\\\
&id=(id_{1}=\textbf{call \%Array}^{*}array\\_create\\_1d(sz,n));\\\
&\overline{id_{2i}=(\textbf{call i}sz^{*}\
array\\_get\\_element\\_ptr\\_1d(qarray,i));id_{3i}=\textbf{bitcast i}sz^{*}\
id_{2i}\ \textbf{to}\ \textbf{\%Qubit}^{**};}^{i=1...n}\\\
&\overline{\textbf{store \%Qubit}^{*}\ q_{i},\textbf{\%Qubit}^{**}\
id_{3i},align;}^{i=1...n}\\}\end{aligned}$

In the above two functions, $array\\_create\\_1d$ and
$array\\_get\\_element\\_ptr\\_1d$ are instructions in QIR.
$array\\_create\\_1d$ returns an array pointer $\textbf{\%Array}^{*}$ of size
$sz$ with length $n$ by inputting byte size $sz$ of array elements and array
length $n$. $array\\_get\\_element\\_ptr\\_1d$ can obtain the
$\textbf{i}sz^{*}$ pointer of the corresponding element by inputting the array
$qarray$ and indices $n$ of the qubit array. Then through the bitcast
instruction of LLVM, it can be converted into a $\textbf{\%Qubit}^{**}$
pointer and the qubit pointer $\textbf{\%Qubit}^{*}$ can be loaded or stored
with load or store instruction.

##### Manipulating qubits in qubit arrays.

The rule Q_LOAD defines the semantics of loading a qubit from the qubit array.
Specifically, besides the necessity to check whether the qubit array has been
released before executing the loaded operation, it is also needed to record
the qubit in the corresponding qubit array of the list QA at the end of the
execution (see Figure 4).

$\displaystyle\frac{\begin{aligned} &\text{if}\
\textbf{checkqarrlist}(\textbf{{QA}},qarray)\ \text{then}\
ptr=(id_{1}=\textbf{call
i}sz^{*}array\\_get\\_element\\_ptr\\_1d(qarray,n))\\\
&qptr=(id_{2}=\textbf{bitcast i}sz^{*}\ ptr\ \textbf{to}\
\textbf{\%Qubit}^{**})\ q=(id_{3}=\textbf{load}\
\textbf{\%Qubit}^{*},\textbf{\%Qubit}^{**}\ qptr,align)\\\
&\textbf{appqarr}(\textbf{{QA}},qarray,q)=\textbf{{QA}}^{\prime}\ \text{else}\
abort\end{aligned}}{\textbf{{QA}},qarray,n\vdash\textbf{{QA}},id=load\\_qubit(qarray,n)\Rightarrow\textbf{{QA}}^{\prime},qarray,n,id\leftarrow
q}\ \text{Q\\_LOAD}$ (10)

##### Forming qubit arrays with allocated qubits.

The rule QARR_CREATE summarizes the semantics of the function that forms an
array qubit from allocated qubits. We add the process of checking whether the
qubit to be stored already exists in the array (checkqarr) before the store
instruction and abort if the qubit already exists in the array. It is because
there should not be two identical qubits in the same qubit array, otherwise,
there will be a risk of qubits cloning. If this qubit array is used as control
qubits, two identical qubits will act as control qubits simultaneously. While
it doesn’t impact the operation’s outcome, it violates the non-cloning
principle of quantum computing. Its management for Q and QA is shown in Figure
4. Specifically, rule QARR_CREATE adds the new array pointer to the QA and
adds the qubits that make up the array to the corresponding row.

$\displaystyle\frac{\begin{aligned} &\text{if}\
\overline{\textbf{checkq}(\textbf{{Q}},q_{i})\ \text{or}\
qarray_{temp}=\textbf{findqarr}(\textbf{{QA}},q_{i})}^{i=1...n}\
\text{then}\\\ \ &qarray=(id_{1}=\textbf{call
\%Array}^{*}array\\_create\\_1d(sz,n))\
\textbf{appqarrlist}(\textbf{{QA}},qarray)\ \\\
&\overline{ptr_{i}=(id_{2i}=(\textbf{call i}sz^{*}\
array\\_get\\_element\\_ptr\\_1d(qarray,i)))\
qptr_{i}=(id_{3i}=\textbf{bitcast i}sz^{*}\ ptr_{i}\ \textbf{to}\
\textbf{\%Qubit}^{**})}^{i=1...n}\\\ &\overline{\text{if not}\
\textbf{checkqarr}(\textbf{{QA}},qarray,q_{i})\ \text{then}\ \textbf{store
\%Qubit}^{*}\ q_{i},\textbf{\%Qubit}^{**}\ qptr_{i},align\ \text{else}\
abort}^{i=1...n}\\\
&\overline{\textbf{appqarr}(\textbf{{QA}},qarray,q_{i})}^{1=1...n}=\textbf{{QA}}^{\prime}\
\text{else}\
abort\end{aligned}}{\textbf{{Q}},\textbf{{QA}},(q_{1},q_{2},...,q_{n})\vdash\textbf{{Q}},\textbf{{QA}},id=create\\_qubit\\_array(q_{1},q_{2},...,q_{n})\Rightarrow\textbf{{Q}},\textbf{{QA}}^{\prime},(q_{1},q_{2},...,q_{n}),id\leftarrow
qarray}\ \text{QARR\\_CREATE}$ (11)

####  3.2.3 Gate Operations

In QIR, gate operations can be divided into two main categories: single-qubit
gate operations and controlled gate operations formed by adding control qubits
to single-qubit gate operations. We will formalize the semantics of these two
types of gate operations separately. In QIR, the gate operations of qubits do
not change in our management model for Q and QA since they do not involve
loading and storing of data as well as allocation and release of qubits. The
rules SG_OP and CG_OP show our formalization of the semantics of single-qubit
gates as well as controlled gates, respectively, where $gateop\\_\\_body$ and
$gateop\\_\\_ctl$ are instructions for gate operations in QIR, and $gateop$ is
a single-qubit gate such as $x$,$Rx$,$h$.

$\displaystyle\frac{\begin{aligned} &\text{if}\
\textbf{checkq}(\textbf{{Q}},q)\ \text{or}\
qarray_{temp}=\textbf{findqarr}(\textbf{{QA}},q)\ \text{then}\
gateop\\_\\_body(option\ d,q)\ \text{else}\
abort\end{aligned}}{\textbf{{Q}},\textbf{{QA}},option\
d,q\vdash\textbf{{Q}},\textbf{{QA}},\textbf{call void}\
gateop\\_\\_body(option\ d,q)\ \Rightarrow\textbf{{Q}},\textbf{{QA}},option\
d,q}\ \text{SG\\_OP}$ (12)

$\displaystyle\frac{\begin{aligned} &\text{if}\
(\textbf{checkq}(\textbf{{Q}},q)\ \ \text{or}\
qarray_{temp}=\textbf{findqarr}(\textbf{{QA}},q))\ \text{and}\
\textbf{checkqarr}(\textbf{{QA}},qarray)\ \\\ &\text{and not}\
\textbf{checkqarr}(\textbf{{QA}},qarray,q)\ \text{then}\
gateop\\_\\_ctl(qarray,(option\ d,q))\ \text{else}\
abort\end{aligned}}{\textbf{{Q}},\textbf{{QA}},option\
d,q\vdash\textbf{{Q}},\textbf{{QA}},\textbf{call void}\
gateop\\_\\_ctl(qarray,(option\
d,q))\Rightarrow\textbf{{Q}},\textbf{{QA}},option\ d,q}\ \text{CG\\_OP}$ (13)

In QIR, the control qubits are entered into the instruction in the form of a
qubit array. So similar to the rule QARR_CREATE, for CG_OP, we also add a
check for whether the target qubit exists in the control qubit array (with
checkqarr) to avoid the problem of qubit cloning.

####  3.2.4 Measurement

For the measurement operation, the measurement result can be returned in QIR
by entering an array of Pauli values and an array of qubits. The semantics of
the measurement operation is:

$\displaystyle\frac{\begin{aligned} \text{if}\
\textbf{checkqarr}(\textbf{{QA}},qarray)\ \text{then}\
result=measure\\_\\_body(Pauliarr,qarray)\ \text{else}\
abort\end{aligned}}{\textbf{{QA}},Pauliarr,qarray\vdash id=\textbf{call
\%Result}^{*}\
measure\\_\\_body(Pauliarr,qarray)\Rightarrow\textbf{{QA}},Pauliarr,qarray,id\leftarrow
result}\ \text{MEASURE}$ (14)

##  4 Verification on Unsafe Code of QIR

This section applies our method to verify some insecure QIR codes. Since QIR
is still not officially in use, the most prominent way to generate QIR code at
present is to use the Q# compiler provided by Microsoft. This provides us with
the inspiration to collect verification samples. If an unsafe Q# program
passes the compiler but fails at runtime, we can generate the corresponding
QIR code from it for verification. Figure 5 shows two samples of unsafe Q#
code referenced from [24], where in Figure 5a the qubit returned is released
at the end of the execution of the function NewQubit, and in Figure 5b the
three qubits called by CCNOT are the same qubit, violating the no-cloning
theorem. In the next subsections, we will present the corresponding QIR code
and apply the semantics we designed to check for faults.

$\footnotesize{\begin{array}[]{l}\texttt{\@EntryPoint()}\\\ \texttt{operation
Deadqubit() : Result \\{}\\\ \quad\quad\texttt{let q = NewQubit();}\\\
\quad\quad\texttt{H(q);}\\\ \quad\quad\texttt{return M(q);}\\\ \texttt{\\}}\\\
\\\ \texttt{operation NewQubit() : Qubit \\{}\\\ \quad\quad\texttt{use q =
Qubit();}\\\ \quad\quad\texttt{return q;}\\\ \texttt{\\} }\end{array}}$

((a)) Return a released qubit.

$\footnotesize{\begin{array}[]{l}${\@EntryPoint()}$\\\ ${operation Cloning() :
Result \\{}$\\\ $\quad\quad{use q1 = Qubit();}$\\\ $\quad\quad{let q2 =
q1;}$\\\ $\quad\quad{let q3 = q2;}$\\\ $\quad\quad{CCNOT(q1, q2, q3);}$\\\
$\quad\quad{return M(q3);}$\\\ ${\\} }$\end{array}}$

((b)) Control qubit and target qubit are the same one.

Figure 5: Example of unsafe Q# codes.

###  4.1 Using Deallocated Qubits

Figure 7 shows the QIR code obtained from the Q# code conversion from Figure
5a. In this example, for the return value of the function
$@NewQubit\\_\\_body$ in line 3, we can analyze it using the rules Q_ALLOC and
Q_DEALLOC, so that we can know that the $\%q$ returned has been released (see
Figure 6a). In the execution of $h\\_\\_body$ in line 4, the rule SG_OP is
applied to interrupt the program since $\%q$ does not exist in Q, thus
avoiding the error of using the released qubit.

Figure 6: Example of applying the formal method to verify unsafe QIR code.

          1   define internal %Result* @Deadqubit__body() {
          2   entry:
          3     %q = call %Qubit* @NewQubit__body()
          4     call void @__quantum__qis__h__body(%Qubit* %q)
          5     %0 = call %Result* @Microsoft__Quantum__Intrinsic__M__body(%Qubit* %q)
          6     ret %Result* %0
          7   }
          8
          9   define internal %Qubit* @NewQubit__body() {
          10   entry:
          11    %q = call %Qubit* @__quantum__rt__qubit_allocate()
          12    call void @__quantum__rt__qubit_release(%Qubit* %q)
          13    ret %Qubit* %q
          14  }
              ...

Figure 7: QIR code converted from Figure 5a. To save space, we have only
intercepted the minimum critical code.

###  4.2 Qubit Cloning

Figure 8 shows the QIR code obtained from the code conversion of the cloned
quantum in Figure 5b. In the example, for the function, $CCNOT\\_\\_body$ in
line 4, two identical $\textbf{Qubit}^{*}$ $\%q1$ are entered as control
qubits, and $\%q1$ itself as the target qubit. Thus for lines 12 to 18 of the
code, the rule QARR_CREATE can be applied, thus interrupting the program in
line 18 due to the transfer to the array $\%\\_\\_controlQubits\\_\\_$ stores
the same $\textbf{Qubit}^{*}$ $\%q1$ and avoiding the qubit cloning problem
(see Figure 6b). Other than that, for line 20 of the code, the rule CG_OP can
be applied, and since $\%q1$, which is the target qubit, is the same as the
element in the control qubit array, qubit cloning can be avoided in this step
as well.

    1   define internal %Result* @Cloning__body() {
    2   entry:
    3     %q1 = call %Qubit* @__quantum__rt__qubit_allocate()
    4     call void @Microsoft__Quantum__Intrinsic__CCNOT__body(%Qubit* %q1, %Qubit* %q1,
                                                                %Qubit* %q1)
        ...
    8   }
    9
    10  define internal void @Microsoft__Quantum__Intrinsic__CCNOT__body(%Qubit* %control1,
                                                    %Qubit* %control2, %Qubit* %target) {
    11  entry:
    12    %__controlQubits__ = call %Array* @__quantum__rt__array_create_1d(i32 8, i64 2)
    13    %0 = call i8* @__quantum__rt__array_get_element_ptr_1d(%Array* %__controlQubits__, i64 0)
    14    %1 = bitcast i8* %0 to %Qubit**
    15    %2 = call i8* @__quantum__rt__array_get_element_ptr_1d(%Array* %__controlQubits__, i64 1)
    16    %3 = bitcast i8* %2 to %Qubit**
    17    store %Qubit* %control1, %Qubit** %1, align 8
    18    store %Qubit* %control2, %Qubit** %3, align 8
    19    call void @__quantum__rt__array_update_alias_count(%Array* %__controlQubits__, i32 1)
    20    call void @__quantum__qis__x__ctl(%Array* %__controlQubits__, %Qubit* %target)
        ...
    24  }

Figure 8: QIR code converted from Figure 5a. To save space, we have only
intercepted the minimum critical code.

##  5 Related Work

This section discusses some related work in the areas of intermediate
representations for both classical and quantum programming languages.

###  5.1 LLVM IR Semantics

As the basis of QIR, the formal approach of LLVM IR is an important reference
for our work. Zhao et al. [30] propose the Vellvm (verified LLVM) framework,
which provides a formalization of the static semantics, memory model, and
several operational semantics of LLVM IR. The framework is implemented using
Coq, through which verified executable code with high confidence can be
extracted directly, and the effectiveness of Vellvm was verified with the
SoftBound [18] case. Li and Gunter [13] design K-LLVM, the complete formal
LLVM IR semantics, including all LLVM IR instructions, intrinsic functions in
the LLVM documentation, etc. Compared to Vellvm, which focuses on formalizing
LLVM semantics as a mathematical object, K-LLVM shows possible implementations
of the semantics in a virtual computer with a more direct approach. K-LLVM is
implemented by $\mathbb{K}$ [17], and its validity is verified by testing
against unit test programs as well as actual LLVM IR programs. However, the
above work is directed toward formalizing LLVM IR and does not address quantum
programming languages or intermediate representations.

###  5.2 Formalized Quantum Intermediate Representation and Programming
Language

As the most relevant work to us, Hietala et al. [10] present VOQC, a verified
optimizer for quantum circuits. As the input to VOQC, a small quantum
intermediate representation (SQIR) was developed to represent quantum circuits
and support the verification of quantum circuit optimization. SQIR is well
formalized, and its syntax and semantics for quantum circuits can guarantee
the correctness of VOQC optimization. Our work differs from SQIR in two main
ways: first, the formal object, which is QIR developed by Microsoft, and its
application scenario is to provide a general solution for quantum programming
languages and back-end hardware. SQIR, on the other hand, is an independently
developed quantum intermediate representation, which is mainly applied to the
verification process of VOQC. The second is the difference in purpose. In our
work, the main goal of the formalization of QIR is to provide guarantees for
the correctness of quantum programs and the behavior of QIR, while SQIR
focuses on the assurance of correctness for quantum circuit optimization.

In terms of formalizations of quantum programming languages, Singhal et al.
[24] present $\lambda_{Q\\#}$, an idealized version of Q#. Based on Staton’s
work [25], they provide a syntactic and semantic formalization of
$\lambda_{Q\\#}$ that enables it to ensure quantum no-cloning theorem and to
provide stacked-like management of qubits. By converting from Q# to
$\lambda_{Q\\#}$, additional safety guarantees can be provided for Q# code.
For the Quipper [9] programming language, Mahmoud and Felty [14] present
Proto-Quipper, which contains the core functionality of Quipper and extends
Quipper’s system based on the linear specification logic (SL). They also
implemented a formalization of Proto-Quipper via Hybird [7], encoded the
complete Proto-Quipper specification, and proved the correctness of its type
system. While these works can serve as valuable references for our research,
it is critical to recognize significant differences between our work and
theirs; our research centers on quantum intermediate representations rather
than quantum programming languages.

##  6 Concluding Remarks

In this paper, we have formalized the core functionality of QIR, particularly
its abstract syntax and the semantics of its several runtime functions. Our
formalization ensures that QIR programs follow the quantum non-cloning theorem
and avoid calls to released qubits and arrays. Based on the analysis of real
QIR code, we also demonstrated the effectiveness of our formalization in
capturing unsafe code in programs.

Our current work is only an initial attempt to formalize the specification of
QIR, and more work is needed to refine it. The QIR functions that have been
formalized so far are only a small part. More functions need to be formalized,
such as $Tuple$ and $String$ in the data type, the semantics of the complete
measurement process, and performing batched gate operations on qubits array.
From a practical perspective, to apply our formal method directly to the QIR
programs for automatic verification (rather than through human analysis as in
this work), we need to implement our formal approach with formal interactive
theorem checkers such as Coq [5] in further work.

## References

  * [1]
  * [2] Gadi Aleksandrowicz, Thomas Alexander, Panagiotis Barkoutsos, Luciano Bello, Yael Ben-Haim, David Bucher, F Jose Cabrera-Hernández, Jorge Carballo-Franquis, Adrian Chen, Chun-Fu Chen et al. (2019): _Qiskit: An open-source framework for quantum computing_.  Accessed on: Mar 16\.
  * [3] QIR Alliance (2022): _QIR Alliance_.  Available at https://www.qir-alliance.org/.
  * [4] Benjamin Bichsel, Maximilian Baader, Timon Gehr & Martin Vechev: _Silq: a high-Level quantum language with safe uncomputation and intuitive semantics_.  In: Proceedings of the 41th ACM SIGPLAN Conference on Programming Language Design and Implementation.
  * [5] The Coq Development Team (2017): _The Coq Proof Assistant Reference Manual, version 8.7_.  Available at http://coq.inria.fr.
  * [6] Andrew W. Cross, Lev S. Bishop, John A. Smolin & Jay M. Gambetta (2017): _Open Quantum Assembly Language_ , 10.48550/ARXIV.1707.03429.  Available at https://arxiv.org/abs/1707.03429.
  * [7] Amy P. Felty & Alberto Momigliano (2008): _Hybrid: A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax_.  CoRR abs/0811.4367.  arXiv:0811.4367.
  * [8] Alan Geller (2020): _Introducing Quantum Intermediate Representation (QIR)_.  Available at https://devblogs.microsoft.com/qsharp/introducing-quantum-intermediate-representation-qir/.
  * [9] Alexander S Green, Peter LeFanu Lumsdaine, Neil J Ross, Peter Selinger & Benoît Valiron (2013): _Quipper: a scalable quantum programming language_.  In: Proceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation, pp. 333–342.
  * [10] Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu & Michael Hicks (2021): _A Verified Optimizer for Quantum Circuits_.  Proc. ACM Program. Lang. 5(POPL), 10.1145/3434318.  Available at https://doi.org/10.1145/3434318.
  * [11] Chris Lattner & Vikram Adve (2004): _LLVM: A Compilation Framework for Lifelong Program Analysis and Transformation_.  San Jose, CA, USA, pp. 75–88.
  * [12] Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques Pienaar, River Riddle, Tatiana Shpeisman, Nicolas Vasilache & Oleksandr Zinenko (2021): _MLIR: Scaling Compiler Infrastructure for Domain Specific Computation_.  In: 2021 IEEE/ACM International Symposium on Code Generation and Optimization (CGO), pp. 2–14, 10.1109/CGO51591.2021.9370308.
  * [13] Liyi Li & Elsa L. Gunter (2020): _K-LLVM: A Relatively Complete Semantics of LLVM IR_.  In Robert Hirschfeld & Tobias Pape, editors: 34th European Conference on Object-Oriented Programming (ECOOP 2020), Leibniz International Proceedings in Informatics (LIPIcs) 166, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp. 7:1–7:29, 10.4230/LIPIcs.ECOOP.2020.7.  Available at https://drops.dagstuhl.de/opus/volltexte/2020/13164.
  * [14] Mohamed Yousri Mahmoud & Amy P. Felty (2018): _Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic_.  CoRR abs/1812.03624.  arXiv:1812.03624.
  * [15] Alexander McCaskey & Thien Nguyen (2021): _A MLIR Dialect for Quantum Assembly Languages_ , 10.48550/ARXIV.2101.11365.  Available at https://arxiv.org/abs/2101.11365.
  * [16] Microsoft (2022): _Quantum Intermediate Representation (QIR)_.  Available at https://github.com/qir-alliance/qir-spec/tree/main/specification.
  * [17] D. Monderer & M. Tennenholtz (2004): _K-Implementation_.  Journal of Artificial Intelligence Research 21, pp. 37–62, 10.1613/jair.1231.  Available at https://doi.org/10.1613%2Fjair.1231.
  * [18] Santosh Nagarakatte, Jianzhou Zhao, Milo M.K. Martin & Steve Zdancewic (2009): _SoftBound: Highly Compatible and Complete Spatial Memory Safety for c_.  In: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’09, Association for Computing Machinery, New York, NY, USA, p. 245–258, 10.1145/1542476.1542504.  Available at https://doi.org/10.1145/1542476.1542504.
  * [19] Santosh Nagarakatte, Jianzhou Zhao, Milo M.K. Martin & Steve Zdancewic (2009): _SoftBound: Highly Compatible and Complete Spatial Memory Safety for c_.  SIGPLAN Not. 44(6), p. 245–258, 10.1145/1543135.1542504.  Available at https://doi.org/10.1145/1543135.1542504.
  * [20] Thien Nguyen, Anthony Santana, Tyler Kharazi, Daniel Claudino, Hal Finkel & Alexander McCaskey (2020): _Extending C++ for Heterogeneous Quantum-Classical Computing_.  arXiv e-prints:arXiv:2010.03935.  arXiv:2010.03935.
  * [21] Michael A Nielsen & Isaac Chuang (2002): _Quantum computation and quantum information_.
  * [22] John Preskill (2018): _Quantum computing in the NISQ era and beyond_.  Quantum 2, p. 79.
  * [23] IBM Research: _Qiskit_.  Accessed on: June, 2021.  Available at https://qiskit.org.
  * [24] Kartik Singhal, Kesha Hietala, Sarah Marshall & Robert Rand (2022): _Q# as a Quantum Algorithmic Language_ , 10.48550/ARXIV.2206.03532.  Available at https://arxiv.org/abs/2206.03532.
  * [25] Sam Staton (2015): _Algebraic Effects, Linearity, and Quantum Programming Languages_.  SIGPLAN Not. 50(1), p. 395–406, 10.1145/2775051.2676999.  Available at https://doi.org/10.1145/2775051.2676999.
  * [26] Sam Staton (2015): _Algebraic Effects, Linearity, and Quantum Programming Languages_.  In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’15, Association for Computing Machinery, New York, NY, USA, p. 395–406, 10.1145/2676726.2676999.  Available at https://doi.org/10.1145/2676726.2676999.
  * [27] Krysta Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade, Bettina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz & Martin Roetteler (2018): _Q#: enabling scalable quantum computing and development with a high-level DSL_.  In: Proceedings of the Real World Domain Specific Languages Workshop 2018, pp. 1–10.
  * [28] Google AI Quantum team (2018): _Cirq_.  Available at https://github.com/quantumlib/Cirq.
  * [29] ProjectQ Team (2017): _ProjectQ_.  Accessed on: April, 2020.  Available at https://projectq.ch/.
  * [30] Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin & Steve Zdancewic (2012): _Formalizing the LLVM Intermediate Representation for Verified Program Transformations_.  In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’12, Association for Computing Machinery, New York, NY, USA, p. 427–440, 10.1145/2103656.2103709.  Available at https://doi.org/10.1145/2103656.2103709.


# jaCappella Corpus: A Japanese a Cappella Vocal Ensemble Corpus

###### Abstract

We construct a corpus of Japanese _a cappella_ vocal ensembles (_jaCappella
corpus_) for vocal ensemble separation and synthesis. It consists of 35
copyright-cleared vocal ensemble songs and their audio recordings of
individual voice parts. These songs were arranged from out-of-copyright
Japanese children’s songs and have six voice parts (lead vocal, soprano, alto,
tenor, bass, and vocal percussion). They are divided into seven subsets, each
of which features typical characteristics of a music genre such as jazz and
enka. The variety in genre and voice part match vocal ensembles recently
widespread in social media services such as YouTube, although the main targets
of conventional vocal ensemble datasets are choral singing made up of soprano,
alto, tenor, and bass. Experimental evaluation demonstrates that our corpus is
a challenging resource for vocal ensemble separation. Our corpus is available
on our project page.

Index Terms—  Corpus, vocal ensemble, singing voice, audio source separation,
singing voice synthesis

##  1 Introduction

Vocal ensemble is a widespread group singing form across cultures and
languages and has been gathering attention in the field of music information
retrieval (MIR) [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]. Owing to successes of deep
learning in the this field [11, 12], recent studies on vocal ensemble have
adopted a data-driven approach: for example, multipitch estimation [3, 4],
vocal ensemble separation [6, 7, 5], automatic transcription [8], synthesis of
unison voices [9], and double-tracking [10]. For the development of such
methods, the availability of suitable vocal ensemble datasets is essential.

There are a few publicly available datasets on vocal ensembles [1, 5, 3, 2].
Table 1 shows the specifications of the vocal ensemble datasets. Most of them
focus on choral singing, particularly four-part singing of soprano (S), alto
(A), tenor (T), and bass (Bs). This SATB format is widespread in Western music
and audio recordings of traditional choral music have been dealt with. Some of
the datasets [3, 2] include recordings of vocal ensembles with multiple
singers per voice part to analyze interactions between singers, while most
vocal ensemble studies focus on vocal ensembles with one singer per voice part
[8, 4, 3, 6, 7, 5]. The datasets of [3, 2] include audio recordings of singing
voices during exercises and a few songs were often used. In [5], more than 40
songs were used to develop a vocal ensemble separation method. This should be
because the use of same songs for training and test leads to data leakage.

Unlike choral singing, recent vocal ensemble songs include more various voice
parts such as lead vocal (Vo) and vocal percussion (VP). VP is the imitation
of percussion sounds by mouth and can accounts for rhythm. Thus, it fits the
vocal ensemble arrangement of various music genre songs such as jazz and
reggae. Such vocal ensemble songs have been actively shared in social media
services (e.g., YouTube and TikTok), forming a new vocal ensemble style.
Despite their importance, there do not exist datasets that feature this style
and can be easily used for research, to the best of our knowledge. Since the
availability of data is crucial for developing MIR methods on vocal ensembles,
the lack of suitable datasets requires a costly and painstaking process of
data collection.

In this paper, we construct a corpus of Japanese a cappella vocal ensembles,
named _jaCappella corpus_ , by arranging out-of-copyright Japanese children’s
songs. It includes 35 vocal ensemble songs composed of seven subsets (five
songs per subset). The songs in each subset were arranged with a different
music genre, which ensures the variety in music genre and singing styles. All
songs have six voice parts: Vo, S, A, T, Bs, and VP. This format is popular in
Japanese vocal ensemble arrangement, which we examined by collecting
commercial vocal ensemble songs. To avoid copyright-related restriction, we
obtained all necessary copyrights and neighboring rights of our songs.
Reserving these rights allows users of the jaCappella corpus to share
processed audio signals to the extent necessary for research and it can also
open the way for commercial use. This is one of the advantages of manually
creating music data because ensuring such a broad use is usually difficult to
achieve with a method that artificially mixes singing voices from existing
datasets [4]. To further enhance the usability of this corpus, we provide the
musical scores of the songs in the MusicXML format [13].

Our corpus includes audio signals of individual voice parts sung by 20 semi-
professional singers. A vocal ensemble was assembled per subset and each voice
part was sung by one singer. The recordings were performed per singer. We can
use the recorded signals for various tasks on vocal ensembles. For example, we
can use the jaCappella corpus for vocal ensemble separation, which we will
demonstrate in Section 3. In this paper, we focus on monaural mixtures but our
corpus can be used for multichannel situations such as bleeding sound
reduction (e.g., [14]). Another task of our interest is singing voice
synthesis for vocal ensemble, which we refer to as vocal ensemble synthesis.
This research direction aims to clarify how to artificially reproduce vocal
ensemble performed by humans. Since our corpus covers various music genres, it
would be useful to synthesize ensemble singing voices with singing styles
other than choral singing. The corpus is available at
https://tomohikonakamura.github.io/jaCappella_corpus/.

Table 1: Specifications of our jaCappella corpus and conventional vocal ensemble datasets Corpus/Dataset | Voice parts | Duration [min] | # songs | Genre | Publicly avail.
---|---|---|---|---|---
Choral Singing [1] | S, A, T, Bs | 7 | 3 | Choral music | Yes
Dagstuhl ChiorSet [2] | S, A, T, Bs | 55 | 2 | Choral music | Yes
ESMUC Choir [3] | S, A, T, Bs | 31 | 3 | Choral music | Yes
Bach Chorales and | S, A, T, Bs | 104 | 48 | Choral and barbershop music | No
Barbershop Quartets [5]
jaCappella (ours) | Vo, S, A, T, Bs, VP | 34 | 35 | Jazz, punk rock, bossa nova, popular, | Yes
reggae, enka, neutral (children’s song)

##  2 Our jaCappella Corpus

We constructed the jaCappella corpus in three steps: corpus design,
arrangement into vocal ensemble songs, and recording of singing voices. In the
following, we describe the details of the three steps and analyze the
distributions of lyrics, comparing the created songs with commercial vocal
ensemble songs.

###  2.1 Corpus design

Table 2: Gender frequency of commercial music collection Gender | Voice part [%]
---|---
Vo | S | A | T | Bs | VP
Male | 81.0 | 0.0 | 0.0 | 66.7 | 100.0 | 100.0
Female | 19.0 | 100.0 | 100.0 | 33.3 | 0.0 | 0.0

We design the jaCappella corpus based on analysis of commercial vocal ensemble
songs. We collected 60 musical pieces from a Japanese sheet music store [15]
and examined them in terms of voice parts, gender of singers, and variety of
music genres. In addition, we address copyright issues to legally distribute
our corpus.

Voice parts: 46 of the 60 musical pieces have six voice parts. 42 of the 46
pieces consist of Vo, S, A, T, Bs, and VP, while the other 4 pieces have
fourth chorus parts instead of Vo. Following the majority, we adopted the six-
part format of Vo, S, A, T, Bs, and VP. We call the 42 pieces _the commercial
music collection_ and determined other conditions on the basis of this
collection.

Gender of singers: Table 2 shows the gender frequencies of the singers of the
commercial music collection. The female singers are dominant for S and A. The
male singers are dominant for T, Bs, and VP. We followed the majority for
these parts. Since the gender of a Vo singer strongly depends on musical
pieces, we chose female Vo singers for convenience on singing voice synthesis.

Variety of music genres: The commercial music collection includes various
music genres, for example, Japanese popular music, rock, and enka (Japanese
traditional ballad). The variety in genre is essentially different from choral
songs and should be considered in corpus design. We divided songs into several
subsets and arranged the songs in each subset to different genres.

Copyrights of musical pieces: The distribution of a corpus that includes
commercial musical pieces is extremely restrictive because we must not violate
their copyrights and neighboring rights. To avoid this restriction, we decided
to arrange out-of-copyright songs into vocal ensemble songs and reserve their
copyrights and neighboring rights necessary for research purposes.

###  2.2 Arrangement into vocal ensemble songs

Fig. 1: Excerpt of musical score of “Poplar” in our jaCappella corpus.

In accordance with our design strategy (see Section 2.1), we arranged 35 out-
of-copyright Japanese children’s songs into vocal ensemble songs. The
arrangement was performed by five arrangers. The original children’s songs
were selected from two books of Japanese children’s songs [16, 17]111The used
songs were categorized into _doyo_ and _shoka_. Doyo are well-known Japanese
children’s songs and shoka are Japanese children’s songs taught in school.,
which include musical scores of melodies with lyrics. The Vo parts of our
songs were arranged in accordance with the musical scores and the other parts
were newly composed. The lyrics were given for all parts except for the VP
part.

The 35 songs are divided into seven subsets (five songs per subset). The six
subsets are named _jazz, punk rock, bossa nova, popular, reggae,_ and _enka_.
The songs in each subset were arranged to the corresponding music genre. For
example, the Bs parts of the jazz subset have sequences of equal-duration
notes whose pitches alternately go up and down (a.k.a. walking bass lines).
This is one of the typical features of jazz music. The remaining subset, named
_neutral_ , consists of the songs that were arranged to retain the mood of the
original songs.

We created musical scores of the songs in the MusicXML format [13]. This
format can include various musical symbols and lyrics and is widely used in
MIR studies [18] and singing voice synthesis [19]. Fig. 1 shows an example of
the created musical scores. The created songs include sections where multiple
singers synchronously sing the same lyrics (the region surrounded by red
lines) and sections where part of singers sing asynchronously with the other
singers (the region surrounded by the blue lines). Our songs well capture
these characteristics that frequently appear in the commercial music
collection.

###  2.3 Recording of singing voices

Table 3: Singer IDs and average durations of audio recordings in our jaCappella corpus. Singer IDs are comma-separated from left to right for Vo, S, A, T, Bs, and VP, respectively Subset | Singer IDs | Total dur. [s]
---|---|---
Jazz | Vo1, S1, A1, T1, Bs1, VP1 | 226.7
Punk rock | Vo2, S2, A2, T2, Bs1, VP2 | 310.7
Bossa nova | Vo3, S3, A2, T3, Bs2, VP3 | 334.5
Popular | Vo1, S1, A1, T1, Bs1, VP1 | 352.5
Reggae | Vo3, S3, A2, T3, Bs2, VP3 | 228.7
Enka | Vo2, S2, A2, T2, Bs1, VP2 | 361.1
Neutral | Vo1, S4, A3, T4, Bs1, VP4 | 260.1

We conducted recordings of singing voices along with the vocal ensemble songs.
The recordings were performed per singer to avoid COVID-19 infection. The
singing voices were recorded with Shure SM58 microphones in recording studios
at a sampling frequency of 48 kHz. We employed 20 Japanese semi-professional
singers: three singers for Vo, four singers for S, three singers for A, four
singers for T, two singers for Bs, and four singers for VP. The Vo, S, and A
singers were female and the T, Bs, and VP singers were male. The vocal
ensembles were assembled per subset. Table 3 shows the singer identifiers
(IDs) and total durations of the songs per subset.

After the recordings, we created the best take by combining several takes as
in an usual music production process. The pitch corrections were applied to
these signals when the pitches of the singing voices differed from those of
the musical scores. We did not use effects such as reverb or an equalizer
often used in a commercial music production process. All voice parts in each
song were time-aligned, which makes it easier to use the data for vocal
ensemble separation and synthesis. We also provided the mixtures of all voice
parts. The resultant audio signals were saved as monaural audio files in the
RIFF WAVE format with 24-bit linear quantization.

(a) Vo (b) S

(c) A (d) T

(e) Bs (f) VP

Fig. 2: Spectrogram examples of all voice parts.

Fig. 2 show examples of spectrograms of all voice parts. We can find that the
energies of S, A, T, and Bs are distributed in partly overlapped pitch ranges
and they change synchronously in part. The spectrogram of VP has percussive
characteristics, but the time-frequency components similar to a voiced
spectrogram appear in the range of around 4 to 5 s. This observation shows
that VP has intermediate characteristics between percussive sounds and voices.

###  2.4 Analysis of lexical and non-lexical syllables

Table 4: Frequency of lexical and non-lexical syllables of our jaCappella corpus and commercial music collection (Commercial) Voice part | jaCappella [%] | Commercial [%]
---|---|---
Lexical | Non-lexical | Lexical | Non-lexical
Vo | 85.2 | 14.8 | 91.1 | 8.9
S | 41.9 | 58.1 | 34.2 | 65.8
A | 32.9 | 67.1 | 35.1 | 64.9
T | 33.3 | 66.7 | 36.3 | 63.7
Bs | 0.4 | 99.6 | 2.9 | 97.1

As in the commercial music collection, the created songs include ordinary
Japanese syllables and nonsense syllables such as “ah” and “dm” (purple lyrics
in Fig. 1). The nonsense syllables appear particularly in S, A, T, and Bs. To
distinguish them, we call the former _the lexical syllables_ and the latter
_the non-lexical syllables_.

The frequencies of these syllables differ in voice part. Table 4 shows the
syllable frequencies of the voice parts in the jaCappella corpus and
commercial music collection. We omitted VP since it does not have lyrics. The
frequency of the lexical syllables is high for Vo and quickly decreases from S
to Bs. Since most of the Bs syllables imitate bass instrument sounds, the
frequency of non-lexical syllables (e.g., “dm”, “bon”, and “ban”) is quite
high. These tendencies commonly appear in both collections, showing that our
corpus captures biases of real vocal ensemble songs in terms of lexical and
non-lexical syllables. For Vo and S, the jaCappella corpus has more non-
lexical syllables than the music commercial collection. This is because some
original songs have short lyrics. When we created vocal ensemble versions of
these original songs, we added non-lexical syllables (e.g., “fu” and “la”)
before and after the original lyrics so that the resultant songs were longer
than at least 30 s.

##  3 Vocal Ensemble Separation Experiment

###  3.1 Experimental settings

As an example application, we used the jaCappella corpus for a vocal ensemble
separation task. This task aims at separating audio signals of the six voice
parts from their monaural mixture. The sampling frequency was set to 48 kHz.
We chose seven songs for test, one from each subset. The total duration of the
test songs was 350.2 s. The other songs were used for training. Note that the
separation was done in the singer-closed setting. We computed average
improvements of scale-invariant source-to-distortion ratio (SI-SDR) [20] as an
evaluation metric. The input SI-SDRs of the test data ranged from -23 to -1.3
dB, which shows the difficulty of the separation task.

To increase the amount of training data, we used an intersong mixing method
proposed in [21]. It synthesizes realistic mixtures by mixing audio signals of
voice parts of different songs, changing their tempi and pitches adequately.
The augmented data of the 28 training songs were divided into training and
validation sets. The total duration of the training and validation sets were
7650.7 and 2811.7 s, respectively. We experimentally observed that this data
augmentation improved the separation performance. We also used on-the-fly data
augmentations [22]: random cropping of the training audio segments and random
amplification within the range of $[0.25,1.25]$.

###  3.2 Compared methods

We compared three methods: X-UMX [22], an adaptation of DPTNet [23] for vocal
ensemble separation (DPTNet) [5], and MRDLA [24]. X-UMX performs the
separation in the spectrogram domain while DPTNet and MRDLA separates mixtures
in the waveform domain. All methods estimated monaural audio signals of voice
parts from monaural mixtures. The first and last layers of the waveform-based
methods were modified to have one input channel and six output channels,
respectively. We trained all methods with a NVIDIA A100 GPU and picked up the
trained models at the epoch with the lowest validation loss. The other
settings were as follows:

X-UMX: This method was a baseline method in Music Demixing Challenge 2021
[25]. It was originally proposed for music source separation and we applied it
to vocal ensemble separation. The number of epochs was 1000 and the other
parameters were the same as in the official
implementation222https://github.com/asteroid-
team/asteroid/tree/master/egs/musdb18/X-UMX.

DPTNet: This method is an adaptation of DPTNet for the separation of four-part
vocal ensembles. We set the kernel sizes and strides of the first
convolutional and last transposed convolutional layers to 32 and 16,
respectively. The number of epochs was 600 and the other settings were the
same as in the official
implementation333https://github.com/saurjya/asteroid/tree/4e00daa4c4da77bbee6c0109fa4e2c3611217e72.
Since this method uses permutation invariant training [26], the SI-SDRs of
this method were computed after the best permutations were obtained.

MRDLA [24]: This method is a wavelet-based extension of Wave-U-Net [27]. It
was originally proposed for music source separation and we adapted it to vocal
ensemble separation. We adopted the network architecture with the Haar
wavelet, which achieved nearly best separation performance in [24] and is easy
to implement. We applied it the following modifications. The number of
channels of all layers were increased. More specifically, with the notation
used in [24], $C^{\text{(e)}}$ increased from 18 to 32. The kernel sizes of
convolutional layers were increased to 21 and parametric rectified linear
units were replaced with Gaussian error linear units. We used a loss function
that combines time-domain and time-frequency-domain loss functions [28]. These
modifications greatly improved the separation performance. The number of
epochs was 1000 and the other settings were the same as X-UMX.

The codes used are publicly available at
https://github.com/TomohikoNakamura/asteroid_jaCappella.

###  3.3 Results

Table 5 shows average SI-SDR improvements per voice part. Compared with X-UMX,
the waveform-based methods (DPTNet and MRDLA) provided higher separation
performance. This result indicates that the waveform-based methods are
suitable for vocal ensemble separation. DPTNet provided highest average SI-
SDRs for Vo, T, and Bs. MRDLA achieved highest average SI-SDRs for the other
voice parts. Their average performances were similar for most of the voice
parts, but DPTNet clearly outperforms MRDLA for Bs. The VP sounds were well
separated in all methods, showing that the percussive characteristics of VP
spectrograms make the separation easier. This result is reminiscent of the
fact that drum sounds tend to be well separated in music source separation of
vocals, bass, drums, and other instruments [25].

Some separated audio signals are available at
https://tomohikonakamura.github.io/Tomohiko-Nakamura/demo/jaCappella_sep. When
listening to them, we can find that the separated signals of X-UMX
(particularly for Bs) tend to lack high frequency components and those of the
waveform-based methods tend to include high frequency noises. A similar
tendency was observed in music source separation [29]. The separated signals
of DPTNet included high frequency noises in all voice parts. MRDLA provided
clearer but sometimes choppy separation results. For all methods, the
separated signals of Vo, S, A, and T were often contaminated with the other
voice parts, sometimes with higher energies than the target sources. This
trend is common in all methods, showing the difficulty of this separation
task. Compared with these voice parts, the separated signals of Bs and VP had
less leakage from the other voice parts. This should be because Bs was in the
much lower pitch range and the timbre of VP greatly differs from the other
voice parts as mentioned in Section 2.3. These results clearly show that the
jaCappella corpus is a challenging resource to develop and test vocal ensemble
separation methods.

Table 5: Average SI-SDR improvements of separation methods Method | Voice part [dB]
---|---
Vo | S | A | T | Bs | VP
X-UMX | 7.5 | 10.7 | 13.5 | 10.2 | 9.1 | 21.0
DPTNet | 8.9 | 8.5 | 11.9 | 14.9 | 19.7 | 21.9
MRDLA | 8.7 | 11.8 | 14.7 | 11.3 | 10.2 | 22.1

##  4 Conclusion

We constructed the jaCappella corpus that consists of 35 Japanese vocal
ensemble songs and separate audio recordings of individual voice parts. The
created songs are vocal ensemble arrangements of Japanese children’s songs.
Unlike conventional vocal ensemble datasets, their voice parts include Vo and
VP and the arrangement cover various music genres. We confirmed that our
corpus has distributions of lexical and non-lexical syllable similar to
commercial vocal ensemble songs. Experimental evaluation demonstrated that the
jaCappella corpus is a challenging resource to develop and test algorithms of
vocal ensemble separation. We believe that our corpus accelerates MIR research
on vocal ensembles.

## References

  * [1] H. Cuesta, E. Gómez, A. Martorell, and F. Loáiciga,  “Analysis of intonation in unison choir singing,”  in Proc. Int. Conf. Music Perception Cognition, 2018.
  * [2] S. Rosenzweig, H. Cuesta, C. Weiß, F. Scherbaum, E. Gómez, and M. Müller,  “Dagstuhl ChoirSet: A multitrack dataset for mir research on choral singing,”  Trans. Int. Soc. Music Inf. Retrieval, vol. 3, no. 1, pp. 98–110, 2020.
  * [3] H. Cuesta,  Data-driven Pitch Content Description of Choral Singing Recordings,  Ph.D. thesis, Universitat Pompeu Fabra, 2022.
  * [4] H. Cuesta, B. McFee, and E. Gómez,  “Multiple f0 estimation in vocal ensembles using convolutional neural networks,”  in Proc. Int. Soc. Music Inf. Retrieval Conf., 2020, pp. 302–309.
  * [5] S. Sarkar, E. Benetos, and M. Sandler,  “Vocal harmony separation using time-domain neural networks,”  in Proc. INTERSPEECH, 2021, pp. 3515–3519.
  * [6] M. Gover and P. Depalle,  “Score-informed source separation of choral music,”  in Proc. Int. Soc. Music Inf. Retrieval Conf., 2020.
  * [7] D. Petermann, P. Chandna, H. Cuesta, J. Bonada, and E. Gómez,  “Deep learning based source separation applied to choir ensembles,”  in Proc. Int. Soc. Music Inf. Retrieval Conf., 2020, pp. 733–739.
  * [8] A. McLeod, R. Schramm, M. Steedman, and E. Benetos,  “Automatic transcription of polyphonic vocal music,”  Appl. Sci., vol. 7, no. 12, 1285, 2017.
  * [9] P. Chandna, H. Cuesta, D. Petermann, and E. Gómez,  “A deep-learning based framework for source separation, analysis, and synthesis of choral ensembles,”  Frontiers Signal Process., vol. 2, 2022.
  * [10] H. Tamaru, Y. Saito, S. Takamichi, T. Koriyama, and H. Saruwatari,  “Generative moment matching network-based neural double-tracking for synthesized and natural singing voices,”  IEICE Trans. Inf. Systems, vol. E103.D, no. 3, pp. 639–647, 2020\.
  * [11] H. Purwins, B. Li, T. Virtanen, J. Schlüter, S.-Y. Chang, and T. Sainath,  “Deep learning for audio signal processing,”  IEEE J. Selected Topics Signal Process., vol. 13, no. 2, pp. 206–219, 2019.
  * [12] J.-P. Briot, G. Hadjeres, and F.-D. Pachet,  Deep Learning Techniques for Music Generation,  Springer, 2020.
  * [13] M. Good,  “MusicXML for notation and analysis,”  in The Virtual Score: Representation, Retrieval, Restoration, Walter B. H. and Eleanor S.-F., Eds., pp. 113–124. MIT Press, 2001.
  * [14] Y. Mizobuchi, D. Kitamura, T. Nakamura, H. Saruwatari, Y. Takahashi, and K. Kondo,  “Prior distribution design for music bleeding-sound reduction based on nonnegative matrix factorization,”  in Proc. Asia-Pacific Signal Inf. Process. Assoc. Annu. Summit Conf., 2021, pp. 651–658.
  * [15] “A cappella musical scores,” [Online]. Available: https://elevato-music.com/?mode=cate&cbid=1727017&csid=0, Accessed Oct. 18, 2022, (in Japanese).
  * [16] Nobara-sya, Ed.,  Syoka: Meiji, Taisho, and Syowa,  Nobara-sya, 2009,  (in Japanese).
  * [17] Nobara-sya and Shoji Kubo, Eds.,  Doyo,  Nobara-sya, revised edition, 2010,  (in Japanese).
  * [18] M. Müller,  Fundamentals of Music Processing: Audio, Analysis, Algorithms, Applications,  Springer, first edition, 2015.
  * [19] Y. Hono, K. Hashimoto, K. Oura, Y. Nankaku, and K. Tokuda,  “Sinsy: A deep neural network-based singing voice synthesis system,”  IEEE/ACM Trans. Audio, Speech, Lang. Process., vol. 29, pp. 2803–2815, 2021.
  * [20] J. Le Roux, S. Wisdom, H. Erdogan, and J. R. Hershey,  “SDR – half-baked or well-done?,”  in Proc. IEEE Int. Conf. Acoust., Speech, Signal Process., 2019, pp. 626–630.
  * [21] A. Défossez,  “Hybrid spectrogram and waveform source separation,”  in Proc. Music Demixing Challenge Workshop, 2021.
  * [22] R. Sawata, S. Uhlich, S. Takahashi, and Y. Mitsufuji,  “All for one and one for all: Improving music separation by bridging networks,” 2020,  arXiv preprint, 2010.04228.
  * [23] J. Chen, Q. Mao, and D. Liu,  “Dual-path transformer network: Direct context-aware modeling for end-to-end monaural speech separation,”  in Proc. INTERSPEECH, Oct. 2020, pp. 2642–2646.
  * [24] T. Nakamura, S. Kozuka, and H. Saruwatari,  “Time-domain audio source separation with neural networks based on multiresolution analysis,”  IEEE/ACM Trans. Audio, Speech, Lang. Process., vol. 29, pp. 1687–1701, 2021.
  * [25] Y. Mitsufuji, G. Fabbro, S. Uhlich, F.-R. Stöter, A. Défossez, M. Kim, W. Choi, C.-Y. Yu, and K.-W. Cheuk,  “Music demixing challenge 2021,”  Frontiers Signal Process., vol. 1, 2022.
  * [26] D. Yu, M. Kolbæk, Z.-H. Tan, and J. Jensen,  “Permutation invariant training of deep models for speaker-independent multi-talker speech separation,”  in Proc. IEEE Int. Conf. Acoust., Speech, Signal Process., 2017, pp. 241–245.
  * [27] D. Stoller, S. Ewert, and S. Dixon,  “Wave-U-Net: A multi-scale neural network for end-to-end audio source separation,”  in Proc. Int. Soc. Music Inf. Retrieval Conf., Sept. 2018, pp. 334–340.
  * [28] Z. Kong, W. Ping, A. Dantrey, and B. Catanzaro,  “Speech denoising in the waveform domain with self-attention,”  in Proc. IEEE Int. Conf. Acoust., Speech, Signal Process., 2022, pp. 7867–7871.
  * [29] N. Schaffer, B. Cogan, E. Manilow, M. Morrison, P. Seetharaman, and B. Pardo,  “Music separation enhancement with generative modeling,” 2022,  arXiv: 2208.12387.