# Secure Aggregation for Federated Learning in Flower

Kwing Hei Li  University of CambridgeUK ,  Pedro Porto Buarque de Gusmão
University of CambridgeUK ,  Daniel J. Beutel  University of CambridgeUK and
Nicholas D. Lane  University of CambridgeUK

###### Abstract.

Federated Learning (FL) allows parties to learn a shared prediction model by
delegating the training computation to clients and aggregating all the
separately trained models on the server. To prevent private information being
inferred from local models, Secure Aggregation (SA) protocols are used to
ensure that the server is unable to inspect individual trained models as it
aggregates them. However, current implementations of SA in FL frameworks have
limitations, including vulnerability to client dropouts or configuration
difficulties.

In this paper, we present Salvia, an implementation of SA for Python users in
the Flower FL framework. Based on the SecAgg(+) protocols for a semi-honest
threat model, Salvia is robust against client dropouts and exposes a flexible
and easy-to-use API that is compatible with various machine learning
frameworks. We show that Salvia’s experimental performance is consistent with
SecAgg(+)’s theoretical computation and communication complexities.

Federated Learning, Secure Aggregation, Secure Multi-party Computation

††ccs: Security and privacy Distributed systems security††ccs: Computing
methodologies Machine learning approaches

##  1\. Introduction

Federated Learning (FL) (McMahan et al., 2017; Shokri and Shmatikov, 2015) is
a recent machine learning (ML) paradigm that allows a centralized _server_ to
compute a global model by aggregating local models trained by a set of
_clients_. Though not having direct access to users’ data, a malicious server
can still infer patterns of private data through inference attacks on clients’
local models (Shokri et al., 2017; Fredrikson et al., 2015; Abadi et al.,
2016).

Secure aggregation (SA) (Bonawitz et al., 2016), in general, refers to any
protocol that allows a group of mutually distrustful parties, each holding a
private value, to compute an aggregate value without revealing any information
about their private value to each other. This is especially relevant in the
context of FL as we would want the server to perform the aggregation step with
SA. That way, the server cannot access clients’ trained models and obtain
information about their private data.

Current implementations of SA in FL frameworks generally fall under one of two
main categories:

Trusted Execution Environment: The data-sensitive computation for aggregating
models is delegated to an isolated processing environment, which is supported
by trusted hardware running parallel to the operating system, e.g. the Intel
Software Guard Extensions (Intel Corporation, 2007). The server is only able
to inspect the final result of the computation, but not any intermediate
results or inputs to the computation performed in the isolated environment.

FL frameworks such as PySyft (Ryffel et al., 2018) and OpenFL (Reina et al.,
2021) provide support for this kind of SA, by using a lightweight library OS,
Graphene (che Tsai et al., 2017), to integrate its code with the secure
hardware. However, a ML engineer may find it difficult to configure the
program files to use the hardware; Configuration steps are long and
complicated, and there is a lack of documentation and examples for using these
trusted hardware to perform SA in FL. In addition, various attacks (Lipp et
al., 2018; Kocher et al., 2019) targeting supposedly-secure hardware have been
discovered in recent years.

Multi-party Computation:  Privacy of locally-trained models is achieved by
applying techniques from cryptography, e.g. Yao’s garbled circuits (Yao,
1982), homomorphic encryption (Damgård et al., 2011) or secret sharing (Boyle
et al., 2015). Instead of relying on trusted hardware, the server operates
directly on encrypted or masked models to calculate the aggregated result
without revealing individual clients’ contributions.

FL frameworks such as Crypten (Knott et al., 2020) provide support for this
kind of SA. Though these SA methods can be designed to expose an easy-to-use
API to engineers, most implementations of multi-party computation SA protocols
cannot work around dropouts, a phenomenon all too common with cross-device FL.
On top of that, these protocols often incur significant computation and
communication overhead, making them infeasible in larger FL experiments.

In summary, most implementations or proposed solutions for SA in common FL
frameworks have one or more of the following limitations that hinder their
usability:

  * •

Not trivial to configure and use. This is the case for most frameworks,
especially those that rely on trusted execution environments for SA, like
PySyft and OpenFL.

  * •

Dependent on certain trusted hardware and prone to existing or future attacks
on it. This is the case for all frameworks that use trusted hardware for SA,
like PySyft and OpenFL.

  * •

Inability to tolerate client dropouts. This is the case for most frameworks
that utilize multi-party computation protocols for SA, like Crypten.

  * •

Computation and communication overhead too significant to be used in larger FL
settings. This is the case for many proposed multi-party computation
protocols, where the protocol itself is computationally expensive (Rastogi and
Nath, 2010).

In this paper, we present Salvia (Li, 2021), an implementation of SA in the
open-source FL framework Flower that aims to address each of the above
limitations by:

  * •

Exposing a flexible and easily-configurable API that works with Flower’s
existing Strategy abstraction.

  * •

Utilizing a multi-party computation protocol that does not require trusted
hardware.

  * •

Tolerating various percentages of client dropouts while providing strong
security guarantees.

  * •

Using a SA algorithm that has low theoretical computation and communication
complexities.

We explain Salvia’s system design and implementation details in section 2 and
section 3, respectively. We also present experiments that explore the
algorithmic aspects of Salvia’s computation and communication costs in section
4. Lastly, we discuss Salvia’s current limitations and directions for future
work in section 5.

##  2\. System Design

We present Salvia’s design goals that address limitations of other SA
implementations, and summarize the assumptions made for our implementation. We
also present Flower and SecAgg(+), which are the chosen underlying framework
and SA protocol for Salvia’s design, respectively.

###  2.1. Design Goals

Many frameworks provide support for SA, though there are weaknesses in their
designs that hinder engineers from using them. Based on these observations, we
present five main design goals for implementing Salvia:

1) Usability: Given the difficulty in using SA for some FL frameworks, Salvia
should be intuitive and easy to use.

2) Flexibility: Given the complexity of FL systems, Salvia should provide a
flexible API for users to configure parameters of the protocol to fit their
experiment/deployment goals.

3) Compatibility: Given the robust and diverse range of existing ML
frameworks, Salvia should be compatible with the most commonly-used ones.

4) Reliability: Given that dropouts of mobile devices in FL is common, Salvia
should be robust against such behaviour.

5) Efficiency: Given that real-world FL is often used on large systems, Salvia
should not incur significant communication and computation overhead to the FL
training.

###  2.2. Assumptions

We present the assumptions made for our implementation:

Semi-honest threat model: Parties cannot deviate from the protocol
specification. However, corrupted parties may cooperate outside the protocol
to exchange information, e.g. secret shares.

Liveness properties on the response time of clients: After sending a request
to a client, the server eventually receives a response or detects a
disconnection from the client.

Secure links between clients and server: Links are encrypted and authenticated
in advance.

###  2.3. Framework Selection – Flower

Flower (Figure 1) (Beutel et al., 2020) is a recent FL framework that provides
higher-level abstractions enabling researchers to extend and implement FL
ideas on a reliable stack. It is one of the very few frameworks that can
support heterogeneous clients running on different ML frameworks (including
TensorFlow (Abadi et al., 2015) and PyTorch (Paszke et al., 2019)) and using
different programming languages. Choosing Flower as Salvia’s underlying FL
framework allows Salvia to be compatible with many existing ML frameworks;
Each client can freely choose which ML framework to use for their local
training pipelines independently. Flower also has a large suite of built-in
Strategies representing state-of-the-art FL algorithms for users to freely
extend, modify, and use for their experiments. We also note that Flower did
not have any support for SA in the past, which is a significant limitation in
terms of privacy promises associated with FL.

Figure 1. Flower’s Basic Architecture (without Salvia)

###  2.4. Protocol Selection – SecAgg(+)

We chose the SecAgg (Segal et al., 2017) and SecAgg+ (Bell et al., 2020)
protocols for semi-honest scenarios (parties cannot deviate from the protocol)
as the base algorithm of Salvia. These multi-party computation protocols rely
on cryptographic primitives to generate private masks for encrypting locally-
trained models seen as a single vector of integer weights. These masks cancel
each other out when the encrypted vectors are aggregated.

We use $n$ and $l$ to denote the number of clients participating in the
protocol and the model size, respectively. We use $k$ to denote the number of
other clients each client communicates with (including itself) in the
protocol, using the server as a relay.

Like SecAgg and SecAgg+, there are five stages in Salvia:

Stage 0 – Setup Parameters: The server sends values of the protocol’s
parameters to each client.

Stage 1 – Ask Keys: Each client generates private-public keys and shares the
public keys via the server.

Stage 2 – Share Keys: Each client generates secret shares of its private key
and a randomly generated seed, and shares it with its $k$ neighbors via the
server.

Stage 3 – Ask Vectors: Each client creates masks for its model vector,
generated with its private key and randomly generated seed. It then sends the
masked vector to the server.

Stage 4 – Unmask Vectors: The server asks clients to contribute secret shares
they have received in the Share Keys Stage to remove the masks of the
aggregated masked vector.

The main difference between SecAgg and SecAgg+ lies in the value of $k$. For
the former, the value of $k$ is the same as $n$. As a result, all clients
consider each other to be close neighbors, and secret shares are generated for
all other clients. For the latter, $k$ is any value smaller than $n$ (usually
$O(\log n)$). Each client thus produces shares for its closest $k$ neighbors
(including itself), thus producing a $(k-1)$-connected communication graph. As
both protocols differ mainly by their $k$ value 111We acknowledge the fact
that there exists an optimization that only works for SecAgg, but not SecAgg+
in the Unmask Vectors Stage. However, since both protocols have many features
in common, we consider SecAgg+ as a generalized version of SecAgg. and that
their underlying algorithms work similarly, we use SecAgg(+) to represent both
protocols.

The computation and communication overhead complexities of Salvia are
summarized in Table 1.

Table 1. SecAgg(+)’s Overhead | Computation | Communication
---|---|---
Server | $O(nk(k+l))$ | $O(n(k+l))$
Client | $O(k(k+l))$ | $O(k+l)$

We chose these two protocols as the base algorithm of Salvia for the following
reasons:

Flexible API:  SecAgg(+) lends itself easily to provide a variety of
parameters to be configured, allowing us to design a set of APIs that is
flexible to the user’s needs. Depending on the parameters used, the protocols
can tolerate various percentages of corrupt users and dropouts, and is
suitable for a wide range of FL scenarios of various complexities. This
enables us to specifically address both our Flexibility and Reliability design
goals.

Simple Configuration:  The execution of these protocols for both the server
and clients do not rely on any special hardware support. This allows much of
the logic to be directly implemented into a FL framework, decreasing the
amount of configuration work a user has to set up to use Salvia. This enables
us to specifically address our Usability design goal.

Low Overhead:  SecAgg’s communication and computation overhead is lower than
other traditional multi-party computation SA protocols. This overhead is even
more significantly lowered when SecAgg+ is used, allowing a smaller value of
$k$ to be used without sacrificing significant security guarantees. For
example, the server’s communication and computation complexities are linear to
$n$. Furthermore, the client’s communication and computation complexities do
not increase with $n$. This enables us to specifically address our Efficiency
design goal.

Clear Specifications:  SecAgg(+) served as the inspiration for many other SA
multi-party computation algorithms, e.g. CCESA (Choi et al., 2020), TurboAgg
(So et al., 2020) and FastSecAgg (Kadhe et al., 2020). We are also not aware
of other common FL frameworks that provide SA via the SecAgg(+) protocols.
Implementing SecAgg(+) in a FL framework could provide valuable insights on
the implementations of other similar protocols.

##  3\. Implementation

We now describe details of implementing Salvia within Flower.

###  3.1. Salvia’s Architecture

Salvia’s architecture consists of three major components: Salvia-compatible
Strategies, the server-side logic (Figure 2), and the client-side logic
(Figure 3).

To use Salvia, the user must provide a Salvia-compatible Strategy that
provides the configuration parameters of the protocol when starting the
server, see subsection 3.3 and subsection 3.4 for details.

Salvia’s server-side logic provides functions that are called by the FL Loop,
the heart of Flower’s core architecture (Figure 1). In a normal FL round, the
loop asks the Strategy to produce configuration parameters, sends those
parameters to the clients via the RPC server and client, receives the trained
clients’ model vectors and delegates the result aggregation to the Strategy.
If the user chooses to use SA in their FL training stage, a special
sec_agg_fit function is executed in the Loop, which first asks the Strategy to
provide parameters that customize core aspects of the SA algorithm. Unlike a
normal FL, the aggregation computation is performed within the Loop instead of
being delegated to the Strategy. Though this limits the flexibility of the
aggregation step (subsection 3.3), this is necessary as the aggregation
computation involves complicated logic to remove the masks of the aggregated
model vector, and should not be exposed to the user directly.

Figure 2. Server-side Architecture with Salvia
The Salvia-compatible Strategy can be one of the standard Strategies provided
by Flower (grey), or one that is implemented by the user themselves (blue).

Salvia’s client-side logic is implemented in a wrapper class of the Flower
client. Depending on the header of the messages received, the client inspects
its contents, executes the corresponding SecAgg(+) function, and responds to
the server’s request for each stage of the SecAgg(+) protocol.

Figure 3. Client-side Architecture with Salvia

###  3.2. Cryptographic Primitives

A suite of functions providing cryptographic primitives are used in both the
server and client-side logic of Salvia. We opted not to directly provide our
own implementations of these cryptographic primitives at the current stage.
Instead, we make use of cryptography modules that are widely used in the
Python community to limit the risk of incorrect implementation of critical
cryptography functions. We discuss the cryptographic primitives used in
Salvia.

Private-Public Key Generation: This is used to create a common seed between
two clients for generating pairwise masks, and a mutual key shared between two
clients for authenticated encryption of secret shares. We used functions
provided by the Elliptic curve cryptography module in Cryptography (Authority,
2021) for this primitive.

Authenticated Encryption: To distribute secret shares during the Share Keys
stage, the message is encrypted by an authenticated encryption function to
guarantee confidentiality and integrity of the message. We used functions
provided by the Fernet module in Cryptography for this primitive.

$t$-out-of-$n$ Secret Sharing Scheme: Depending whether a client dropped out
after the Ask Vectors Stage, the server asks all clients for a secret share
they received, either from the original client’s first private key, or its
private seed. If at least $t$ out of $n$ shares are received by the server,
then the secret is reconstructed (Shamir, 1979). Otherwise, the shares cannot
give any extra information about the secret. We used the Shamir’s secret
sharing module from the PyCryptodome (Eijs, 2020) library for this primitive.

Random Number Generator: Each client produces a random number that acts as the
seed for generating its own private mask of its model vector. We used the
random function provided by the Python (Van Rossum and Drake Jr, 1995) os
library for this primitive.

Pseudo Random Number Generator: To ensure pairs of clients generate the same
pairwise masks, a pseudo-random number generator is required so that the same
mask is produced among clients when given identical seeds. We used the
standard random function in Python’s standard library for this primitive.

###  3.3. Federation Strategies

In Flower, users can experiment with state-of-the-art algorithms and modify
the behavior of their FL workload through the Strategy abstraction. A Strategy
customizes core aspects of the FL process, e.g. client sampling and training
parameters. Currently, Flower provides a comprehensive suite of FL Strategies,
representing the wide range of FL algorithms used by the FL community, e.g.
FedAvg (McMahan et al., 2017) and FedProx (Sahu et al., 2018). In addition,
users can extend or modify these built-in Strategies, or even implement their
own. We address our Usability and Compatibility design goals by allowing
Salvia to be compatible with this Strategy abstraction, i.e. users can choose
Strategies easily and flexibly to be used in conjunction with Salvia.

For a Strategy to be Salvia-compatible, the Strategy must also be a subclass
of the SecAggStrategy abstract base class. This means that the user needs to
provide a definition of get_sec_agg_param(), a function called by the FL Loop
at the beginning of the round to obtain a dictionary of SecAgg(+)-related
parameters, see subsection 3.4. After assigning default values for undefined
parameters, the FL Loop verifies that all parameters are valid for the
SecAgg(+) protocol and passes the dictionary to clients in the Setup
Parameters Stage. Since the FL Loop automatically fills in default values for
undefined parameters, the implementation of the get_sec_agg_param() could be
as simple as returning an empty dictionary.

Like a normal Strategy, a Salvia-compatible one provides arbitrary logic and
parameters to customize the client sampling and client’s model fitting
process. However, as mentioned in subsection 3.1, it cannot tune the weighted
aggregation process which occurs together with the Unmask Vectors Stage in the
FL Loop, see subsection 3.5.

###  3.4. API Parameters

To achieve our Flexibility goal, users can specify values of Salvia-related
parameters for configuring the SA protocol via the dictionary returned by the
get_sec_agg_param() function of their Strategy. These parameters are
categorized into these classes:

Minimum Number of Clients: To prevent the server from computing an aggregated
vector of too few people (an aggregated vector from a single client in the
extreme case), the user can specify the minimum number of clients required to
be available by the end of the protocol. If the number of available clients
drops below this limit, the server and clients refuse to continue the protocol
for security reasons.

The user can control this limit through one of two ways, by providing an exact
value of this limit with the parameter min_num, or by specifying a fraction
with respect to the number of clients sampled in min_frac. If both are
provided, the least restrictive of the two is used.

Secret Sharing: The generation and reconstruction functions of the secret
sharing cryptographic primitive is controlled by two parameters provided by
the user. share_num specifies the number of shares generated for each secret,
and threshold specifies the minimum number of shares required to reconstruct
the secret. Incidentally, share_num also represents the value of $k$, i.e. the
number of neighbors each client communicates with (including itself).
Therefore, if the value of share_num is identical to the number of clients
sampled, the protocol executed is SecAgg.

Quantization: For masks generated by cryptographic primitives to work
properly, client’s locally-trained model vector must be quantized beforehand.
This quantization step can be configured through the clipping_range and
target_range parameters. For each real value of the trained model vector,
clients first clip the value within the range $[-$clipping_range,
clipping_range$]$ and then map it to an integer between 0 and (target_range-1)
uniformly. Similarly, an inverse translation is performed on the server’s side
by converting each integer element of the quantized aggregated vector to the
float type, and mapping it to a real value in the range $[-$clipping_range,
clipping_range$]$ uniformly to produce the real-valued aggregated model
vector.

Though information is lost after quantization which might affect the accuracy
of the FL, this procedure is compulsory for the cryptographic primitives to
work properly. A user can decrease the amount of information lost from
quantization by providing a sufficiently large value of target_range.

Weighted Aggregation:  max_weights_factor denotes the maximum weight that
could be applied to a client’s model vector for weighted aggregation. The
mod_range parameter specifies the modulus of the aggregation computation, and
also the range of values elements in client’s vector masks can take, see
subsection 3.5.

###  3.5. Weighted Aggregation

Fundamentally, the SecAgg and SecAgg+ protocols only allow the server to
calculate an unweighted average of all received model vectors. However, we
often want to calculate a weighted average of all vectors, e.g. a client who
has trained on more data should have a larger influence on the final global
model than one who has trained with fewer. This is not trivial because the
server cannot perform arbitrary operations on clients’ masked vectors without
modifying the masks themselves.

We address this issue by applying the technique described in the appendix of
(Segal et al., 2017): Salvia’s client-side logic automatically multiplies the
client’s model vector by the amount of training data used, and appends that
factor to the front of the vector, producing a modified vector to be masked.
On the server’s side, at the end of the Unmask Vectors Stage, the server pops
the first element of the vector, representing the sum of all factors, and
divides the rest of the vector by that value to obtain a weighted average of
all input vectors.

The max_weights_factor prevents clients from multiplying their vector by too
large a factor that risks ‘overflowing’ the field and affecting the
aggregation result. If a client trains its model by an amount of data that
exceeds max_weights_factor, the vector is only multiplied by
max_weights_factor instead of the actual amount of data trained. In addition,
after all Salvia-related parameters are defined, the FL Loop checks that
mod_range is at least as large as $($max_weights_factor $\times$ target_range
$\times$ number of sampled clients $)$ so that it is impossible for the
aggregated vector to exceed the chosen modulus field.

An interesting side-effect of this design choice is that we can execute
unweighted aggregation by setting max_weights_factor to $1$, as each client
automatically multiplies their vector by the same factor of value $1$.

##  4\. Evaluation

$0$$100$$200$$300$$400$$500$$0$$200$$400$$600$$800$$1{,}000$Number of sampled
clientsCPU running time (s)0% dropout5% dropout (a) Running time of server
with increasing number of clients

$0$$100$$200$$300$$400$$500$$0$$20$$40$$60$$80$$100$Number of sampled
clientsCPU running time (s)0% dropout5% dropout (b) Running time of client
with increasing number of clients

$0$$100$$200$$300$$400$$500$$0$$5$$10$$15$$20$Number of sampled clientsData
transferred (MB)0% dropout5% dropout (c) Total data transfer per client with
increasing number of clients

$0$$1$$2$$3$$4$$5$$\cdot 10^{5}$$0$$50$$100$$150$$200$$250$$300$Model vector
sizeCPU running time (s)0% dropout5% dropout (d) Running time of server with
increasing vector size

$0$$1$$2$$3$$4$$5$$\cdot 10^{5}$$0$$50$$100$$150$$200$$250$$300$Model vector
sizeCPU running time (s)0% dropout5% dropout (e) Running time of client with
increasing vector size

$0$$1$$2$$3$$4$$5$$\cdot 10^{5}$$0$$5$$10$$15$$20$Model vector sizeData
transferred (MB)0% dropout5% dropout (f) Total data transfer per client with
increasing vector size

Figure 4. Experiment Results

To verify that Salvia’s behavior matches our expectations in theoretical
complexity, we evaluate the changes of Salvia’s computation and communication
overhead with the number of clients or the model vector size. We ran our FL
simulations on a Linux workstation with an Intel Xeon E-2136 CPU (3.30GHz),
with 256 GB of RAM. In our simulations, all entries of our local vectors were
of size 24 bits. We ignore communication latency in our simulations. Moreover,
all dropouts simulated happened after stage 2, i.e. Share Keys Stage. This is
because this would impose the most significant overhead as the server not only
needs to regenerate their secret, but also compute their pairwise masks
generated between their neighbors.

For our simulations, share_num and threshold were set to 51 and 26,
respectively. These parameters were chosen to reference SecAgg+’s proven
correctness and security guarantees, where we can tolerate up to $5\%$
dropouts and $5\%$ corrupted clients with correctness holding with probability
$1-2^{-20}$ and security holding with probability $1-2^{-40}$. Though not
shown in our following simulations, users can choose larger values for
share_num and threshold to tolerate higher percentages of dropouts and
corrupted clients.

We observe that all our experiment results are consistent with the theoretical
computation and communication overhead complexities for SecAgg(+) from Table
1, thus achieving our Efficiency design goal.

Varying the number of clients:  We measured the CPU running times of the
server and a client, and the total data transfer per client, as the number of
sampled clients increases. Fixing the model vector size to 100k entries, we
plotted the results measured through sampling 100 clients to sampling up to
500 clients in Figure 4(a), 4(b), and 4(c). We also measured how the
performance would change after client dropouts by repeating the experiments
with a $5\%$ dropouts.

We observe that the server’s running time increases linearly with the number
of sampled clients, which matches the expected computation cost’s complexity
as the server repeats the same operations for each available client, e.g.
reconstructing secrets and generating masks. The server’s running time
increases whenever there are $5\%$ clients dropping out, as the server has to
perform extra computations to calculate all $k$ pairwise masks for each client
dropped out in the Unmask Vectors Stage. On the other hand, the client’s
running time remains constant with the number of sampled clients regardless
whether there are dropouts. This is because each client only communicates with
$k$ other neighbors and the actual number of sampled clients does not affect
the client-side logic. Lastly, we note that the total data transferred per
client remains unchanged as each client is only communicating with exactly $k$
neighbors regardless of the total number of clients and dropouts.

Varying vector size:  We measured the CPU running times of the server and a
client, and the total data transfer per client, as the model vector size
increases. Fixing the number of sampled clients to 100, we plotted the results
measured through aggregating a vector of size 100k entries to aggregating one
of size 500k entries in Figure 4(d), 4(e), and 4(f). Like before, we repeated
our experiments with a $5\%$ dropouts.

We observe that both the server’s and clients’ running times increase linearly
with the model vector size. This matches both expected computation cost’s
complexities because all computation costs involving model vectors are linear
to the vectors’ sizes, e.g. generating masks and unmasking vectors. In
addition, like before, the server’s running time increases and the client’s
running time remains unchanged when there are $5\%$ clients dropping out. We
also observe that the total data transferred per client increases linearly
with the model vector size as expected, because each client sends the vector
to the server for aggregation.

##  5\. Limitations and Future Work

We recognize a few limitations of our current work and we point out future
work to address these issues.

At this moment, the secret sharing scheme function is one of the most
significant bottlenecks on Salvia’s computation cost. In the future, we wish
to provide our own implementation of the secret sharing mechanism that is more
efficient while not sacrificing security guarantees.

In addition, our support for SA on Flower is only limited to Python users. We
aim to rewrite cryptographic functions that are specific to the Python
library, such that it can be used in FL scenarios where clients are running
under different programming languages on their backends, e.g. C++.

Lastly, we would want to allow users to customize more aspects of their FL
experiments. For example, Salvia fixes clients’ weights factor to be the
amount of training data used. In addition, users cannot customize the
quantization step. We hope to extend our implementation to allow users to
provide arbitrary logic specifying how clients compute the weights factor and
how quantization is performed via the Salvia-compatible Strategy.

##  6\. Conclusion

We presented Salvia, an open-source implementation of SA based on the
SecAgg(+) protocols in the FL framework Flower. Leveraging Flower’s ML
framework-agnostic property, Salvia is compatible with a diverse range of ML
frameworks. We explained how Salvia’s API provides a set of flexible and
easily-configurable parameters and how it works together with Flower’s
Strategy abstraction. We showed that Salvia can handle client dropouts, and
its performance is consistent with SecAgg(+)’s theoretical computation and
communication complexities. Future work includes improving the efficiency of
the secret-sharing functions, extending Salvia for clients running in other
programming languages, and providing support for configuring the weights
factor via the Strategy abstraction.

###### Acknowledgements.

This work was supported by the UK’s Engineering and Physical Sciences Research
Council (EPSRC) with grant EP/S001530/1 (the MOA project) and the European
Research Council (ERC) via the REDIAL project (Grant Agreement ID: 805194). We
would also like to thank Prof. Mycroft and the anonymous reviewers for helpful
discussions and suggestions.

## References

  * (1)
  * Abadi et al. (2015) Martín Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenberg, Dandelion Mané, Rajat Monga, Sherry Moore, Derek Murray, Chris Olah, Mike Schuster, Jonathon Shlens, Benoit Steiner, Ilya Sutskever, Kunal Talwar, Paul Tucker, Vincent Vanhoucke, Vijay Vasudevan, Fernanda Viégas, Oriol Vinyals, Pete Warden, Martin Wattenberg, Martin Wicke, Yuan Yu, and Xiaoqiang Zheng. 2015\.  TensorFlow: Large-Scale Machine Learning on Heterogeneous Systems.  https://www.tensorflow.org/ Software available from tensorflow.org.
  * Abadi et al. (2016) Martin Abadi, Andy Chu, Ian Goodfellow, H. Brendan McMahan, Ilya Mironov, Kunal Talwar, and Li Zhang. 2016.  Deep Learning with Differential Privacy.  _Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security_ (Oct 2016).  https://doi.org/10.1145/2976749.2978318
  * Authority (2021) Python Cryptographic Authority. 2021\.  Cryptography (version 3.4.8).  https://github.com/pyca/cryptography
  * Bell et al. (2020) James Henry Bell, Kallista A. Bonawitz, Adrià Gascón, Tancrède Lepoint, and Mariana Raykova. 2020.  Secure Single-Server Aggregation with (Poly)Logarithmic Overhead. In _Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security_ (Virtual Event, USA) _(CCS ’20)_. Association for Computing Machinery, New York, NY, USA, 1253–1269.  https://doi.org/10.1145/3372297.3417885
  * Beutel et al. (2020) Daniel J. Beutel, Taner Topal, Akhil Mathur, Xinchi Qiu, Titouan Parcollet, and Nicholas D. Lane. 2020.  Flower: A Friendly Federated Learning Research Framework.  _CoRR_ abs/2007.14390 (2020).  arXiv:2007.14390 https://arxiv.org/abs/2007.14390
  * Bonawitz et al. (2016) Kallista A. Bonawitz, Vladimir Ivanov, Ben Kreuter, Antonio Marcedone, H. Brendan McMahan, Sarvar Patel, Daniel Ramage, Aaron Segal, and Karn Seth. 2016\.  Practical Secure Aggregation for Federated Learning on User-Held Data.  _CoRR_ abs/1611.04482 (2016).  arXiv:1611.04482 http://arxiv.org/abs/1611.04482
  * Boyle et al. (2015) Elette Boyle, Kai-Min Chung, and Rafael Pass. 2015\.  Large-Scale Secure Computation: Multi-party Computation for (Parallel) RAM Programs. In _CRYPTO_. Springer, 742–762.  https://doi.org/10.1007/978-3-662-48000-7_36
  * che Tsai et al. (2017) Chia che Tsai, Donald E. Porter, and Mona Vij. 2017.  Graphene-SGX: A Practical Library OS for Unmodified Applications on SGX. In _2017 USENIX Annual Technical Conference (USENIX ATC 17)_. USENIX Association, Santa Clara, CA, 645–658.  https://www.usenix.org/conference/atc17/technical-sessions/presentation/tsai
  * Choi et al. (2020) Beongjun Choi, Jy-yong Sohn, Dong-Jun Han, and Jaekyun Moon. 2020.  Communication-Computation Efficient Secure Aggregation for Federated Learning.  _CoRR_ abs/2012.05433 (2020).  arXiv:2012.05433 https://arxiv.org/abs/2012.05433
  * Damgård et al. (2011) Ivan Damgård, Valerio Pastro, Nigel Smart, and Sarah Zakarias. 2011.  Multiparty Computation from Somewhat Homomorphic Encryption.  _IACR Cryptology ePrint Archive_ 2011 (01 2011), 535\.  https://doi.org/10.1007/978-3-642-32009-5_38
  * Eijs (2020) Helder Eijs. 2020\.  PyCryptodome (version 3.9.9).  https://github.com/Legrandin/pycryptodome
  * Fredrikson et al. (2015) Matt Fredrikson, Somesh Jha, and Thomas Ristenpart. 2015\.  Model Inversion Attacks That Exploit Confidence Information and Basic Countermeasures. In _Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security_ (Denver, Colorado, USA) _(CCS ’15)_. Association for Computing Machinery, New York, NY, USA, 1322–1333.  https://doi.org/10.1145/2810103.2813677
  * Intel Corporation (2007) Intel Corporation 2007.  _Intel 64 and IA-32 Architectures Software Developer’s Manual - Volume 3B_.  Intel Corporation.
  * Kadhe et al. (2020) Swanand Kadhe, Nived Rajaraman, Onur Ozan Koyluoglu, and Kannan Ramchandran. 2020.  FastSecAgg: Scalable Secure Aggregation for Privacy-Preserving Federated Learning.  _CoRR_ abs/2009.11248 (2020).  arXiv:2009.11248 https://arxiv.org/abs/2009.11248
  * Knott et al. (2020) B. Knott, S. Venkataraman, A.Y. Hannun, S. Sengupta, M. Ibrahim, and L.J.P. van der Maaten. 2020\.  CrypTen: Secure Multi-Party Computation Meets Machine Learning. In _Proceedings of the NeurIPS Workshop on Privacy-Preserving Machine Learning_.
  * Kocher et al. (2019) Paul Kocher, Jann Horn, Anders Fogh, , Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2019\.  Spectre Attacks: Exploiting Speculative Execution. In _40th IEEE Symposium on Security and Privacy (S &P’19)_.
  * Li (2021) Kwing Hei Li. 2021\.  SecAgg Experimental.  https://github.com/hei411/flower/tree/secagg_experimental.
  * Lipp et al. (2018) Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. 2018\.  Meltdown: Reading Kernel Memory from User Space. In _27th USENIX Security Symposium (USENIX Security 18)_.
  * McMahan et al. (2017) Brendan McMahan, Eider Moore, Daniel Ramage, Seth Hampson, and Blaise Aguera y Arcas. 2017\.  Communication-Efficient Learning of Deep Networks from Decentralized Data. In _Proceedings of the 20th International Conference on Artificial Intelligence and Statistics_ _(Proceedings of Machine Learning Research, Vol. 54)_ , Aarti Singh and Jerry Zhu (Eds.). PMLR, 1273–1282.  https://proceedings.mlr.press/v54/mcmahan17a.html
  * Paszke et al. (2019) Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Köpf, Edward Yang, Zach DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. 2019.  PyTorch: An Imperative Style, High-Performance Deep Learning Library.  _CoRR_ abs/1912.01703 (2019).  arXiv:1912.01703 http://arxiv.org/abs/1912.01703
  * Rastogi and Nath (2010) Vibhor Rastogi and Suman Nath. 2010.  Differentially Private Aggregation of Distributed Time-Series with Transformation and Encryption. In _Proceedings of the 2010 ACM SIGMOD International Conference on Management of Data_ (Indianapolis, Indiana, USA) _(SIGMOD ’10)_. Association for Computing Machinery, New York, NY, USA, 735–746.  https://doi.org/10.1145/1807167.1807247
  * Reina et al. (2021) G Anthony Reina, Alexey Gruzdev, Patrick Foley, Olga Perepelkina, Mansi Sharma, Igor Davidyuk, Ilya Trushkin, Maksim Radionov, Aleksandr Mokrov, Dmitry Agapov, Jason Martin, Brandon Edwards, Micah J. Sheller, Sarthak Pati, Prakash Narayana Moorthy, Shih han Wang, Prashant Shah, and Spyridon Bakas. 2021\.  OpenFL: An open-source framework for Federated Learning.  arXiv:2105.06413 [cs.LG]
  * Ryffel et al. (2018) Theo Ryffel, Andrew Trask, Morten Dahl, Bobby Wagner, Jason Mancuso, Daniel Rueckert, and Jonathan Passerat-Palmbach. 2018\.  A generic framework for privacy preserving deep learning.  _CoRR_ abs/1811.04017 (2018).  arXiv:1811.04017 http://arxiv.org/abs/1811.04017
  * Sahu et al. (2018) Anit Kumar Sahu, Tian Li, Maziar Sanjabi, Manzil Zaheer, Ameet Talwalkar, and Virginia Smith. 2018\.  On the Convergence of Federated Optimization in Heterogeneous Networks.  _CoRR_ abs/1812.06127 (2018).  arXiv:1812.06127 http://arxiv.org/abs/1812.06127
  * Segal et al. (2017) Aaron Segal, Antonio Marcedone, Benjamin Kreuter, Daniel Ramage, H. Brendan McMahan, Karn Seth, K. A. Bonawitz, Sarvar Patel, and Vladimir Ivanov. 2017.  Practical Secure Aggregation for Privacy-Preserving Machine Learning. In _CCS_.  https://eprint.iacr.org/2017/281.pdf
  * Shamir (1979) Adi Shamir. 1979\.  How to Share a Secret.  _Commun. ACM_ 22, 11 (Nov. 1979), 612–613.  https://doi.org/10.1145/359168.359176
  * Shokri and Shmatikov (2015) Reza Shokri and Vitaly Shmatikov. 2015.  Privacy-preserving deep learning. In _2015 53rd Annual Allerton Conference on Communication, Control, and Computing (Allerton)_. 909–910.  https://doi.org/10.1109/ALLERTON.2015.7447103
  * Shokri et al. (2017) Reza Shokri, Marco Stronati, Congzheng Song, and Vitaly Shmatikov. 2017.  Membership Inference Attacks Against Machine Learning Models. In _2017 IEEE Symposium on Security and Privacy (SP)_. 3–18.  https://doi.org/10.1109/SP.2017.41
  * So et al. (2020) Jinhyun So, Basak Guler, and Amir Salman Avestimehr. 2020\.  Turbo-Aggregate: Breaking the Quadratic Aggregation Barrier in Secure Federated Learning.  _CoRR_ abs/2002.04156 (2020).  arXiv:2002.04156 https://arxiv.org/abs/2002.04156
  * Van Rossum and Drake Jr (1995) Guido Van Rossum and Fred L Drake Jr. 1995.  _Python reference manual_.  Centrum voor Wiskunde en Informatica Amsterdam.
  * Yao (1982) Andrew C. Yao. 1982\.  Protocols for secure computations. In _23rd Annual Symposium on Foundations of Computer Science (sfcs 1982)_. 160–164.  https://doi.org/10.1109/SFCS.1982.38


# Ruling Out Short Proofs of Unprovable Sentences is Hard

Hunter Monroe

###### Abstract

If no optimal propositional proof system exists, we (and independently Pudlák)
prove that ruling out length $t$ proofs of any unprovable sentence is hard.
This mapping from unprovable to hard-to-prove sentences powerfully translates
facts about noncomputability into complexity theory. For instance, because
proving string $x$ is Kolmogorov random ($x{\in}R$) is typically impossible,
it is typically hard to prove “no length $t$ proof shows $x{\in}R$”, or
tautologies encoding this. Therefore, a proof system with one family of hard
tautologies has these densely in an enumeration of families. The assumption
also implies that a natural language is NP-intermediate: with $R$ redefined to
have a sparse complement, the complement of the language $\\{\langle
x,1^{t}\rangle|$ no length $t$ proof exists of $x{\in}R\\}$ is also sparse.

Efficiently ruling out length $t$ proofs of $x{\in}R$ might violate the
constraint on using the fact of $x{\in}R$’s unprovability. We conjecture: any
computable predicate on $R$ that might be used in if-then statements (or case-
based proofs) does no better than branching at random, because $R$ appears
random by any effective test. This constraint could also inhibit the
usefulness in circuits and propositional proofs of NOT gates and
cancellation—needed to encode if-then statements. If $R$ defeats if-then
logic, exhaustive search is necessary.

##  1 Introduction

We prove a deep linkage between noncomputability and complexity under a widely
believed conjecture—that there is no optimal propositional proof system for
tautologies.111This paper was prepared in honor of past and present faculty of
Davidson College, including Hansford Epes, L. Richardson King, Benjamin Klein,
and Clark Ross. Comments are appreciated from Pavel Pudlák and Bill Gasarch.
The ideas in this paper and earlier versions have benefited from discussions
with the following: Scott Aaronson, Eric Allender, Olaf Beyersdorff, Ilario
Bonacina, Maria Luisa Bonet, Cristian Calude, Marco Carmosino, Yuval Filmus,
Vijay Ganesh, Bill Gasarch, Valentina Harizonov, Pavel Hrubeš, Rahul Ilango,
Russell Impagliazzo, Valentine Kabanets, Mehmet Kayaalp, Yanyi Liu, Ian Mertz,
Daniel Monroe, Igor Oliveira, Toniann Pitassi, Hanlin Ren, Rahul Santhanam,
Till Tantau, Neil Thapen, Luca Trevisan, Avi Wigderson, Ryan Williams, Marius
Zimand, and other participants in seminars at George Washington University and
Davidson College, the Simons Institute 2023 Meta-Complexity Program, the
Computational Complexity Conference 2022, the Workshop on Proof Complexity
2022, and the Conference on Complexity with a Human Face 2022. Remaining
errors are my own. That conjecture originated as an assertion that a
noncomputability result also holds with a resource bound. Gödel’s Second
Incompleteness Theorem states that no consistent sufficiently powerful theory
can prove its own consistency. Pudlák[19] and Friedman independently
formulated a feasible consistency conjecture: it is hard to rule out any
length $t$ proof in a theory of its own inconsistency.222See Pudlák[21]
Section 6.4 and [22]. Pudlák[19] shows the initial conjecture was incorrect—a
theory $\mathcal{T}$ can efficiently prove that $\mathcal{T}$ lacks a length
$t$ proof of ‘$0{=}1$’. The 1989 reformulation refers to the lack of efficient
proofs in a weaker theory. See also Theorem 59 of Pudlák[21]. Krajíček and
Pudlák[12] proved the lack of efficient proofs (in a weaker theory) of
inconsistency is equivalent to the nonexistence of an optimal proof system,
which remains a key conjecture in proof complexity theory.333See also
Krajíček[11] Section 21.3.

We show: if it is possible to efficiently rule out length $t$ proofs of some
unprovable sentence $\phi$, it is also possible to efficiently rule out a
slightly shorter proof of inconsistency, which could be used in a length $t$
proof of $\phi$ by contradiction. This implies a powerful generalization—if it
is hard to rule out length $t$ proofs of inconsistency, it is hard to rule of
length $t$ proofs of any unprovable sentence. This in turn implies that facts
about unprovability and noncomputability, which are well understood, can be
imported into complexity theory. This has wide ramifications—diverse types of
unprovable sentences translate into assertions that open questions in
complexity theory have the expected answers. For instance, unprovable
sentences of the form $x{\in}R$ are dense, so hard families of tautologies
encoding “no length $t$ proof shows $x{\in}R$” are also dense. With $R$
redefined to have a sparse complement—a string is in $R$ unless exponentially
compressible—the complement of the language $\\{\langle x,1^{t}\rangle|$ no
length $t$ proof exists of $x{\in}R\\}$ is neither in P nor NP-complete, but
is NP-intermediate.

The hardness of ruling out length $t$ proofs of any unprovable sentence
implies a deep linkage between noncomputability and complexity. We show that
the implicit mapping from unprovable sentences to families of hard-to-prove
sentences in a theory is an isomorphism. This would be a significant
previously unnoticed structural feature of theories such as ZFC.

Formalizing the intuition “ruling out length $t$ proofs is hard” requires
specifying which theory lacks length $t$ proofs and which theory has
difficulty ruling them out. These theories must be different, as a theory that
proves it lacks short proofs of some $\phi$ would prove its own consistency.
Our main result is:

###### Theorem 1.1

The following are equivalent:444Monroe[17] shows another equivalent condition:
For any $M$ accepting $\texttt{coBHP}=\\{\langle N,y,1^{t}\rangle|$ there is
no accepting path of nondeterministic TM (NTM) $N$ on input $y$ with $t$ or
fewer steps$\\}$, there exists some $\langle N^{\prime},y^{\prime}\rangle$
where $N^{\prime}$ does not halt on $y^{\prime}$ such that $\langle
N^{\prime},y^{\prime},1^{t}\rangle$ is a hard family of inputs.

(i) No optimal propositional proof system exists.

(ii) For consistent theory $\mathcal{S}$, for some stronger theory
$\mathcal{T}$, $\mathcal{S}$ cannot efficiently rule out length $t$ proofs in
$\mathcal{T}$ of $0{=}1$ (that is,
$\mathcal{S}\,{\centernot{\sststile{}{t^{\mathcal{O}(1)}}}}\mathcal{T}\,{\centernot{\sststile{}{t}}}`0{=}1$’).

(iii) For the $\mathcal{S}$ and $\mathcal{T}$ in (ii) and for any $\phi$
unprovable in $\mathcal{T}$, $\mathcal{S}$ cannot efficiently rule out length
$t$ proofs in $\mathcal{T}$ of $\phi$ (that is,
$\mathcal{T}\,{\centernot{\sststile{}{}}}\phi$ implies
$\mathcal{S}\,{\centernot{\sststile{}{t^{\mathcal{O}(1)}}}}\mathcal{T}\,{\centernot{\sststile{}{t}}}\phi$).555This
conjecture was formulated by the author and proved independently by Pudlák in
general and by the author for sentences $x{\in}R$.

Proof:  (i) and (ii) are equivalent by Krajíček and Pudlák[12].

(ii)$\rightarrow$(iii) Suppose (ii) holds. If $\mathcal{T}$ lacks a length $t$
proof of $\phi$, there can be no proof of $0{=}1$ slightly shorter than $t$,
as that would yield a length $t$ proof by contradiction of $\phi$. Therefore,
if $\mathcal{S}$ efficiently proves that $\mathcal{T}$ lacks a length $t$
proof of $\phi$, contrary to (iii), it also efficiently proves that there can
be no proof of $0{=}1$ slightly shorter than $t$. This contradicts (ii).
Therefore, (ii) implies (iii). If $\phi$ is provable in $\mathcal{T}$, it is
provable within some length $t$, so (iii) cannot hold, as $\mathcal{S}$ is
consistent and cannot show $\mathcal{T}$ lacks a proof of that length.

(iii)$\rightarrow$(i) Chen et al[4].

In the notation above in parentheses, write $\mathcal{T}\,{\sststile{}{}}\phi$
or $\mathcal{T}\,{\centernot{\sststile{}{}}}\phi$ respectively if
$\mathcal{T}$ does or does not have a proof of $\phi$ of any length
respectively. Write $\mathcal{T}\,{\sststile{}{t}}\phi$ if theory
$\mathcal{T}$ has a length $t$ (or shorter) proof of sentence $\phi$ and
$\mathcal{T}\,{\centernot{\sststile{}{t}}}\phi$ if not, where proof length is
the number of symbols in the binary string representing the proof.666See
Pudlák[20]’s survey on proof length. Likewise,
$\mathcal{T}\,{\centernot{\sststile{}{t^{\mathcal{O}(1)}}}}\phi$ signifies
that $\mathcal{T}$ does not have an efficient (polynomially bounded) proof of
$\phi$. $\mathcal{T}\,{\sststile{}{}}\phi$ and
$\mathcal{T}\,{{\sststile{}{\mathcal{O}(1)}}}\phi$ are equivalent; a provable
sentence has a finite proof and is therefore provable within a constant bound.

Below, we will show that the nonexistence of an optimal proof system implies
various complexity theory conjectures, by identifying some set of unprovable
sentences and invoking Theorem 1.1(iii). In many cases, we choose unprovable
sentences stating that a string $x$ is Kolmogorov random (written $x{\in}R$),
that is, $x$ is incompressible by half, with no short description in the form
of a program that prints $x$.777The definition in terms of incompressibility
by half is arbitrary, except for Theorem 5.1 which requires logarithmic
incompressibility. Chaitin’s Incompleteness Theorem states that proving
$x{\in}R$ is typically impossible in a theory with a computably enumerable
(c.e.) set of theorems. Otherwise, “the first length $n$ string that provably
has no short description” would itself be a short description of some string,
which is a contradiction. Here, $x{\in}R$ is an arithmetic sentence encoding
that a string $x$ (represented as a binary number) lacks a short description.
Because, $R$ is dense and noncomputable, the set of $x{\in}R$ provides a dense
nonconstructive pool of unprovable sentences.888For an overview of Kolmogorov
complexity, see Li and Vitanyi[14]. There is a rapidly growing recent
literature on meta-complexity; see Santhanam[25].

More formally, define the set of Kolmogorov random strings as
$R{=}\\{x|\forall p{:}$ if $|p|{\leq}|x|/2$, then $p{\nearrow}$ or
$p{\downarrow}$ with $U(p){\neq}x\\}$, with $U$ a deterministic universal TM
with no limit on its running time (not necessarily prefix free), $x$ and $p$
binary strings with $|x|$ denoting $x$’s length, $p{\downarrow}$ and
$p{\nearrow}$ signifying program $p$ does or does not halt, and ‘$x{\in}R$’ is
an arithmetic sentence encoding $x{\in}R$. Single and double quotes signify a
sentence, a sequence of symbols, encoding a mathematical statement.

If there is no optimal proof system, there are strong implications by Theorem
1.1:

  * •

Ruling out length $t$ proofs is hard on with positive density, because
unprovable sentences $x{\in}R$ have positive density. Equivalently, proving
tautologies encoding “there is no length $t$ proof of $x{\in}R$” is hard with
positive density. There is no optimal proof system for tautologies, with dense
set of hard P-uniform families witnessing the nonoptimality.

  * •

A natural language is NP-intermediate: the sparse complement of the language
“$x{\in}R$ lacks a length $t$ proof” (where $R$ is redefined, by requiring
logarithmic incompressibility, to have a sparse complement). This language is
not in P but has P/poly circuits.

  * •

The implicit mapping from unprovable to hard-to-prove sentences is an
isomorphism. However, it is incomplete—for instance, stronger conjectures are
required to imply that the polynomial hierarchy (PH) does not collapse—and
substantial work may be needed to identify conjectures related to other open
complexity questions and the associated isomorphisms.

The paper is organized as follows. Section 2 provides preliminaries. Section 3
shows that unprovable sentences ‘$x{\in}R$’ are dense among length $n$
sentences. Section 4 discusses implications for tautologies and proof systems.
Section 5 shows that a natural language is NP-intermediate. Section 6 shows
that the mapping from unprovable to hard-to-prove sentences is an isomorphism
and discusses open questions. Section 7 concludes.

##  2 Preliminaries

_Strings_ : With a binary alphabet $\\{0,1\\}$, let $S^{n}$ be the set of
length $n$ strings, which are ordered $n$-tuples. Let $|x|$ be the length of a
string and $|S|$ be the cardinality of set $S$. A language $L$ is a subset of
$\cup_{n\geq 0}S^{n}$.

_Density_ : Say the share of length $n$ strings in $L$ is bounded above zero
if there exists $c>0$ such that $|L\cap S^{n}|/n\geq c$ for sufficiently large
$n$. This implies the weaker condition that $L$ has positive upper density,
i.e., that
$\displaystyle\limsup_{n\rightarrow\infty}\frac{|L\cap\\{1,2,\ldots,n\\}|}{n}>0$.
If an event depending on $n$ occurs with probability that tends to one as $n$
tends to infinity, such as $x{\in}R$ where $|x|{=}n$, say that it occurs with
high probability (w.h.p.).

_Theories_ : Theories are assumed to be the Peano arithmetic (PA) or an
extension of PA.999The conjecture could coherently refer to a weaker theory
such as Robinson’s Q without induction or unbounded quantifiers, which can
still prove ‘$p{\downarrow}$’ if in fact $p{\downarrow}$, by verifying the
transcript of a halting computation. To allow for average-case analysis, the
standard definition of PA is modified so binary strings are encoded in
arithmetic sentences as natural numbers, in binary not unary, adding a leading
“1” to avoid losing leading zeros.

_Proof Systems_ : A propositional proof system is a polynomial time function
$h\in\textbf{FP}$ with range TAUT (Cook and Reckhow[6]). For tautology $\tau$,
any string $w$ such that $h(w)=\tau$ is a proof of $\tau$. The proof system
$h$ is _optimal_ if there exists $c\geq 1$ such that the length of minimal $f$
proofs of $x$ are polynomially bounded in $|x|$ with exponent $c$ by minimal
$h$ proofs (Krajíček and Pudlák[12]). A proof system is not optimal if and
only if there is a P-uniform family of tautologies for which it requires
superpolynomial proof length.

##  3 Density of Unprovable Sentences

Calude and Jürgensen[3] show that the share of length $n$ arithmetic sentences
that are true and unprovable is bounded above zero. The result relies on two
facts: ‘$x{\in}R$’ is typically unprovable, and length $n$ strings are in $R$
w.h.p.101010See the proof of Theorem 5.2 in [3]. With that context, Theorem
1.1 implies that a similar result holds for $\texttt{coTHEOREMS}_{\leq t}{=}$
$\\{\langle\phi,1^{t}\rangle|\mathcal{T}\,{\centernot{\sststile{}{t}}}\phi\\}$.

Chaitin’s Incompleteness Theorem states:

###### Theorem 3.1

For every consistent, arithmetically sound theory $\mathcal{T}$ with a c.e.
set of theorems, $\exists k\forall x{:}|x|{>}k$,
$\mathcal{T}\,{\centernot{\sststile{}{}}}`x{\in}R$’.

Proof:  Otherwise, a string $x$ could be concisely described as “the first
string $x$ of length $n$ such that $\mathcal{T}$ proves ‘$x{\in}R$”’, contrary
to the definition of $R$. A TM with input $n$ in binary (of length $\log n$)
could enumerate the theorems of $\mathcal{T}$, printing the first string $x$
such that $\mathcal{T}$ proves ‘$x{\in}R$’. Then, $k$ is determined by the
length of the description of this TM, which would need to be doubled as $R$
consists of strings not compressible by half. See Li and Vitanyi[14] Corollary
2.7.2 for a formal treatment.

###### Lemma 3.2

$x{\in}R$ w.h.p.

Proof:  By a counting argument, the number of possible short descriptions is
small. The number of length $n$ strings is $2^{n}$. The number of programs $p$
with $|p|{\leq}n/2$ is $2^{n/2+1}-1$, which is an upper bound on the number of
length $n$ strings not in $R$. Therefore, $R$’s share of length $n$ strings is
at least $1-2^{-n/2}$, so $x{\in}R$ w.h.p.

Calude and Jürgensen’s result implies:

###### Theorem 3.3

For every theory $\mathcal{T}$, the share of sentences $\\{`x{\in}R$’$\,|$
$x{\in}R$ and $\mathcal{T}\,{\centernot{\sststile{}{}}}`x{\in}R$’$\\}$ in
length $n$ arithmetic sentences is bounded above zero, for $n$ sufficiently
large. In an enumeration of sentences, for instance in lexicographic order,
unprovable sentences have positive upper density.

Proof:  Theory $\mathcal{T}$ cannot typically prove sentences ‘$x{\in}R$’
where $x{\in}R$, by Theorem 3.1. The sentences ‘$x{\in}R$’ satisfy
$|`x{\in}R$’$|=|x|+c$, where $c$ is a constant not depending on $|x|$, giving
the overhead of encoding ‘$x{\in}R$’ net of $|x|$. The share of length $n$
sentences of form ‘$x{\in}R$’ is exactly $2^{-c}$ and these satisfy $x{\in}R$
w.h.p. Therefore, for $\epsilon{>}0$, this share is bounded below by
$2^{-c}{-}\epsilon$ for $n$ sufficiently large. Therefore, in an enumeration
of sentences, unprovable sentences have positive upper density.

The fact that a sentence ‘$x{\in}R$’ needs only a constant $c$ bits of
overhead, net of $|x|$, to encode $x{\in}R$ is needed in the next section.

##  4 Tautologies and Proof Systems

A tautology can encode the sentence
$\mathcal{T}{\centernot{\sststile{}{t}}}`x{\in}R$’ as follows. For a given
$x$, $\mathcal{T}{\centernot{\sststile{}{t}}}`x{\in}R$’ is equivalent to
$\langle`x{\in}R$’$,1^{t}\rangle{\in}\texttt{coTHEOREMS}_{\leq t}$.
$\texttt{coTHEOREMS}_{\leq t}$ and TAUT are both coNP-complete languages, so
some polynomial-time reduction $r$ from $\texttt{coTHEOREMS}_{\leq t}$ to TAUT
maps $\langle\phi,1^{t}\rangle$ to tautology $r(\langle\phi,1^{t}\rangle)$.

Tautologies produced by the reduction $r$ confirm that every possible proof of
$\mathcal{T}{\centernot{\sststile{}{t}}}`x{\in}R$’ is not a valid proof. The
reduction $r$ translates a family of sentences stating that no length $t$
proof exists to a family of tautologies. It should not be confused with
propositional translations, which translate sentences with a single universal
bounded quantifier that are easy to prove in a weak fragment of arithmetic
into easy-to-prove tautologies.111111See Krajíček[11] and Cook and Nguyen[5].

With this encoding, two implications immediately follow: families of
tautologies that are hard to prove have positive upper density in an
enumeration of families, and there are dense witnesses to the nonoptimality of
proof systems.

###  4.1 Proving Tautologies is Hard with Positive Density

$R$’s density immediately implies families of tautologies hard to prove have
positive upper density in an enumeration of such families. Consider an
enumeration of families of Boolean formulas encoding “no length $t$ proof of
$\phi$ exists”, with each family for $\phi$ indexed by $t$, with families
enumerated in lexicographic order by $\phi$. Some formulas will not be
tautologies, when $\phi$ is provable within length $t$. In this enumeration,
families with $\phi$ of the form ‘$x{\in}R$’ where $x{\in}R$ have positive
upper density, and these families are typically hard-to-prove tautologies.

This definition does not necessarily imply that length $n$ elements of TAUT
are average-case hard to accept. For instance, an algorithm allowed to make
errors with small probability can accept for any $\phi$ of the form
‘$x{\in}R$’ and be correct w.h.p. An error-free probabilistic polynomial time
algorithm would necessarily fail with non-zero probability.

###  4.2 Dense Witnesses to Nonoptimality

If there is no optimal proof system, then for any proof system $P$, there is a
dense set of hard families of tautologies $r(\langle`x{\in}R$’$,1^{t}\rangle)$
letting $x$ range over all $x{\in}R$. A probabilistic, polynomial-time
computable procedure to produce such a family w.h.p. is to choose a
sufficiently long random string $x$. Then, $x{\in}R$ w.h.p. by Lemma 3.2, so
tautologies $r(\langle`x{\in}R$’$,1^{t}\rangle)$ are hard for $P$ w.h.p.
Tautologies that are hard for ZFC to prove are also hard for any other known
proof system, as their soundness is proved by ZFC. “Sufficiently long” is the
same as $k$ in Chaitin’s theorem, based on the length of the description of a
TM that enumerates the theorems of a theory.

##  5 From Turing Intermediate to NP Intermediate

The set $R$ is Turing intermediate—it is not computable, and its complement is
c.e. but not complete under many-one computable reductions (Rogers[10] Theorem
8.I(a) and (c)). This raises the question whether Theorem 1.1 implies that
some related language is NP-intermediate—that is, in NP, not in P, and not NP-
complete under polynomial time many-one reductions. The final paragraph
provides context on NP-intermediate languages.

We show that deciding the language “has no proof of ‘$x{\in}R$’ within length
$t$” is NP-intermediate relaxing $R$’s definition to make its complement
sparse. This relaxed definition counts strings as random unless they can be
compressed exponentially, not just by half. This makes the set of possible
short descriptions sparse, growing polynomially in $|x|$, so the the set of
non-random strings is also sparse. Define this sparse version of $R$ as
$R^{sp}{=}\\{x|\forall p{:}$ if $|p|{\leq}\log|x|$, then $p{\nearrow}$ or
$p{\downarrow}$ with $U(p){\neq}x\\}$. $R^{sp}$, like $R$, is noncomputable.
Chaitin’s Theorem still holds, but the parameter $k$ is exponentially larger.
Fix $\mathcal{S}$ and $\mathcal{T}$ per Theorem 1.1.
$\mathcal{T}{\centernot{\sststile{}{t}}}`x{\in}R^{sp}$’ iff
$\langle`x{\in}R^{sp}$’$,1^{t}\rangle{\in}\texttt{coTHEOREMS}_{\leq t}$, by
definition. Let
$R^{sp}_{t}{=}\\{\langle`x{\in}R^{sp}$’$,1^{t}\rangle|$$\mathcal{T}{\centernot{\sststile{}{t}}}`x{\in}R^{sp}$’$\\}$,
so $R^{sp}_{t}{\in}\texttt{coTHEOREMS}_{\leq t}$. Define
$\overline{R^{sp}_{t}}{=}\\{\langle`x{\in}R^{sp}$’$,1^{t}\rangle|\neg$$\mathcal{T}{\centernot{\sststile{}{t}}}`x{\in}R^{sp}$’$\\}$.
Based on $x$, $\overline{R^{sp}_{t}}$ can be divided into $x{\notin}R^{sp}$
where $\langle`x{\in}R^{sp}$’$,1^{t}\rangle{\in}\overline{R^{sp}_{t}}$ for all
$t$, and $x{\in}R^{sp}$ where
$\langle`x{\in}R^{sp}$’$,1^{t}\rangle{\in}\overline{R^{sp}_{t}}$ for
sufficiently large $t$. Then:

###### Theorem 5.1

If there is no optimal proof system, then: (i) $\overline{R^{sp}_{t}}$ is NP-
intermediate; and (ii) $\overline{R^{sp}_{t}}$ and therefore $R^{sp}_{t}$ have
minimal circuits in P/poly which are not P-uniform.

Proof:  (i) $R^{sp}{\notin}\textbf{P}$ by assumption and Theorem 1.1.
$\overline{R^{sp}_{t}}$ is sparse, as $R^{sp}$ was defined to ensure this. A
sparse language is not NP-complete under many-one reductions unless
$\textbf{P}{=}\textbf{NP}$, which the assumption rules out (Mahaney[16]).

(ii) $\overline{R^{sp}_{t}}$ is sparse, so it has minimal circuits in P/poly.
These are not P-uniform, which would imply $R^{sp}{\in}\textbf{P}$, which does
not hold by assumption.

Ladner[13] constructed artificial NP-intermediate languages, assuming
$\textbf{P}{\neq}\textbf{NP}$. Mahaney showed that a sparse language is not
NP-complete under many-one reductions unless $\textbf{P}{=}\textbf{NP}$, and
under Turing reductions unless PH collapses at the second level. Ogiwara and
Watanabe[18] provide a result employing bounded truth table reductions. Homer
and Longpré[9] provide additional results and alternative proofs.

Allender and Hirahara[1] also provide examples of natural languages that are
conditionally NP-intermediate. They show that if one-way functions exist, then
approximating minimum circuit size and time-bounded Kolmogorov complexity are
NP-intermediate. Determining whether these problems without approximation are
NP-hard or not is an area of active research; see for instance Hirahara[8].

If no optimal proof system exists, then $\textbf{NEXP}{\neq}\textbf{coNEXP}$
(Krajíček and Pudlák[12]), and therefore there are sparse languages in NP but
not in P (Hartmanis et al[7]). Our example differs by providing an explicit
natural language.

##  6 Isomorphisms and Open Questions

If there is no optimal proof system, there is an implicit mapping from
unprovable sentences $\phi$ to families of hard-to-prove sentences “no length
$t$ proof exists of $\phi$”. This mapping can be extended to map provable
sentences to families of sentences with a length $t$ proof. If this mapping
were onto, it would be an isomorphism. This is an elegant picture—an unnoticed
symmetry within mathematics. However, there are several loose ends.

First, the mapping is not onto within the set of all families of hard-to-prove
sentences. Suppose theory $\mathcal{S}$ cannot efficiently prove some family
of sentences not of the form “no length $t$ proof of $\phi$ in $\mathcal{T}$
exists” and that this family is P-uniform. We can make the mapping onto as
follows. For each such family hard for $\mathcal{S}$ not in the range of the
mapping, there is a sentence unprovable in $\mathcal{S}$ which states
“$\mathcal{S}$ cannot efficiently prove the family“. This is unprovable since
$\mathcal{S}$ is consistent by assumption, and $\mathcal{S}$ cannot prove that
it has a hard family, as it would prove its own consistency. Therefore, map
this unprovable sentence onto the hard family. This extended mapping is onto.
A similar solution can address the fact that a mapping from unprovable
sentences to families of tautologies encoding “no length $t$ proof exists” is
not onto.121212Suppose the P-uniform family of tautologies $\tau_{n}$ is hard
for proof system $P$ proven sound by theory $\mathcal{S}$ such that the family
$\tau_{n}$ is also hard for $\mathcal{S}$. Then there unprovable sentences in
$\mathcal{S}$: “$\mathcal{S}$ cannot efficiently prove $\tau_{n}$” and “$P$
cannot efficiently prove $\tau_{n}$”. A curious interpretation is that the
role of hard families of tautologies in proof complexity, with a powerful
theory such as ZFC as a proof system, can be fully understood by focusing
solely on the role of unprovable sentences in ZFC. Thus, one can understand
proof complexity without reference to tautologies.

Second, additional conjectures are needed to extend this question to other
open questions. For instance, the conjecture “no optimal proof system exists
TAUT”, a $\Pi_{1}^{p}$-complete language, and is not strong enough to imply
that PH does not collapse. The stronger conjecture “no optimal proof system
exists for a $\Pi_{2}^{p}$-complete language, even for a proof system with an
oracle for TAUT” implies that $\Pi_{2}^{p}{\neq}\Pi_{1}^{p}$.131313Chen et
al[4] show that a $\Pi_{2}^{p}$-complete language does not have an optimal
proof system if and only if TAUT does not have an optimal proof system, so the
reference to an oracle is necessary to separate $\Pi_{2}^{p}$ and
$\Pi_{1}^{p}$. A version of Theorem 1.1(iii) would hold for $\mathcal{S}$ with
a predicate for membership in $\Pi_{1}$ in the arithmetic hierarchy (AH),
setting up an isomorphism for sentences with a higher degree of
unsolvability.141414See Pudlák[21] p. 569 for the construction for TAUT. A set
of such conjectures for each level of PH would assert: PH does not collapse
due to the existence of unprovable sentences at each level of AH. These would
assert, elegantly, that PH does not collapse because AH does not collapse.

This suggests a research program could identify a conjecture and implied
isomorphism associated with each open question in complexity theory, or
identify obstacles to doing so. For instance, the recent flurry of results by
Liu and Pass[15] and others suggest that asserting the hardness of showing
$\mathcal{T}{\centernot{\sststile{}{t}}}`x{\in}R^{t}$’, where $R^{t}$ is
defined with respect to time-bounded Kolmogorov complexity, would imply the
existence of one-way functions by asserting the average-case hardness of time-
bounded Kolmogorov complexity.

To the extent each of these conjectures has the same structure, they can be
rolled up into a single overarching conjecture, potentially providing insight
into multiple open questions. A very strong conjecture is that some condition
of the form in Theorem 1.1(iii) asserts the resolution of most open questions
in complexity theory.

##  7 Conclusion

The conditions in Theorem 1.1 have such strong implications for complexity
theory, determining whether they are true and even provable would be
desirable. An informal argument is: ruling out length $t$ proofs of an
unprovable sentence $\phi$ is hard because the crucial fact is inaccessible
that no proof exists of any length. This informal argument seems strongest for
sentences $x{\in}R$, which are dense, nonconstructive, and typically
impossible to prove. To state this in the most extreme form, suppose no other
effectively computable fact about $x{\in}R$ may be useful at all in ruling out
length $t$ proofs. In any program ruling out length $t$ proofs of $x{\in}R$,
an if-then statement would need to compute a predicate on $R$ to determine
which branch to take. Likewise, in any proof doing the same, any case-based
reasoning would need to compute a predicate on $R$. However, predicates on $R$
are constrained by the fact that $R$ passes all known and conceivable
effective tests of randomness (Li and Vitanyi[14] Section 2.4). It is possible
that if-then statements and case-based proofs might appear to behave in a
purely random manner in ruling out length $t$ proofs of $x{\in}R$. If so, a
program or proof can do no better than loops that exhaustively check all
cases.

This constraint might also bind non-uniformly. Boolean circuits and
propositional proofs require NOT gates and cancellation to implement
conditional logic, such as encoding if-then statements and case-based
reasoning. Such circuits and proofs may therefore gain limited benefit their
use of NOT gates and cancellation, in line with an old conjecture. It is known
that for some monotone Boolean functions, the gap between their non-monotone
and monotone circuit complexity (the number of gates in minimal circuits with
and without NOT gates respectively) is exponential (Razborov[23], Tardos[27]),
and hoped that it is small for some other monotone Boolean functions such as
CLIQUE (Razborov[24], Alon and Boppana[2]). This conjecture generalized to
non-monotone Boolean functions is that for certain functions, the gap is small
between their cancellative and non-cancellative circuit complexity is small,
where a non-cancellative circuit has a formal polynomial in which no monomial
includes both a literal and its negation (Sengupta and
Venkateswaran[26]).151515Shannon’s counting argument shows that most Boolean
functions require $2^{n}/n$ gates, the gap between cancellative and non-
cancellative circuits for a random Boolean functions cannot be so large as to
reduce circuits to polynomial size, as with Tardos’ example. This argument
might support a claim that computational tasks such as decryption of small
messages are hard in practice and not just asymptotically.

## References

  * [1] Eric Allender and Shuichi Hirahara, _New insights on the (non-)hardness of circuit minimization and related problems_ , ACM Trans. Comput. Theory 11 (2019), no. 4, 27:1–27:27.
  * [2] Noga Alon and Ravi Boppana, _The monotone circuit complexity of Boolean functions_ , Combinatorica 7 (1987), 1–22.
  * [3] Cristian S. Calude and Helmut Jürgensen, _Is complexity a source of incompleteness?_ , Advances in Applied Mathematics 35 (2005), no. 1, 1–15.
  * [4] Yijia Chen, Jörg Flum, and Moritz Müller, _Hard instances of algorithms and proof systems_ , How the World Computes (Berlin, Heidelberg) (S. Barry Cooper, Anuj Dawar, and Benedikt Löwe, eds.), Springer Berlin Heidelberg, 2012, pp. 118–128.
  * [5] Stephen Cook and Phuong Nguyen, _Foundations of proof complexity: Bounded arithmetic and propositional translations_ , Cambridge University Press, 2014.
  * [6] Stephen Cook and Robert Reckhow, _The relative efficiency of propositional proof systems_ , J. Symb. Log. 44 (1979), 36–50.
  * [7] Juris Hartmanis, Neil Immerman, and Vivian Sewelson, _Sparse sets in NP-P: EXPTIME versus NEXPTIME_ , Inf. Control. 65 (1985), no. 2/3, 158–181.
  * [8] Shuichi Hirahara, _NP-hardness of learning programs and partial MCSP_ , Electron. Colloquium Comput. Complex. TR22-119 (2022).
  * [9] Steven Homer and Luc Longpré, _On reductions of NP sets to sparse sets_ , J. Comput. Syst. Sci. 48 (1994), no. 2, 324–336.
  * [10] Hartley Rogers Jr., _Theory of recursive functions and effective computability_ , MIT Press, Cambridge, MA, 1987.
  * [11] Jan Krajíček, _Proof complexity_ , Cambridge University Press, New York, NY, 2019.
  * [12] Jan Krajíček and Pavel Pudlák, _Propositional proof systems, the consistency of first order theories and the complexity of computations_ , J. Symb. Log. 54 (1989), 1063–79.
  * [13] Richard E. Ladner, _On the structure of polynomial time reducibility_ , J. ACM 22 (1975), no. 1, 155–171.
  * [14] Ming Li and Paul M. B. Vitányi, _An introduction to Kolmogorov complexity and its applications_ , Texts in Computer Science, Springer, 2008.
  * [15] Yanyi Liu and Rafael Pass, _On one-way functions and Kolmogorov complexity_ , 2020 IEEE 61st Annual Symposium on Foundations of Computer Science (FOCS), 2020, pp. 1243–1254.
  * [16] Stephen R. Mahaney, _Sparse complete sets of NP: solution of a conjecture of Berman and Hartmanis_ , J. Comput. Syst. Sci. 25 (1982), no. 2, 130–143.
  * [17] Hunter Monroe, _Speedup for natural problems and noncomputability_ , Theoretical Computer Science 412 (2011), no. 4-5, 478–481.
  * [18] Mitsunori Ogiwara and Osamu Watanabe, _On polynomial-time bounded truth-table reducibility of NP sets to sparse sets_ , SIAM J. Comput. 20 (1991), no. 3, 471–483.
  * [19] Pavel Pudlák, _On the length of proofs of finitistic consistency statements in first order theories_ , Studies in Logic and the Foundations of Mathematics, vol. 120, Elsevier, 1986, pp. 165–196.
  * [20] , _The lengths of proofs_ , Handbook of Proof Theory (Samuel R. Buss, ed.), Elsevier, 1998.
  * [21] , _Logical foundations of mathematics and computational complexity: A gentle introduction_ , Springer, 2013.
  * [22] , _Incompleteness in the finite domain_ , Bull. Symb. Log. 23 (2017), no. 4, 405–441.
  * [23] Alexander A. Razborov, _A lower bound on the monotone network complexity of the logical permanent_ , Mathematical Notes of the Academy of Sciences of the USSR 37 (1985), 485–493.
  * [24] , _Lower bounds on the monotone complexity of some Boolean functions_ , Doklady Akademii Nauk SSSR 281 (1985), 798–801, In Russian. English translation in Soviet Mathematics Doklady, 31:354–57, 1985\.
  * [25] Rahul Santhanam, _Introduction to meta-complexity_ , Meta-Complexity Boot Camp, Simons Institute for the Theory of Computing, January 2023.
  * [26] Rimli Sengupta and H. Venkateswaran, _Non-cancellative Boolean circuits: a generalization of monotone Boolean circuits_ , Theor. Comput. Sci. 237 (2000), 197–212.
  * [27] Éva Tardos, _The gap between monotone and non-monotone circuit complexity is exponential_ , Combinatorica 8 (1988), 141–42.