latest Julia version + Onnx reader

[phK3]

The ONNX parser using NaiveNASflux and ONNXNaiveNASflux prevented updating to the latest Julia version.
So I deleted those packages and replaced them with an ONNX reader I implemented in my colleagues package VNNLib.jl
(see github repo here: https://github.com/samysweb/VNNLib.jl/tree/extension).
The new ONNX reader is currently still on the extension branch of VNNLib.jl, but should be on the main branch soon.

An example showing the necessary changes for running the introductory example in the Readme.md using the new ONNX reader from VNNLib.jl is implemented in develop/onnx_parser_adaptations.jl in my fork of ModelVerification.jl.

The modifications I've already done for the version update and a general description of the steps necessary to move to the new ONNX reader are described in the changes.md of my fork.

A main difference would be that the propagate_layer_batch() method would have to dispatch on the subtype of VNNLib.OnnxParser.Node instead of directly dispatching on the Flux operation.
But this is necessary, as many ONNX operations don't directly map to Flux (e.g. Gemm with transposed inputs).

How does this align with your plans for the future of ModelVerification.jl?

Feel free to suggest any requirements, that you need to be met.

All the best,
Philipp

[Wei-TianHao]

Hi Phillip! Thanks for your contribution! Could you revise the CI (continuous integration) file to remove the following lines? The current PR could not pass the continuous integration test because of the file changes.

          julia --project=. -e 'using Pkg; Pkg.develop(path="onnx_parser/NaiveNASflux")'
          julia --project=. -e 'using Pkg; Pkg.develop(path="onnx_parser/ONNXNaiveNASflux")'

https://github.com/phK3/ModelVerification.jl/blob/783e2cabd657eee2188c13b386c5d90c34fb14dd/.github/workflows/CI.yml#L50

My orignal plan was to wait until https://github.com/FluxML/ONNX.jl is ready to use because it is native to Flux. But it takes much longer than I expected. What's your future plan to maintain VNNlib.jl? It seems to be a better choice than ONNXNaiveNASflux because we don't really need the NAS part, but only a ONNX parser. If VNNlib.jl will be long term supported, it may be a better choice for MV.jl.

[phK3]

I deleted the lines you indicated from the CI.yml.

Note that most tests will probably fail. For the verifiers to work, one would have to implement the changes outlined in develop/onnx_parser_adaptations.jl.

My colleague (Samuel) and me plan to maintain VNNLib.jl for as long as we are working in research.

We also have some NN verifiers of our own written in Julia (e.g. VeryDiff, NNPoly) that we want to migrate to VNNLib.jl - so we also have some intrinsic motivation to maintain the repo.

When ONNX.jl gets to a state where it is usable and has wider support among the Julia community, it is probably the best choice, but I don't know when that will be the case.

[phK3]

VNNLib.jl currently uses Flux v0.16.4 which requires Julia 1.10.

I bumped the version in the CI.yml to 1.10, 1.11 and pre.

Installing the package should work in that case.

[phK3]

It looks like 'pre' is not a valid version specifier for julia-actions/setup-julia@v1, I have another project that uses

- uses: julia-actions/setup-julia@v2

where 'pre' seems to work.

Do you think upgrading the julia-actions/setup-julia version is safe? I don't know how to test that locally.

Otherwise, we could just not test for the latest prerelease and delete the 'pre' from CI.yml.

Let me know what you think is the best option.

[Wei-TianHao]

Hi Philipp,
Thanks for the update!

Note that most tests will probably fail. For the verifiers to work, one would have to implement the changes outlined in develop/onnx_parser_adaptations.jl.

Do you mean the change may break the current pipeline? Is there a particular reason that you didn't directly replace the original verify function? If my understanding is correct, the original onnx handling pipeline will be broken anyway after replacing the ONNXNaiveNASflux with you package.

Upgrading the julia-actions/setup-julia version should be safe. To test it, I would suggest setup the github workflow on your forked branch. It's free and should be quite intuitive.

Thanks!

[phK3]

The tests for Ai2z, StarSet, StarSet w/ Ai2z pre-bound now run successfully for Julia 1.11 - I am still working on getting it to run for 1.10 and the latest pre-release of 1.12.

The tests for BetaCrown CPU, however, are failing with the following error message:

BetaCrown CPU: Error During Test at /home/runner/work/ModelVerification.jl/ModelVerification.jl/test/test_mlp.jl:20
  Test threw exception
  Expression: (verify(search_method, split_method, prop_method, Problem(onnx_path, in_hyper, comp_violated))).status == :violated
  KeyError: key :pre_lower not found
  Stacktrace:
    [1] getindex(h::Dict{Any, Any}, key::Symbol)
      @ Base ./dict.jl:477
    [2] batchify_inheritance(inheritance_list::Vector{Dict{Any, Any}}, node::String, key::Symbol, use_gpu::Bool)
      @ ModelVerification ~/work/ModelVerification.jl/ModelVerification.jl/src/solvers/beta-crown.jl:142
    [3] prepare_method(prop_method::BetaCrown, batch_input::Vector{ModelVerification.ReLUConstrainedDomain}, out_specs::ModelVerification.LinearSpec, inheritance_list::Vector{Dict{Any, Any}}, model_info::ModelVerification.ModelGraph, sub::Bool)
      @ ModelVerification ~/work/ModelVerification.jl/ModelVerification.jl/src/solvers/beta-crown.jl:227
    [4] joint_optimization(pre_bound_method::BetaCrown, batch_input::Vector{ModelVerification.ReLUConstrainedDomain}, model_info::ModelVerification.ModelGraph, batch_info::Dict{Any, Any})
      @ ModelVerification ~/work/ModelVerification.jl/ModelVerification.jl/src/solvers/beta-crown.jl:181
    [5] prepare_method(prop_method::BetaCrown, batch_input::Vector{ModelVerification.ReLUConstrainedDomain}, out_specs::ModelVerification.LinearSpec, inheritance_list::Vector{Nothing}, model_info::ModelVerification.ModelGraph, sub::Bool)
      @ ModelVerification ~/work/ModelVerification.jl/ModelVerification.jl/src/solvers/beta-crown.jl:241
    [6] prepare_method(prop_method::BetaCrown, batch_input::Vector{ModelVerification.ReLUConstrainedDomain}, batch_output::Vector{Complement{Float64, Hyperrectangle{Float64, Vector{Float64}, Vector{Float64}}}}, batch_inheritance::Vector{Nothing}, model_info::ModelVerification.ModelGraph, sub::Bool)
      @ ModelVerification ~/work/ModelVerification.jl/ModelVerification.jl/src/solvers/beta-crown.jl:136
    [7] prepare_method(prop_method::BetaCrown, batch_input::Vector{ModelVerification.ReLUConstrainedDomain}, batch_output::Vector{Complement{Float64, Hyperrectangle{Float64, Vector{Float64}, Vector{Float64}}}}, batch_inheritance::Vector{Nothing}, model_info::ModelVerification.ModelGraph)
      @ ModelVerification ~/work/ModelVerification.jl/ModelVerification.jl/src/solvers/beta-crown.jl:131
    [8] search_branches(search_method::BFS, split_method::Bisect, prop_method::BetaCrown, problem::Problem{ModelVerification.ReLUConstrainedDomain, Complement{Float64, Hyperrectangle{Float64, Vector{Float64}, Vector{Float64}}}}, model_info::ModelVerification.ModelGraph; collect_bound::Bool, comp_verified_ratio::Bool, pre_split::Nothing, verbose::Bool, time_out::Nothing)
      @ ModelVerification ~/work/ModelVerification.jl/ModelVerification.jl/src/branching/search.jl:172
    [9] search_branches
      @ ~/work/ModelVerification.jl/ModelVerification.jl/src/branching/search.jl:139 [inlined]
   [10] verify(search_method::BFS, split_method::Bisect, prop_method::BetaCrown, problem::Problem{Hyperrectangle{Float64, Vector{Float64}, Vector{Float64}}, Complement{Float64, Hyperrectangle{Float64, Vector{Float64}, Vector{Float64}}}}; time_out::Int64, attack_restart::Int64, collect_bound::Bool, summary::Bool, pre_split::Nothing, search_adv_bound::Bool, comp_verified_ratio::Bool, verbose::Bool)
      @ ModelVerification ~/work/ModelVerification.jl/ModelVerification.jl/src/ModelVerification.jl:272
   [11] verify
      @ ~/work/ModelVerification.jl/ModelVerification.jl/src/ModelVerification.jl:257 [inlined]
   [12] macro expansion
      @ /opt/hostedtoolcache/julia/1.11.6/x64/share/julia/stdlib/v1.11/Test/src/Test.jl:677 [inlined]
   [13] (::var"#test_mlp#1")(prop_method::BetaCrown)
      @ Main ~/work/ModelVerification.jl/ModelVerification.jl/test/test_mlp.jl:20

see the CI logs in my fork for the full output.

Can you help me here? I didn't change anything (apart from adjusting Flux.functor and removing an convenience constructor) in the BetaCrown specific methods.

[Wei-TianHao]

Hi Philipp, sorry I'm quite busy recently. I will take a look when I got time

[Wei-TianHao]

Hi Philipp, @phK3

Thank you again for your PR to ModelVerification.jl. I really appreciate your initiative and the thoughtful contribution.

I graduated last year and have since been fully occupied with work, so unfortunately I haven’t had the time to properly review or maintain the repository. Given your familiarity with the package and continued interest, I wanted to ask if you might be interested in taking over as the maintainer of ModelVerification.jl.

I’d be very happy to provide any background or context you need to get started. The package has been a valuable part of our research toolkit, and I’d love to see it continue to grow under your stewardship if you’re open to it.

Best regards,
Tianhao

[phK3]

Hi Tianhao,

I'm open to help with the repo as a co-maintainer.

While I've needed to work with some aspects of ModelVerification.jl, I haven't even looked into large parts of the codebase - so I don't feel capable of maintaining the repo on my own.

If you want to, we can schedule a meeting in the week from 20th to 24th of October.

All the best,
Philipp