About the partitions when verifying ACAS Xu

[dgl-prc]

Hi,

when verifying the ACAS Xu property, the input constraint is firstly split into several disjoint partitions, and then recursively verify each sub-partition by the divide-and-conquer method.

My question is that what is the intuition behind the partitioning?

https://github.com/eth-sri/eran/blob/d775968e2aa3380dfa2576c2c2de5a0f45253f31/tf_verify/__main__.py#L516 https://github.com/eth-sri/eran/blob/7c0f89dfca599e29b8960c654b0b88759dab1d8c/tf_verify/__main__.py#L283

[GgnDpSngh]

Hi there,

Thanks for your interest. We compute the gradient of the output with respect to the input features and then use the gradient information to determine the number of splits for each dimension. Each dimension is then uniformly split according to the computed number of splits.

Let me know if this answers your question.

Cheers, Gagandeep Singh

[dgl-prc]

Hi, Singh

There are still some points I am not clear

1. Does the smear indicate the "importance" of each input feature that should be refined? https://github.com/eth-sri/eran/blob/d775968e2aa3380dfa2576c2c2de5a0f45253f31/tf_verify/__main__.py#L519

2. What does the "split_multiple" mean? Why is "20" used? https://github.com/eth-sri/eran/blob/d775968e2aa3380dfa2576c2c2de5a0f45253f31/tf_verify/__main__.py#L520

[GgnDpSngh]

Hi there,

Yes, smears identify the number of splits for a given input feature. This is used for computing split_multiple which determines the number of splits. We tried different numerators and 20 seemed to perform best.

Let me know if it explains your question.

Cheers, Gagandeep Singh

[dgl-prc]

Many thanks~