How is the dronet.onnx model in rq3/benchmark created?

[billchen0]

Hello!

I am interested in experimenting the DFV program with my own DroNet variations. I trained my own DroNet with the resources in their repository and converted it to onnx and imported it to the DFV codebase. However, I noticed that the model originally included in the DFV (rq3/benchmark/dronet.onnx) codebase has a slightly different architecture from the one I trained. I was wondering if you can provide some information on if or how you modified the original DroNet code to obtain the network included in this repository?

Thank you very much!

[dlshriver]

Hi, thanks for your interest in our artifact. We used the best_model as provided in the DroNet repo. I believe we converted this model to onnx using onnxmltools. This was 3 or so years ago so the output of this tool may be slightly different now (I believe we used version 1.5 or 1.6). I believe the only change that we made was to add a Concat operation at the end to get a single output vector with 2 values, rather than 2 vectors with 1 value each. This was done due to some limitations of other tools we were using at the time of conversion (unrelated to this work). The Concat doesn't affect the functionality of the model, and our properties actually slice it off the end of the network, e.g., N[:-1].

[billchen0]

Hi, thanks for your interest in our artifact. We used the best_model as provided in the DroNet repo. I believe we converted this model to onnx using onnxmltools. This was 3 or so years ago so the output of this tool may be slightly different now (I believe we used version 1.5 or 1.6). I believe the only change that we made was to add a Concat operation at the end to get a single output vector with 2 values, rather than 2 vectors with 1 value each. This was done due to some limitations of other tools we were using at the time of conversion (unrelated to this work). The Concat doesn't affect the functionality of the model, and our properties actually slice it off the end of the network, e.g., N[:-1].

Hi! Thank you very much for the reply. Unfortunately when I tried the conversion with onnxmltools and I still encounter the same problem. I wanted to provide more detail so maybe you can spot the issue. The experiments of rq3 run successfully for me with the original dronet.onnx file included in the repository however fails with dronet models that I tried to train from scratch. The falsification process seems to be running however no counter examples are generated (even for a model that has the same architecture as the dronet included in the artifact repo). The output files from running the experiment looks something like this (doesn't have falsification stats from dnnf):

I'm trying to find the reason that is causing the experiment pipeline to not generate counter-examples. I inspected and found that the dronet.onnx model included in the artifact repo has some "identity" blocks that are not in the dronet models that I have trained and converted. The models are included in the figures below:

I then tried generating the onnx file with the best_model provided in the DroNet repo and the resulted model also didn't have identity block. I'm not sure why that is since you generated the dronet.onnx file in this artifact repo with those weights and model_struc or if this even effects the experiment output.

Thank you very much again for your time!

[dlshriver]

If you used install.sh to install DNNV and DNNF for this artifact, then the Identity operations should not matter, since the version of DNNF at that time v0.0.4 automatically simplified the network immediately after loading (the newest version does not). However, it looks like your network does not have the Concat operation, which is in our model. This will affect DNNF since the property slices operations off the end of the network. Not having that extra operation means it will be sliced at the wrong place, leading to a completely different property. Property specifications are not completely independent of the network, and things like slicing can add an implicit dependence on the architecture.

You probably need to add a Concat operation, or change:

N_prob_coll = N[2:-2, 1]
N_steer_angle = N[2:-1, 0]

to

N_prob_coll = N[2:-1, 1]
N_steer_angle = N[2:, 0]

in the property files for your network.