# Towards Auto-Modeling of Formal Verification for NextG Protocols: A
Multimodal cross- and self-attention Large Language Model Approach

Jingda Yang1 Ying Wang1
1Stevens Institute of Technology, Hoboken, NJ
Email: 1{jyang76<EMAIL_ADDRESS>
###### Abstract

This paper introduces Auto-modeling of Formal Verification with Real-world
Prompting for 5G and NextG protocols (AVRE), a novel system designed for the
formal verification of Next Generation (NextG) communication protocols,
addressing the increasing complexity and scalability challenges in network
protocol design and verification. Utilizing Large Language Models (LLMs), AVRE
transforms protocol descriptions into dependency graphs and formal models,
efficiently resolving ambiguities and capturing design intent. The system
integrates a transformer model with LLMs to autonomously establish
quantifiable dependency relationships through cross- and self-attention
mechanisms. Enhanced by iterative feedback from the HyFuzz experimental
platform, AVRE significantly advances the accuracy and relevance of formal
verification in complex communication protocols, offering a groundbreaking
approach to validating sophisticated communication systems. We compare CAL’s
performance with state-of-the-art LLM-based models and traditional time
sequence models, demonstrating its superiority in accuracy and robustness,
achieving an accuracy of 95.94% and an AUC of 0.98. This NLP-based approach
enables, for the first time, the creation of exploits directly from design
documents, making remarkable progress in scalable system verification and
validation.

###### Index Terms:

Formal verification, cross-attention, self-attention, natural language
protocol, formal flow graph

##  I Introduction

The third generation partnership project (3GPP) published its Release 17
(Rel-17) specifications at the end of the first quarter of 2022 [1]. Since
then, parallel and subsequent releases have been rolled out to enhance and
address new and unfulfilled requirements from previous releases. It ensures
ongoing innovation and improvement in mobile communication technologies,
aligning with the evolving needs and advancements in the field. 3GPP protocols
consist of a multitude of technical specifications and documents that cover
various aspects of mobile communication networks, including radio access, core
network, and service capabilities. 3GPP protocols, encompassing a wide array
of technical specifications, are extensive, with documents like the Radio
Resource Control (RRC) in Release 17 spanning over a thousand pages [2]. The
extensive nature of these documents, coupled with their distributed security
protocols, renders manual verification and testing both time-intensive and
susceptible to error. This complexity escalates in future network generations,
exacerbating the risk of zero-day vulnerabilities.

Furthermore, the incorporation of O-RAN and network function virtualization
introduces additional layers of complexity and potential attack vectors
through cloud APIs into 5G and future G infrastructure [3]. These advancements
offer enhanced functionality but expose operators to novel security
challenges, especially in the relatively uncharted territory of cloud
security. This complexity, compounded by the involvement of various entities
in development, heightens the risk of security breaches, particularly through
misconfigured containers and exposed APIs.

Thus, in 5G and future G systems and networks, logical attacks exploiting
protocol logic errors represent a significant vulnerability category. These
attacks are challenging to detect due to the scale and complexity of the
network systems. Formal verification encompasses a broad range of techniques
used to prove or disprove the correctness of algorithms, protocols, systems,
or software with respect to certain formal specifications. It also involves
mathematical analysis to ensure that a system behaves as intended. Utilizing
the Dolev-Yao (DY) formal attack model [4, 5], one of the widely adopted
methodologies, formal verification has demonstrated its effectiveness in
identifying flaws in infrastructure and communication protocols. However, this
approach is limited to abstract specifications, and, as of now, the full
automation of protocol verification and validation of their implementations
remains beyond the reach of current technologies [6, 7].

With the recent advancements in Large Language Models (LLMs), an intriguing
question emerges: Can LLMs contribute to accelerating the design and
verification of large-scale protocols, and can they be effectively integrated
with system validation processes that involve existing implementations?

To answer this question, two crucial conditions must be addressed: clarifying
ambiguities and capturing design intentions. The first condition involves
resolving the conflict between the ambiguity inherent in natural language
processing and the need for explicitness in formal verification modeling.
Resolving this conflict is essential to demonstrate the potential to provide
measurable and verifiable trustworthiness. The second condition requires
differentiating intentional relationships or dependencies from unintentional
ones identified by LLMs in targeting protocol designs. The differentiation is
crucial in transforming the design-intended relationships into mathematical
and logical expressions in formal verification.

In the past several months, both academic and industry sectors have
increasingly focused on applying LLMs in the realm of formal verification. Two
major areas of this application are using prompt engineering and LLMs for
hardware assertion [8, 9, 10] and software system Bounded Model Checking (BMC)
[8, 9]. To our knowledge, no published work yet explores the use of LLMs in
verifying communication-related protocols and specifications, especially for
the large and complex protocols of 3GPP releases. One of the reasons is due to
a common challenge in existing research is capturing trustworthy design intent
in a set of assertions for use in formal verification or testing-based
checking. This challenge intensifies as system distribution and complexity
increase in the case of 5G and the future G, particularly when intertwined
with a broad spectrum of various usage scenarios and verticals. The iterative
prompts to the LLMs has limitations due to the complex and broad dependencies
among identifiers, commands, and properties.

Further more, our previous work on non-LLM-based NLP approach for 5G and other
communication protocols [11] marked a significant shift from manual to
automated, accuracy-focused analysis in translating natural language oriented
protocols into formal models. While it revealed limitations in handling
complex semantic relationships with strong contextual control, it also
highlighted the potential and direction for LLM-based NLP in formal modeling.
We found this approach becomes particularly promising in detecting design
intentions with greater intelligence and enhancing trustworthiness through its
connection to learn from real-world experiments [12].

In this paper, we introduce a novel approach, named Auto-modeling of Formal
Verification with Real-world Prompting for 5G and NextG protocols (AVRE),
which addresses the need for scalable formal verification in the domains of 5G
and NextG. AVRE uses LLMs to clarify ambiguities and capture design intent,
transforming protocol descriptions into dependency graphs and formal models.
Our method differs from existing techniques by integrating a transformer model
with the LLM, allowing quantifiable dependency relationships to be generated
under supervision and enabling transformative learning without human
involvement. This system, enhanced by iterative feedback from an experimental
platform: HyFuzz [12], fills a research gap by combining experience-based and
logical dependency analyses in protocol documentation, thereby significantly
improving the accuracy and relevance of formal verification in complex
communication protocols.

###  I-A Related Work

Converting Informal Natural Language System Designs and Protocols to Formal
Description: Approaches to transforming natural language descriptions into
formal models have seen considerable advancements, evolving through the
introduction of diverse methodologies over the years. A decade ago, Drechsler
et al. [13] proposed a paradigm that incorporated the Formal Specification
Level (FSL), adeptly bridging the gap between informal textbook specifications
and formal Electronic System Level (ESL) interpretations. Subsequently,
Banarescu et al. [14] proposed a hybrid methodology that converted linguistic
expressions into formal paradigms by merging symbolic and statistical
techniques. With the advent of deep learning, Dong and Lapata [15] employed
neural networks to convert natural language instructions into executable
codes. This work was further enhanced by the contributions of Reddy et al.
[16] in 2019, who focused on semantic parsing, utilizing denotations to
transform complex linguistic structures into formalized notations. Meanwhile,
the application of regular expressions has been identified as a viable means
to extract formal specifications from natural language narratives, providing
advanced components in deep learning frameworks [17]. Despite these
developments, models based on these previous methodologies have achieved an
accuracy threshold of approximately 90%, which is inadequate for ensuring
complete recall. This poses a challenge in the precise conversion of natural
language protocols into formal formulations.

LLMs Based Formal Verification: LLMs have demonstrated impressive reasoning
and assertion capabilities for formal verification [9, 18, 19]. Research in
[8, 9] has explored using LLMs to generate temporal logic specifications and
assertions from unstructured natural languages. Meanwhile, studies in [20, 21]
focus on leveraging LLMs to enhance BMC for identifying software
vulnerabilities and deriving counterexamples. In [10], the authors trained
GPT-4 to generate correct SystemVerilog Assertions (SVA) through iterative
prompt refinement with rules. However, it remains unclear how these models
derive answers and whether they rely on simple heuristics rather than a
generated chain-of-thought [18]. The current state of the art prioritizes
producing formal specifications and properties quickly, albeit with slight
inaccuracies, over generating perfect specifications or correctness statements
[19]. The non-transparency related to LLM heuristics leads to a large number
of irrelevant dependencies, resulting in low precision in dependency
classification. To address this, our experimental platform connects to guide
and refine the dependency graph range.

Prompting Limitations in LLM Enabled Formal Verification: Furthermore, the
majority of existing work relies on prompt engineering. LLM-integrated
applications blur the line between data and instructions [22]. LLMs can
produce non-deterministic outputs, potentially yielding different results for
the same prompt. This variability poses a potential threat to the validity of
scientific conclusions unless researchers adapt their methods to account for
it in their empirical analyses [23]. The adoption of prompting methods
introduces challenges in iterative formal verification without human
involvement. The randomness in LLMs is influenced by the sampling methods used
during text generation, such as top-k sampling or nucleus sampling [24],
limiting its application in classifiers or deterministic types of
applications. To address the non-determinism and iterative formal
verification, distinct from current formal verification methods that utilize
prompt engineering, we designed an open-access LLM, integrated with a
transformer model, to achieve supervised dependency.”

Digital Engineering Aided Formal Guided System Validation: In the field of
integrated Design Validation, there has been recent research progress in
combining formal verification with simulation, resulting in a practical
validation engine with reasonable run-time [25]. Experimental work in the
context of 5G has gained significant attention over the past few years,
shifting from the simulation-driven research used in previous mobile network
generations to system implementation prototyping [26]. In our previous work,
we explored a Formal-guided Fuzzing testing approach [27, 28] to bridge design
verification and system validation. This approach complements the scalability
limitations of formal verification and addresses the impacts of detected
vulnerabilities. We have introduced a fuzzing digital twin [29] to provide an
open and automated platform for systematically that enables an autonomous
detection of vulnerabilities and unintended emergent behaviors in 5G
infrastructures. However, a constraint of this initial approach is heavy
reliance on expert insights to identify and articulate formal relationships.

###  I-B Contribution

The main original contributions of this work are summarised as follows:

  * •

The research introduces a novel approach that utilizes LLMs to address
critical challenges in formal verification, specifically in clarifying
ambiguities and capturing design intent. This approach combines experience-
based prior-probability distribution with logical dependency analysis in
protocol documentation, and leverage experimental-based posterior-probability
to enhances the accuracy and relevance of the dependency graph by the cross-
attention-based LLM (CAL) model.

  * •

The paper presents a new systematic solution named AVRE, which equipped with
CAL, a continuously-learning, cross-attention-based LLMs. CAL is desined to
interpret and transform protocol descriptions into dependency graphs, which
can then be converted into formal models. CAL is enhanced by incorporating
iterative feedback from an experimental platform, HyFuzz, to focuse on
refining the capture of intentions and resolution of ambiguities.

  * •

In CAL, we introduce a novel multi-session detection method that bypasses
traditional token count barriers. By segmenting comprehensive protocols into
manageable sections and concurrently processing them, it can output detailed
and quality analysis without token constraints. CAL incorporates refined
cross-attention mechanisms instead of prompting based scheme, achieves high
efficiency to identify and interpret complex formal relationships with
enhanced accuracy and insight.

  * •

We have developed a scalable cross sessions dependency graph that supports the
hierarchy of formal analysis, facilitating the revelation of in-depth
relationships embedded within protocols to systematically pinpoint and
counteract vulnerabilities.

The rest of our paper is organized as follows. Section I-A listed the existing
literature in the field of LLMs, dependency graph, formal verification, and
experimental based validation. We introduce our proposed EVRA and show the
architecture of the system in Section II, followed by the the detailed
description of the system in Section III and Section IV. We provide the
performance analysis and in Section V. Lastly, we concluse our work with
future research directions in Section VI.

##  II System Overview

In addressing the critical need for scalable formal verification in the
rapidly evolving domains of 5G and NextG protocols and specifications, in this
paper, we present a pioneering approach that utilizes LLMs to overcome key
challenges of clarifying ambiguities and capturing design intent. We present a
novel systematic solution AVER as shown in Fig. 1 : Auto-modeling of Formal
Verification with Real-world Prompting for 5G and NextG protocols.

Figure 1: System Overview of Auto-Modeling and Trustworthy for Formal
Verification and Validation in 5G and NextG Security Protocols. Red line shows
the process from informal system protocols to dependency graph and formal
expression, and green line shows the formal guided fuzz testing feedback to
the CAL and refine the results

At the heart of AVRE is a continuously-learning, CAL designed to interpret and
transform protocol descriptions into dependency graphs, which are subsequently
converted into formal models. Differing from the current state of the art in
using LLM prompting for formal verification, our approach integrates the
transformer model with the LLM model, enabling it to generate a quantifiable
dependency relationship under supervision. This facilitates the transformative
learning of the LLM without human involvement, meeting the requirements for
formal explicitness. This system is further enhanced by incorporating
iterative feedback from our experimental platform: HyFuzz [12], aimed at
refining intention capture and ambiguity resolution.

CAL is trained on labeled identifiers (step 1 and step 2) and formal
properties, designed to predict formal properties (step 3) with a more
controlled environments. The design of cross-attention mechanisms utilization
the LLM model improve the capability of the model in complex protocol.

The experimental platform serves as two purpose: intention and the
trustworthy. As shown in step 4 and step 5 in Fig. 1, it provides relevancy
and design intention information , which is used with the dependency
relationships detected by CAL together to form the dependency graph. For
trustworthy, as shown in step 6 and step 7, the low confident prediction is
set to the experimental platform to return evidence that could be added to
ground truth dependence database. With multiple iterations, a robust
dependency graph will be generated to sent to formal method verification. The
detected vulnerability will be further used in protocol fortification.

The design of the system AVRE uniquely fills a gap in the existing research
landscape by integrating experience-based prior-probability distribution with
logical dependency analysis in protocol documentation using LLMs. Moreover, by
leveraging experimental-based posterior-probability through real-world
prompting, AVRE establishes an iterative learning loop, significantly
enhancing the accuracy and relevance of the intention of the CAL model. This
advancement marks a pivotal contribution to the field, offering new directions
in the formal verification of complex communication protocols.

##  III Protocol Analysis and Data Pre-Process and Annotation

###  III-A Protocol Analysis and Formal Properties Definition

In this paper, we use 3GPP Release 17 Radio Resource Control [30] as an
example to illustrate AVRE. We identify two fundamental elements: procedures
and identifiers. Procedures are defined as sequences of actions and
interactions among different entities. Identifiers in the protocols are
specific labels or names used to uniquely recognize various elements within
mobile telecommunications networks. For instance, IMSI (International Mobile
Subscriber Identity) is a unique number associated with all cellular networks,
used primarily for identifying individual subscribers for billing and
identification purposes. IMEI (International Mobile Equipment Identity) is
defined as a unique number to identify mobile devices, primarily used for
identifying the device itself, rather than the subscriber [30]. The procedures
define the structure of a set of identifiers that are connected dependently.
The dependent relationship between the identifiers, framed by the structure
defined in the procedures, generates the dependency graph, which is then
converted for formal analysis. As shown in Table. I, while the extraction of
entities from protocol identifiers is straightforward, the classification of
their dependency is a problem that CAL targets. However, the procedures
include intricate interactions and designs, with unspecified space for various
vendors to implement based on their existing infrastructures and devices. In
this paper, we innovatively connect to real-world or simulated experimental
platforms to aid in procedure formulation.

TABLE I: RRCSetupRequest-IEs field descriptions Identifier |  Description
---|---
establishmentCause |  Provides the establishment cause for the RRCSetupRequest in accordance with the information received from upper layers. gNB is not expected to reject an RRCSetupRequest due to unknown cause value being used by the UE.
ue-Identity |  UE identity included to facilitate contention resolution by lower layers.

Considering confidentiality, integrity, and availability (CIA) triad which is
widely accepted security model, along with the Dolev-Yao model for
communication protol formal verification, we have proposed four essential
properties to describe the dependency among identifiers [27]. These
properties, each addressing a distinct facet of security augmentation within
the specifications, are defined as follows:

  1. 1.

Confidentiality: the capability of source to prevent private information from
leakage of the destination. The source should be the selected encryption
algorithm or the key of encryption algorithm, and the destination should be
command or specific identifier, which are confidentiality protected by source.

  2. 2.

Integrity : the capability of source to keep the destination information
unmodified. Similar to confidentiality, the source should be the selected
integrity algorithm or the key of integrity algorithm, and the destination
should be the command or specific identifier, which are integrity protected by
source.

  3. 3.

Authentication: the ability of source to help User Equipment (UE) or gNodeB
(gNB) to identify where and when the destination was sent from. The source
should be the distinctive identifier, which can uniquely represent a entity
(like gNB) or a communication session (like UE id).

  4. 4.

Accounting: the source of accounting relationship is the counting identifier
which can sequentially track and distinguish each transmitted command. The
destination should be the sequence-protected command.

  5. 5.

Include: the destination identifier is included in the source identifier.

  6. 6.

Generate: the destination identifier is generated by the source identifier.

###  III-B Data Preparation

In our study, we annotated dependencies (formal properties) of identifiers in
the 5G Radio Resource Control (RRC) protocol [30], focusing on Sections 5.3.1
to 5.3.5. From these sections, approximately 16,428 samples were annotated,
including source, destination, and dependency relationships. Out of these,
1,218 samples were identified by domain experts who analyzed the documents to
determine relationships. The remaining samples consist of source and
destination pairs lacking a dependency relationship. In our proposed model, we
treat this as a classification problem for all potential source-destination
pairs, encompassing both relevant and non-relevant ones. Consequently, the
large number of source and destination pairs results in highly imbalanced
data.

Figure 2: Formal Properties Statistical Counts and Intersections

In our analysis of the annotated data samples, we have identified an imbalance
in the distribution between positive and negative samples. To address this
issue and improve the model’s performance, we propose employing a weight-
balanced binary cross-entropy loss. Fig. 2 illustrates the size of each
property type and the intersection sizes among them. It is clear from Fig. 2
that ’include’ has the largest number of detections. Furthermore, the
intersections of ’include’ with ’account’ and ’integrity’ represent the two
largest intersection counts, indicating a strong correlation between these
properties. It is also important to note the significant presence of
’integrity’ in multiple intersections, which is consistent with the importance
of integrity in RRC protocols 3GPP in release 17.

##  IV Methodology

###  IV-A Building Multimodal cross- and self-attention Large Language Model

In this work, we proposed CAL, an LLM embedded with cross- and self-attention
model, as delineated in Fig. 3, considering both the contextual information
from the original protocols and learns the defined dependency relationships
among identifiers. CAL model employs a pretrained LLM (GPT-2), which consists
of $N$ transformer layers, to extract hidden insights from protocol
descriptions. Here, considering the scalability of training and the
performance accuracy, we select $N=12$.

We incorporate cross-attention mechanisms to discern the relationships between
the extracted latent information and query entities [31]. To further enrich
the contextual understanding, we deploy self-attention frameworks that
evaluate inter-relations among all positions from the preceding stage, guided
by weighted considerations. In the final stage of the presented model, a
linear classifier is implemented to infer probabilities associated with
distinct formal attributes.

Self-attention generates contextual representations for a single sequence by
computing weighted averages of all tokens, while cross-attention evaluates
interdependent contextual relationships between the query sequence and the
context sequence in transformer models [32, 33, 34]. In the proposed CAL model
for converting complex contextual protocols into explicit dependency graphs,
self-attention serves as the mechanism to understand the context within the
protocols, while cross-attention understands and recognizes the relationships
across the identifier sequences.

Figure 3: Attention Driven Formal Identifier and Property Abstraction Model

Self-attention calculates a weighted average of feature representations, where
the weight represents the similarity score between pairs of feature
representations. As defined in [32], an input sequence of $n$ tokens of
dimensions $d$, $X\in R^{n\times d}$, is extracted by three projection
matrices $W_{Q}\in R^{d\times d_{q}}$, $W_{K}\in R^{d\times d_{k}}$ and
$W_{V}\in R^{d\times d_{v}}$ ($d_{q}=d_{k}$). The input consists of queries
and keys with dimension $d_{k}$, and values with dimension $d_{v}$. Three
different feature representations $Q=XW_{Q},K=XW_{K},$ and $V=XW_{V}$, where
$Q\in R^{n\times d_{q}}$, $K\in R^{n\times d_{k}}$ and $V\in R^{n\times
d_{v}}$. Intuitively, $Q$, $K$ and $V$ are separately regarded as query, key
and value. Normalized dot-product of query and key is used to represent the
attention score $A\in R^{n\times n}$ of each query and paired keys as:

$A=softmax(\frac{QK^{T}}{\sqrt{d_{q}}})$ (1)

where division by $\sqrt{d_{q}}$ normalizes the dot-product of $Q$ and
$K^{T}$, ensuring that the distribution of the dot-product aligns with
expectation $\mathrm{E}=0$ and variance $\mathrm{Var}=1$. Ultimately,
attention value is calculated as follow,

$\mbox{Self-attention}(Q,K,V)=softmax(\frac{QK^{T}}{\sqrt{d_{q}}})V=AV$ (2)

where output $\mbox{Self-attention}(Q,K,V)\in R^{n\times d_{v}}$ is the
weighted average of extracted features. Normally, a residual linear feed
forward layer is incorporated to further distill the acquired knowledge
represented by the weighted average features.

Utilizing the self-attention mechanism, cross-attention takes two input
sequences with different sequence length $X_{1}\in R^{n_{1}\times d}$ and
$X_{2}\in R^{n_{2}\times d}$ as inputs. Subsequently,
$Q=X_{1}W_{Q},K=X_{2}W_{K},$ and $V=X_{2}W_{V}$ are derived from $X_{1}$ and
$X_{2}$ respectively and the dimension of attention value can be succinctly
expressed as $R^{n_{1}\times d_{v}}$.

###  IV-B Balanced Loss Function

In Section III-B, we observed the imbalance in the data distribution of
relationships amongst entities, and is evident in Table II. In response to
this challenge, we adopt a weight-balanced binary cross-entropy loss,
articulated in Equation 3. In this equation, $N$ signifies the total number of
cases, $y_{i}$ represents the ground truth, $p(y_{i})$ is the predicted
probability, and $n_{(y_{i})}$ denotes the proportion of class $y_{i}$ within
all cases. Utilizing the inverse class ratio amplifies the impact of the
underrepresented class while tempering the dominance of the majority class,
offering a balanced approach to mitigate the skewed data distribution.

TABLE II: Imbalanced Nature of Formal Property Data Relationship | Class | Count | Relationship | Class | Count
---|---|---|---|---|---
Confidentiality | 0 | 16421 | Accounting | 0 | 16399
Confidentiality | 1 | 7 | Accounting | 1 | 29
Integrity | 0 | 16408 | Include | 0 | 16329
Integrity | 1 | 20 | Include | 1 | 99
Authentication | 0 | 16417 | Generate | 0 | 16389
Authentication | 1 | 11 | Generate | 1 | 39

$\begin{gathered}L_{i}=-\left[y_{i}\cdot log(p(y_{i}))+(1-y_{i})\cdot
log(1-p(y_{i}))\right]\\\
L=\frac{1}{N}\sum_{i=1}^{N}L_{i}\cdot(1-\frac{n_{(yi)}}{N})\end{gathered}$ (3)

###  IV-C Connection to Experimental Platform

Inspired by the iterative prompting to the LLM, the experimental platform
serves as the prompting server in real world. In order to clarify the
ambiguity in the LLM model, the counterpart experiments configuration could be
auto-generated and performed, in which the results generated is feedback to
the LLM to improve the trustworthiness. Through the digital engineering
module, which facilitates connections to available real-world execution
platforms or digital twins, the process effectively bridges the gap between
design intentions and real-world operations for mission-critical
infrastructures.

The experimental platform, HyFuzz, employs a hybrid system model [12] that
incorporates two distinct platforms: a ZeroMQ virtual model and an Over the
Air (OTA) physical model. In addition to running 5G tests in various
scenarios, the uniqueness of the HyFuzz platform is its ability to serve as
relay nodes to perform various fuzzing tests. The relay node is capable of
modifying and permutating commands and accessing messages exchanged between
the UE and the gNB. HyFuzz facilitates multi-step Man-In-The-Middle (MITM)
attacks, enabling the identification and analysis of vulnerabilities and the
detection of various prompts due to the uncertainty of CAL model outputs and
providing an accurate real-world ground truth. An overview of the HyFuzz is
shown in Fig. 4.

Figure 4: Virtual and Over the Air (OTA) Mode Experimental of HyFuzz[12]

As illustrated in Fig. II, the experimental platform is seamlessly integrated
with the CAL model, supporting it from two key aspects: design intention and
trustworthiness. Regarding design intention, the platform supplies relevant
information and design intents to the CAL model, enabling it to continue
training based on novel evidence of dependency relationships, thus effectively
constructing an accurate dependency graph. In terms of trustworthiness, low-
confidence predictions are referred back to the experimental platform for
further validation, potentially contributing new data to the ground truth
dependency database. This iterative process aims to create a robust dependency
graph, which will be utilized for formal method verification. Detected
vulnerabilities will then be leveraged in protocol fortification.”

##  V System Performance Assessment

###  V-A CAL Experiment Setting

Considering the openness and accessibility of the LLMs, in this paper, we
select the pre-trained GPT-2 model with 12 transformer layers and 12 attention
heads as embedded pre-trained LLM included in CAL. The GPT-2’s embedding size
is set to 768, and the sequence length is configured to 1024, allowing for the
effective extraction of hidden information from the extended protocols.
Subsequent to the application of the LLM, the extracted hidden information is
processed through 6 layers of self-attention with 6 attention heads and 6
layers of cross-attention with 6 attention heads. This structure aids in
recognizing and processing the comprehensive relationships between the
protocols and the associated query entities. Further details of the model’s
configuration are presented in Table III.

TABLE III: Configuration of Model Parameter | Value
---|---
GPT-2’s Embedding Size | $768$
GPT-2’s Sequentce Length | $104$
GPT-2’s Layers | $12$
GPT-2’s Attention Head | $12$
Cross-attention Layer | $6$
Cross-attention Attention Head | $6$
Self-attention Layer | $6$
Self-attention Attention Head | $6$
Learning Rate | $1e^{-7}$
Epoch | $100$
dropout rate | $0.1$
Train/Validation Ratio | $9:1$

###  V-B CAL Experiment Result Analysis

As depicted in Fig. 5, the consistent trends in both training and validation
accuracy of CAL underscore the model’s proficiency in extracting the
dependency relationship information from the examined protocols and entities.
In our experiment setting, formal properties are designated as positive, while
their absence is categorized as negative. As presented in TableIV, our model
performs stable accuracy of $95.94$%, and achieves $100$% accuracy in recall,
indicating the high and stable performance in formal property prediction and
the trustworthiness of the model.

We further compared our model with other state of art model performance. Table
IV leads to an explicit conclusion that the CAL significantly outperforms all
other models delineated in Section V-A. Fig. 6 reveals that only the LSTM
model and the hybrid LLMs with LSTM model exhibit a deficiency in the
efficient extraction of information during the training phase, resulting in
trapping in local optima. The result also indicates the necessity of LLMs in
processing complex protocols and standards.

Figure 5: Training Loss: the training loss indicate the incapability of
traditional models like LSTM in processing complex dependency and text. Figure
6: Training Result: Suboptimal models, such as those utilizing LLM with LSTM
and standalone LSTM, often get trapped in local minima due to Class Imbalance
and Specially Designed Loss.

To compare the performance of transformer-based models with traditional non-
transformer models, the LSTM, known for effectively capturing long-range
dependencies and typically performs better than CNN and RNN, is chosen to
replace the cross-attention and self-attention. To ensure consistency of
experimentation, the LSTM is set with a hidden state size of $768$ and $6$
recurrent layers. Additionally, the LSTM alone was used to directly process
natural language to predict formal properties, also with a hidden state size
of $768$ and $6$ layers.

TABLE IV: Accuracy of Different Models Model | Accuracy
---|---
CAL | 95.94%
LLM with LSTM | 66.76%
LSTM | 50.21%

The Area Under the Curve (AUC) is commonly described as a statistical measure
used to evaluate the performance of a classification model. As shown in Fig.7,
we can see that via the True Positive Rate (TPR) against the False Positive
Rate (FPR), CAL has an AUC value of 0.98, indicating excellent performance.

Figure 7: Receiver Operating Characteristic (ROC) curve of CAL Model

Then, we further analyze the AUC for each type of dependency, as shown in Fig.
8. Confidentiality: This curve appears to be the closest to the top-left
corner, suggesting it has the best performance among the four criteria.
Integrity, Authentication, Accounting: These curves are further from the top-
left corner compared to Confidentiality. While they still demonstrate good
performance, they are not as effective as the Confidentiality curve.

Figure 8: Dependency Relations Specific ROC curve of CAL Model

To better visualize the interactions between relevant entities and protocol
procedure descriptions, we utilize the Actions related to the transmission of
“RRCSetupRequest” message as an example. This verification process aims to
determine whether our model can effectively extract valuable information from
the human-written protocol procedure descriptions.

In transformer-based models, each transformer layer has the capability to
extract distinct information through different attention scores. In this
study, we leverage the average score of cross-attention layers to visualize
the interactions between relevant entities and protocol procedure
descriptions. Taking the entities “establishmentCause” and “RRCSetupRequest”,
along with their corresponding procedure as an example, we generate an
attention map (Fig. 9). The attention map clearly reveals that these two
entities place more emphasis on specific terminologies, such as
“establishmentCause”, “mps-PriorityAccess”, and “RRC”, as well as the levels
of indentation, such as “1$>$” and “2:”. This observation highlights the
cross-attention component’s ability to effectively focus on and extract
essential information from key terms within the input text.

Figure 9: Attention Map Depicting Average Attention Scores Across Layers:
Lighter Shades Indicate Higher Attention; Darker Shades Signify Reduced
Attention.

###  V-C Case Study of Design Intention Capturing and Trustworthy Enhancement
via the connection to real-world testbed

Case 1: Design Intention With the CAL model, the generated dependencies
include both intended and unintended ones. Compared to extraction from human
expertise, a portion of unintended dependency relationships is also detected.
These unintended dependencies can be filtered out via connection to a real-
world experimental platform.

We took the example of “RRC_setup_request” and “Security_mode_command”, as
shown in Fig. 10. Figure 10(a) illustrates the raw dependency relationships
detected by CAL, while Figure 10(b) shows the experimentally filtered, design-
intended dependency graph. Using the information flow from the experiment
platform, as shown in Fig.11, we can derive the design-intended dependency
graph presented in Fig. 10(b) and Fig. 10(d). Figures 10(c) and 10(e) are
equivalent to Figures 10(b) and 10(d) respectively, offering a more user-
friendly visualization.

Figure 10: Design Intention: (a) is the raw dependency relationships that
detected by CAL, and (b) is the experiments filtered design intended
dependency graph. Figure 11: Information Flow-graph detected in Experiment
Platform

Case 2: Trustworthy For dependencies predicted by CAL with low confidence, the
uncertain dependency can be converted into test scripts and sent to an
experimental platform to generate evidence. This evidence can be used to
confirm or refute the existence of the dependency. As shown in Fig. 12, the
dependency between KRRCenc and CipherAlgorithm shows low confidence in the
detected “Integrity”. This is automatically converted into fuzzing scripts to
generate evidence, proving that there is no dependency between them, as
indicated in the parsed information from the log file 13.

Figure 12: Information Flow-graph detected in Experiment Platform Figure 13:
Fuzzing Log File to Parse Evidence Information

(a) RRC Connection Flow Graph

(b) Security Mode Command Flow Graph

Figure 14: Flow Graph

(a) Predicted RRC Connection Dependency Graph

(b) Ground Truth RRC Connection Dependency Graph

(c) Predicted Security Mode Command Dependency Graph

(d) Ground Truth Security Mode Command Dependency Graph

Figure 15: Comparison between Predicted and Ground Truth Dependency Graph

###  V-D Formal Verification and Attack Model

Based on the predicted relationship between entities, our next objective is to
perform the formal verification, as shown in Fig. 14. The interconnected
sections and communicated commands consisting of identifiers. We can first
fill up the interconnected sections and communicated commands, which is
depicted in natural language protocols, shown in Fig. 14a and Fig. 14b. And
from the command table in natural language protocols, we can easily identify
which identifiers are included in the commands.

Utilizing the identified formal properties, we construct a comprehensive
dependency graph, which facilitates the derivation of formal dependencies
through this graph.

We consider the RRC connection establishment procedure as an example. Nodes
were manually extracted from the natural language protocol, as depicted in
Figs. 15a and 15b. The visual representation employs boxes to signify
“Include” and uses various arrow types to delineate distinct formal
properties. Leveraging our predicted formal properties, we generated the RRC
connection dependency graph (see Fig. 15a). Remarkably, this aligns perfectly
with the ground truth of the RRC connection dependency graph. However, during
the Security Mode procedure, there were discrepancies between the predicted
formal properties (as presented in Fig. 15c) and the ground truth (see Fig.
15d). Therefore, subsequent manual verification is advisable. Notably, while
there may be the inclusion of extraneous formal properties, none are omitted.
Building on previous related work [27], this dependency graph can be
transformed into Proverif code, enabling formal verification. Compared to
solely manual labeling of formal properties, our proposed model streamlines
the process by narrowing down the entirety of natural language protocols to
the task of parsing redundant formal properties from the crafted formal
dependency graph.

##  VI Conclusion

In conclusion, we present AVRE, a novel system for the formal verification of
NextG protocols, leveraging Large Language Models (LLMs) to transform protocol
descriptions into dependency graphs and formal models. Enhanced by the HyFuzz
experimental platform, AVRE demonstrates significant advances in the accuracy
and relevance of formal verification in complex communication protocols. The
research underscores the efficiency of CAL, a continuously-learning, cross-
attention-based LLM, in extracting formal properties and dependencies,
outperforming traditional methods. The study emphasizes the potential of LLMs
in enhancing trustworthiness and clarifying ambiguities in protocol
verification, marking a significant contribution to the field. By reducing
reliance on manual labeling and associated human errors, our method offers a
more efficient approach, focusing only on the most pertinent formal
relationships. Our work in extracting formal relationships from natural
language protocols enhances the clarity and understanding of these protocols,
ensuring a more robust, reliable, and efficient approach for protocol
verification and system validation in large-scale, complex systems.

## Acknowledgment

This effort was sponsored by the Defense Advanced Research Project Agency
(DARPA) under grant no. D22AP00144. The views and conclusions contained herein
are those of the authors and should not be interpreted as necessarily
representing the official policies or endorsements, either expressed or
implied, of DARPA or the U.S. Government.

## References

  * [1] 3GPP, “5g evolution toward 5g advanced: An overview of 3gpp releases 17 and 18,” _IEEE Xplore_ , 2022.
  * [2] “Nr; radio resource control (rrc); protocol specification,” 3rd Generation Partnership Project (3GPP), Technical Specification (TS) 38.331, 2021, available: 3GPP website. [Online]. Available: https://www.3gpp.org
  * [3] “Open ran – 5g hacking just got a lot more interesting,” Karsten Nohl, Security Research Labs, Tech. Rep., 2022.
  * [4] D. Dolev and A. Yao, “On the security of public key protocols,” _IEEE Transactions on information theory_ , vol. 29, no. 2, pp. 198–208, 1983.
  * [5] I. Cervesato, “The dolev-yao intruder is the most powerful attacker,” in _16th Annual Symposium on Logic in Computer Science—LICS_ , vol. 1. Citeseer, 2001, pp. 1–2.
  * [6] M. Ammann, L. Hirschi, and S. Kremer, “Dy fuzzing: Formal dolev-yao models meet cryptographic protocol fuzz testing,” in _45th IEEE Symposium on Security and Privacy_ , 2024.
  * [7] I. Rakotonirina, G. Barthe, and C. Schneidewind, “Decision and complexity of dolev-yao hyperproperties (technical report),” in _Symposium on Principles of Programming Languages (POPL)_ , 2024.
  * [8] R. Kande, H. Pearce, B. Tan, B. Dolan-Gavitt, S. Thakur, R. Karri, and J. Rajendran, “Llm-assisted generation of hardware assertions,” _arXiv preprint arXiv:2306.14027_ , 2023.
  * [9] M. Cosler, C. Hahn, D. Mendoza, F. Schmitt, and C. Trippel, “nl2spec: Interactively translating unstructured natural language to temporal logics with large language models,” _arXiv preprint arXiv:2303.04864_ , 2023.
  * [10] M. Orenes-Vera, M. Martonosi, and D. Wentzlaff, “Using llms to facilitate formal verification of rtl,” _arXiv e-prints_ , pp. arXiv–2309, 2023.
  * [11] S. Yuan, J. Yang, S. Arya, C. Lipizzi, and Y. Wang, “From ambiguity to explicitness: Nlp-assisted 5g specification abstraction for formal analysis,” _arXiv preprint arXiv:2308.03277_ , 2023.
  * [12] J. Yang and Y. Wang, “A nextg hybrid testing platform for multi-step deep fuzzing and performance assessment from virtualization to over-the-air,” in _IEEE Cloudnet_ , 2023.
  * [13] R. Drechsler, M. Soeken, and R. Wille, “Formal specification level: Towards verification-driven design based on natural language processing,” in _Proceeding of the 2012 Forum on Specification and Design Languages_. IEEE, 2012, pp. 53–58.
  * [14] L. Banarescu, C. Bonial, S. Cai, M. Georgescu, K. Griffitt, U. Hermjakob, K. Knight, P. Koehn, M. Palmer, and N. Schneider, “Abstract meaning representation for sembanking,” in _Proceedings of the 7th linguistic annotation workshop and interoperability with discourse_ , 2013, pp. 178–186.
  * [15] L. Dong and M. Lapata, “Language to logical form with neural attention,” _arXiv preprint arXiv:1601.01280_ , 2016.
  * [16] S. Reddy, D. Chen, and C. D. Manning, “Coqa: A conversational question answering challenge,” _Transactions of the Association for Computational Linguistics_ , vol. 7, pp. 249–266, 2019.
  * [17] C. Hahn, F. Schmitt, J. J. Tillman, N. Metzger, J. Siber, and B. Finkbeiner, “Formal specifications from natural language,” _arXiv preprint arXiv:2206.01962_ , 2022.
  * [18] A. Saparov and H. He, “Language models are greedy reasoners: A systematic formal analysis of chain-of-thought,” _arXiv preprint arXiv:2210.01240_ , 2022.
  * [19] P. Srikumar, “Fast and wrong: The case for formally specifying hardware with llms,” in _Proceedings of the International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). ACM. ACM Press_ , 2023.
  * [20] N. Tihanyi, T. Bisztray, R. Jain, M. A. Ferrag, L. C. Cordeiro, and V. Mavroeidis, “The formai dataset: Generative ai in so ware security through the lens of formal verification,” _PROMISE’23_ , p. 33, 2023.
  * [21] Y. Charalambous, N. Tihanyi, R. Jain, Y. Sun, M. A. Ferrag, and L. C. Cordeiro, “A new era in software security: Towards self-healing software via large language models and formal verification,” _arXiv preprint arXiv:2305.14752_ , 2023.
  * [22] S. Abdelnabi, K. Greshake, S. Mishra, C. Endres, T. Holz, and M. Fritz, “Not what you’ve signed up for: Compromising real-world llm-integrated applications with indirect prompt injection,” in _Proceedings of the 16th ACM Workshop on Artificial Intelligence and Security_ , 2023, pp. 79–90.
  * [23] S. Ouyang, J. M. Zhang, M. Harman, and M. Wang, “Llm is like a box of chocolates: the non-determinism of chatgpt in code generation,” _arXiv preprint arXiv:2308.02828_ , 2023.
  * [24] K. Krishna, Y. Chang, J. Wieting, and M. Iyyer, “Rankgen: Improving text generation with large ranking models,” _arXiv preprint arXiv:2205.09726_ , 2022.
  * [25] L. Li and M. Thornton, _Digital system verification: A combined formal methods and simulation framework_. Springer Nature, 2022.
  * [26] Y. Wang, A. Gorski, and A. P. da Silva, “Development of a data-driven mobile 5g testbed: Platform for experimental research,” in _2021 IEEE International Mediterranean Conference on Communications and Networking (MeditCom)_. IEEE, 2021, pp. 324–329.
  * [27] J. Yang, S. Arya, and Y. Wang, “Formal-guided fuzz testing: Targeting security assurance from specification to implementation for 5g and beyond,” _arXiv preprint arXiv:2307.11247_ , 2023.
  * [28] J. Yang and Y. Wang, “Formal and fuzzing amplification: Targeting vulnerability detection in 5g and beyond,” _arXiv preprint arXiv:2307.05758_ , 2023.
  * [29] D. Dauphinais, M. Zylka, H. Spahic, F. Shaik, J. Yang, I. Cruz, J. Gibson, and Y. Wang, “Automated vulnerability testing and detection digital twin framework for 5g systems,” in _2023 IEEE 9th International Conference on Network Softwarization (NetSoft)_. IEEE, 2023, pp. 308–310.
  * [30] “3gpp ts 38.331: Radio resource control (rrc),” 3GPP, Report, 2022.
  * [31] A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, L. Kaiser, and I. Polosukhin, “Attention is all you need,” 2017. [Online]. Available: https://arxiv.org/pdf/1706.03762.pdf
  * [32] A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, Ł. Kaiser, and I. Polosukhin, “Attention is all you need,” _Advances in neural information processing systems_ , vol. 30, 2017.
  * [33] J. Devlin, M.-W. Chang, K. Lee, and K. Toutanova, “Bert: Pre-training of deep bidirectional transformers for language understanding,” _arXiv preprint arXiv:1810.04805_ , 2018.
  * [34] T. B. Brown, B. Mann, N. Ryder, M. Subbiah, J. Kaplan, P. Dhariwal, A. Neelakantan, P. Shyam, G. Sastry, A. Askell _et al._ , “Language models are few-shot learners,” _arXiv preprint arXiv:2005.14165_ , 2020.


revtex4-2Repair the float

# Assessing quantum dot SWAP gate fidelity using tensor network methods

Jacob R. Taylor  Nathan L. Foulk  Sankar Das Sarma  Condensed Matter Theory
Center and Joint Quantum Institute, Department of Physics, University of
Maryland, College Park, Maryland 20742-4111 USA

###### Abstract

Advanced tensor network numerical methods are used to explore the fidelity of
repeated SWAP operations on a system comprising 20 to 100 quantum dot spin
qubits in the presence of valley leakage and electrostatic crosstalk. The
fidelity of SWAP gates is largely unaffected by Zeeman splitting and valley
splitting, except when these parameters come into resonance. The fidelity
remains independent of the overall valley phase for valley eigenstates, while
for generic valley states, some minor corrections arise. We analyze the
fidelity scaling for long qubit chains without valley effects, where crosstalk
represents the only error source.

##  I Introduction

A standard operation in quantum computing is the SWAP gate, which allows for
the exchange (or “swapping”) of the quantum states between two qubits. The
SWAP gate has important applications in quantum computing, such as in quantum
error correction [1], measurement schemes [2], and quantum state engineering
[3]. The root $\sqrt{\text{SWAP}}$ is entangling and thus, in combination with
arbitrary single-qubit gates, allows for the implementation of general unitary
operations, sufficient for universal quantum computation [4]. This fact,
combined with the SWAP gate’s ubiquity within quantum error correction, makes
the creation of high fidelity SWAP gates essential for building a quantum
computer on any platform.

Si-based quantum dot spin qubits have emerged as a promising candidate for
realizing quantum computers due to their long coherence times [5, 6]. Both
28Si and 30Si are common spin-0 isotopes, and thus it is possible to remove
the decoherence arising from nuclear spin noise by isotopic purification [7].
In addition, electrical gate operations implemented directly from the
Heisenberg interaction between different qubits, such as SWAP gates, have
durations on the order of 1 ns [8]. These long coherence times arising from
such isotopic purification, combined with the available short gate operation
times, make Si especially well-suited for hosting qubits. Most importantly,
silicon-based qubits can be easily integrated into the existing semiconductor
industry, allowing for more straightforward scalability. A silicon-based
quantum computer platform could potentially host millions of qubits in a small
chip similar to existing CMOS-based integrated circuits, and there has been
spectacular recent progress in producing scalable multiqubit Si circuits, with
the largest devices—currently fabricated in commercial foundries—now at twelve
qubits [9, 10]. Based on this trajectory, it seems that devices of twenty or
more dots are in the not so distant future. It is therefore both timely and
important to consider SWAP gates in large spin qubit systems. Standard
theoretical and computational techniques, such as exact diagonalization,
cannot handle the simulation of large numbers of qubits since the Hilbert
space size grows exponentially with the number of qubits. The goal of the
current work is to introduce the powerful tensor network techniques to study
systems of many entangled spin qubits in order to establish the tensor network
method as a viable theoretical tool in the modeling of spin qubit arrays.

Tensor networks provide a framework for representing many-body quantum states
and operators in a computationally compact and efficient way, allowing for
accurate simulations of large quantum systems which are intractable with
direct methods [11]. Acting on matrix product states (MPS) with tensor network
time evolution methods such as TEBD [12] or TDVP [13] provides a technique to
accurately approximate the time evolution of interacting quantum systems and
can be used to investigate model-intrinsic sources of error. Systems of
hundreds of qubits that would be utterly intractable through direct simulation
can often be represented efficiently by restricting one’s system to an
approximate low-entanglement subspace using tensor networks. This is what we
do in the current work by studying spin qubit arrays up to 100 qubits using
the tensor network technique, establishing the feasibility of tensor networks
as an effective tool for spin qubit theories and analyses.

The valley degeneracy in Si introduces additional states to the qubit manifold
and possible avenues for leakage and relaxation [14, 15, 16, 6]. Here we seek
to expand previous work into the effects of valley states on spin qubit
devices by directly including the additional valley states within our
simulation and quantifying the effects of valley leakage. We also include the
effects of crosstalk in the theory as explained later in the text. Previous
work into the fidelity of sequences of SWAP gates on a spin qubit chain has
looked into the effects of charge noise and dissipation on the fidelity of
SWAP gates [17, 18]. Such work did not include dynamical valley states or
their interactions and was done only on small-scale systems due to
computational constraints in exact diagonalization. Our work can address tens
to hundreds of spin qubits in contrast to all earlier works on the subject by
using state-of-the-art methods within tensor networks to accurately model the
effect of the initial valley state and different experimentally relevant
parameters on the fidelity of a sequence of chained SWAP gates.

We first introduce our spin qubit model and describe the tensor network based
numerical methods used to perform the calculations. We then present the
results of those numerical calculations, demonstrating the effect of valley
splitting, Zeeman splitting, and SWAP exchange strength on the fidelity of
SWAP operations. Of particular interest are the effects of the spin-valley
coupling and its phase on different initial valley states. We conclude with an
investigation into the single gate fidelity scaling up to 100 spin qubits,
isolating the influence of crosstalk.

##  II Model

In exchange-coupled spin qubits [4], the spin states of individual electrons
serve as the computational basis. The basis states of our model are labeled by
the valley and spin degrees of freedom. The Hilbert space of each electron
includes the lowest two valley states $\lvert\pm\rangle$ of each dot,
corresponding to $k=\pm z$, along with, within each valley, the spin states
$\lvert\uparrow\rangle$ and $\lvert\downarrow\rangle$. It is reasonable to
focus on the spin-valley mixing and not consider orbital and valley effects
separately since the states $\lvert\pm\rangle$ are, in actuality, valley-orbit
states. This is because of large valley-orbit couplings in Si/SiGe quantum
dots which make the valley index in general not a good quantum number [15].
Nonetheless, the energy gap between the two lowest energy eigenstates is
always referred to as the “valley splitting”. Our work focuses on the effects
of spin-valley mixing specifically and the associated leakage.

Our model is a one-dimensional (1D) spin chain with both valley and spin
degree of freedom using the following Hamiltonian:

$H=\sum_{n=1}^{L-1}J_{n}\left(\boldsymbol{\sigma}_{n}\cdot\boldsymbol{\sigma}_{n+1}+1\right)\left(\boldsymbol{\tau}_{n}\cdot\boldsymbol{\tau}_{n+1}+1\right)+\\\
h\sum_{n}^{L}\sigma_{n}^{z}+\Delta\sum_{n}^{L}\tau_{n}^{z}+\\\
\frac{\gamma_{1}}{2}\sum_{n}^{L}\left(\tau_{n}^{x}\sigma_{n}^{x}+\tau_{n}^{y}\sigma_{n}^{y}\right)+\frac{\gamma_{2}}{2}\sum_{n}^{L}\left(\tau_{n}^{y}\sigma_{n}^{x}-\tau_{n}^{x}\sigma_{n}^{y}\right)$
(1)

where $L$ is the number of qubits in the spin chain, $h$ is the spin Zeeman
splitting, $\Delta$ is the valley splitting and $\gamma_{1}$,$\gamma_{2}$ are
the real and imaginary parts of the spin-valley coupling
$\gamma=\gamma_{1}+i\gamma_{2}$.
$\boldsymbol{\sigma}_{n}=(\sigma_{n}^{x},\sigma_{n}^{y},\sigma_{n}^{z})$ is
the $n^{\text{th}}$ site Pauli vector in the spin basis, while
$\boldsymbol{\tau}_{n}$ is the same but in the valley basis. The Hamiltonian
defined by Eq. 1 should be thought of as the minimal model for a spin qubit
array including spin-valley coupling, which is sufficient for our purpose of
establishing the power of the tensor network techniques in studying systems of
spin qubits. Experimental spin qubit systems are likely to have additional
nonessential complications, which would vary from sample to sample, which
cannot be captured in a universal theoretical description. These sample-
dependent complications must necessarily focus on specific samples, thus
losing the generality and the universality of the minimal theory which must be
developed first.

The role of the spin-valley coupling becomes clear in the matrix
representation of the single-site Hamiltonian,

$H_{n}=\begin{pmatrix}h+\Delta&0&0&0\\\ 0&h-\Delta&\gamma&0\\\
0&\gamma*&\Delta-h&0\\\ 0&0&0&-\Delta-h\end{pmatrix}.$ (2)

The valley splitting is material-specific and cannot be controlled. In the
case of zero magnetic field, the two lowest states are the $\lvert-s\rangle$,
where $s=\uparrow$ or $\downarrow$. As the magnetic field strength increases,
the electron forms a spin qubit two-level system, but this becomes entangled
by spin-valley mixing as $h\to\Delta$. But this spin-valley mixing is only
relevant between $\lvert-\uparrow\rangle$ and $\lvert+\downarrow\rangle$ since
the gap between these states shrinks as the magnetic field is increased. The
gap between the $\lvert-\downarrow\rangle$ and $\lvert+\uparrow\rangle$ is at
a minimum at zero magnetic field and only grows in the spin qubit regime
($h>0$). Therefore, the coupling between these states is negligible. The main
concern of this work is the effect of spin-valley leakage, which is the loss
of spin fidelity as a result of coherent evolution into a nearby valley state
of a different spin, as the spin and valley eigenstates get entangled by the
last two terms in Eq. 1. Therefore, the other couplings can be set to zero, as
transitions between different valley states of the same spin do not impact our
computational state, and intra-valley spin relaxation is beyond the scope of
this work (and is very weak in Si anyway).

The spin-valley coupling originates in both Rashba and Dresselhaus spin-orbit
coupling of the host material [19]. When the external magnetic field is
aligned in the [110] direction, the relevant spin-valley matrix element
simplifies [20] to

$\gamma=\frac{2m^{*}(\alpha_{R}+\alpha_{D})r^{-+}_{x}}{\hbar}\Delta,$ (3)

where $r^{-+}_{x}$ is the electric dipole matrix element between valley
states, $m^{*}$ is the effective electron mass, and $\alpha_{R}$ and
$\alpha_{D}$ are the Rashba and Dresselhaus spin-orbit interaction constants,
respectively. Reasonable estimates of these parameters for silicon quantum
dots lead to an order-of-magnitude estimate of $\frac{|\gamma|}{\Delta}\sim
1/500$. The precise number for this coupling is not important for our
considerations in this work, where the goal is to establish the efficacy of
the tensor network techniques.

The SWAP operation is performed using a $\frac{\pi}{4}$ pulse Heisenberg
interaction between the swapping sites. Ideally, the exchange coefficient
should be zero for non-swapping sites. In reality, this is never true [21, 22,
23, 24]. The exchange coefficient $J_{n}$ is set as follows:

$J_{n}=\left\\{\begin{array}[]{lr}J_{0},&\text{if }n\neq l\\\
J_{\text{SWAP}},&\text{if }n=l\end{array}\right\\},$ (4)

where the SWAP gate is between sites $l$ and $l+1$. For simplicity, $J_{0}$,
$\gamma$, $\Delta$ and $h$ are all taken to be site independent. These
nonessential assumptions are easy to relax in our method; they have little
impact on the simulation runtimes. Since these parameters would vary among
experimental samples, it makes little sense to include them as site-dependent
in our work although it is straightforward to do so at the cost of having a
large number of unknown qubit-dependent parameters in the theory.

The initial state is a product state between an initial spin state
$\lvert\psi_{i}\rangle_{s}$ and the valley state $\lvert\psi_{i}\rangle_{v}$
up to a normalization factor,

$\lvert\psi_{i}\rangle_{v}\propto(1-\alpha)\lvert-...-\rangle+\alpha\lvert-_{x}...-_{x}\rangle,$
(5)

where

$\lvert-_{x}\rangle=\frac{1}{\sqrt{2}}\left(\lvert+\rangle-\lvert-\rangle\right).$

When $\alpha>0$, this simply represents the deviation from the ideal case,
which is when each electron is initialized in the valley down state.

The total fidelity for our sequence of SWAP gates is defined as:

$F_{\text{tot}}=\text{Tr}_{s}\left[\text{Tr}_{v}[U\rho_{i}U^{\dagger}]\text{Tr}_{v}[R\rho_{i}R^{\dagger}]\right],$
(6)

where $R$ is an operator which performs the SWAP gate sequence with perfect
fidelity, $U$ represents the actual SWAP gate sequence with errors, and
$\rho_{i}=\lvert\psi_{i}\rangle\\!\langle\psi_{i}\rvert$ is the initial state
of the system. $\text{Tr}_{s}[...]$ and $\text{Tr}_{v}[...]$ are the partial
trace operators over spin and valley degrees of freedom, respectively. In our
case, the SWAP sequence transports a spin state from one side of the spin
chain to the other. The transport is performed by swapping sites
$1\leftrightarrow 2$, then $2\leftrightarrow 3$, and so forth until the first
spin state is transported to the end of the chain. The effective single gate
fidelity $F=(F_{tot})^{1/(L-1)}$ is used to be able to compare gate sequences
of different lengths.

Our absolute fidelities are not relevant from an experimental perspective. The
calculations here obviously cannot be used to predict fidelities of actual
physical devices, since those values will depend on a plethora of unknown
variables that are unique to each experimental setup, not to mention the many
error mechanisms that are not included in our simulations. The calculated
fidelities are only useful in a relative sense and can only give information
about the general model of interacting spin qubits, which is universal to all
spin qubit samples. If system dependent parameters are available, our
technique can easily be used to predict the behavior of individual samples.
For example, one can compare the infidelities of our model from spin-valley
mixing relative to the infidelities caused by residual exchange. But the exact
value of infidelity for a single calculation has limited experimental
application.

Since each physical spin qubit consists of spin and valley states, each can be
split into two separate two-level sites in the tensor network representation.
The two-level tensors are arranged in two rows, with the top row representing
the spin states and the bottom row representing the valley states. To
construct the tensor network Hilbert space, the sites are ordered such that
the $2j-1$ and $2j$ MPS sites map to the $j$th physical qubit’s spin and
valley states, respectively. The coupling between those sites $2j-1$ and $2j$
corresponds to the spin-valley coupling $\gamma$. The interweaving of the two
states is ideal because it minimizes the number of long-range interactions
necessary within the Hamiltonian, thus improving the efficiency of the MPS
algorithm.

Figure 1: Tensor network diagram for the MPS of the spin chain. The blue and
red sites represent the spin ($\lvert\psi_{s}\rangle$) and valley
($\lvert\psi_{v}\rangle$) degrees of freedom respectively. The tensors are
ordered so they snake between the spin and valley degrees of freedom to
minimize long-range interactions.

The system is initialized by constructing the spin state MPS and the valley
state MPS independently and then interspersing them with standard tensor
network operations to build a single total MPS for the entire system. In the
case of the random spin state MPS, an initial MPS of bond dimension $M=10$
with complex matrix elements is generated. The time evolution of the total MPS
is performed using Time Evolving Block Decimation (TEBD) [12] with SWAP gate
time $T=\frac{\pi/4}{J_{\text{SWAP}}}$. The state is mapped to a rotating
reference frame to correct for the background rotation caused by the external
magnetic fields. This simple mapping is achieved by applying a set of local
unitary operations to all sites $U_{r}=\Pi_{n=1}^{L}\exp(ih\sigma^{z}_{n}T)$
when computing the fidelity. The resulting MPS is then converted into a
projector matrix product operator (MPO), used in Eq. 6. For each of our
results using tensor network methods, the calculations were repeated for
smaller chain lengths ($L<15$), and independently confirmed using exact
diagonalization. There was no significant discrepancy between calculated
fidelities, both in a qualitative and quantitative sense. This gives us
confidence that our calculations for longer chain lengths are well-grounded in
reality and provides a clear success story for the use of tensor networks in
spin qubit systems.

##  III Calculations

As discussed before, our gate sequence consists of interleaved SWAP gates on a
Heisenberg-coupled spin chain. The sequence swaps the first and second spins,
then the second and third spins, iterating through the entire chain.

To assess the effects of different parameters on the fidelity of SWAP gates,
it is reasonable to first consider the impact of the SWAP gate exchange
coupling $J_{\text{SWAP}}$. The larger $J_{\text{SWAP}}$ is relative to the
residual exchange $J_{0}$, the larger the fidelities of the SWAP gate will be
since this would trivially make the SWAP gates faster. Our results, as
illustrated in Fig. 2, affirm this expectation. This observation is consistent
across different initial spin basis states, underscoring the robustness of the
relationship.

It is also apparent that the choice of initial spin state is crucial. Being
able to represent and manipulate entangled states is a critical quality of a
successful quantum computer, and in this case, our results suggest that
anything short of a product state leads to dramatically higher infidelities.
It is worth noting that the only sources of error present in this calculation
are crosstalk and spin-valley coupling. Crosstalk arises from the unintended
coupling among different spin qubits because of the electrostatic control used
in gate operations [25, 18]. Even increasing $J_{\text{SWAP}}$ to relatively
large values cannot compensate for the errors resulting from crosstalk and
valley degeneracy.

It is worth noting that in all results, the relevant parameters $\Delta$, $h$,
$J_{\text{SWAP}}$, $\gamma_{1}$ and $\gamma_{2}$ are in units of $J_{0}$, the
residual exchange. In a recent experiment, the residual exchange was measured
on the average to be about $J_{0}\approx 40$ kHz [24].

Figure 2: Single gate infidelity $(1-F)$ of a $L=50$ spin chain initialized
with $\lvert\uparrow_{x}\downarrow_{x}\downarrow_{x}...\downarrow_{x}\rangle$,
$\lvert\uparrow\downarrow\downarrow...\downarrow\rangle$ and a random spin
state for $\alpha=0$, $h=750$, $\Delta=500$, $\gamma_{1}=1$ and
$\gamma_{2}=0$.

We next consider the effects of the spin splitting $h$, valley splitting
$\Delta$, and spin-valley coupling $\gamma=\gamma_{1}+i\gamma_{2}$. In Fig. 3,
there is a significant impact on the fidelity of the SWAP sequence when the
spin and valley splittings come into resonance ($h\approx\Delta$). Large
values of $J_{\text{SWAP}}$ broaden the $h\approx\Delta$ resonance regime,
though they also suppress the infidelity peak in that regime. For example, in
Fig. 3(a), the error attributable to spin-valley coupling makes up about 40%
of the total error. However, for a larger value of $J_{\text{SWAP}}$ in Fig.
3(b), the spin-valley mixing makes up about 30% of the error.

The magnitude $|\gamma|=\sqrt{\gamma_{1}^{2}+\gamma_{2}^{2}}$ of the spin
valley coupling significantly impacts the fidelity of the SWAP gate. A larger
$\gamma$ is detrimental to the SWAP gates’ reliability due to local spin-
valley state mixing. This can be seen in Fig. 3, and our results suggest that
the magnitude of $\gamma$ dominates over its phase in the case of repeated
SWAP gates. This is a non-obvious finding of our calculations.

(a)

(b)

(c)

(d)

Figure 3: Single gate fidelity for variable $h$ and $\Delta$ for a $L=20$,
$\alpha=0$, random spin initial state with parameters $\gamma_{1}=\Delta/500$,
$\gamma_{2}=0$, (a) $J_{\text{SWAP}}=100$ and (b) $J_{\text{SWAP}}=250$. (c)
Single gate fidelity for variable $J_{\text{SWAP}}$ and $\Delta$ of a $L=20$,
random spin, $\alpha=0$ initial state. The other parameters used were $h=750$,
$\gamma_{1}=\Delta/500$, $\gamma_{2}=0$. The small deviation at
$h\approx\Delta$ can be seen when $\Delta$ and $h$ are in resonance. (d)
Single gate fidelity for variable $\gamma_{1}$ and $\gamma_{2}$ with $h=750$
and $\Delta=500$, and a $L=20$, $\alpha=0$, random initial spin state.

The implication that the valley phase is unimportant for spin qubit SWAPs is
surprising and important for experimental systems. To highlight this
phenomenon, the fidelities of the SWAPs are examined as a function of only the
spin valley coupling phase $\theta=\text{arg}(\gamma)$. The SWAP fidelity is
shown for six random initial spin states at $\alpha=0$ and $\alpha=1$ in Fig.
4. For the $\lvert-\ldots-\rangle$ initial valley state ($\alpha=0$), there is
absolutely no valley phase dependence on fidelity, and only $|\gamma|$ has any
effect. The irrelevance of the valley phase is confirmed numerically up to
machine precision. Analytically, if either of the spin or valley states is
initialized to a $z$ basis state, the effect of $\text{arg}(\gamma)$ reduces
to a global phase, which does not enter into the fidelity.

However, there is an obvious phase dependence when the valley state is
initially $\lvert-_{x}\ldots-_{x}\rangle$ ($\alpha=1$). Interestingly, each
state’s fidelity curve as a function of the valley phase varies in effect size
and shape. Each curve exhibits a wavelike shape, though each has its own
amplitude and period. Several curves are composed of several frequencies. It
is outside this paper’s scope to explain what causes this variance, focusing
instead on the fact that the infidelity amplitude is generally small and can
be set to exactly zero by careful valley state preparation.

(a)

(b)

Figure 4:  Single gate fidelity for six random $L=20$ initial spin states.
This was calculated for different phases of $\gamma=10e^{i\theta}$. The
initial states had (a) $\alpha=0$ (b) $\alpha=1$. In both cases $h=30$ and
$\Delta=100$.

The crossover between these two behaviors can be investigated by tuning
$\alpha$ from 0 to 1, which corresponds to tuning between
$\lvert-\ldots-\rangle$ to $\lvert-_{x}\ldots-_{x}\rangle$ (Eq. 5). The
results of this tuning are seen in Fig. 5. The crossover between these
behaviors is smooth, so that if a spin chain suffers from imperfect
initialization to a valley $z$ eigenstate, the resulting infidelity will be
commensurate with that valley initialization error.

(a)

(b)

Figure 5:  Average single gate fidelity of a spin SWAP gate across spin chains
of (a) $L=20$ and (b) $L=50$. For each plot, the valley $z$ state projection
$\alpha$ and valley phase $\arg(\gamma)$ are the variables of interest, and
the initial spin state is kept constant. Calculations were performed using
$|\gamma|=10$, $h=30$, $\Delta=100$ and $J_{\text{SWAP}}=250$.

The effects of electrostatic crosstalk can be isolated by setting $\gamma=0$.
Crosstalk among the qubits (arising from the electrostatic gate control)
represents a significant hurdle for qubit devices, since it is impossible to
eliminate crosstalk altogether. Residual exchange between unintended dots will
always be present, despite the great progress in fidelities made in recent
years [21, 22, 23]. This crosstalk can be calibrated out experimentally
through gate virtualization, but this process is done manually, and to do so
for each pair of neighboring dots becomes increasingly impractical as device
sizes grow. Therefore, understanding the errors that can arise from either
miscalibration or the lack of calibration altogether is a current research
need. In Fig. 6, the effects of crosstalk for a wide range of system sizes
($L=[5,100]$) with a uniform residual exchange $J_{0}$ are shown. In
actuality, this is a generous assumption, as the residual exchange is not
usually uniform, and a decreased barrier potential between the two dots for
SWAP also affects the exchange coupling between the next nearest neighboring
dots. Therefore, our calculated fidelities are likely an overestimate. Again,
if the quantitative details underlying crosstalk are available for specific
samples, our work can be easily adapted to study specific systems of spin
qubits.

It is apparent that single gate fidelities drop to critically low values even
for relatively large values of $J_{\text{SWAP}}$. This is because the residual
exchange $J_{0}$ crosstalk has more sites to entangle and more time overall to
do so. The compounded errors result in a significant amount of information
loss. Again, this is the best possible case for electrostatic crosstalk even
when valley effects are entirely ignored. Reducing the strength of residual
exchange relative to the energy scales of intended quantum operations is
likely necessary to perform any meaningful quantum circuits on systems larger
than ten quantum dots. This is another important finding of our work

Figure 6: Single gate infidelities ($1-F$) for chains of varying lengths with
different values of $J_{\text{SWAP}}\in[150,500]$. This simulation was run
using $h=750$, $\Delta=500$, $\alpha=0$, and $\gamma=0$, averaging over five
random initial spin states.

##  IV Conclusion

In conclusion, we investigate the effects of valley leakage on the fidelity of
SWAP gates in long quantum spin qubit systems (20-100 qubits). Using state-of-
the-art tensor network methods, the large-scale behavior of our model of a
spin qubit chain can be simulated, including both spin, valley, and their
coupling as well as crosstalk effects. We calculate how the fidelity of
repeated SWAP gates is directly affected by factors such as valley splitting,
spin-valley coupling, Zeeman splitting, and crosstalk.

Our findings are that the fidelity is only weakly affected by Zeeman splitting
and valley splitting except when brought into resonance. For $z$ basis valley
states (or spin states), there is no dependence on the phase of the spin-
valley coupling. When not in the valley $z$ basis due to initialization
errors, the effect on fidelity is state-dependent. These findings further
underscore the importance of reliable valley state initialization. However,
valley phase effects remain a minor correction relative to electrostatic
crosstalk. This is seen in the scaling of the SWAP fidelity as a function of
chain length due to the effects of crosstalk alone. Based on this scaling
behavior, electrostatic crosstalk alone seems a major problem for quantum
circuits consisting of more than ten spins, even in the best-case scenario of
uniform and constant residual exchange. Our establishing the tensor network
technique as an effective method for studying large spin qubit arrays should
have significant future impact on the fabrication and modeling of spin qubits
as they scale up to larger sizes.

##  V Acknowledgement

The authors thank Donovan Buterakos for helpful discussions and suggestions.
This work is supported by the Laboratory for Physical Sciences.

## References

  * Gottesman [1997] D. Gottesman,  _Stabilizer codes and quantum error correction_ (California Institute of Technology, 1997).
  * Barenco  _et al._ [1997] A. Barenco, A. Berthiaume, D. Deutsch, A. Ekert, R. Jozsa, and C. Macchiavello, SIAM Journal on Computing 26, 1541 (1997).
  * Nielsen and Chuang [2010] M. Nielsen and I. Chuang, Quantum computation and quantum information, 10th anniversary cambridge university press (2010).
  * Loss and DiVincenzo [1998] D. Loss and D. P. DiVincenzo, Physical Review A 57, 120 (1998).
  * Kobayashi  _et al._ [2021] T. Kobayashi, J. Salfi, C. Chua, J. van der Heijden, M. G. House, D. Culcer, W. D. Hutchison, B. C. Johnson, J. C. McCallum, H. Riemann, _et al._ , Nature Materials 20, 38 (2021).
  * Burkard  _et al._ [2023] G. Burkard, T. D. Ladd, A. Pan, J. M. Nichol, and J. R. Petta, Rev. Mod. Phys. 95, 025003 (2023).
  * Witzel  _et al._ [2010] W. M. Witzel, M. S. Carroll, A. Morello, L. Cywiński, and S. Das Sarma, Phys. Rev. Lett. 105, 187602 (2010).
  * Medford  _et al._ [2013] J. Medford, J. Beil, J. M. Taylor, E. I. Rashba, H. Lu, A. C. Gossard, and C. M. Marcus, Physical review letters 111, 050501 (2013).
  * Neyens  _et al._ [2023] S. Neyens, O. Zietz, T. Watson, F. Luthi, A. Nethwewala, H. George, E. Henry, A. Wagner, M. Islam, R. Pillarisetty, R. Kotlyar, K. Millard, S. Pellerano, N. Bishop, S. Bojarski, J. Roberts, and J. S. Clarke, arXiv:2307.04812 (2023), arXiv preprint.
  * [10] https://www.intel.com/content/www/us/en/research/quantum-computing.html, accessed: 2023-07-27.
  * Biamonte and Bergholm [2017] J. Biamonte and V. Bergholm, arXiv preprint arXiv:1708.00006 (2017).
  * Daley  _et al._ [2004] A. J. Daley, C. Kollath, U. Schollwöck, and G. Vidal, Journal of Statistical Mechanics: Theory and Experiment 2004, P04005 (2004).
  * Haegeman  _et al._ [2011] J. Haegeman, J. I. Cirac, T. J. Osborne, I. Pižorn, H. Verschelde, and F. Verstraete, Physical review letters 107, 070601 (2011).
  * Koiller  _et al._ [2001] B. Koiller, X. Hu, and S. Das Sarma, Phys. Rev. Lett. 88, 027903 (2001).
  * Friesen and Coppersmith [2010] M. Friesen and S. N. Coppersmith, Phys. Rev. B 81, 115324 (2010).
  * Zwanenburg  _et al._ [2013] F. A. Zwanenburg, A. S. Dzurak, A. Morello, M. Y. Simmons, L. C. L. Hollenberg, G. Klimeck, S. Rogge, S. N. Coppersmith, and M. A. Eriksson, Rev. Mod. Phys. 85, 961 (2013).
  * Foulk  _et al._ [2022] N. L. Foulk, R. E. Throckmorton, and S. Das Sarma, Physical Review B 105, 155411 (2022).
  * Throckmorton and Das Sarma [2020] R. E. Throckmorton and S. Das Sarma, Physical Review B 102, 035439 (2020).
  * Tahan and Joynt [2014] C. Tahan and R. Joynt, Phys. Rev. B 89, 075302 (2014).
  * Huang and Hu [2014] P. Huang and X. Hu, Physical Review B 90, 235315 (2014).
  * Mills  _et al._ [2022] A. R. Mills, C. R. Guinn, M. J. Gullans, A. J. Sigillito, M. M. Feldman, E. Nielsen, and J. R. Petta, Science Advances 8, eabn5130 (2022).
  * Noiri  _et al._ [2022] A. Noiri, K. Takeda, T. Nakajima, T. Kobayashi, A. Sammak, G. Scappucci, and S. Tarucha, Nature Communications 13, 5740 (2022).
  * Takeda  _et al._ [2022] K. Takeda, A. Noiri, T. Nakajima, T. Kobayashi, and S. Tarucha, Nature 608, 682 (2022).
  * Philips  _et al._ [2022] S. G. J. Philips, M. T. Mądzik, S. V. Amitonov, S. L. de Snoo, M. Russ, N. Kalhor, C. Volk, W. I. L. Lawrie, D. Brousse, L. Tryputen, B. P. Wuetz, A. Sammak, M. Veldhorst, G. Scappucci, and L. M. K. Vandersypen, Nature 609, 919 (2022).
  * Buterakos  _et al._ [2018] D. Buterakos, R. E. Throckmorton, and S. Das Sarma, Phys. Rev. B 97, 045431 (2018).