verification of models with customized 'forward' function wrapping pre-trained networks and nonlinear functions

[JianqiangDing]

Hi,

I am trying to use alpha-beta CROWN to verify compositions of trained models and nonlinear functions by wrapping the trained model into a new model with customized forward function, such as NN(f(x)), where NN represents a neural network and f denotes some given nonlinear funcitons. I have two questions regarding this setup,

1. Based on my understand of the methods in alpha-beta CROWN, the bounds computation should relies on detecting the structure of the network. Does the alpha-beta CROWN supports the verification for such models that wrap pre-trained models and involve nonlinear functions of the output of trained models? Will this affect the precision of the bounds computation?
2. I have used an online demo to perform verification in the aforementioned settings, and it seems it works for NN(f(x)) . However, it fails when involving the computation jacobian of trained networks within the customize forward function, could you please provide some advice on why the second case failed and how to proceed if I want to use alpha-beta CROWN to verify some functions including jacobian of a trained network?

Any suggestions would be greatly appreciated, thank you for your time and consideration on these questions, and I look forward to your guidance!

Best regards