Technical Summary: Data Verification is the Future of Quantum Computing Copilots

Problem Statement

The generation and compilation of quantum programs require a level of precision that conflicts with the statistical reasoning inherent in Large Language Models (LLMs). Quantum computing tasks involve crossing multiple abstraction layers (from high-level circuit descriptions to low-level gate arrangements) and adhering to rigorous mathematical constraints (e.g., unitarity, hardware topology, gate fidelity). Unlike natural language tasks where errors can be tolerated or averaged out, quantum program generation demands zero tolerance for errors; a single invalid gate sequence violates fundamental physical laws.

Current LLM-based approaches face three critical limitations:

1. Infeasible Solutions: Without data verification, infeasible solutions are mathematically inevitable due to the statistical nature of LLMs, regardless of model scaling.
2. Data Scarcity: Comprehensive, verified quantum datasets are extremely difficult to generate. Existing datasets (e.g., QDataSet) required months of HPC time to cover only small systems (1-2 qubits).
3. Search Space Constraints: The valid subspace of quantum circuits is exponentially small compared to the total design space, bounded by unitarity and hardware constraints. Current LLM architectures cannot internally provide the necessary verification mechanisms to navigate this space.

Methodology and Framework

The paper proposes a paradigm shift from "inference-only" or "post-hoc filtering" to verification-first architectures. The authors define three core positions supported by theoretical arguments and preliminary experiments:

1. Data Verification as a Minimum Requirement (P1)

The authors argue that training data must be formally verified before inclusion in the training set.

• Concept: A "Verification-aware model" is trained exclusively on data where every example satisfies domain-specific correctness constraints (e.g., proven via automated theorem provers like Lean or Z3).
• Rationale: Training on unverified data (e.g., low-quality code repositories) constitutes "implicit data poisoning." Unlike natural language, where massive data volumes average out noise, a single invalid example in quantum circuit data violates unitarity regardless of surrounding valid examples. This leads to an "anti-scaling" phenomenon where more unverified data amplifies errors rather than diluting them.
• Mechanism: Verified datasets allow models to internalize constraints as learned structures rather than statistical approximations.

2. A Priori Constraints over A Posteriori Filtering (P2)

Verification must constrain the generation process before output, rather than filtering outputs after generation.

• Rationale: In quantum circuit design, the fraction of valid designs decreases exponentially as the number of components (qubits/gates) increases. For a design space growing as $O(d^n)$, constraints reduce valid designs to $O(\delta^n)$ where $\delta < d$.
• Consequence: Relying on post-hoc filtering (generating many candidates and rejecting invalid ones) incurs exponential computational costs and has a vanishingly low probability of success. Verification must be embedded as an architectural primitive to prevent invalid paths during token generation.

3. Verification-First Paradigm for AI4Research (P3)

The authors advocate extending this verification-first approach to other scientific domains governed by physical laws or mathematical axioms (e.g., drug discovery, materials science, engineering design).

• Concept: These domains share "leaky abstraction" and "non-decomposability" issues, where locally optimal choices do not guarantee global optimality. Verification-aware architectures are necessary to handle these hard constraints.

Experimental Results

To substantiate Position 1, the authors conducted an evaluation using a dataset derived from verified MAJ/UMA (Majority/UnMajority-and-Add) circuit corpora.

• Setup: 34 publicly available LLMs (ranging from 270M to 120B parameters) were tested on 70,000 multiple-choice questions regarding quantum adder optimization (2 to 8 qubits). The ground truth was the circuit with the minimum weighted score of Toffoli count, depth, and total gates.
• Accuracy: Models trained or fine-tuned with verification knowledge (e.g., gemma3:12b, gpt-oss:120b) achieved accuracy between 0.60 and 0.79. In contrast, generic models without verification awareness hovered near the random baseline (0.21–0.29).
• Calibration: Verification-aware models demonstrated superior uncertainty quantification. gpt-oss models assigned 60–80% confidence to correct answers, whereas gemma3 models remained in the 20–35% range.
• Failure Modes: Several models (e.g., mixtral:8x7b, deepseek-r1 variants) scored below the random baseline due to malformed outputs (verbose refusals or explanations instead of single-letter answers), reinforcing that without verification training, models cannot reliably engage with formally constrained tasks.
• Search Space Analysis: The authors generated a dataset of 200,000 verified adder designs. They noted that while the total possible gate arrangements for MAJ/UMA modules across depths 3–6 exceed 148 trillion configurations, formal verification identified only ~200,000 valid designs (a ratio of $\approx 10^{-9}$), illustrating the prohibitive nature of post-hoc filtering.

Key Contributions

1. Formal Definition of Verification-Aware Models: Distinguishing between models trained on verified constraints versus those trained on unverified code repositories.
2. Three Core Positions: Establishing that data verification is a minimum requirement, that constraints must be a priori, and that this paradigm is essential for scientific AI.
3. Empirical Evidence: Providing quantitative data showing that without data verification, LLMs fail to achieve high accuracy or proper calibration on quantum optimization tasks, regardless of parameter scale.
4. Identification of "Leaky Abstraction": Highlighting how quantum program generation requires merging abstraction levels (e.g., module design vs. gate decomposition) in ways that make local optimization insufficient for global correctness.

Significance and Future Directions

The paper argues that for AI to be viable in domains governed by strict physical or mathematical laws, verification must be elevated from an "afterthought" to an "architectural foundation."

The authors propose two specific future research directions:

• FD1 (Architecture): Quantum copilot architectures must integrate formal verification (e.g., Satisfiability Modulo Theories or symbolic specifications) directly into the LLM's token generation loop, transforming verification from a binary filter into a structured exploration guide.
• FD2 (Benchmarks): The community needs constraint-rich benchmarks paired with executable verification oracles. These should extend beyond simple adders to include modular multiplication, quantum Fourier transforms, and hardware-specific routing, enabling reproducible standards for cross-system comparison.

The paper concludes that while the arguments focus on quantum computing, the principles apply broadly to any field where correctness is binary, valid solutions occupy an exponentially small subspace, and formal verification methods exist.