arXiv subjects

Jacob M. Taylor

Publications and source records attributed to Jacob M. Taylor.

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

Achieving Sub-Zeptonewton Force Sensitivity and Spin-Motion Entanglement in Levitated Diamond via Pulsed Backaction Evasion

We propose a system to achieve sub-zeptonewton force sensing and robust spin-mechanical entanglement in a levitated diamond system. By coupling a nitrogen-vacancy (NV) center spin to the motion of its host diamond within a magnetic trap, we develop a platform designed to surpass the standard quantum limit. We develop and compare three distinct pulse sequences -- Ramsey, Hahn echo, and Carr-Purcell-Meiboom-Gill (CPMG) -- to create increasing amounts of backaction evasion while mitigating the effects of shot noise and thermal decoherence. Our results show that the CPMG sequences yield the most significant performance gains, reaching a force sensitivity of better than $10^{-23} \text{ N}/\sqrt{\text{Hz}}$ for broadband sensing around $10^4 \text{ Hz}$. Furthermore, we derive an entanglement witness protocol that accounts for pulsed dynamical decoupling, proving that spin-motion entanglement remains detectable even when occurring much faster than the mechanical period. These findings provide a more practical path for using levitated nanodiamonds both as high-precision sensors and as non-classical mechanical systems for fundamental tests of quantum mechanics.

quant-ph↗

arXiv2026

Deciding the Attainability of the Multiparameter Quantum Fisher Information is NP-Hard

The quantum Fisher information (QFI) sets a fundamental bound on the attainable precision when estimating multiple parameters simultaneously. Incompatibility among the individually optimal measurements can, in some cases, imply that the precision limit set by the QFI is not attainable. In certain special cases, including pure states and full-rank states, the exact conditions for when the precision limit set by the QFI can be saturated are known. However, general conditions for the attainability of the QFI with measurements on individual copies of the quantum state have long been sought. Indeed, this was recently stated as one of the five problems in quantum information theory highlighted by [P. Horodecki et al, PRX Quantum 3, 010101 (2022)]. In this work we prove that exact attainability with individual measurements is NP-hard to decide, even for a restricted set of real, constant-rank quantum models. The source problem for our proof is the NP-hard problem of deciding whether a given bipartite density matrix is separable or not. Our result shows that the longstanding difficulty in obtaining general conditions for QFI attainability reflects a fundamental computational obstruction, rather than merely a limitation of existing mathematical techniques: unless P=NP, no efficiently computable necessary-and-sufficient criterion can exist in general.

quant-ph↗

arXiv2026

AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics

Formalizing mathematics in a proof assistant, where a machine checks every definition, statement and proof, has set a new standard of rigor. Large language models are now capable of formalizing autonomously, even at the scale of whole textbooks. We bring this standard of rigor to physics, where theoretical arguments carry idealizations that are rarely stated fully, and any logical gaps could have a cascading effect on interdependent results. Recognizing the need to evaluate autoformalization systems for physics, we release AxQM, 1,019 kernel-checkable proof-synthesis tasks over 479 items drawn from the textbook Quantum Computation and Quantum Information by Nielsen and Chuang. The tasks are stated in a custom Lean library of finite-dimensional quantum mechanics. By task count, it is the largest proof-synthesis benchmark in physics by a factor of four. AxQM is derived from a near-complete formalization of the formal portions of the textbook, so every task is guaranteed a solution, which we keep private. Grading of the benchmark is done deterministically by the Lean kernel, which checks that the proof compiles, that no sorry appears in it or in any declaration it depends on, and that it introduces no new axioms.

quant-ph↗

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

An Approach to Probing Particles and Quasi-particles in the Condensed Bose-Hubbard Model

Measurement plays a crucial role in a quantum system beyond just learning about the system state: it changes the post-measurement state and hence influences the subsequent time evolution; further, measurement can even create entanglement in the post-measurement conditional state. In this work, we study how careful choice of parameters for a typical measurement process on cold atoms systems -- phase contrast imaging -- has a strong impact on both what the experimentalist observes but also on the backaction the measurement has on the system, including the creation and diffusion of quasiparticles emerging from the quantum many-body dynamics. We focus on the case of a Bose-Einstein-condensate array, in the low-temperature and low-momentum limit. Our theoretical investigation reveals regimes where the imaging light probes either the bare particle or quasiparticle dynamics. Moreover, we find a path to selectively measuring quasiparticle modes directly, as well as controlling over the measurement-induced creation and diffusion of quasiparticles into different momentum states. This lays a foundation for understanding the effects of both experimental approaches for probing many-body systems, but also more speculative directions such as observable consequences of `spontaneous collapse' predictions from novel models of quantum gravity on aspects of the Standard Model.

cond-mat.quant-gas↗

arXiv2026

QDFlow: A Python package for physics simulations of quantum dot devices

Recent advances in machine learning (ML) have accelerated progress in calibrating and operating quantum dot (QD) devices. However, most ML approaches rely on access to large, representative datasets designed to capture the full spectrum of data quality encountered in practice, with both high- and low-quality data for training, benchmarking, and validation, with labels capturing key features of the device state. Collating such datasets experimentally is challenging due to limited data availability, slow measurement bandwidths, and the labor-intensive nature of labeling. QDFlow is an open-source physics simulator for multi-QD arrays that generates realistic synthetic data with ground-truth labels. QDFlow combines a self-consistent Thomas-Fermi solver, a dynamic capacitance model, and flexible noise modules to simulate charge stability diagrams and ray-based data that closely resemble experimental results. With an extensive set of parameters that can be varied and customizable noise models, QDFlow supports the creation of large, diverse datasets for ML development, benchmarking, and quantum device research.}}

cond-mat.mes-hall↗

arXiv2026

Nanofabricated torsion pendulums for tabletop gravity experiments

Measurement of mutual gravitation on laboratory scales is an outstanding challenge and a prerequisite to probing theories of quantum gravity. A leading technology in tabletop gravity experiments is the torsion balance, with limitations due to thermal decoherence. Recent demonstrations of lithographically defined suspensions in thin-film silicon nitride with macroscale test masses suggest a path forward, as torsion pendulums dominated by gravitational stiffness may achieve higher mechanical quality factors through dilution of material losses. Here we demonstrate a 250 micron by 5 mm by 1.8 micron torsion fiber supporting 87 grams and forming a Cavendish-style torsion pendulum with tungsten test masses that -- to our knowledge -- is the largest thin-film silicon-nitride-based oscillator to date. Torsion pendulums with thin-film, nanofabricated suspensions provide a test bed for near-term tabletop experiments probing classical and quantum gravitational interaction between oscillators.

physics.ins-det↗

arXiv2025

In situ calibration of unitary operations during quantum error correction

Quantum error correction uses the measurement of syndromes and classical decoding algorithms to estimate the location and type of errors while protecting the encoded quantum bits. Here we consider how prior information and Bayesian updates can play a critical role in improving the performance of QEC in the scenario of a particularly noisy qubit. This allows for leveraging even distance codes, which typically are less valued in QEC, to handle the noisy qubit, changing the power-law scaling of the logical error rate with the baseline physical error rate. A crucial component of this is updating the prior by real time feeding of decoder outputs into a approximate Kalman filter. Thus our approach provides a bootstrap to the actual error rates. We show this via simulation of the full closed-loop system: starting from uniform priors, the update procedure gradually learns site-specific error rates, enabling the decoder to outperform a fixed-prior baseline. In turn, we show that this enables in situ calibration of unitary operations via injection of gate set tomography operations with only moderate overhead in the more typical scenario of low noise qubits.

quant-ph↗

arXiv2025

Mechanical Sensors for Ultraheavy Dark Matter Searches via Long-range Forces

Dark matter candidates with masses around the Planck-scale are theoretically well-motivated, and it has been suggested that it might be possible to search for dark matter solely via gravitational interactions in this mass range. In this work, we explore the pathway towards searching for dark matter candidates with masses around the Planck-scale using mechanical sensors while considering realistic experimental constraints, and develop analysis techniques needed to conduct such searches. These dark matter particles are expected to leave tracks as their signature in mechanical sensor arrays, and we show that we can effectively search for such tracks using statistical approaches to track-finding. We analyze a range of possible experimental setups and compute sensitivity projections for searches for ultraheavy dark matter coupling to the Standard Model via long-range forces. We find that while a search for Planck-scale dark matter purely via gravitational couplings would be exceedingly difficult, requiring $\sim 80\,\mathrm{dB}$ of quantum noise reduction with a $100^3$ array of devices, there is a wide range of currently unexplored dark matter candidates which can be searched for with already existing or near-term experimental platforms.

hep-ph↗

arXiv2025

Combining quantum noise reduction resources: a practical approach

Optomechanical sensors are capable of transducing external perturbations to resolvable optical signals. A particular regime of interest is that of high-bandwidth force detection, where an impulse is delivered to the system over a short period of time. Exceedingly sensitive impulse detection has been proposed to observe very weak signals like those due to long range interactions with dark matter that require much higher sensitivities than current sensors can provide. Quantum resources to go beyond the traditional standard quantum limit of these sensors include squeezing of the light used to transduce the signal, backaction evasion by measuring the optimal quadrature, and quantum non-demolition (QND) measurements that reduce backaction directly. These methods have been developed in the context of gravitational wave detection for target frequencies in the audio band range. Here, we provide the theoretical limits to quantum noise reduction for higher and broader frequency targets, such as those from dark matter signals, while combining quantum enhanced readout techniques based on squeezed light and QND measurements with optomechanical sensors. We demonstrate that backaction evasion through QND techniques dramatically reduces the technical challenges presented when using squeezed light for broadband force detection, paving the way for combining multiple quantum noise reduction techniques for enhanced sensitivity in the context of impulse metrology.

quant-ph↗

arXiv2025

Accurate and Honest Approximation of Correlated Qubit Noise

Accurate modeling of noise in realistic quantum processors is critical for constructing fault-tolerant quantum computers. While a full simulation of actual noisy quantum circuits provides information about correlated noise among all qubits and is therefore accurate, it is, however, computationally expensive as it requires resources that grow exponentially with the number of qubits. We propose an efficient systematic construction of approximate noise channels, where their accuracy can be enhanced by incorporating noise components with higher qubit-qubit correlation degree. To formulate such approximate channels, we first present a method, dubbed the cluster expansion approach, to decompose the Lindbladian generator of an actual noise channel into components based on interqubit correlation degree. We generate a $k$-th order approximate noise channel by truncating the cluster expansion and incorporating noise components with correlations up to the $k$-th degree. We require that the approximate noise channels must be accurate and also ``honest", i.e., the actual errors are not underestimated in our physical models. As an example application, we apply our method to model noise in a three-qubit quantum processor that stabilizes a [[2,0,2]] codeword, which is one of the four Bell states. We find that, for realistic noise strength typical for fixed-frequency superconducting qubits coupled via always-on static interactions, correlated noise beyond two-qubit correlation can significantly affect the code simulation accuracy. Since our approach provides a systematic characterization of multi-qubit noise correlations, it enables the potential for accurate, honest and scalable approximations to simulate large numbers of qubits from full modeling or experimental characterizations of small enough quantum subsystems, which are efficient yet still retain essential noise features of the entire device.

quant-ph↗

arXiv2025

Entanglement witness for combined atom interferometer-mechanical oscillator setup

We investigate how to entangle an atom interferometer and a macroscopic mechanical oscillator in order to create non-classical states of the oscillator. We propose an entanglement witness, from whose violation, the generation of entanglement can be determined. We do this for both the noiseless case and when including thermal noise. Thermal noise can arise from two sources: the first being when the oscillator starts in a thermal state, and the second when a continuous thermal bath is in contact with the oscillator. We find that for the appropriate oscillator quality factor $Q$, violation always exists for any value of magnetic coupling $λ$ and thermal occupancy $\bar n$. Cooling the oscillator to its ground state provides an $O(\bar n)$ improvement in the EW violation than starting in a thermal state. However, this still requires at least 10$^{5}$ measurements to be determined. We then consider how to use magnetic interactions to realize this idea.

quant-ph↗

arXiv2025

Utilizing discrete variable representations for decoherence-accurate numerical simulation of superconducting circuits

Given the prevalence of superconducting platforms for uses in quantum computing and quantum sensing, the simulation of quantum superconducting circuits has become increasingly important for identifying system characteristics and modeling their relevant dynamics. Various numerical tools and software packages have been developed with this purpose in mind, typically utilizing the harmonic oscillator basis or the charge basis to represent a Hamiltonian. In this work, we instead consider the use of discrete variable representations (DVRs) to model superconducting circuits. In particular, we use `sinc DVRs' of both charge number and phase to approximate the eigenenergies of several prototypical examples, exploring their use and effectiveness in the numerical analysis of superconducting circuits. We find that not only are these DVRs capable of achieving decoherence-accurate simulation, i.e., accuracy at the resolution of experiments subject to decay, decoherence, and dephasing, they also demonstrate improvements in efficiency with smaller basis sizes and better convergence over standard approaches, showing that DVRs are an advantageous alternative for representing superconducting circuits.

quant-ph↗

arXiv2025

On the quantum mechanics of entropic forces

It was conjectured thirty years ago that gravity could arise from the entropic re-arrangement of information. In this paper, we offer a set of microscopic quantum models which realize this idea in detail. In particular, we suggest a simple mechanism by which Newton's law of gravity arises from extremization of the free energy of a collection of qubits or oscillators, rather than from the exchange of virtual quanta of a fundamental field. We give both a local and non-local version of the construction, and show how to distinguish a range of these entropic models from ordinary perturbative quantum gravity using existing observations and near-term experiments.

hep-th↗

arXiv2024

Data needs and challenges for quantum dot devices automation

Gate-defined quantum dots are a promising candidate system for realizing scalable, coupled qubit systems and serving as a fundamental building block for quantum computers. However, present-day quantum dot devices suffer from imperfections that must be accounted for, which hinders the characterization, tuning, and operation process. Moreover, with an increasing number of quantum dot qubits, the relevant parameter space grows sufficiently to make heuristic control infeasible. Thus, it is imperative that reliable and scalable autonomous tuning approaches are developed. This meeting report outlines current challenges in automating quantum dot device tuning and operation with a particular focus on datasets, benchmarking, and standardization. We also present insights and ideas put forward by the quantum dot community on how to overcome them. We aim to provide guidance and inspiration to researchers invested in automation efforts.

cond-mat.mes-hall↗

arXiv2024

Feasibility of a trapped atom interferometer with accelerating optical traps

In order to increase the measured phase of an atom interferometer and improve its sensitivity, researchers attempt to increase the enclosed space-time area using two methods: creating larger separations between the interferometer arms and having longer evolution times. However, increasing the evolution time reduces the bandwidth that can be sampled, whereas decreasing the evolution time worsens the sensitivity. In this paper, we attempt to address this by proposing a setup for high-bandwidth applications, with improved overall sensitivity. This is realized by accelerating and holding the atoms using optical dipole traps. We find that accelerations of up to $10^{3}$-$10^{5}$ m/s$^2$ can be achieved using acousto-optic deflectors (AODs) to move the traps. By comparing the sensitivity of our approach to acceleration as a baseline to traditional atom interferometry, we find a substantial improvement to the state of the art. In the limit of appropriate beam and optics stabilization, sensitivities approaching 10$^{-14}$ (m/s$^2$)/$\sqrt{\rm Hz}$ may be achievable at 1 Hz, while detection at 1 kHz with a sensitivity an order of magnitude better than traditional free-fall atom interferometers is possible with today's systems.

physics.atom-ph↗

arXiv2023

Precision Bounds on Continuous-Variable State Tomography using Classical Shadows

Shadow tomography is a framework for constructing succinct descriptions of quantum states using randomized measurement bases, called classical shadows, with powerful methods to bound the estimators used. We recast existing experimental protocols for continuous-variable quantum state tomography in the classical-shadow framework, obtaining rigorous bounds on the number of independent measurements needed for estimating density matrices from these protocols. We analyze the efficiency of homodyne, heterodyne, photon number resolving (PNR), and photon-parity protocols. To reach a desired precision on the classical shadow of an $N$-photon density matrix with a high probability, we show that homodyne detection requires an order $\mathcal{O}(N^{4+1/3})$ measurements in the worst case, whereas PNR and photon-parity detection require $\mathcal{O}(N^4)$ measurements in the worst case (both up to logarithmic corrections). We benchmark these results against numerical simulation as well as experimental data from optical homodyne experiments. We find that numerical and experimental homodyne tomography significantly outperforms our bounds, exhibiting a more typical scaling of the number of measurements that is close to linear in $N$. We extend our single-mode results to an efficient construction of multimode shadows based on local measurements.

quant-ph↗