Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 24 additions & 2 deletions .github/workflows/act-frontend.yml
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,29 @@ jobs:
cd ${{ github.workspace }}
python -m act.pipeline --verify act2torch --device cpu --dtype float64

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

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@guanqin-123 guanqin-123 Jan 19, 2026 •

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🧬 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.

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

python -m act.pipeline --verify torch2act --device cpu --dtype float64 --dataset MNIST --model simple_cnn

- name: Run Torch2ACT Pipeline Tests - MNIST ResNet18
run: |
cd ${{ github.workspace }}
python -m act.pipeline --verify torch2act --device cpu --dtype float64 --dataset MNIST --model resnet18

- name: Run Torch2ACT Pipeline Tests - MNIST EfficientNet family
run: |
cd ${{ github.workspace }}
python -m act.pipeline --verify torch2act --device cpu --dtype float64 --dataset MNIST --model efficientnet_b0
python -m act.pipeline --verify torch2act --device cpu --dtype float64 --dataset MNIST --model lenet5

- name: Run Torch2ACT Pipeline Tests - CIFAR10 - EfficientNet family
run: |
cd ${{ github.workspace }}
python -m act.pipeline --verify torch2act --device cpu --dtype float64 --dataset CIFAR10 --model efficientnet_b0
python -m act.pipeline --verify torch2act --device cpu --dtype float64 --dataset CIFAR10 --model mobilenet_v2

- name: Run Torch2ACT Pipeline Tests - CIFAR10 - ResNet18
run: |
cd ${{ github.workspace }}
python -m act.pipeline --verify torch2act --device cpu --dtype float64 --dataset CIFAR10 --model resnet18
145 changes: 67 additions & 78 deletions act/back_end/interval_tf/tf_cnn.py
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,10 @@

import torch
import torch.nn.functional as F
from typing import List, Tuple
from typing import List, Tuple, Union
from act.back_end.core import Bounds, Con, ConSet, Fact, Layer
from act.back_end.utils import affine_bounds, pwl_meta, bound_var_interval, scale_interval
from act.back_end.layer_util import normalize_to_tuple


def tf_conv2d(L: Layer, Bin: Bounds) -> Fact:
Expand All @@ -26,46 +27,37 @@ def tf_conv2d(L: Layer, Bin: Bounds) -> Fact:
# Extract convolution parameters
weight = L.params["weight"] # [out_channels, in_channels, kernel_h, kernel_w]
bias = L.params.get("bias", None)
stride = L.meta.get("stride", 1)
padding = L.meta.get("padding", 0)
dilation = L.meta.get("dilation", 1)
stride = normalize_to_tuple(L.meta.get("stride", 1), 2)
padding = normalize_to_tuple(L.meta.get("padding", 0), 2)
dilation = normalize_to_tuple(L.meta.get("dilation", 1), 2)
groups = L.meta.get("groups", 1)

# Normalize stride/padding/dilation to tuples
if isinstance(stride, int):
stride = (stride, stride)
if isinstance(padding, int):
padding = (padding, padding)
if isinstance(dilation, int):
dilation = (dilation, dilation)

# Get weight dimensions
out_channels, in_channels_per_group, kernel_h, kernel_w = weight.shape
in_channels = in_channels_per_group * groups

# Get ACTUAL input size from bounds (not metadata - metadata may be wrong!)
actual_input_size = Bin.lb.numel()

# Infer spatial dimensions from actual input size
spatial_size = actual_input_size // in_channels
in_h = in_w = int(spatial_size ** 0.5) # Assume square initially
# Require input_shape in metadata (4D: batch, channels, height, width)
if "input_shape" not in L.meta or len(L.meta["input_shape"]) != 4:
raise ValueError(
f"CONV2D layer {L.id} requires 'input_shape' metadata with 4 dimensions. "
f"Got: {L.meta.get('input_shape', 'missing')}"
)

# Verify and adjust if needed
if in_h * in_w * in_channels != actual_input_size:
# Try to find correct rectangular dimensions
for h in range(int(spatial_size ** 0.5) + 10, 0, -1):
if spatial_size % h == 0:
in_h = h
in_w = spatial_size // h
if in_h * in_w * in_channels == actual_input_size:
break
meta_input_shape = tuple(L.meta["input_shape"])
_, _, in_h, in_w = meta_input_shape

# Construct input_shape with in_channels from weight tensor (ensures consistency)
input_shape = (1, in_channels, in_h, in_w)

# Compute output dimensions using standard conv formula
out_h = (in_h + 2 * padding[0] - dilation[0] * (kernel_h - 1) - 1) // stride[0] + 1
out_w = (in_w + 2 * padding[1] - dilation[1] * (kernel_w - 1) - 1) // stride[1] + 1
output_shape = (1, out_channels, out_h, out_w)
# Use metadata output shape if available, otherwise compute
if "output_shape" in L.meta and len(L.meta["output_shape"]) == 4:
output_shape = tuple(L.meta["output_shape"])
_, _, out_h, out_w = output_shape
else:
# Compute output dimensions using standard conv formula
out_h = (in_h + 2 * padding[0] - dilation[0] * (kernel_h - 1) - 1) // stride[0] + 1
out_w = (in_w + 2 * padding[1] - dilation[1] * (kernel_w - 1) - 1) // stride[1] + 1
output_shape = (1, out_channels, out_h, out_w)

# Create equivalent linear transformation matrix using im2col
# This converts the convolution to matrix multiplication
Expand Down Expand Up @@ -340,9 +332,9 @@ def _conv2d_to_linear_matrix(
weight: torch.Tensor,
input_shape: Tuple[int, ...],
output_shape: Tuple[int, ...],
stride: int = 1,
padding: int = 0,
dilation: int = 1,
stride: Union[int, Tuple[int, ...]] = 1,
padding: Union[int, Tuple[int, ...]] = 0,
dilation: Union[int, Tuple[int, ...]] = 1,
groups: int = 1
) -> torch.Tensor:
"""
Expand All @@ -361,13 +353,15 @@ def _conv2d_to_linear_matrix(
# Initialize the equivalent weight matrix
W_equiv = torch.zeros(output_flat_size, input_flat_size, dtype=weight.dtype, device=weight.device)

# Convert stride, padding, dilation to tuples if they're integers
if isinstance(stride, int):
stride = (stride, stride)
if isinstance(padding, int):
padding = (padding, padding)
if isinstance(dilation, int):
dilation = (dilation, dilation)
# Normalize stride, padding, dilation to tuples
stride = normalize_to_tuple(stride, 2)
padding = normalize_to_tuple(padding, 2)
dilation = normalize_to_tuple(dilation, 2)

# Handle grouped convolutions
# Weight shape is [out_channels, in_channels_per_group, kH, kW]
in_channels_per_group = in_channels // groups
out_channels_per_group = out_channels // groups

# For each output position, find corresponding input positions
for out_c in range(out_channels):
Expand All @@ -376,8 +370,8 @@ def _conv2d_to_linear_matrix(
# Calculate output linear index
out_idx = out_c * (out_h * out_w) + out_y * out_w + out_x

# For each kernel position
for in_c in range(in_channels):
# For each kernel position - loop only over channels within the group
for in_c in range(in_channels_per_group):
for k_y in range(kernel_h):
for k_x in range(kernel_w):
# Calculate input position
Expand All @@ -386,10 +380,14 @@ def _conv2d_to_linear_matrix(

# Check bounds
if 0 <= in_y < in_h and 0 <= in_x < in_w:
# Calculate input linear index
in_idx = in_c * (in_h * in_w) + in_y * in_w + in_x
# Calculate actual input channel with group offset
group_idx = out_c // out_channels_per_group
actual_in_c = group_idx * in_channels_per_group + in_c

# Calculate input linear index using actual input channel
in_idx = actual_in_c * (in_h * in_w) + in_y * in_w + in_x

# Set weight in equivalent matrix
# Use local in_c for weight access (weight has in_channels_per_group)
W_equiv[out_idx, in_idx] = weight[out_c, in_c, k_y, k_x]

return W_equiv
Expand Down Expand Up @@ -450,9 +448,9 @@ def tf_avgpool2d(L: Layer, Bin: Bounds) -> Fact:
def _avgpool2d_to_linear_matrix(
input_shape: Tuple[int, ...],
output_shape: Tuple[int, ...],
kernel_size: int,
stride: int,
padding: int
kernel_size: Union[int, Tuple[int, ...]],
stride: Union[int, Tuple[int, ...]],
padding: Union[int, Tuple[int, ...]]
) -> torch.Tensor:
"""Convert AvgPool2d to equivalent linear transformation matrix."""
batch_size, channels, in_h, in_w = input_shape
Expand All @@ -463,12 +461,10 @@ def _avgpool2d_to_linear_matrix(

W_equiv = torch.zeros(output_flat_size, input_flat_size)

if isinstance(kernel_size, int):
kernel_size = (kernel_size, kernel_size)
if isinstance(stride, int):
stride = (stride, stride)
if isinstance(padding, int):
padding = (padding, padding)
# Normalize to tuples
kernel_size = normalize_to_tuple(kernel_size, 2)
stride = normalize_to_tuple(stride, 2)
padding = normalize_to_tuple(padding, 2)

kernel_h, kernel_w = kernel_size

Expand Down Expand Up @@ -746,9 +742,9 @@ def _conv3d_to_linear_matrix(
weight: torch.Tensor,
input_shape: Tuple[int, ...],
output_shape: Tuple[int, ...],
stride: int = 1,
padding: int = 0,
dilation: int = 1,
stride: Union[int, Tuple[int, ...]] = 1,
padding: Union[int, Tuple[int, ...]] = 0,
dilation: Union[int, Tuple[int, ...]] = 1,
groups: int = 1
) -> torch.Tensor:
"""Convert Conv3d to equivalent linear transformation matrix."""
Expand All @@ -762,13 +758,10 @@ def _conv3d_to_linear_matrix(

kernel_d, kernel_h, kernel_w = weight.shape[2], weight.shape[3], weight.shape[4]

# Handle stride/padding as tuples or ints
if isinstance(stride, int):
stride = (stride, stride, stride)
if isinstance(padding, int):
padding = (padding, padding, padding)
if isinstance(dilation, int):
dilation = (dilation, dilation, dilation)
# Normalize stride/padding/dilation to tuples
stride = normalize_to_tuple(stride, 3)
padding = normalize_to_tuple(padding, 3)
dilation = normalize_to_tuple(dilation, 3)

for out_c in range(out_channels):
for out_d_idx in range(out_d):
Expand Down Expand Up @@ -802,10 +795,10 @@ def _convtranspose2d_to_linear_matrix(
weight: torch.Tensor,
input_shape: Tuple[int, ...],
output_shape: Tuple[int, ...],
stride: int = 1,
padding: int = 0,
output_padding: int = 0,
dilation: int = 1,
stride: Union[int, Tuple[int, ...]] = 1,
padding: Union[int, Tuple[int, ...]] = 0,
output_padding: Union[int, Tuple[int, ...]] = 0,
dilation: Union[int, Tuple[int, ...]] = 1,
groups: int = 1
) -> torch.Tensor:
"""Convert ConvTranspose2d to equivalent linear transformation matrix."""
Expand All @@ -819,15 +812,11 @@ def _convtranspose2d_to_linear_matrix(

kernel_h, kernel_w = weight.shape[2], weight.shape[3]

# Handle stride/padding as tuples or ints
if isinstance(stride, int):
stride = (stride, stride)
if isinstance(padding, int):
padding = (padding, padding)
if isinstance(output_padding, int):
output_padding = (output_padding, output_padding)
if isinstance(dilation, int):
dilation = (dilation, dilation)
# Normalize stride/padding/dilation to tuples
stride = normalize_to_tuple(stride, 2)
padding = normalize_to_tuple(padding, 2)
output_padding = normalize_to_tuple(output_padding, 2)
dilation = normalize_to_tuple(dilation, 2)

# Transpose convolution: each input position contributes to multiple output positions
for in_c in range(in_channels):
Expand Down
16 changes: 8 additions & 8 deletions act/back_end/layer_schema.py
Comment thread
yuleisui marked this conversation as resolved.
Original file line number Diff line number Diff line change
Expand Up @@ -194,19 +194,19 @@ class LayerKind(str, enum.Enum):
LayerKind.RELU.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["input_shape","output_shape"]},
LayerKind.LRELU.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["negative_slope"]},
LayerKind.PRELU.value: {"params_required": ["weight"], "params_optional": [], "meta_required": [], "meta_optional": []},
LayerKind.SIGMOID.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": []},
LayerKind.TANH.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": []},
LayerKind.SOFTPLUS.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": []},
LayerKind.SIGMOID.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["input_shape","output_shape"]},
LayerKind.TANH.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["input_shape","output_shape"]},
LayerKind.SOFTPLUS.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["input_shape","output_shape"]},
LayerKind.SILU.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["input_shape","output_shape"]},
LayerKind.GELU.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["approximate"]},
LayerKind.RELU6.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": []},
LayerKind.RELU6.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["input_shape","output_shape"]},
LayerKind.HARDTANH.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["min_val","max_val"]},
LayerKind.HARDSIGMOID.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["alpha","beta"]},
LayerKind.HARDSWISH.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": []},
LayerKind.SOFTSIGN.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": []},
LayerKind.ABS.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": []},
LayerKind.HARDSWISH.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["input_shape","output_shape"]},
LayerKind.SOFTSIGN.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["input_shape","output_shape"]},
LayerKind.ABS.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["input_shape","output_shape"]},
LayerKind.CLIP.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["min","max"]},
LayerKind.ADD.value: {"params_required": [], "params_optional": ["bias"], "meta_required": [], "meta_optional": ["broadcast","axis","input_shape","output_shape","original_shape"]},
LayerKind.ADD.value: {"params_required": [], "params_optional": ["bias"], "meta_required": [], "meta_optional": ["broadcast","axis","input_shape","output_shape","original_shape","x_vars","y_vars","x_src","y_src"]},
LayerKind.SUB.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["broadcast","axis"]},
LayerKind.MUL.value: {"params_required": [], "params_optional": ["scale"], "meta_required": [], "meta_optional": ["broadcast","axis","input_shape","output_shape","original_shape"]},
LayerKind.DIV.value: {"params_required": [], "params_optional": [], "meta_required": [], "meta_optional": ["broadcast","axis"]},
Expand Down
16 changes: 15 additions & 1 deletion act/back_end/layer_util.py
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@
#===---------------------------------------------------------------------===#

from __future__ import annotations
from typing import Dict, Any, List
from typing import Dict, Any, List, Union, Tuple
import difflib

# Import validation components
Expand Down Expand Up @@ -301,3 +301,17 @@ def create_layer(id: int, kind: str, params: Dict[str, Any], meta: Dict[str, Any
print("OK — wrapper model passes with", len(layers), "layers.")
except Exception as e:
print("Example failed:\n", e)

def normalize_to_tuple(value: Union[int, Tuple[int, ...]], n: int = 2) -> Tuple[int, ...]:
"""Convert int to n-tuple, pass through existing tuples.

Args:
value: Integer or tuple to normalize
n: Number of dimensions (1 for Conv1d, 2 for Conv2d, 3 for Conv3d)

Returns:
Tuple of n integers
"""
if isinstance(value, int):
return (value,) * n
return tuple(value)
12 changes: 6 additions & 6 deletions act/back_end/solver/solver_gurobi.py
Original file line number Diff line number Diff line change
Expand Up @@ -23,22 +23,22 @@ def setup_gurobi_license():
if 'GRB_LICENSE_FILE' not in os.environ:
if 'ACTHOME' in os.environ:
license_path = os.path.join(os.environ['ACTHOME'], 'modules', 'gurobi', 'gurobi.lic')
print(f"[ACT] Using ACTHOME environment variable: {os.environ['ACTHOME']}")
print(f"[ACT] Using ACTHOME environment variable: {os.path.relpath(os.environ['ACTHOME'])}")
Comment thread
yuleisui marked this conversation as resolved.
else:
project_root = get_project_root()
license_path = os.path.join(project_root, 'modules', 'gurobi', 'gurobi.lic')
print(f"[ACT] Auto-detecting project root: {project_root}")
print(f"[ACT] Auto-detecting project root: {os.path.relpath(project_root)}")

license_path = os.path.abspath(license_path)

if os.path.exists(license_path):
os.environ['GRB_LICENSE_FILE'] = license_path
print(f"[ACT] Gurobi license found and set: {license_path}")
print(f"[ACT] Gurobi license found: {os.path.relpath(license_path)}")
else:
print(f"[WARN] Gurobi license not found at: {license_path}")
print(f"[INFO] Please ensure gurobi.lic is placed in: {os.path.dirname(license_path)}")
print(f"[WARN] Gurobi license not found: {os.path.relpath(license_path)}")
print(f"[INFO] Please place gurobi.lic in: {os.path.relpath(os.path.dirname(license_path))}")
else:
print(f"[ACT] Using existing Gurobi license: {os.environ['GRB_LICENSE_FILE']}")
print(f"[ACT] Using existing Gurobi license: {os.path.relpath(os.environ['GRB_LICENSE_FILE'])}")

setup_gurobi_license()

Expand Down
Loading
Loading