Human-AI Collaboration Discovers Entanglement-Assisted Quantum Code Families Through Evolution

From Finite Constructions to Provable Code Families

LLM-guided program evolution can generate mathematical constructions, but the validity, generality, and reproducibility of these constructions require different types of evidence. A recent study proposes a "researcher-in-the-loop" discovery pipeline that combines program evolution, exact evaluation, mathematical generalization, non-existence certification checks, and formal proof verification, applying it to the discovery of entanglement-assisted quantum error-correcting codes (EAQECCs). This work demonstrates how finite computational discoveries can be transformed into mathematical theorems with independently verifiable evidence, providing a reusable paradigm for AI-assisted mathematical discovery.

Core Method: A Five-Step Evidence Chain

The core of this pipeline lies in constructing a complete evidence chain, where each step has an independent verification mechanism:

1. Program evolution: Starting from a task without a specified family formula, LLM-guided evolutionary algorithms generate candidate programs. These programs output finite qubit constructions rather than direct algebraic expressions.
2. Exact evaluation: The generated constructions undergo precise numerical evaluation to ensure they satisfy the basic parameter requirements of entanglement-assisted quantum error-correcting codes.
3. Mathematical generalization: Researchers analyze the structure of finite constructions and generalize them into general family formulas. In this case, the researchers generalized the structure into the $[[n,1,n-1;n-q-1]]_q$ family, applicable to prime powers $q\ge3$ with $n\ge2q+1$, as well as $q=2$ with odd $n\ge5$.
4. Non-existence certification: Through DRAT proof checking, the non-existence of codes under certain parameters is verified, providing 115 verified code records and 10 non-existence results with checked DRAT proofs.
5. Formal proof verification: The Lean theorem prover is used to check the algebraic certificates behind this family, ensuring the rigor of mathematical derivations.

This multi-layered verification strategy ensures that AI-generated mathematical discoveries no longer remain at the stage of being "interesting but unproven," but instead achieve publication-level rigor.

Entanglement-assisted quantum error-correcting codes (EAQECCs) are a generalization of standard quantum error-correcting codes that allow the encoder and decoder to share pre-entangled qubit pairs (ebits), thereby breaking limitations such as the Singleton bound for standard quantum codes. Their parameters are typically denoted as $[[n,k,d;c]]_q$, where $n$ is the number of physical qubits, $k$ is the number of logical qubits, $d$ is the minimum distance, $c$ is the number of consumed entangled bits, and $q$ is the finite field size. Entanglement assistance can trade for higher encoding efficiency or greater distance, but requires consuming additional entanglement resources, creating a trade-off between coding gain and entanglement overhead. The $[[n,1,n-1;n-q-1]]_q$ family discovered in this study describes a concrete instance of this trade-off.

DRAT (Deletion Resolution Asymmetric Tautology) proofs are a machine-checkable proof format output by SAT solvers. When a solver determines that a Boolean formula is unsatisfiable, it can generate a sequence of clause addition and deletion steps; an independent DRAT checker verifies whether each step preserves satisfiability, thereby confirming that the original formula is indeed unsatisfiable. In this study, the verification of code non-existence is encoded as a SAT problem; if the solver returns "unsatisfiable," its DRAT proof, after checking, serves as a rigorous certificate of non-existence. This is more trustworthy than relying solely on solver output, because the proof can be independently reviewed by third parties without needing to trust the correctness of the solver itself.

The Lean theorem prover is an interactive formal proof assistant based on dependent type theory, whose mathematical library Mathlib covers a large amount of modern mathematics. In Lean, every proof is ultimately translated into a series of inference steps that can be automatically checked by the kernel, so as long as a proof compiles, hidden assumptions or computational errors are ruled out. This study uses Lean to check the algebraic certificates behind this code family, meaning that the derivation of the family formula (not just finite instances) receives formal guarantees. This fills the gap between numerical evaluation and SAT non-existence proofs, giving the generalization step from "finite construction to general family" independently verifiable evidence.

Experimental Data and Performance Comparison

The research team conducted experiments in controlled eight paired generation blocks, comparing the performance of iterative programs selected on validation sets versus independently generated programs on unseen lengths $n=13,15$. Results show that the iterative programs achieved success rates of 46.1% and 31.6% in held-out executions, while independently generated programs achieved only 19.5% and 3.1%. This significant difference indicates that program evolution combined with researcher analysis can effectively improve the generalization ability of discoveries.

Furthermore, combined with entanglement boosting techniques, this code family filled 54 gaps in the archived EAQECC table. These results not only validate the effectiveness of the method but also demonstrate the practical contribution of AI in mathematical construction discovery.

Iterative versus independent generation in program evolution are two different search paradigms. Independent generation means running the evolutionary algorithm from scratch each time, with no information sharing between runs; iterative programs use the best-performing candidate program from the previous round's validation set as the starting point for the next round, progressively accumulating effective structures. The difference in success rates on unseen lengths (46.1% vs 19.5%, 31.6% vs 3.1%) reflects the generalization advantage brought by the iterative mechanism: the program does not memorize constructions for specific $n$, but learns transferable construction patterns. This comparative design controls for generation length, allowing the success rate difference to be attributed to the evolutionary strategy rather than task difficulty.

Reproducibility and Evidence Release

The study emphasizes reproducibility and has released a complete evidence package, including:

• 115 verified code records
• 10 non-existence results with checked DRAT proofs
• Family implementation code
• Preserved search programs for exact checking and seeded replay

This open evidence approach enables other researchers to independently verify the results and conduct further exploration on this basis.

Significance and Outlook

This work combines LLM-guided program evolution with rigorous formal verification, providing a viable path for AI-assisted mathematical discovery. The researcher-in-the-loop pipeline leverages AI's advantages in search space exploration while preserving the critical role of human researchers in pattern recognition and mathematical generalization. As formal tools mature and LLM capabilities improve, similar pipelines are expected to be applied to broader mathematical domains, accelerating the transformation from computational experiments to mathematical theorems.

One-line Summary

A researcher-in-the-loop pipeline combines LLM program evolution with formal verification to discover provable quantum code families.

Paragraph Summary

This study proposes a "researcher-in-the-loop" discovery pipeline that chains LLM-guided program evolution, exact numerical evaluation, mathematical generalization, DRAT non-existence certification, and Lean formal proof checking into a five-step evidence chain, applied to the discovery of entanglement-assisted quantum error-correcting codes. Researchers distilled the $[[n,1,n-1;n-q-1]]_q$ family from finite constructions, covering prime powers $q\ge3$ with $n\ge2q+1$ and $q=2$ with odd $n\ge5$. Experiments show that iterative programs achieve significantly higher success rates on unseen lengths than independently generated programs, and combined with entanglement boosting techniques, filled 54 gaps in the archived EAQECC table. The study released 115 verified code records, 10 non-existence results with DRAT proofs, and replayable search programs, providing a reproducible paradigm for AI-assisted mathematical discovery.