From d3e761a2286d04a3c0005b199653df2f6501f070 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Fri, 19 Jun 2026 12:39:13 +0200 Subject: refined core --- references.bib | 116 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 114 insertions(+), 2 deletions(-) (limited to 'references.bib') diff --git a/references.bib b/references.bib index 8ddabea..194a8b4 100644 --- a/references.bib +++ b/references.bib @@ -16,9 +16,9 @@ } @inproceedings{demoura2008z3, author="de Moura, Leonardo - and Bj{\o}rner, Nikolaj", + and Bj{\o}rner, Nikolaj", editor="Ramakrishnan, C. R. - and Rehof, Jakob", + and Rehof, Jakob", title="Z3: An Efficient SMT Solver", booktitle="Tools and Algorithms for the Construction and Analysis of Systems", year="2008", @@ -28,4 +28,116 @@ abstract="Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.", isbn="978-3-540-78800-3" } +@misc{kumar2019equivalentapproximatetransformationsdeep, + title={Equivalent and Approximate Transformations of Deep Neural Networks}, + author={Abhinav Kumar and Thiago Serra and Srikumar Ramalingam}, + year={2019}, + eprint={1905.11428}, + archivePrefix={arXiv}, + primaryClass={cs.LG}, + url={https://arxiv.org/abs/1905.11428}, +} +@article{JMLR:v24:21-0579, + author = {Fenglei Fan and Rongjie Lai and Ge Wang}, + title = {Quasi-Equivalence between Width and Depth of Neural Networks}, + journal = {Journal of Machine Learning Research}, + year = {2023}, + volume = {24}, + number = {183}, + pages = {1--22}, + url = {http://jmlr.org/papers/v24/21-0579.html} +} +@misc{kaulen20256thinternationalverificationneural, + title={The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results}, + author={Konstantin Kaulen and Tobias Ladner and Stanley Bak and Christopher Brix and Hai Duong and Thomas Flinkow and Taylor T. Johnson and Lukas Koller and Edoardo Manino and ThanhVu H Nguyen and Haoze Wu}, + year={2025}, + eprint={2512.19007}, + archivePrefix={arXiv}, + primaryClass={cs.LG}, + url={https://arxiv.org/abs/2512.19007}, +} +@article{fisher1936iris, + author = {FISHER, R. A.}, + title = {THE USE OF MULTIPLE MEASUREMENTS IN TAXONOMIC PROBLEMS}, + journal = {Annals of Eugenics}, + volume = {7}, + number = {2}, + pages = {179-188}, + doi = {https://doi.org/10.1111/j.1469-1809.1936.tb02137.x}, + url = {https://onlinelibrary.wiley.com/doi/abs/10.1111/j.1469-1809.1936.tb02137.x}, + eprint = {https://onlinelibrary.wiley.com/doi/pdf/10.1111/j.1469-1809.1936.tb02137.x}, + abstract = {The articles published by the Annals of Eugenics (1925–1954) have been made available online as an historical archive intended for scholarly use. The work of eugenicists was often pervaded by prejudice against racial, ethnic and disabled groups. The online publication of this material for scholarly research purposes is not an endorsement of those views nor a promotion of eugenics in any way.}, + year = {1936} +} +@article{lecun2010mnist, + title={MNIST handwritten digit database}, + author={LeCun, Yann and Cortes, Corinna and Burges, CJ}, + journal={ATT Labs [Online]. Available: http://yann.lecun.com/exdb/mnist}, + volume={2}, + year={2010} +} +@InProceedings{eleftheriadis2022equivalence, + author="Eleftheriadis, Charis + and Kekatos, Nikolaos + and Katsaros, Panagiotis + and Tripakis, Stavros", + editor="Bogomolov, Sergiy + and Parker, David", + title="On Neural Network Equivalence Checking Using SMT Solvers", + booktitle="Formal Modeling and Analysis of Timed Systems", + year="2022", + publisher="Springer International Publishing", + address="Cham", + pages="237--257", + abstract="Two pretrained neural networks are deemed (approximately) equivalent if they yield similar outputs for the same inputs. Equivalence checking of neural networks is of great importance, due to its utility in replacing learning-enabled components with (approximately) equivalent ones, when there is need to fulfill additional requirements or to address security threats, as is the case when using knowledge distillation, adversarial training, etc. In this paper, we present a method to solve various strict and approximate equivalence checking problems for neural networks, by reducing them to SMT satisfiability checking problems. This work explores the utility and limitations of the neural network equivalence checking framework, and proposes avenues for future research and improvements toward more scalable and practically applicable solutions. We present experimental results, for diverse types of neural network models (classifiers and regression networks) and equivalence criteria, towards a general and application-independent equivalence checking approach.", + isbn="978-3-031-15839-1" +} + +@article{rosenblatt1958perceptron, + added-at = {2017-07-19T15:29:59.000+0200}, + author = {Rosenblatt, F.}, + biburl = {https://www.bibsonomy.org/bibtex/214ee8da21c66cd4d00d7ab6eca2d96a9/andreashdez}, + citeulike-article-id = {13697582}, + citeulike-linkout-0 = {http://dx.doi.org/10.1037/h0042519}, + doi = {10.1037/h0042519}, + interhash = {dc0cef9dc06033a04f525efdcde7a660}, + intrahash = {14ee8da21c66cd4d00d7ab6eca2d96a9}, + issn = {0033-295X}, + journal = {Psychological Review}, + keywords = {imported}, + number = 6, + pages = {386--408}, + posted-at = {2016-05-02 20:23:36}, + priority = {2}, + timestamp = {2017-07-19T15:31:02.000+0200}, + title = {{The perceptron: A probabilistic model for information storage and organization in the brain.}}, + url = {http://dx.doi.org/10.1037/h0042519}, + volume = 65, + year = 1958 +} + +@inproceedings{katz2017reluplex, + title={Reluplex: An efficient SMT solver for verifying deep neural networks}, + author={Katz, Guy and Barrett, Clark and Dill, David L and Julian, Kyle and Kochenderfer, Mykel J}, + booktitle={International Conference on Computer Aided Verification}, + pages={97--117}, + year={2017}, + organization={Springer} +} + +@inproceedings{katz2019marabou, + title={The Marabou framework for verification and analysis of deep neural networks}, + author={Katz, Guy and Huang, Derek A and Ibeling, Duligur and Julian, Kyle and Burns, Ryan and Sadigh, Dorsa and Barrett, Clark and Dill, David L and Kochenderfer, Mykel J}, + booktitle={International Conference on Computer Aided Verification}, + pages={443--452}, + year={2019}, + organization={Springer} +} + +@article{barrett2016smtlib, + title={The SMT-LIB standard: Version 2.6}, + author={Barrett, Clark and Stump, Aaron and Tinelli, Cesare}, + journal={Department of Computer Science, The University of Iowa, Tech. Rep}, + year={2016} +} -- cgit v1.2.3