Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

elina_zonotope bugfix #49

Merged
merged 2 commits into from
Jun 21, 2019
Merged

elina_zonotope bugfix #49

merged 2 commits into from
Jun 21, 2019

Conversation

ljlin
Copy link
Contributor

@ljlin ljlin commented Jun 19, 2019

Hi Gagan.

When we used elina_zonotope, we found that the output is abnormal. Through debugging, we think there is a bug in the following code snippet.

ELINA/elina_zonotope/zonotope_internal.h

Lines 1399 to 1402 in e824898

elina_scalar_sub(c0,dmax,dmin, ELINA_SCALAR_DOUBLE);
elina_scalar_div_2(c0, c0);
res->c_inf = c0->val.dbl;
res->c_sup = c0->val.dbl;

When we changed the 1401st line as follows, the precision is improved a lot.

res->c_inf = -c0->val.dbl;

And when we convert an abstract element into a lincons array, the elina abstract0 API generates MPQ scalars, which is then read as a double when we use this lincons array to intersect with a zonotope in the following code snippet.

ELINA/elina_zonotope/elina_box_meetjoin.c

Lines 385 to 392 in 3be0c7e

if(cst->discr==ELINA_COEFF_SCALAR){
*itv_inf = -cst->val.scalar->val.dbl;
*itv_sup = cst->val.scalar->val.dbl;
}
else{
*itv_inf = -cst->val.interval->inf->val.dbl;
*itv_sup = cst->val.interval->sup->val.dbl;
}

Thanks,
Jianlin

@GgnDpSngh
Copy link
Contributor

GgnDpSngh commented Jun 19, 2019 •
edited
Loading

Hi Jianlin,

Thanks for spotting it, note that ELINA no longer supports Join for the Zonotope domain based on [1] as it turns out to be imprecise for analysis, e.g., for approximating the ReLU activation in the neural networks (Instead, we compute a more precise ReLU transformer based on [2] via the "zonoml" domain which builds on top of "elina_zonotope"). A version of ELINA that has the Zonotope join implemented could be found here:
ELINA with Zonotope Join.

From our experience, the Join above gives more precise results than Apron.

References:

  1. A logical product approach to zonotope intersection, CAV 2009.
  2. Fast and Effective Robustness Certification, NeurIPS 2018.

Cheers,
Gagandeep Singh

@GgnDpSngh GgnDpSngh merged commit 9f066a8 into eth-sri:master Jun 21, 2019
@ljlin
Copy link
Contributor Author

ljlin commented Jun 30, 2019

Hi Gagan.
Thank you very much for the information you provided, but I found that both cfdbc46 and 7a2def1 have memory leaks when I use them. I found that after aef18a8, there is no such problem.

Although there is no best join transformer in the Zonotope domain, I need one. Is it feasible to add the join operation (with minor modification) in

ELINA/elina_zonotope/zonotope_meetjoin.c

Line 178 in cfdbc46

zonotope_t* zonotope_join(elina_manager_t* man, bool destructive, zonotope_t* z1, zonotope_t* z2)
to the latest version?

@GgnDpSngh
Copy link
Contributor

Hi Jianlin,

I have added support for the Zonotope join in the latest version of ELINA and tested it on many examples. It seems to be correct, let me know if you have any further problems/questions regarding ELINA.

Cheers,
Gagandeep Singh

cwright7101 pushed a commit to cwright7101/ELINA that referenced this pull request Nov 12, 2020
Merge pull request eth-sri#49 from ljlin/master
1bc0d24 
elina_zonotope bugfix
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@ljlin @GgnDpSngh