Input splitting for LSTM

[mhmd97z]

Hello, I was wondering if CROWN and its variants support the verification of models with LSTM layers in the input splitting mode.

[shizhouxing]

It should be able to support LSTM.

Our GenBaB paper (https://arxiv.org/abs/2405.21063 https://arxiv.org/abs/2405.21063) has shown splitting general nonlinearities with experiments on LSTM.

Input splitting is less dependent on the network architecture if the model can be supported by auto_LiRPA.

On Sep 6, 2024, at 7:50 AM, Mohammad Zangooei @.***> wrote:

Hello, I was wondering if CROWN and its variants support the verification of models with LSTM layers in the input splitting mode.

— Reply to this email directly, view it on GitHub https://github.com/Verified-Intelligence/alpha-beta-CROWN/issues/74, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACUBARFKORSLGJIUUGK74ATZVG6KVAVCNFSM6AAAAABNYXXDKGVHI2DSMVQWIX3LMV43ASLTON2WKOZSGUYTANRRGQZTKMY. You are receiving this because you are subscribed to this thread.

[mhmd97z]

Great. Thanks for the prompt response.

Could you give me a sample yaml config file? I have a model with LSTM to be verified.

[shizhouxing]

You may try the config for ViT and just replace the model: https://github.com/Verified-Intelligence/alpha-beta-CROWN/blob/main/complete_verifier/exp_configs/vnncomp23/vit.yaml

On Sep 6, 2024, at 7:59 AM, Mohammad Zangooei @.***> wrote:

Great. Thanks for the prompt response.

Could you give me a sample yaml config file? I have a model with LSTM to be verified.

— Reply to this email directly, view it on GitHub https://github.com/Verified-Intelligence/alpha-beta-CROWN/issues/74#issuecomment-2334249860, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACUBARCN43OIFZIDMVTSJL3ZVG7OHAVCNFSM6AAAAABNYXXDKGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMZUGI2DSOBWGA. You are receiving this because you commented.

[mhmd97z]

Thanks. I tried it, but it failed. Am I missing something here?

Here's the model:

def lstm_model():
    class RNNBase(nn.Module):
        def __init__(self, state_dim=5, action_dim=100):
            super(RNNBase, self).__init__()
            hidden_dim = 5 
            self.lstm = nn.LSTM(input_size=state_dim, hidden_size=hidden_dim, bidirectional=False, batch_first=True)
            self.lin1 = nn.Linear(hidden_dim, 50)
            self.lin2 = nn.Linear(50, 40)
            self.lin3 = nn.Linear(40, action_dim)
            self.relu = nn.ReLU()

        def forward(self, x):
            output, (h_n, c_n) = self.lstm(x)
            x = output[:, -1, :]

            x = self.lin1(x)
            x = self.relu(x)

            x = self.lin2(x)
            x = self.relu(x)

            x = self.lin3(x)
            x = self.relu(x)

            return x

    return RNNBase()

And this is the error:

ERROR    15:47:33     The node has an unsupported operation: Node(name='/87', ori_name=None, inputs=['/24', '/80', '/82', '/84', '/25', '/23', '/23'], attr={'hidden_size': 5}, op='onnx::LSTM', param=OrderedDict(), input_index=None, bound_node=None, output_index=2, perturbation=None)
ERROR    15:47:33     Unsupported operations:
ERROR    15:47:33     Name: onnx::LSTM, Attr: {'hidden_size': 5}
ERROR    15:47:33     Name: onnx::LSTM, Attr: {'hidden_size': 5}
ERROR    15:47:33     Name: onnx::LSTM, Attr: {'hidden_size': 5}
Traceback (most recent call last):
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 710, in <module>
    abcrown.main()
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 642, in main
    incomplete_verification_output = self.incomplete_verifier(
                                     ^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 116, in incomplete_verifier
    model = LiRPANet(model_ori, in_size=data.shape, c=c)
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 53, in __init__
    self.net = BoundedModule(
               ^^^^^^^^^^^^^^
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 130, in __init__
    self._convert(model, global_input)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 849, in _convert
    nodesOP, nodesIn, nodesOut, template = self._convert_nodes(
                                           ^^^^^^^^^^^^^^^^^^^^
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 741, in _convert_nodes
    raise NotImplementedError('There are unsupported operations')
NotImplementedError: There are unsupported operations

[shizhouxing]

nn.LSTM is not supported. But nn.LSTMCell is supported (with an additional for-loop to iterate through the time steps).

See the example used in the auto_LiRPA paper (https://arxiv.org/abs/2002.12920 https://arxiv.org/abs/2002.12920): https://github.com/Verified-Intelligence/auto_LiRPA/blob/master/examples/language/lstm.py#L9-L44

On Sep 6, 2024, at 8:52 AM, Mohammad Zangooei @.***> wrote:

Thanks. I tried it, but it failed. Am I missing something here?

Here's the model:

def lstm_model(): class RNNBase(nn.Module): def init(self, state_dim=5, action_dim=100): super(RNNBase, self).init() hidden_dim = 5 self.lstm = nn.LSTM(input_size=state_dim, hidden_size=hidden_dim, bidirectional=False, batch_first=True) self.lin1 = nn.Linear(hidden_dim, 50) self.lin2 = nn.Linear(50, 40) self.lin3 = nn.Linear(40, action_dim) self.relu = nn.ReLU()

    def forward(self, x):
        output, (h_n, c_n) = self.lstm(x)
        x = output[:, -1, :]

        x = self.lin1(x)
        x = self.relu(x)

        x = self.lin2(x)
        x = self.relu(x)

        x = self.lin3(x)
        x = self.relu(x)

        return x

return RNNBase()

And this is the error:

ERROR 15:47:33 The node has an unsupported operation: Node(name='/87', ori_name=None, inputs=['/24', '/80', '/82', '/84', '/25', '/23', '/23'], attr={'hidden_size': 5}, op='onnx::LSTM', param=OrderedDict(), input_index=None, bound_node=None, output_index=2, perturbation=None) ERROR 15:47:33 Unsupported operations: ERROR 15:47:33 Name: onnx::LSTM, Attr: {'hidden_size': 5} ERROR 15:47:33 Name: onnx::LSTM, Attr: {'hidden_size': 5} ERROR 15:47:33 Name: onnx::LSTM, Attr: {'hidden_size': 5} Traceback (most recent call last): File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 710, in abcrown.main() File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 642, in main incomplete_verification_output = self.incomplete_verifier( ^^^^^^^^^^^^^^^^^^^^^^^^^ File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 116, in incomplete_verifier model = LiRPANet(model_ori, in_size=data.shape, c=c) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 53, in init self.net = BoundedModule( ^^^^^^^^^^^^^^ File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 130, in init self._convert(model, global_input) File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 849, in _convert nodesOP, nodesIn, nodesOut, template = self._convert_nodes( ^^^^^^^^^^^^^^^^^^^^ File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 741, in _convert_nodes raise NotImplementedError('There are unsupported operations') NotImplementedError: There are unsupported operations — Reply to this email directly, view it on GitHub https://github.com/Verified-Intelligence/alpha-beta-CROWN/issues/74#issuecomment-2334355508, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACUBARDI75KJHW5WEXSA4GLZVHFTRAVCNFSM6AAAAABNYXXDKGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMZUGM2TKNJQHA. You are receiving this because you commented.