Integrate `tqec` with `LaSsynth`

[inmzhang]

Is your feature request related to a problem? Please describe.

What is LaSsynth?

LaSsynth is a synthesis for lattice surgery subroutines. After specifying the desired inputs/outputs ports and the stabilizer flows, it will use a SAT solver to solve the internal structure of the lattice surgery construction under limited spacetime volume. You can take a look at this demo to learn more about it.

Why is it useful for tqec?

1. LaSsynth provides a way to automatically construct a valid spacetime model but can not run simulations for it. Then it's natural to take the output of LaSsynth as the input of tqec to run and verify the construction at the circuit level.
2. LaSsynth provides a text format representation(LaSre) of the spacetime model and it can be taken as a starting point for the design of a portable text format of tqec computation structure.
3. LaSsynth provides the functionality to convert a LaSre file to a .gltf model and visualized the model as well as the correlation surfaces.
4. LaSsynth provides the functionality to convert a LaSre file to the corresponding zx diagrams(using stimzx) representation and verify the the stabilizer flows.

How it can be used with tqec?

LaSsynth provides a representation of the Lattice Surgery subroutine in a text format called LaSre.

LaSre of CNOT

It can be seen as a complete description of the structure of a 3D spacetime model or our BlockGraph. To be more specific:

• n_i/j/ks specify the the spacetime volume
• n_p/ports/port_cubes specify the number and positions of inputs/outputs of the subroutine. And these ports can corresponds to the virtual cubes in the BlockGraph.
• n_s/stabs specifies the stabilizer flow generators. The concept of the stabilizer flow translates naturally to the correlation surface in the lattice surgery model. And it relates to the existing correlation subgraphs in BlockGraph.
• ExistI/J/K specifies the positions of block structures including the cubes and pipes.
• ColorI/J specifies the type of the block structures.
• CorrIJ... specifies the explicit correlation surfaces presented in each pipe for each stabilizer flows.
• NodeY specifies the existence of the Y basis initialization/measurements, which currently is not implemented in tqec but is planned for sure.

As above, the one-to-one translation between LaSre and BlockGraph should be possible.

Limitations

To integrate the two libraries, there are some problems that we need to solve in my mind:

• Spatial Hadamard in LaSynth is not allowed by default, but can be enabled with some changes to the code.
• Y cubes need to be implemented in tqec, or turn off the option for now.
• If we want to use LaSre to represent the BlockGraph, we need to be able to fill the ports with actual cubes, which corresponds to logical initialization/measurements that instantiate a subroutine into a real computation.

[nelimee]

I agree that this would be a very sensible and interesting addition. It might be too soon though. In my opinion, here are the steps we should focus on right now:

1. Have a fully working logical CNOT computation. This has been our main goal since the beginning, we are very close now, so we should prioritize as much as possible that goal.
2. Clean up the code, removing/simplifying/refactoring everything to have a clean code base that can still output a fully functional CNOT. This includes (non-exhaustive):
   • Template refactoring,
   • A huge documentation and testing improvement,
   • Removing now useless code,
3. Implement new features with the stabilized and cleaned-up code base.

I think this feature is 1) not needed for the completion of our first goal and 2) can wait until we finished cleaning up the codebase. An argument for implementing that now (instead of waiting) is that this feature is, at its core, "just" a translator from LaSre to BlockGraph, which only requires the API to create a BlockGraph instance (i.e., a small portion of the API) and so might not be impacted too much by a refactor. Any opinion?

[inmzhang]

Yes this should not be a goal for the near term and I should note that in the first place. I had conversation with Austin about LaSsynth some times ago but forgot to write it up as an issue... And I do think it won't take too much work to implement this feature after finalizing and refactoring our library.

[afowler]

Would be great to get you to review the current status of this tool in a future meeting.

On Tue, Sep 3, 2024 at 12:27 AM Yiming Zhang @.***> wrote:

Yes this should not be a goal for the near term and I should note that in the first place. I had conversation with Austin about LaSsynth some times ago but forgot to write it up as an issue... And I do think it won't take too much work to implement this feature after finalizing and refactoring our library.

— Reply to this email directly, view it on GitHub https://github.com/QCHackers/tqec/issues/315#issuecomment-2325791640, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKAXTF4ZMFE7SV63K4VI33ZUVQH7AVCNFSM6AAAAABNRFITYCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMRVG44TCNRUGA . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[pranshiusc]

@nelimee Can I start looking into this issue, I understand it is marked as future enhancement but maybe I can get accustomed to the tool

[inmzhang]

@nelimee Can I start looking into this issue, I understand it is marked as future enhancement but maybe I can get accustomed to the tool

Several possible integration points in my mind:

1. Read LaSsynth’s output format and convert it into a BlockGraph for simulation.
2. Convert a BlockGraph into LaSsynth’s format to optimize spacetime volume or use its gltf visualization module to write the BlockGraph to gltf.
3. Use LaSsynth to do "block synthesis" that construct a valid BlockGraph from a reduced PyZX graph.

[inmzhang]

I've spent some time experimenting with LaSsynth and will document my tests and thoughts here.

Brief Introduction

Given the port positions, the bounding box of the block graph, and the stabilizer flows that should be supported at the ports, LaSsynth builds an SMT model, which can then be solved to synthesize a block graph.

Experiments

I've run some basic experiments with LaSsynth, including the synthesis of a logical CNOT, CZ gate, and the Steane encoding circuit. For this write-up, I'll use the Steane encoding circuit as an example.

First, there's a constraint that LaSsynth imposes by default: the spatial pipes do not support Hadamard effects. However, this isn't the case in tqec. I forked the source code and made slight modifications to expose the option for allowing spatial Hadamard operations through the public interface. The fork can be found here.

With spatial Hadamard enabled, LaSsynth omits the colors of the cubes and pipes, only synthesizing the valid topological structure of the computation. Its default color assignment method in the post-processing script does not work for spatial pipes. Using the uncolored output in LaSRe format, I wrote some (untested and messy) code to infer the color of the blocks and generate a BlockGraph in tqec. The code can be found here. The synthesized blocks can then be visualized using view_as_html() in tqec, and we can even verify their correctness by computing the correlation surface.

For the Steane encoding circuit, the following script can synthesize a block graph with all 7 output ports positioned at the top of the graph.

import subprocess
from pathlib import Path
from typing import Any

from lassynth import LatticeSurgerySynthesizer
from tqec.interop.lassynth.lasre import convert_lasre_to_block_graph


def resolve_kissat_path():
    """Resolves the path to the kissat binary using the 'which' command.

    Returns:
      str: The path to the kissat binary, or None if not found.
    """
    try:
        result = subprocess.run(
            ["which", "kissat"], capture_output=True, text=True, check=True
        )
        return str(Path(result.stdout.strip()).resolve().parent)
    except subprocess.CalledProcessError:
        return None

subroutine = "steane"
input_dict: dict[str, Any] = {"max_i": 3, "max_j": 3, "max_k": 4}
input_dict["ports"] = [
    {"location": [0, 0, 4], "direction": "-K", "z_basis_direction": "J"},
    {"location": [1, 0, 4], "direction": "-K", "z_basis_direction": "J"},
    {"location": [2, 0, 4], "direction": "-K", "z_basis_direction": "J"},
    {"location": [0, 2, 4], "direction": "-K", "z_basis_direction": "J"},
    {"location": [1, 2, 4], "direction": "-K", "z_basis_direction": "J"},
    {"location": [2, 2, 4], "direction": "-K", "z_basis_direction": "J"},
    {"location": [0, 1, 4], "direction": "-K", "z_basis_direction": "J"},
]
input_dict["stabilizers"] = [
    "XXXX...",
    "XX..XX.",
    "X.X.X.X",
    "ZZZZ...",
    "ZZ..ZZ.",
    "Z.Z.Z.Z",
]

if __name__ == "__main__":
    # Resolve kissat path
    kissat_path = resolve_kissat_path()
    solver = "kissat" if kissat_path is not None else "picosat"

    las_synth = LatticeSurgerySynthesizer(
        solver=solver,
        kissat_dir=kissat_path,
    )
    result = las_synth.optimize_depth(
        specification=input_dict, color_ij=False, start_depth=2
    )
    assert result is not None
    result = result.after_default_optimizations()
    result.save_lasre(f"{subroutine}.lasre.json")
    bg = convert_lasre_to_block_graph(f"{subroutine}.lasre.json")
    bg.view_as_html(
        f"{subroutine}.html",
    )

Thoughts

• LaSsynth is a solid tool for synthesizing a BlockGraph that can be simulated in tqec.
• It requires specifying the port positions and bounding box of the graph, which can be difficult without a baseline design. Additionally, the mapping between stabilizer operators and ports can vary with permutations, which can significantly affect synthesis results.
• It does not try to minimize the "real" spatice time volume, which is the spacetime occupied by the cubes. That means it can synthesis multiple different structures when alternating the random seeds for the solver.
• Since it relies on solving a SAT problem, its scalability may become an issue. The speed is fast for small-scale, satisfiable problems, but can slow down for large or unsatisfiable ones.
• If a ZX diagram representation of a computation already exists, LaSsynth doesn’t utilize the information provided by the ZX diagram, except for the stabilizer flows at the ports. This isn't an issue for Clifford circuits, as ZX diagrams can easily be constructed from stabilizer flows, providing no extra information. However, for non-Clifford circuits, the ZX diagram and its computed structured Pauli webs/correlation surface could offer additional insights. This remains an open problem worth exploring.

Useful Links

• Paper: https://arxiv.org/abs/2404.18369
• Introduction Video: https://www.youtube.com/watch?v=tp0mh-MHglk&t=1947s
• Source code: https://github.com/quantumlib/Stim/tree/main/glue/lattice_surgery

[qu-tan-um]

Reproduce the construction on Slide 94? I tried the following spec:

input_dict: dict[str, Any] = {"max_i": 5, "max_j": 3, "max_k": 2, "optional": {}}
input_dict["ports"] = [
    {"location": [3, 1, 2], "direction": "-K", "z_basis_direction": "I"},
    {"location": [4, 1, 2], "direction": "-K", "z_basis_direction": "I"},
    {"location": [4, 0, 2], "direction": "-K", "z_basis_direction": "I"},
    {"location": [2, 1, 2], "direction": "-K", "z_basis_direction": "I"},
    {"location": [1, 1, 2], "direction": "-K", "z_basis_direction": "I"},
    {"location": [2, 0, 2], "direction": "-K", "z_basis_direction": "I"},
    {"location": [0, 1, 2], "direction": "-K", "z_basis_direction": "I"},
]

input_dict["stabilizers"] = [
    "XXXX...",
    "ZZ..Z..",
    "Z.Z..Z.",
    "Z..Z..Z",
    ".XX.XX.",
    "..XX.XX",
    "....ZZZ",
]
input_dict["optional"]["forbidden_cubes"] = [
    [0,0,0], [1,0,0], [2,0,0], [3,0,0], [4,0,0],
    [0,1,0], [0,2,0], [1,2,0], [2,2,0], [3,2,0], [4,2,0], [4,2,1]
]

[HaoTy]

I wrote some (untested and messy) code to infer the color of the blocks and generate a BlockGraph in tqec. The code can be found here.

Thanks for writing the conversion function! I feel LaSsynth is a very suitable alternative/complement to the greedy ZX->3D algorithm currently being developed, and I hope this integration can make its way to main.

I want to report two corner cases not handled by the current implementation.

1. BFS from only one of ports won't work when the graph has multiple connected components, which may originate from, for example, an idling qubit. https://github.com/tqec/tqec/blob/0bc57c93dab028954d01ab985a6b8d81e5e3d15f/src/tqec/interop/lassynth/lasre.py#L78-L80

2. LaSsynth may produce a an output where a NodeY is connected to two K pipes. This should translate to two Y cubes connecting to the pipe above and below, respectively, but currently only converts to one Y cube (see the leftmost pipe below), rendering the graph invalid.

[jbolns]

Replying due to mention of #523 . Can LaSynth produce a graph made of nodes with standard ZX type and edges, with additional information tied to either a/several nodes or a/several edges?

If so, the solution to this issue might be the same solution than for PyZX.

[HaoTy]

Can LaSynth produce a graph made of nodes with standard ZX type and edges, with additional information tied to either a/several nodes or a/several edges?

LaSsynth's output is a description of the cubes and pipes of the synthesized lattice surgery operations, similar to a BlockGraph, so it may be easier to convert it to the latter directly instead of relying on ZX graphs (though LaSsynth can also generate StimZX graphs). The conversion function linked above already achieves this goal in most cases.

[inmzhang]

Replying due to mention of #523 . Can LaSynth produce a graph made of nodes with standard ZX type and edges, with additional information tied to either a/several nodes or a/several edges?

If so, the solution to this issue might be the same solution than for PyZX.

As Tianyi noted above, LaSsynth's output can be viewed as equivalent to a BlockGraph. It does not contain more structural information about the corresponding ZX graph than what is already represented in a block graph.

[jbolns]

Yeah, that makes sense. I also just re-read the mention of the issue. I read it wrong, initially.

though LaSsynth can also generate StimZX graphs

... Based on figure 12 in the paper, it's technically feasible to get a ZX graph out of it, but if it can give a (or almost a) blockgraph, it 100% makes sense to want a more direct route.