1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
@inproceedings{lafont1990interactionnets,
author = {Lafont, Yves},
title = {Interaction nets},
year = {1989},
isbn = {0897913434},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/96709.96718},
doi = {10.1145/96709.96718},
abstract = {We propose a new kind of programming language, with the following features:Interaction nets generalize Girard's proof nets of linear logic and illustrate the advantage of an integrated logic approach, as opposed to the external one. In other words, we did not try to design a logic describing the behaviour of some given computational system, but a programming language for which the type discipline is already (almost) a logic.In fact, we shall scarcely refer to logic, because we adopt a na\"{\i}ve and pragmatic style. A typical application we have in mind for this language is the design of interactive softwares such as editors or window managers.},
booktitle = {Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {95–108},
numpages = {14},
location = {San Francisco, California, USA},
series = {POPL '90}
}
@inproceedings{demoura2008z3,
author="de Moura, Leonardo
and Bj{\o}rner, Nikolaj",
editor="Ramakrishnan, C. R.
and Rehof, Jakob",
title="Z3: An Efficient SMT Solver",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2008",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="337--340",
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}
}
|
