Kfir Sulimany

Kfir Sulimany, Sri Krishna Vadlamani, Ryan Hamerly et al.

Secure multiparty computation enables the joint evaluation of multivariate functions across distributed users while ensuring the privacy of their local inputs. This field has become increasingly urgent due to the exploding demand for computationally intensive deep learning inference. These computations are typically offloaded to cloud computing servers, leading to vulnerabilities that can compromise the security of the clients' data. To solve this problem, we introduce a linear algebra engine that leverages the quantum nature of light for information-theoretically secure multiparty computation using only conventional telecommunication components. We apply this linear algebra engine to deep learning and derive rigorous upper bounds on the information leakage of both the deep neural network weights and the client's data via the Holevo and the Cramér-Rao bounds, respectively. Applied to the MNIST classification task, we obtain test accuracies exceeding $96\%$ while leaking less than $0.1$ bits per weight symbol and $0.01$ bits per data symbol. This weight leakage is an order of magnitude below the minimum bit precision required for accurate deep learning using state-of-the-art quantization techniques. Our work lays the foundation for practical quantum-secure computation and unlocks secure cloud deep learning as a field.

Zhihui Gao, Sri Krishna Vadlamani, Kfir Sulimany et al.

Modern edge devices, such as cameras, drones, and Internet-of-Things nodes, rely on deep learning to enable a wide range of intelligent applications, including object recognition, environment perception, and autonomous navigation. However, deploying deep learning models directly on the often resource-constrained edge devices demands significant memory footprints and computational power for real-time inference using traditional digital computing architectures. In this paper, we present WISE, a novel computing architecture for wireless edge networks designed to overcome energy constraints in deep learning inference. WISE achieves this goal through two key innovations: disaggregated model access via wireless broadcasting and in-physics computation of general complex-valued matrix-vector multiplications directly at radio frequency. Using a software-defined radio platform with wirelessly broadcast model weights over the air, we demonstrate that WISE achieves 95.7% image classification accuracy with ultra-low operation power of 6.0 fJ/MAC per client, corresponding to a computation efficiency of 165.8 TOPS/W. This approach enables energy-efficient deep learning inference on wirelessly connected edge devices, achieving more than two orders of magnitude improvement in efficiency compared to traditional digital computing.

Benjamin Breen, Marco Del Tredici, Jacob McCarran et al.

We present Ax-Prover, a multi-agent system for automated theorem proving in Lean that can solve problems across diverse scientific domains and operate either autonomously or collaboratively with human experts. To achieve this, Ax-Prover approaches scientific problem solving through formal proof generation, a process that demands both creative reasoning and strict syntactic rigor. Ax-Prover meets this challenge by equipping Large Language Models (LLMs), which provide knowledge and reasoning, with Lean tools via the Model Context Protocol (MCP), which ensure formal correctness. To evaluate its performance as an autonomous prover, we benchmark our approach against frontier LLMs and specialized prover models on two public math benchmarks and on two Lean benchmarks we introduce in the fields of abstract algebra and quantum theory. On public datasets, Ax-Prover is competitive with state-of-the-art provers, while it largely outperforms them on the new benchmarks. This shows that, unlike specialized systems that struggle to generalize, our tool-based agentic theorem prover approach offers a generalizable methodology for formal verification across diverse scientific domains. Furthermore, we demonstrate Ax-Prover's assistant capabilities in a practical use case, showing how it enabled an expert mathematician to formalize the proof of a complex cryptography theorem.

Sri Krishna Vadlamani, Kfir Sulimany, Zhihui Gao et al.

Machine intelligence on edge devices enables low-latency processing and improved privacy, but is often limited by the energy and delay of moving and converting data. Current systems frequently avoid local model storage by sending queries to a server, incurring uplink cost, network latency, and privacy risk. We present the opposite approach: broadcasting model weights to clients that perform inference locally using in-physics computation inside the radio receive chain. A base station transmits weights as radio frequency (RF) waveforms; the client encodes activations onto the waveform and computes the result using existing mixer and filter stages, RF components already present in billions of edge devices such as cellphones, eliminating repeated signal conversions and extra hardware. Analysis shows that thermal noise and nonlinearity create an optimal energy window for accurate analog inner products. Hardware-tailored training through a differentiable RF chain preserves accuracy within this regime. Circuit-informed simulations, consistent with a companion experiment, demonstrate reduced memory and conversion overhead while maintaining high accuracy in realistic wireless edge scenarios.

Kfir Sulimany, Guy Pelc, Rom Dudkiewicz et al.

High-dimensional quantum key distribution (QKD) offers secure communication, with secure key rates that surpass those achievable by QKD protocols utilizing two-dimensional encoding. However, existing high-dimensional QKD protocols require additional experimental resources, such as multiport interferometers and multiple detectors, thus raising the cost of practical high-dimensional systems and limiting their use. Here, we present and analyze a novel protocol for arbitrary-dimensional QKD, that requires only the hardware of a standard two-dimensional system. We provide security proofs against individual attacks and coherent attacks, setting an upper and lower bound on the secure key rates. Then, we test the new high-dimensional protocol in a standard two-dimensional QKD system over a 40 km fiber link. The new protocol yields a two-fold enhancement of the secure key rate compared to the standard two-dimensional coherent one-way protocol, without introducing any hardware modifications to the system. This work, therefore, holds great potential to enhance the performance of already deployed time-bin QKD systems through a software update alone. Furthermore, its applications extend across different encoding schemes of QKD qudits.