Onnx Gather format supported?

[Dovermore]

Hi,

We have recently tried to use VeriNet to run some certifications on NN. But encountered a problem when it failed to identify nodes with Op_type: Gather (the nodes are not recognized, thus raising a key error).

Is are the following functions supported by VertiNet (torch.cat, torch.chunk, index slicing)? If not supported but feasible, can you point me to some help to implement this?

Best, Calvin

[pat676]

Hi Calvin,

Sorry, but chunk and index slicing are not supported. I believe it would be feasible to implement, but we do unfortunately not actively develop VeriNet anymore.

Sorry I could not be of more help.

Best, Patrick

On 24 Aug 2023, at 15:58, Calvin Huang @.***> wrote:

Hi,

We have recently tried to use VeriNet to run some certifications on NN. But encountered a problem when it failed to identify nodes with Op_type: Gather (the nodes are not recognized, thus raising a key error).

Is are the following functions supported by VertiNet (torch.cat, torch.chunk, index slicing)? If not supported but feasible, can you point me to some help to implement this?

Best, Calvin

— Reply to this email directly, view it on GitHub https://github.com/vas-group-imperial/VeriNet/issues/9, or unsubscribe https://github.com/notifications/unsubscribe-auth/AES3SPAJPTOE4USO7TQJDCLXW5T2DANCNFSM6AAAAAA35FHIYA. You are receiving this because you are subscribed to this thread.

[vas-group-imperial]

Hi Calvin

I agree with what Patrick has said below. But would you be able to give a little bit more background on your request in terms of problem domain that you'd like to apply Verinet to, etc?

Best

-Alessio

On 24/08/2023 17:02, Patrick Henriksen wrote:

Hi Calvin,

Sorry, but chunk and index slicing are not supported. I believe it would be feasible to implement, but we do unfortunately not actively develop VeriNet anymore.

Sorry I could not be of more help.

Best, Patrick

On 24 Aug 2023, at 15:58, Calvin Huang @.***> wrote:

Hi,

We have recently tried to use VeriNet to run some certifications on NN. But encountered a problem when it failed to identify nodes with Op_type: Gather (the nodes are not recognized, thus raising a key error).

Is are the following functions supported by VertiNet (torch.cat, torch.chunk, index slicing)? If not supported but feasible, can you point me to some help to implement this?

Best, Calvin

— Reply to this email directly, view it on GitHub https://github.com/vas-group-imperial/VeriNet/issues/9, or unsubscribe https://github.com/notifications/unsubscribe-auth/AES3SPAJPTOE4USO7TQJDCLXW5T2DANCNFSM6AAAAAA35FHIYA. You are receiving this because you are subscribed to this thread.

— Reply to this email directly, view it on GitHub https://github.com/vas-group-imperial/VeriNet/issues/9#issuecomment-1691973650, or unsubscribe https://github.com/notifications/unsubscribe-auth/ASHHU5OE4KUQYNIG6QXRGHTXW53ITANCNFSM6AAAAAA35FHIYA. You are receiving this because you are subscribed to this thread.Message ID: @.***>

-- Alessio Lomuscio, PhD, FEurAI Royal Academy of Engineering Chair in Emerging Technologies Verification of Autonomous Systems Group Department of Computing, Imperial College London, London, SW7 2AZ, UK URL: http://www.doc.ic.ac.uk/~alessio/

[Dovermore]

We are looking at NLP domain with VeriNet (in particular we have adopted similar structure as Efficient Verification of Neural Networks against LVM-based Specifications, which I presume is also from your group). In particular, we are interested in normalizing flow as the encoder layer, which requires indexing, chunking and concatenation.

Would it be difficult to implement slicing, and concatenation ourselves?

[vas-group-imperial]

Hi Calvin

Would you be able to share your email address so that we can continue the conversation with private emails?

Best

-A

On 25/08/2023 03:31, Calvin Huang wrote:

We are looking at NLP domain with VeriNet (in particular we have adopted similar structure as Efficient Verification of Neural Networks against LVM-based Specifications, which I presume is also from your group). In particular, we are interested in normalizing flow as the encoder layer, which requires indexing, chunking and concatenation.

Would it be difficult to implement slicing, and concatenation ourselves?

— Reply to this email directly, view it on GitHub https://github.com/vas-group-imperial/VeriNet/issues/9#issuecomment-1692668963, or unsubscribe https://github.com/notifications/unsubscribe-auth/ASHHU5PZTJFQPCVHVXPTG3DXXAE7VANCNFSM6AAAAAA35FHIYA. You are receiving this because you commented.Message ID: @.***>

-- Alessio Lomuscio, PhD, FEurAI Royal Academy of Engineering Chair in Emerging Technologies Verification of Autonomous Systems Group Department of Computing, Imperial College London, London, SW7 2AZ, UK URL: http://www.doc.ic.ac.uk/~alessio/

[Dovermore]

Hi,

My email is calvin.huang@unimelb.edu.au. Can you also cc benjamin.rubinstein@unimelb.edu.au (he is my supervisor).

Best, Calvin