8 papers
Quantum Cryptography and Autoformalization in Lean
Maor Ben Shahar, Jonathan Morag, Dirk Englund +1
Quantum key distribution provides secure communication by relying on physics principles and mathematical reasoning. Security proofs across the field can contain gaps, often between…
AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics
Weichen Winston Yin, Jacob M. Taylor, Dirk R. Englund +1
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 o…
From Pixels to PCells: A Neurosymbolic Approach to Photonic Component Creation
Aadarsh Agarwal, Kenaish Al Qubaisi, Dirk Englund
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 languag…
Agentic AI for Scalable and Robust Optical Systems Control
Zehao Wang, Mingzhe Han, Wei Cheng +12
We present AgentOptics, an agentic AI framework for high-fidelity, autonomous optical system control built on the Model Context Protocol (MCP). AgentOptics interprets natural langu…
Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics
Benjamin Breen, Marco Del Tredici, Jacob McCarran +6
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 collab…
LightCode: Compiling LLM Inference for Photonic-Electronic Systems
Ryan Tomich, Zhizhen Zhong, Dirk Englund
The growing demand for low-latency, energy-efficient inference in large language models (LLMs) has catalyzed interest in heterogeneous architectures. While GPUs remain dominant, th…
Hardware Co-Designed Optimal Control for Programmable Atomic Quantum Processors via Reinforcement Learning
Qian Ding, Dirk Englund
Developing scalable, fault-tolerant atomic quantum processors requires precise control over large arrays of optical beams. This remains a major challenge due to inherent imperfecti…
Time-keeping with electron spin states in diamond
Jonathan S. Hodges, Dirk Englund
Frequency standards based on atomic states, such as Rb or Cs vapors, or single trapped ions, are the most precise measures of time. Here we introduce a complementary device based o…