Searcharxiv⌕ Search

arXiv subjects

Dirk Englund

Publications and source records attributed to Dirk Englund.

At least 19 recordsLinked to original sources
arXiv2026

Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics

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.

cs.AI↗
arXiv2026

Gradient-Based Optimization Enables Scalable Fault-Tolerant Quantum Gate Synthesis

We develop a numerical approach to optimizing a quantum circuit over a discrete gate set by using gradient descent to tune $R_Z$ angles to a solution where many $R_Z$ gates can be rounded to a Clifford or $T$ gate without introducing further synthesis error. Through benchmarking, we show that our approach is able to match state-of-the-art techniques for multi-qubit Clifford + $T$ circuit synthesis, and is able to find circuits for unitaries that previous approaches fail to find solutions for. Our approach can adapt to any discrete gate set, which we demonstrate using the Clifford + $T$ + $\sqrt T$ gate set.

quant-ph↗
arXiv2026

Quantum Cryptography and Autoformalization in Lean

Quantum key distribution provides secure communication by relying on physics principles and mathematical reasoning. Security proofs across the field can contain gaps, often between individually valid theorems integrated under mismatched assumptions. We produce an end-to-end security theorem formalized in the Lean proof assistant, eliminating hidden hypotheses by building only on Lean's standard axioms. Our proof covers composable security of the entanglement-based qubit BB84 protocol against coherent attacks by the postselection technique, accounting for finite block size, and is written in a language that enforces local operations and classical communication to help ensure a faithful representation of the protocol. The proof itself was enabled by LLM-based autoformalization, and with the proof complete, we used the same pipeline as a discovery machine, reducing the finite-size penalty on the key rate. Our work sets a reproducible standard for security arguments in quantum cryptography and shows how formal proof engines can accelerate discovery across quantum information science.

quant-ph↗
arXiv2026

AIR-LLM: Broadcasting AI Weights over Radio for Memory-Free Edge LLM Inference via RF Computing

Next-generation large language models (LLMs) are expanding from the cloud to ubiquitous edge devices. However, edge devices typically either lack the memory to store increasingly large LLM weights or, even with enough memory, spend unaffordable energy on loading the weights. This raises our question: can an edge device run an LLM without storing or loading its weights, but receive them over the air and consume them on the fly? Inspired by wireless broadcasting, we present AIR-LLM, an LLM inference architecture for edge devices, which is composed of: (i) a central radio (e.g., 5G base stations) that broadcasts the LLM weights into the air, and (ii) the edge user that receives the weights and completes the general matrix-vector multiplication (GEMV) of LLM inference directly in the radio frequency (RF) domain using RF mixers. To further shorten the airtime, AIR-LLM exploits MIMO spatial multiplexing and proposes an energy-efficient precoder-postcoder pair on the edge to calibrate its own wireless channel. Since the central radio stays user-unaware, AIR-LLM is user-scalable so that one broadcast serves unlimited users within its coverage. We implement AIR-LLM on the NVIDIA Sionna ray-traced channels of two real-world urban scenes and the profiling of a real RF mixer. With a WikiText-2 perplexity degradation of 4.0% on LLaMA-3.1-8B, AIR-LLM saves the energy by 157.7x/40.4x against the FP16 and weight-only quantization baselines; with 20 users, its airtime is 104.1x/26.0x shorter, respectively.

cs.IT↗
arXiv2026

Agentic AI for Scalable and Robust Optical Systems Control

We present AgentOptics, an agentic AI framework for high-fidelity, autonomous optical system control built on the Model Context Protocol (MCP). AgentOptics interprets natural language tasks and executes protocol-compliant actions on heterogeneous optical devices through a structured tool abstraction layer. We implement 64 standardized MCP tools across 8 representative optical devices and construct a 410-task benchmark to evaluate request understanding, role-aware responses, multi-step coordination, robustness to linguistic variation, and error handling. We assess two deployment configurations--commercial online LLMs and locally hosted open-source LLMs--and compare them with LLM-based code generation baselines. AgentOptics achieves 87.7%--99.0% average task success rates, significantly outperforming code-generation approaches, which reach up to 50% success. We further demonstrate broader applicability through five case studies extending beyond device-level control to system orchestration, monitoring, and closed-loop optimization. These include DWDM link provisioning and coordinated monitoring of coherent 400 GbE and analog radio-over-fiber (ARoF) channels; autonomous characterization and bias optimization of a wideband ARoF link carrying 5G fronthaul traffic; multi-span channel provisioning with launch power optimization; closed-loop fiber polarization stabilization; and distributed acoustic sensing (DAS)-based fiber monitoring with LLM-assisted event detection. These results establish AgentOptics as a scalable, robust paradigm for autonomous control and orchestration of heterogeneous optical systems.

eess.SY↗
arXiv2026

Radio-Frequency Convolutional Neural Networks

Running artificial intelligence (AI) models directly on edge devices such as smartphones, wearables, and drones offers low latency, pervasive scalability, and data privacy, but these devices rarely carry the computing capability that modern neural networks demand. Edge accelerators have been developed in response, yet each adds computing hardware to devices already constrained in size, weight, power, and cost (SWaP-C). An alternative lies in what these devices already carry: the frequency mixer in every wireless radio multiplies signals in time, natively performing convolution in the frequency domain. Here we introduce radio-frequency convolutional neural networks (RF-CNNs), which repurpose existing communication hardware for CNN inference. Multi-channel convolutions are mapped onto frequency tones for a passive mixer to execute in a single pass. We experimentally demonstrate that RF-CNN runs deep CNNs up to 26.4 million parameters and nine layers from classification of wireless signals and images to controllable image generation, close to full-precision performance. Because the weights arrive over the air and the analog hardware is shared with communication, the edge device spends energy only on data preparation and readout-down to 0.72 femtojoules per multiply-accumulate, two orders of magnitude less than it would cost on an added digital processor. These results suggest that deployed wireless infrastructure can bring efficient, state-of-the-art AI inference to the billions of devices it already connects.

cs.LG↗
arXiv2026

Broadband Spatio-Spectral Mode Conversion via Four-Wave Mixing

We introduce a framework for scalable and broadband free-space phase-matched four-wave mixing in ring resonators. This method for four-wave mixing reduces the complexity of coupling an emitter to a quantum network by combining the spatial and spectral interfaces between them into one nonlinear optical process. The device is compliant with current heterogeneous integration capabilities and has a bandwidth of 165 nm for efficient spatio-spectral conversion. We outline a fabrication-ready diamond-on-insulator pathway towards modular unit cells that natively bridge visible color centers to the infrared spectrum for scalable quantum networks. We also present and analyze an end-to-end framework for considering single-photon coupling efficiency from a color center to a quantum network. This framework represents a step forwards in analyzing and reducing system-scale losses in a spin-photon interface.

quant-ph↗
arXiv2026

From Pixels to PCells: A Neurosymbolic Approach to Photonic Component Creation

We present PixCell, a neurosymbolic system in which multimodal agents convert a visually presented photonic component into a parametric program over a small domain-specific language (DSL) of geometric primitives. A system enabling deterministic visual verification renders evaluation asymmetrically cheaper than the generation attempt. While models using multi-seed sampling and iterative revision reach a mean best-turn IoU of only 0.416, multimodal agents through PixCell's interface and verifier consistently exceed 0.9 mean IoU, with scores reaching 0.974 and 0.955 across eight component targets while also satisfying source contracts. These results demonstrate that frontier multimodal agents can reliably understand and render executable parametric representations from visual targets. Using these live parameters, cross-stack studies on an interferometer reconstruct primitive programs that satisfy an 8.0 nm free spectral range target and the original footprint constraint on modeled 220-nm SOI, 400-nm SiN, and 400-nm TFLN stacks. PixCell further carries a paper-derived splitter from visual reconstruction through SOI full-wave simulation, producing symmetric propagation and balanced outputs. Finally, the same executable verifier supplies a training reward and dataset used to train a Qwen3.6-35B-A3B model with LoRA and GRPO without supervised demonstrations. On eight training-excluded paper figures, its mean champion IoU rises from 0.422 after eight initial attempts to 0.491 after three verifier-guided revision rounds. These results therefore establish a controlled framework for measuring, retargeting, and improving visual-to-parametric photonic component design.

cs.CV↗
arXiv2026

Strategic Plan for Neutral Atom Quantum Computation

We present a strategic plan for neutral atom quantum computation, bringing together hardware development and theory advancements to achieve the goal of practical quantum advantage. The concept of practical quantum advantage is defined, along with how to verify claims of advantage, and approaches to designing quantum algorithms that deliver practical advantage. Future directions for neutral atom quantum processor hardware are described: scaling-up system size, Qubit encodings and atomic platforms, going further below threshold with neutral-atom logical-qubit performance, continuous reloading of qubits, and fast readout. We also explore opportunities for scalable integrated photonic control technologies. Alongside hardware advancements, new developments in quantum error correction and compilation of quantum circuits are proposed. Finally, we examine the opportunity of networking multiple neutral atom quantum processors together to perform distributed quantum computing and overcome possible limitations of a single system.

quant-ph↗
arXiv2026

Foundry CMOS platform for multimodal quantum materials characterization

Quantum materials experiments increasingly rely on microwave, electrical, thermal, optical, and structural probes, but these capabilities are typically assembled from custom hardware that limits reproducibility and scalability. Here we show that a commercial 65-nm CMOS process can be repurposed as a passive, foundry-manufacturable characterization platform by functionally partitioning its metal stack into microwave, thermal, and electrical subsystems within a 1 mm2 footprint. The integrated RF architecture enables cryogenic magnetic susceptibility measurements of Fe3GeTe2 heterostructures at 1.75 K without sample-specific fabrication. We further demonstrate NV-center optically detected magnetic resonance (ODMR) with >20% contrast at 4-9 dBm microwave power, reducing power requirements by 20-25 dB relative to conventional antenna-based approaches while maintaining sensitivities of 2-3 uT/sqrt(Hz). We additionally confirm compatibility with in-situ electron-beam imaging, showing no measurable degradation in image quality upon device operation. These results establish a scalable, foundry-manufacturable platform for multimodal quantum sensing and materials characterization.

cond-mat.mtrl-sci↗
arXiv2026

Monolithic Integration of Piezo-Optomechanical Photonics and CMOS Electronics

Next-generation photonic architectures for AI, sensing, and quantum computing require thousands to millions of reprogrammable photonic devices on a chip[1]. The monolithic integration of Electronically-backed Photonic Integrated Circuits (EPICs) allows for very high density electrical interconnection and electronic drivers that can scale with photonics. Piezo-optomechanical photonic integrated circuits (POMPICs) offer low power consumption, high speed modulation, cryogenic compatibility and broadband optical transparency from ultraviolet to infrared wavelengths[2,3], but have not been demonstrated with monolithically integrated CMOS electronics. Here, we show a fully monolithic, all-CMOS fabricated platform for POMPICs co-fabricated with commercial control electronics. 200 millimeter photonic wafers are constructed directly on completed CMOS driver wafers by back-end-of-line processing, connecting integrated piezoelectric actuators under broadband silicon nitride waveguides to a high-density digital backplane comprising >2 million electrical connections per die with 6.4x6.4 micron electrode pitch. We introduce segmented POMPIC components as Photonic Digital-to-Analog converters (PDACs) that convert low-voltage digital electronic signals to multi-bit analog optical phase and amplitude modulation, and we demonstrate parallel control of optical phase shifters, Mach-Zehnder interferometers, optical routing trees, and tunable ring resonators using a standard HDMI interface to program CMOS electronics. We test multiple reticles and perform electronic and photonic characterization across the entire wafer to establish uniformity and yield, demonstrating wafer-scale integration of POMPICs on an electronic backplane and enabling dense, scalable electronic control of piezo-optomechanical circuits.

physics.optics↗
arXiv2026

A Machine-Verified Proof of a Quantum-Optimization Conjecture

We report a machine-verified resolution of a problem open for over a decade in quantum optimization: the Farhi, Goldstone and Gutmann (FGG) conjecture that depth-$p$ Quantum Approximate Optimization Algorithm (QAOA) on the ring of disagrees attains approximation ratio $(2p+1)/(2p+2)$ exactly. We found the proof using a large language model, Claude Fable 5, and verified its correctness end-to-end by the Lean 4 proof assistant. Our methodology includes several ingredients: building on a substantial Lean library of quantum information, we formalized the QAOA components and the known parts of the problem, and reduced the conjecture to a single open mathematical statement. The model was then handed the library and our agentic toolkit, and tasked with closing that gap by constructing a proof in Lean. The resulting process is a feedback loop between the model's natural-language reasoning and Lean's mechanical verification, which converged to a machine-verified proof. Human verification is required only for the structural scaffolding - that the formal statement faithfully encodes the intended claim - while the proof itself is supplied by the model and certified mechanically by Lean. The proof is nevertheless striking - the model uncovered a hidden dynamical symmetry of the problem and exploited it, borrowing tools and machinery from an adjacent field to turn a hard existence problem into an explicit construction. This work paves the way for resolving open conjectures in quantum information science and beyond.

quant-ph↗
arXiv2026

Recirculating Quantum Photonic Networks for Fast Deterministic Quantum Information Processing

A fundamental challenge in photonics-based deterministic quantum information processing is to realize key transformations on time scales shorter than those of detrimental decoherence and loss mechanisms. This challenge has been addressed through device-focused approaches that aim to increase nonlinear interactions relative to decoherence rates. In this work, we adopt a complementary architecture-focused approach by proposing a recirculating quantum photonic network (RQPN) that minimizes the duration of quantum information processing tasks, thereby reducing the requirements on nonlinear interaction rates. The RQPN consists of a network of all-to-all connected nonlinear cavities with dynamically controlled waveguide couplings, and it processes information by capturing a photonic input state, recirculating photons between the cavities, and releasing a photonic output state. We demonstrate the RQPN's architectural advantage through two examples: first, we show that processing all qubits simultaneously yields faster operations than single- and two-qubit decompositions of the three-qubit Toffoli gate. Second, we demonstrate implementations of a measurement-free correction for single-photon loss, achieving up to seven-fold speedups and significantly improved hardware efficiency relative to state-of-the-art architecture proposals. Our work shows that a single hardware-efficient recirculating architecture substantially reduces the temporal overhead of multi-qubit gates and quantum error correction, thereby lowering the barrier to experimental realizations of deterministic photonic quantum information processing.

quant-ph↗
arXiv2026

18-dB on-chip vacuum squeezing in an adaptively poled lithium niobate waveguide

Quantum squeezed states of light can enhance measurement sensitivity beyond classical limits and enable quantum information processing, but scalable low-loss sources remain challenging. We demonstrate continuous-wave quantum squeezing on a chip, achieving 18 dB of squeezing and 20 dB of anti-squeezing at 1570 nm in a 1.6-cm traveling-wave adaptively poled thin-film lithium niobate waveguide. A distributed model independently determines facet losses, phase noise, and nonlinear interaction strength without prior assumptions, enabling rigorous inference of on-chip performance. We estimate a 95% confidence interval of [-18.96, -17.25] dB squeezing and [19.96, 21.35] dB anti-squeezing. These values represent the highest squeezing reported for any integrated photonic platform and the first assumption-free statistical validation of integrated squeezing performance. Our results establish thin-film lithium niobate as a high-performance, scalable platform for continuous-variable quantum sensing, communications, and photonic computing.

physics.optics↗
arXiv2026

Microring Perceptron Sensing for Low-Power Radio-Frequency Detection with Quantum-Compatible Photonic Preprocessing

Radio-frequency (RF) sensing underpins applications ranging from radar and wireless communication to biomedical and quantum measurement, where detection sensitivity at low signal-to-noise ratio (SNR) directly limits the achievable range, resolution, and information capacity. Machine learning has been widely applied to enhance sensing performance, but predominantly as post-detection analysis of already-acquired data. At low SNR, however, the information missing from acquired data cannot be recovered downstream, making pre-detection processing essential. Here we introduce microring perceptron (MiRP) sensing, a framework that exploits RF-photonic transduction in a microring resonator, where a programmable optical pump performs three-wave mixing to implement a learned mapping from the incoming RF signal to optical feature signals prior to detection. The transducer front end and digital neural-network back end are jointly optimized within a single end-to-end training pipeline, allowing the sensing system to learn an encoding that preserves task-relevant information through detection. Across benchmark tasks, MiRP sensing achieves substantially higher task performance than conventional processing at low input RF power levels where detection noise dominates. The algorithmic gain reported here offers an orthogonal axis of improvement that composes with, and amplifies the impact of, existing and future advances along complementary dimensions, including hardware efficiency and quantum-enhanced optical sensing.

eess.SP↗
arXiv2026

Hardware Co-Designed Optimal Control for Programmable Atomic Quantum Processors via Reinforcement Learning

Developing scalable, fault-tolerant atomic quantum processors requires precise control over large arrays of optical beams. This remains a major challenge due to inherent imperfections in classical control hardware, such as inter-channel crosstalk and beam leakage. In this work, we introduce a hardware co-designed intelligent quantum control framework to address these limitations. We construct a mathematical model of the photonic control hardware, integrate it into the quantum optimal control (QOC) framework, and apply reinforcement learning (RL) techniques to discover optimal control strategies. We demonstrate that the proposed framework enables robust, high-fidelity parallel single-qubit gate operations under realistic control conditions, where each atom is individually addressed by an optical beam. Specifically, we implement and benchmark three optimization strategies: a classical hybrid Self-Adaptive Differential Evolution-Adam (SADE-Adam) optimizer, a conventional RL approach based on Proximal Policy Optimization (PPO), and a novel end-to-end differentiable RL method. Using SADE-Adam as a baseline, we find that while PPO performance degrades as system complexity increases, the end-to-end differentiable RL consistently achieves gate fidelities above 99.9$\%$, exhibits faster convergence, and maintains robustness under varied channel crosstalk strength and randomized dynamic control imperfections.

quant-ph↗
arXiv2026

Breaking On/Off-coupling Loss Degeneracies via Bidirectional Nonlinear Optics

Accurate evaluation of nonlinear photonic integrated circuits requires separating input and output coupling efficiencies (i.e., $η_1$ and $η_2$), yet the conventional linear-transmission calibration method recovers only their product (i.e., $η_1\,η_2$) and therefore introduces systematic bias when inferring on-chip performance from off-chip data. We present bidirectional nonlinear optical tomography (BNOT), a direction-aware metrology that uses forward and backward pumping of complementary nonlinear probes, with process-appropriate detection, to break the ``degeneracy'' of $η_1\,η_2$ and estimate individual interface efficiencies with tight confidence intervals. The method links off-chip measurements to on-chip quantities through a compact observation model that explicitly incorporates pump fluctuations and detector noise, and it frames efficiency extraction as a joint constrained optimization. Monte Carlo studies show unbiased convergence of the estimated efficiencies to ground truth with low error across realistic operating regimes. Using these efficiency estimates to reconstruct on-chip nonlinear figures of merit yields distributions centered on the true values with reduced variance, whereas conventional ``degenerate'' calibration is biased and can substantially misestimate on-chip performance. BNOT is hardware-compatible and platform-agnostic, and provides unbiased characterization of off- and on-chip coupling efficiencies across nonlinear processes, enabling reproducible, coupling-resolved benchmarking for scalable systems in quantum optics, frequency conversion, and precision metrology.

physics.optics↗
arXiv2026

Quantum squeezing in an all-resonant periodically poled lithium niobate microresonator

Quantum noise limits the sensitivity of optical measurements, but squeezed states of light enable quantum-enhanced metrology, sensing, and information processing. Most on-chip squeezed-light sources rely on Kerr ($χ^{(3)}$) nonlinearities, remain limited by pump power and excess loss constraints. Quadratic ($χ^{(2)}$) platforms instead provide stronger parametric interactions, lower pump power requirements, and greater spectral engineering flexibility. Here, we demonstrate strong, broadband squeezed-light generation on a thin-film lithium niobate (TFLN) photonic chip using a dual-resonant optical parametric amplifier implemented in a single periodically poled LN (PPLN) microresonator. Near-full-depth domain inversion is achieved simultaneously with highly over-coupled resonances, exhibiting escape efficiencies exceeding 90% and intrinsic quality factors above 2.5 million in a 0.6 mm$^2$ X-cut TF-PPLN resonator, enabling efficient squeezing at 1587 nm when pumped at 793.5 nm. Operating in the continuous-wave regime, we directly measure -0.81 dB of squeezing below the shot-noise limit with a pump power of 27 mW, together with +4.29 dB of anti-squeezing. From these measurements, we infer an on-chip squeezing level of -7.52 dB $\pm$ 0.22 dB (95% confidence interval: [-7.96,-7.10] dB), and an on-chip anti-squeezing level of +9.62 dB $\pm$ 0.25 dB. We demonstrate single-mode squeezing at degeneracy with a squeezed-light spectrum exceeding 10.3 THz. This work reports the highest squeezing ratio among integrated $χ^{(2)}$ cavity platforms and the first quasi-phase matched, fully resonant $χ^{(2)}$ cavity squeezer on chip, establishing a scalable route to fully integrated power-efficient squeezed-light sources for quantum-enhanced sensing and metrology.

physics.optics↗