Possibility of Parallel Verification for Accelerating Large Model Verification

[ExcellentHH]

Description

I am currently using ekzl to verify a large model composed of approximately 60 layers, including 13 Conv layers. However, when I ran the command ezkl mock, it took a very long time to complete the verification (around 10,000 seconds), as the model generates 71,055,362 constraints. Here are the specific parameters I used:

"args": {
 |          "allocated_constraints": null,
 |          "batch_size": 1,
 |          "bits": 25,
 |          "input_visibility": "Private",
 |          "logrows": 26,
 |          "output_visibility": "Public",
 |          "pack_base": 1,
 |          "param_visibility": "Private",
 |          "scale": 4,
 |          "tolerance": {
 |            "Abs": {
 |              "val": 6
 |            }
 |          }
 |        },

Question

I have several questions and would appreciate any help and advice.

1. Are there any methods to accelerate the verification process for large models? Is it possible to perform parallel verification? One naive idea is to partition the large model into multiple small models and perform parallel verification on each small model while adding constraints that ensure the input and output of adjacent small models are equal.
2. How to effectively determine the value of parameters, especially the parameters --bits, --logrows, --scale, --tolerance?
3. Additionally, when verifying a large model, I set the parameters as follows:

"args": {
 |          "allocated_constraints": null,
 |          "batch_size": 1,
 |          "bits": 16,
 |          "input_visibility": "Private",
 |          "logrows": 17,
 |          "output_visibility": "Public",
 |          "pack_base": 1,
 |          "param_visibility": "Private",
 |          "scale": 7,
 |          "tolerance": {
 |            "Abs": {
 |              "val": 6
 |            }
 |          }
 |        },

and encounter the following error:

[D] [5891s, ezkl_lib::graph::model] - laying out 56: CONST, offset:71049771
[D] [5891s, ezkl_lib::graph::model] - laying out 57: ADD, offset:71049771
[D] [5891s, ezkl_lib::graph::model] - model outputs are nodes: [57]
[*] [5891s, ezkl_lib::graph::model] - computing...
error: constraint not satisfied

  Cell layout in region 'model':
    | Offset | A2 |A545|thread 'main' panicked at 'capacity overflow', library/alloc/src/raw_vec.rs:518:5

Could this error be related to the parameters including --bits, --logrows, --scale, --tolerance?

Any insights are appreciated, thanks for the hard work!

[alexander-camuto]

Hey @ExcellentHH thank you as always for your questions. Can you send me the full pipeline of commands you're using ? from proving to verification so I can replicate what you're seeing.

It looks like you're changing the parameters between proving and verification -- which shouldn't be done :)

[ExcellentHH]

Thanks very much for your prompt reply. Sorry for my unclear description. I have rephrased the question below:

In fact, for the same onnx and json, when I set the parameters as follows:

"args": {
 |          "allocated_constraints": null,
 |          "batch_size": 1,
 |          "bits": 25,
 |          "input_visibility": "Private",
 |          "logrows": 26,
 |          "output_visibility": "Public",
 |          "pack_base": 1,
 |          "param_visibility": "Private",
 |          "scale": 4,
 |          "tolerance": {
 |            "Abs": {
 |              "val": 6
 |            }
 |          }
 |        },

ezkl mock can run successfully.
But before this, I tried to set the parameters to:

"args": {
 |          "allocated_constraints": null,
 |          "batch_size": 1,
 |          "bits": 16,
 |          "input_visibility": "Private",
 |          "logrows": 17,
 |          "output_visibility": "Public",
 |          "pack_base": 1,
 |          "param_visibility": "Private",
 |          "scale": 7,
 |          "tolerance": {
 |            "Abs": {
 |              "val": 6
 |            }
 |          }
 |        },

and encountered the following error:

[D] [5891s, ezkl_lib::graph::model] - laying out 56: CONST, offset:71049771
[D] [5891s, ezkl_lib::graph::model] - laying out 57: ADD, offset:71049771
[D] [5891s, ezkl_lib::graph::model] - model outputs are nodes: [57]
[*] [5891s, ezkl_lib::graph::model] - computing...
error: constraint not satisfied

  Cell layout in region 'model':
    | Offset | A2 |A545|thread 'main' panicked at 'capacity overflow', library/alloc/src/raw_vec.rs:518:5

So I guess it is because of the setting of these parameters that caused this error. This has led me to wonder how to set valid parameters for verification. I have noticed that the ezkl command has been updated and now includes a gen-circuit-params parameter that may help with this issue. I plan to try using this parameter later.

Furthermore, when verifying a large model, the ezkl mock command already takes a significant amount of time. I anticipate that running ezkl prove will take even longer. Are there any ways to speed up the verification process for a large model?

If the full pipeline of commands is needed, I will post it later.

Thanks again for your prompt reply as always!

[alexander-camuto]

Hey @ExcellentHH looks like with 2^17 you hit the column limit for halo2 :) we have a "calibration" pass which helps pick those parameters out. As you've noticed its in the gen-circuit-params command. We have some instructions in the docs on how to use it but we have an update in #300 that we're about to merge which makes it even easier to use and splits it into a separate calibrate-settings command

[ExcellentHH]

@alexander-camuto Thank you for your response. Additionally, I would like to inquire whether there are any methods to accelerate the verification process for large models. Does ezkl have any plans to develop parallelized verification capabilities? (I have a naive and unverified idea, which is to partition the large model into smaller models and perform parallel verification on each of these smaller models. I would add constraints that ensure the inputs and outputs of adjacent small models are equal.)

[alexander-camuto]

Do you mean parallelized proving like splitting the circuit into sub-circuits which we prove in parallel ?

[ExcellentHH]

Exactly！

[alexander-camuto]

Eventually we'd like to get there :) it would involve using recursion -- and we're hoping to integrate it if / when it comes to halo2 or if we ever switch to a proving backend like nova