problems with embedding layers?

[ramonbejar]

Describe the bug
Hi, Running abcrown with a model that uses pytorch embedding layer (torch.nn.Embedding(vocabulary_size, embd_size, padding_idx = padding_idx, sparse=False)) gives this error :

File "/home/ramon/miniconda3/envs/alpha-beta-crown/lib/python3.11/site-packages/torch/autograd/graph.py", line 744, in _engine_run_backward
return Variable._execution_engine.run_backward( # Calls into the C++ engine to run the backward pass
RuntimeError: element 0 of tensors does not require grad and does not have a grad_fn

It seems that a "possible" way to make this error to dissapear is to modify in your function:

def attack_with_general_specs(model, x, data_min, data_max,
list_target_label_arrays, initialization="uniform", GAMA_loss=False): (module attack_pgd)

these lines (not allowing to set off the gradient property:

Set all parameters without gradient, this can speedup things significantly.

grad_status = {}
for p in model.parameters():
    grad_status[p] = p.requires_grad
#    p.requires_grad_(False)

But then I get a different error (but in a different VNNLIB instance from my test set of three instances).

The new error I get then is this one:

File "/home/ramon/research/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/indexing.py", line 42, in forward
raise ValueError('Unsupported shapes in Gather: '
ValueError: Unsupported shapes in Gather: data torch.Size([257, 8]), indices torch.Size([1, 20]), axis 0

^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

System configuration:

• OS: Linux ramon-HP-Z1-G9-Tower-Desktop-PC 6.8.0-48-generic alpha-beta-crown behavior #48~22.04.1-Ubuntu SMP PREEMPT_DYNAMIC Mon Oct 7 11:24:13 UTC 2 x86_64 x86_64 x86_64 GNU/Linux

• Python version: Python 3.11.9

• Pytorch Version: the same of the miniconda environment provided for abcrown

• Hardware: HP-Z1-G9-Tower-Desktop-PC

• Have you tried to reproduce the problem in a cleanly created conda/virtualenv environment using official installation instructions and the latest code on the main branch?: Yes

• pytorch model:

  class CNN(torch.nn.Module):
  ''' Simple CNN model for testing purposes.
  Inputs a sequence of bytes of random length and outputs a single value:
  0 = most of bytes are < 128, 1 = most of bytes are >= 128.
  '''

  def init(self, max_bytes, vocabulary_size: int = 257, embd_size: int = 8, channels: int = 64, kernel_size: int = 3, padding_idx: int = 256, out_size: int = 1):
  super().init()
  self.max_bytes = max_bytes
  self.vocabulary_size = vocabulary_size
  self.embd_size = embd_size
  self.channels = channels
  self.kernel_size = kernel_size
  self.padding_idx = padding_idx
  self.out_size = out_size
  # self.fc0 = torch.nn.Linear(max_bytes, max_bytes * embd_size)
  # self.conv1 = torch.nn.Conv1d(embd_size, channels, kernel_size)
  # self.fc1 = torch.nn.Linear(max_bytes - (kernel_size - 1), channels) # https://pytorch.org/docs/stable/generated/torch.nn.Conv1d.html
  # self.drop1 = torch.nn.Dropout1d()
  # self.fc2 = torch.nn.Linear(channels, out_size)
  # self.fc3 = torch.nn.Linear(channels, out_size)
  self.embd = torch.nn.Embedding(vocabulary_size, embd_size, padding_idx = padding_idx, sparse=False)
  if max_bytes == 20:
  self.max_pooling_length = 6
  else:
  raise Exception("Undefined max pooling length")
  self.max_pooling = torch.nn.MaxPool2d((self.max_pooling_length, 1))
  self.conv_1 = torch.nn.Conv1d(embd_size, channels, kernel_size, stride=kernel_size, bias=True)
  self.fc_1 = torch.nn.Linear(channels, channels)
  self.fc_2 = torch.nn.Linear(channels, out_size)

  def forward(self, x):
  #print(f'Input size: {x.size()}')
  x = x.to(torch.long)
  x = self.embd(x)
  #print(f'Embd size: {x.size()}')
  x = torch.transpose(x, 1, 2)
  #print(f'Transpose size: {x.size()}')
  conv_value = self.conv_1(x)
  #print(f'Conv1 size: {conv_value.size()}')
  conv_value = torch.unsqueeze(conv_value, 3)
  #print(f'US size: {conv_value.size()}')
  max_value = self.max_pooling(conv_value)
  #print(f'Max pooling size: {max_value.size()}')
  max_value = torch.squeeze(max_value, dim=3)
  max_value = torch.squeeze(max_value, dim=2)
  #print(f'Squeeze size: {max_value.size()}')
  penult = x = torch.nn.functional.relu(self.fc_1(max_value))
  #print(f'Relu size: {x.size()}')
  x = self.fc_2(x)
  #print(f'FC2 size: {x.size()}')
  if self.out_size == 1:
  x = torch.squeeze(x, dim = 1)
  x = torch.sigmoid(x)
  #print(f'Squeeze size: {x.size()}')

   return x#, penult, max_value
  

def cnntwoclasses():
return CNN(20,out_size=2)

• yaml conf file:

  Configuration file for running the collins_rul_cnn benchmark (all properties).

general:
root_path: /home/ramon/research/shared/github/robustmalware/data/josep/abcrown-example
csv_name: instances_twoclasses.csv
enable_incomplete_verification: false

enable_incomplete_verification: False

loss_reduction_func: maxinstances_twoclasses.csv

conv_mode: matrix

save_adv_example: true # Saved in file test_cex.txt, can be changed with argument --cex_path or in Config['attack']['cex_path']. Not in vnncomp format.
model:
name: Customized("cnn_emdedding", "cnntwoclasses" )
path: models/cnntwoclasses.pth
input_shape: [ 1, 20]
solver:
batch_size: 512
alpha-crown:
iteration: 100
beta-crown:
iteration: 100
#data:

num_outputs: 1

bab:
timeout: 130
debug:
view_model: true
lp_test: null
rescale_vnnlib_ptb: null
test_optimized_bounds: false
test_optimized_bounds_after_n_iterations: 0
print_verbose_decisions: true

• Instance that gives the first error (the one I am able to correct by not deactivating gradient functions):

; Input file: test.csv
; Max bytes: 20
; Input name: X
; Output name: Y
; Epsilon: 10.0

; Input variables:

(declare-const X_0 Real)
(declare-const X_1 Real)
(declare-const X_2 Real)
(declare-const X_3 Real)
(declare-const X_4 Real)
(declare-const X_5 Real)
(declare-const X_6 Real)
(declare-const X_7 Real)
(declare-const X_8 Real)
(declare-const X_9 Real)
(declare-const X_10 Real)
(declare-const X_11 Real)
(declare-const X_12 Real)
(declare-const X_13 Real)
(declare-const X_14 Real)
(declare-const X_15 Real)
(declare-const X_16 Real)
(declare-const X_17 Real)
(declare-const X_18 Real)
(declare-const X_19 Real)

; Output variables:

(declare-const Y_0 Real)
(declare-const Y_1 Real)

; Input constraints:

(assert (>= X_0 181.0))
(assert (<= X_0 201.0))

(assert (>= X_1 182.0))
(assert (<= X_1 202.0))

(assert (>= X_2 8.0))
(assert (<= X_2 28.0))

(assert (>= X_3 144.0))
(assert (<= X_3 164.0))

(assert (>= X_4 146.0))
(assert (<= X_4 166.0))

(assert (>= X_5 76.0))
(assert (<= X_5 96.0))

(assert (>= X_6 57.0))
(assert (<= X_6 77.0))

(assert (>= X_7 34.0))
(assert (<= X_7 54.0))

(assert (>= X_8 215.0))
(assert (<= X_8 235.0))

(assert (>= X_9 56.0))
(assert (<= X_9 76.0))

(assert (>= X_10 256))
(assert (<= X_10 256))

(assert (>= X_11 256))
(assert (<= X_11 256))

(assert (>= X_12 256))
(assert (<= X_12 256))

(assert (>= X_13 256))
(assert (<= X_13 256))

(assert (>= X_14 256))
(assert (<= X_14 256))

(assert (>= X_15 256))
(assert (<= X_15 256))

(assert (>= X_16 256))
(assert (<= X_16 256))

(assert (>= X_17 256))
(assert (<= X_17 256))

(assert (>= X_18 256))
(assert (<= X_18 256))

(assert (>= X_19 256))
(assert (<= X_19 256))

; Output constraints:

(assert (>= Y_0 Y_1))

• Instance that gives the second error (that I do not know how to fix it):

; Input file: test.csv
; Max bytes: 20
; Input name: X
; Output name: Y
; Epsilon: 10.0

; Input variables:

(declare-const X_0 Real)
(declare-const X_1 Real)
(declare-const X_2 Real)
(declare-const X_3 Real)
(declare-const X_4 Real)
(declare-const X_5 Real)
(declare-const X_6 Real)
(declare-const X_7 Real)
(declare-const X_8 Real)
(declare-const X_9 Real)
(declare-const X_10 Real)
(declare-const X_11 Real)
(declare-const X_12 Real)
(declare-const X_13 Real)
(declare-const X_14 Real)
(declare-const X_15 Real)
(declare-const X_16 Real)
(declare-const X_17 Real)
(declare-const X_18 Real)
(declare-const X_19 Real)

; Output variables:

(declare-const Y_0 Real)
(declare-const Y_1 Real)

; Input constraints:

(assert (>= X_0 170.0))
(assert (<= X_0 190.0))

(assert (>= X_1 53.0))
(assert (<= X_1 73.0))

(assert (>= X_2 39.0))
(assert (<= X_2 59.0))

(assert (>= X_3 57.0))
(assert (<= X_3 77.0))

(assert (>= X_4 15.0))
(assert (<= X_4 35.0))

(assert (>= X_5 87.0))
(assert (<= X_5 107.0))

(assert (>= X_6 98.0))
(assert (<= X_6 118.0))

(assert (>= X_7 150.0))
(assert (<= X_7 170.0))

(assert (>= X_8 7.0))
(assert (<= X_8 27.0))

(assert (>= X_9 40.0))
(assert (<= X_9 60.0))

(assert (>= X_10 256))
(assert (<= X_10 256))

(assert (>= X_11 256))
(assert (<= X_11 256))

(assert (>= X_12 256))
(assert (<= X_12 256))

(assert (>= X_13 256))
(assert (<= X_13 256))

(assert (>= X_14 256))
(assert (<= X_14 256))

(assert (>= X_15 256))
(assert (<= X_15 256))

(assert (>= X_16 256))
(assert (<= X_16 256))

(assert (>= X_17 256))
(assert (<= X_17 256))

(assert (>= X_18 256))
(assert (<= X_18 256))

(assert (>= X_19 256))
(assert (<= X_19 256))

; Output constraints:

(assert (>= Y_1 Y_0))