add DAG to model converter by guanqin-123 · Pull Request #21 · SVF-tools/ACT

guanqin-123 · 2026-01-17T00:52:58Z

add DAG to torch2act, enable resNet-like networks that has DAG structure that uses torch.fx
processing the nodes should be in the topological order and process the merge points (so added necessary parameter for ADD operator)

yuleisui · 2026-01-17T01:02:56Z

Describe what this pull request is and why we need this one.

yuleisui · 2026-01-17T01:51:43Z


+# -------- Helper Functions --------
+
+def _normalize_to_tuple(value: Union[int, Tuple[int, ...]], n: int = 2) -> Tuple[int, ...]:


It is unclear to me why we need a tuple here. The conversation should be general enough for all types of NNs not only resnet. Also this method should be moved to layer_util if we really need this one.

This patch looks ad hoc. What is difference between previous recursively parse the torch model and dag one? Why do we need a dag parser?

In the previous version, recursive parse doesnot support the skipping, especically with the two incoming edge on the operator concat. The predecessor is always one.
I could do a clean approach on graph-based parsing for once.

Shall we do this in the front-end while building the torch model? Do we need to change the nn.sequential before getting to torch2act.py

By now, I believe we have to change. nn.sequentail cannot fully preserve the information on ResNet. But for the onnx to torch loading, we are using the torch_model, so I think it is ok. It is well preserved the model information.

Is your dag used to convert to nn.sequential? We need a more unified nn.model for both front and back ends then

With the new updates, we already unified to VerifiableModule(nn.Module) which wraps any nn.Module, not just Sequential. The old VerifiableModel(nn.Sequential) with index-based access has been deleted.

Both front-end (fuzzing) and back-end (verification) now use this unified VerifiableModule

yuleisui · 2026-01-17T10:22:46Z

+        self.is_dag_model: bool = False  # Flag for DAG mode
+        self.node_outputs: Dict[str, List[int]] = {}  # node_name -> out_vars
+        self.node_shapes: Dict[str, Tuple[int, ...]] = {}  # node_name -> shape
+        self.node_to_layer_id: Dict[str, int] = {}  # node_name -> layer_id
+        self.graph_edges: Dict[str, List[str]] = {}  # node_name -> [predecessor_node_names]
+        self.fx_graph: Optional[fx.Graph] = None  # torch.fx graph if available
+        self.fx_modules: Dict[str, nn.Module] = {}  # module_name -> module (from traced model)
+
+        # ONNX-specific DAG state (for onnx2pytorch models)
+        self.is_onnx_dag: bool = False  # Flag for ONNX-based DAG mode
+        self.onnx_model: Optional[Any] = None  # ONNX ModelProto
+        self.onnx_graph: Optional[Any] = None  # ONNX GraphProto
+        self.onnx_mapping: Dict[str, Any] = {}  # onnx2pytorch node mapping
+        self.onnx_modules: Dict[str, nn.Module] = {}  # module_name -> module
+        self.onnx_output_to_node: Dict[str, Any] = {}  # output_name -> ONNX node


Better not to create specific fields for DAG and onnx. It would be good to be done in the front-end.

Sure. please check the updated one. We don't need that.

CI failed, need to fix.

yuleisui · 2026-01-18T00:52:14Z

        with torch.no_grad():
            output = model(input_tensor)
-            # Extract tensor if model returns dict (VerifiableModel)
+            # Extract tensor if model returns dict (VerifiableModule)


VerifiableModule => VerifiableModel
make sure all revert this name back.

ok, already replaced back to VerifiableModel

yuleisui · 2026-01-18T01:16:01Z

+# -------- Helper Functions --------
+
+
+def _infer_spatial_from_flat(flat_size: int, channels: int) -> Tuple[int, int]:


It is unclear why we need to revert this flattening, as the tensors have already been flattened before the backend tfs stage. The core ACT net design was supposed to handle flat tensors.

All the helper functions are in layer_util.py.

yes, I believe, we don't need this.

yuleisui · 2026-01-18T01:17:18Z

-    output_spec: OutputSpec
-) -> Tuple[VerifiableModel, WrapReport]:
+    output_spec: OutputSpec,
+) -> Tuple[nn.Module, WrapReport]:


The return should be VerifiableModel as the function name says.

sure, fixed.

yuleisui · 2026-01-18T01:20:53Z

-        model = VerifiableModel(*torch_layers)
-        model.eval()  # Set to evaluation mode by default
+        # Build the core model as nn.Sequential
+        core_model = nn.Sequential(*torch_layers)


Not sure why nn.Sequential still the core model?

I fixed, and now nn.Sequential is discard.

yuleisui · 2026-01-18T01:21:40Z

+      "[ACT] Auto-detecting project root: /data1/guanqin/newACT/fix/ACT\n",
+      "[WARN] Gurobi license not found at: /data1/guanqin/newACT/fix/ACT/modules/gurobi/gurobi.lic\n",
+      "[INFO] Please ensure gurobi.lic is placed in: /data1/guanqin/newACT/fix/ACT/modules/gurobi\n",


remove path information and use relative path.

yuleisui · 2026-01-18T02:49:20Z

+                return False, f"OUTPUT: Misclassified (pred={pred}, true={y_true})"
+        return True, f"OUTPUT: Spec kind {spec.kind} (not checked)"
+
+    def to_net(self):


to_net => to_act_net

yuleisui · 2026-01-18T02:49:36Z

+            self._net = self._build_net()
+        return self._net
+
+    def _build_net(self):


_build_net => _build_act_net

yuleisui · 2026-01-18T02:50:50Z

        net.assert_last_is_validation()
        return net
+
+    def _build_preds_succs_from_tracer(self) -> Tuple[Dict[int, List[int]], Dict[int, List[int]]]:


What does tracer mean here? better to have the explicit and understandable name.

how about _build_layer_graph() ？

where ModelTracer is defined? This function should return act Net?

yuleisui · 2026-01-18T02:51:36Z

@@ -12,27 +12,35 @@
    },
    {
      "cell_type": "code",
-      "execution_count": 1,
+      "execution_count": 2,


need to do local runs for the two ipynb files and update them in the pull request.

it's wired, it passed locally
📊 Final Results:
✅ Conversions: 96/96 (100.0%)

yuleisui · 2026-01-18T03:11:16Z

+
+    def _build_net(self):
+        """Build ACT Net from model and specifications."""
+        from act.pipeline.verification.model_tracer import ModelTracer


what is model_tracer? I didn't find this class

in the forced pushed, losed. now added back.

yuleisui · 2026-01-18T03:48:13Z

+# Purpose:
+#   Traces nn.Module to extract computation graph and convert to ACT layers.
+#   Works with any nn.Module (sequential or DAG structures).
+#
+# Key Features:
+#   - Generic: Works with any nn.Module
+#   - Unified: Single graph-based parsing for both sequential and DAG models
+#   - Supports torch.fx tracing and ONNX fallback for onnx2pytorch models


This looks redundant to me. Could we only include necessary methods in act2torch and remove this file?

It has lots of post-fixing and uncessary alignment which should be fixed either in front-end or during act2torch.

I merged and re-run

yuleisui · 2026-01-18T07:08:45Z

+        # ONNX-specific state (for onnx2pytorch models)
+        self.onnx_model: Optional[Any] = None
+        self.onnx_graph: Optional[Any] = None
+        self.onnx_mapping: Dict[str, Any] = {}
+        self.onnx_modules: Dict[str, nn.Module] = {}
+        self.onnx_output_to_node: Dict[str, Any] = {}


These states can be mapped to all the graph processing states? If so, we could remove these redundant data structures.

ok, now removed

good, this torch2act is an important file. Could you try to optimise and remove any redundancy to make it more readable and robust. It is still a bit complicated now

i used mapped lambda for processing onnx_handlers, nested the converters and added necessary comments

yuleisui · 2026-01-18T07:10:03Z

+        self.onnx_modules: Dict[str, nn.Module] = {}
+        self.onnx_output_to_node: Dict[str, Any] = {}
+
+    def trace(self) -> Tuple[List[Layer], Dict[int, List[int]], Dict[int, List[int]]]:


The name trace looks odd as this is building the graph not dynamic tracing.

still lots of trace keywords and the lambda is unnecessarily complex. Better to simplify the code in torch2act to make it more readable.

yuleisui · 2026-01-18T07:11:57Z

        net.assert_last_is_validation()
        return net
+
+    def _build_layer_graph(self) -> Tuple[Dict[int, List[int]], Dict[int, List[int]]]:


Is this graph strictly a DAG graph? Can the graph have cycles? Please make comments and necessarily assertions if necessary.

i added a _assert_dag function.

yuleisui · 2026-01-18T10:49:10Z

torch2act CI keeps failing, it needs to be fixed.

yuleisui · 2026-01-18T11:10:37Z

For this fuzzer ipynb, there are too many output here and here, try to make output concise.

The counterexample towards the end of this file shows only one image for now. Please add more images and counterexamples. Also make sure when printing the label, not only the number of cifar, but only the name of the class.

I ignored the debug log. the fuzzing before the report can already generate serval counterexamples.

It would be good to also generate counterexamples based on multiple images.

yuleisui · 2026-01-19T03:52:02Z

+      - name: Run Torch2ACT Pipeline Tests - MNIST Simple CNN
        run: |
          cd ${{ github.workspace }}
-          python -m act.pipeline --verify torch2act --device cpu --dtype float64


It looks that many are not exercised in the CI. Could you compare and try to include as many as possible as the previous CI.

🧬 Synthesizing models from 10 spec result(s)...
✓ CIFAR10 + resnet18: Created 24 wrapped model(s)
✓ CIFAR10 + resnet34: Created 24 wrapped model(s)
✓ CIFAR10 + resnet50: Created 24 wrapped model(s)
✓ CIFAR10 + vgg16: Created 24 wrapped model(s)
✓ CIFAR10 + mobilenet_v2: Created 24 wrapped model(s)
✓ CIFAR10 + efficientnet_b0: Created 24 wrapped model(s)
✓ MNIST + simple_cnn: Created 24 wrapped model(s)
✓ MNIST + lenet5: Created 24 wrapped model(s)
✓ MNIST + resnet18: Created 24 wrapped model(s)
✓ MNIST + efficientnet_b0: Created 24 wrapped model(s)

🎉 Synthesized 240 wrapped models from specs!

For now, only skip the Resnet 34 with cifar10. Because it gives a "134" issue from git actions, which is over time indicator.

The CI still failed, and need to be fixed before merging

yuleisui · 2026-01-19T03:54:18Z

try to simplify this file as much as possible, current the file is a bit too large to review.

yuleisui · 2026-01-19T03:57:17Z

+
            try:
-                torch2act.main()
+                _run_torch2act_with_filter(dataset_filter=dataset_filter, model_filter=model_filter)


not sure why we need this filter function if we have data and models specified in the terminal cli.

filter to accept the specific model and dataset.

yuleisui · 2026-01-19T05:52:46Z

@@ -0,0 +1,79 @@
+name: ACT Frontend Tests -2


Is this a testing CI yml? We can only keep on yml for the front-end testing.

revised. leave one only

guanqin-123 · 2026-01-20T10:29:51Z

Finalized in three Phase. Upgrade done.

guanqin-123 commented Jan 17, 2026

View reviewed changes

Comment thread act/back_end/layer_schema.py

yuleisui reviewed Jan 17, 2026

View reviewed changes

guanqin-123 force-pushed the fix branch 2 times, most recently from 9b7e7df to 19fa351 Compare January 18, 2026 00:39