From 3e338c3be65638ef1898c32c707c50422acafb18 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Thu, 26 Mar 2026 20:28:38 +0100 Subject: added LICENSE --- .gitignore | 27 +- LICENSE | 661 +++++++++++++++++++++ README.md | 6 + examples/fashion_mnist/fashion_mnist.py | 53 ++ examples/fashion_mnist/fashion_mnist_argmax.vnnlib | 133 +++++ .../fashion_mnist/fashion_mnist_epsilon.vnnlib | 124 ++++ examples/fashion_mnist/fashion_mnist_strict.vnnlib | 123 ++++ examples/verify_fashion_mnist.py | 50 ++ examples/verify_xor.py | 50 ++ examples/xor/xor.py | 40 ++ examples/xor/xor_argmax.vnnlib | 14 + examples/xor/xor_epsilon.vnnlib | 15 + examples/xor/xor_strict.vnnlib | 14 + fashion_mnist/fashion_mnist.py | 53 -- fashion_mnist/fashion_mnist_argmax.vnnlib | 133 ----- fashion_mnist/fashion_mnist_epsilon.vnnlib | 124 ---- fashion_mnist/fashion_mnist_strict.vnnlib | 123 ---- nneq.py | 15 + notes.norg | 111 ---- verify_fashion_mnist.py | 32 - verify_xor.py | 32 - xor/xor.py | 40 -- xor/xor_argmax.vnnlib | 14 - xor/xor_epsilon.vnnlib | 15 - xor/xor_strict.vnnlib | 14 - 25 files changed, 1312 insertions(+), 704 deletions(-) create mode 100644 LICENSE create mode 100644 examples/fashion_mnist/fashion_mnist.py create mode 100644 examples/fashion_mnist/fashion_mnist_argmax.vnnlib create mode 100644 examples/fashion_mnist/fashion_mnist_epsilon.vnnlib create mode 100644 examples/fashion_mnist/fashion_mnist_strict.vnnlib create mode 100644 examples/verify_fashion_mnist.py create mode 100644 examples/verify_xor.py create mode 100644 examples/xor/xor.py create mode 100644 examples/xor/xor_argmax.vnnlib create mode 100644 examples/xor/xor_epsilon.vnnlib create mode 100644 examples/xor/xor_strict.vnnlib delete mode 100644 fashion_mnist/fashion_mnist.py delete mode 100644 fashion_mnist/fashion_mnist_argmax.vnnlib delete mode 100644 fashion_mnist/fashion_mnist_epsilon.vnnlib delete mode 100644 fashion_mnist/fashion_mnist_strict.vnnlib delete mode 100644 notes.norg delete mode 100644 verify_fashion_mnist.py delete mode 100644 verify_xor.py delete mode 100644 xor/xor.py delete mode 100644 xor/xor_argmax.vnnlib delete mode 100644 xor/xor_epsilon.vnnlib delete mode 100644 xor/xor_strict.vnnlib diff --git a/.gitignore b/.gitignore index 08dbf27..9fa256b 100644 --- a/.gitignore +++ b/.gitignore @@ -1,16 +1,17 @@ /inpla */__pycache__ /vnncomp2025_benchmarks/ -/fashion_mnist/FashionMNIST/raw -/fashion_mnist/fashion_mnist_a.onnx -/fashion_mnist/fashion_mnist_a.onnx.data -/fashion_mnist/fashion_mnist_b.onnx -/fashion_mnist/fashion_mnist_b.onnx.data -/fashion_mnist/script_argmax.fish -/fashion_mnist/script_epsilon.fish -/fashion_mnist/script_strict.fish -/xor/xor_a.onnx -/xor/xor_a.onnx.data -/xor/xor_b.onnx -/xor/xor_b.onnx.data -/fashion_mnist/FashionMNIST/raw +/examples/fashion_mnist/FashionMNIST/raw +/examples/fashion_mnist/fashion_mnist_a.onnx +/examples/fashion_mnist/fashion_mnist_a.onnx.data +/examples/fashion_mnist/fashion_mnist_b.onnx +/examples/fashion_mnist/fashion_mnist_b.onnx.data +/examples/fashion_mnist/script_argmax.fish +/examples/fashion_mnist/script_epsilon.fish +/examples/fashion_mnist/script_strict.fish +/examples/xor/xor_a.onnx +/examples/xor/xor_a.onnx.data +/examples/xor/xor_b.onnx +/examples/xor/xor_b.onnx.data +/examples/fashion_mnist/FashionMNIST/raw +/notes.norg diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..0307b44 --- /dev/null +++ b/LICENSE @@ -0,0 +1,661 @@ + GNU AFFERO GENERAL PUBLIC LICENSE + Version 3, 19 November 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The GNU Affero General Public License is a free, copyleft license for +software and other kinds of works, specifically designed to ensure +cooperation with the community in the case of network server software. + + The licenses for most software and other practical works are designed +to take away your freedom to share and change the works. By contrast, +our General Public Licenses are intended to guarantee your freedom to +share and change all versions of a program--to make sure it remains free +software for all its users. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +them if you wish), that you receive source code or can get it if you +want it, that you can change the software or use pieces of it in new +free programs, and that you know you can do these things. + + Developers that use our General Public Licenses protect your rights +with two steps: (1) assert copyright on the software, and (2) offer +you this License which gives you legal permission to copy, distribute +and/or modify the software. + + A secondary benefit of defending all users' freedom is that +improvements made in alternate versions of the program, if they +receive widespread use, become available for other developers to +incorporate. Many developers of free software are heartened and +encouraged by the resulting cooperation. However, in the case of +software used on network servers, this result may fail to come about. +The GNU General Public License permits making a modified version and +letting the public access it on a server without ever releasing its +source code to the public. + + The GNU Affero General Public License is designed specifically to +ensure that, in such cases, the modified source code becomes available +to the community. It requires the operator of a network server to +provide the source code of the modified version running there to the +users of that server. Therefore, public use of a modified version, on +a publicly accessible server, gives the public access to the source +code of the modified version. + + An older license, called the Affero General Public License and +published by Affero, was designed to accomplish similar goals. This is +a different license, not a version of the Affero GPL, but Affero has +released a new version of the Affero GPL which permits relicensing under +this license. + + The precise terms and conditions for copying, distribution and +modification follow. + + TERMS AND CONDITIONS + + 0. Definitions. + + "This License" refers to version 3 of the GNU Affero General Public License. + + "Copyright" also means copyright-like laws that apply to other kinds of +works, such as semiconductor masks. + + "The Program" refers to any copyrightable work licensed under this +License. Each licensee is addressed as "you". "Licensees" and +"recipients" may be individuals or organizations. + + To "modify" a work means to copy from or adapt all or part of the work +in a fashion requiring copyright permission, other than the making of an +exact copy. The resulting work is called a "modified version" of the +earlier work or a work "based on" the earlier work. + + A "covered work" means either the unmodified Program or a work based +on the Program. + + To "propagate" a work means to do anything with it that, without +permission, would make you directly or secondarily liable for +infringement under applicable copyright law, except executing it on a +computer or modifying a private copy. Propagation includes copying, +distribution (with or without modification), making available to the +public, and in some countries other activities as well. + + To "convey" a work means any kind of propagation that enables other +parties to make or receive copies. Mere interaction with a user through +a computer network, with no transfer of a copy, is not conveying. + + An interactive user interface displays "Appropriate Legal Notices" +to the extent that it includes a convenient and prominently visible +feature that (1) displays an appropriate copyright notice, and (2) +tells the user that there is no warranty for the work (except to the +extent that warranties are provided), that licensees may convey the +work under this License, and how to view a copy of this License. If +the interface presents a list of user commands or options, such as a +menu, a prominent item in the list meets this criterion. + + 1. Source Code. + + The "source code" for a work means the preferred form of the work +for making modifications to it. "Object code" means any non-source +form of a work. + + A "Standard Interface" means an interface that either is an official +standard defined by a recognized standards body, or, in the case of +interfaces specified for a particular programming language, one that +is widely used among developers working in that language. + + The "System Libraries" of an executable work include anything, other +than the work as a whole, that (a) is included in the normal form of +packaging a Major Component, but which is not part of that Major +Component, and (b) serves only to enable use of the work with that +Major Component, or to implement a Standard Interface for which an +implementation is available to the public in source code form. A +"Major Component", in this context, means a major essential component +(kernel, window system, and so on) of the specific operating system +(if any) on which the executable work runs, or a compiler used to +produce the work, or an object code interpreter used to run it. + + The "Corresponding Source" for a work in object code form means all +the source code needed to generate, install, and (for an executable +work) run the object code and to modify the work, including scripts to +control those activities. However, it does not include the work's +System Libraries, or general-purpose tools or generally available free +programs which are used unmodified in performing those activities but +which are not part of the work. For example, Corresponding Source +includes interface definition files associated with source files for +the work, and the source code for shared libraries and dynamically +linked subprograms that the work is specifically designed to require, +such as by intimate data communication or control flow between those +subprograms and other parts of the work. + + The Corresponding Source need not include anything that users +can regenerate automatically from other parts of the Corresponding +Source. + + The Corresponding Source for a work in source code form is that +same work. + + 2. Basic Permissions. + + All rights granted under this License are granted for the term of +copyright on the Program, and are irrevocable provided the stated +conditions are met. This License explicitly affirms your unlimited +permission to run the unmodified Program. The output from running a +covered work is covered by this License only if the output, given its +content, constitutes a covered work. This License acknowledges your +rights of fair use or other equivalent, as provided by copyright law. + + You may make, run and propagate covered works that you do not +convey, without conditions so long as your license otherwise remains +in force. You may convey covered works to others for the sole purpose +of having them make modifications exclusively for you, or provide you +with facilities for running those works, provided that you comply with +the terms of this License in conveying all material for which you do +not control copyright. Those thus making or running the covered works +for you must do so exclusively on your behalf, under your direction +and control, on terms that prohibit them from making any copies of +your copyrighted material outside their relationship with you. + + Conveying under any other circumstances is permitted solely under +the conditions stated below. Sublicensing is not allowed; section 10 +makes it unnecessary. + + 3. Protecting Users' Legal Rights From Anti-Circumvention Law. + + No covered work shall be deemed part of an effective technological +measure under any applicable law fulfilling obligations under article +11 of the WIPO copyright treaty adopted on 20 December 1996, or +similar laws prohibiting or restricting circumvention of such +measures. + + When you convey a covered work, you waive any legal power to forbid +circumvention of technological measures to the extent such circumvention +is effected by exercising rights under this License with respect to +the covered work, and you disclaim any intention to limit operation or +modification of the work as a means of enforcing, against the work's +users, your or third parties' legal rights to forbid circumvention of +technological measures. + + 4. Conveying Verbatim Copies. + + You may convey verbatim copies of the Program's source code as you +receive it, in any medium, provided that you conspicuously and +appropriately publish on each copy an appropriate copyright notice; +keep intact all notices stating that this License and any +non-permissive terms added in accord with section 7 apply to the code; +keep intact all notices of the absence of any warranty; and give all +recipients a copy of this License along with the Program. + + You may charge any price or no price for each copy that you convey, +and you may offer support or warranty protection for a fee. + + 5. Conveying Modified Source Versions. + + You may convey a work based on the Program, or the modifications to +produce it from the Program, in the form of source code under the +terms of section 4, provided that you also meet all of these conditions: + + a) The work must carry prominent notices stating that you modified + it, and giving a relevant date. + + b) The work must carry prominent notices stating that it is + released under this License and any conditions added under section + 7. This requirement modifies the requirement in section 4 to + "keep intact all notices". + + c) You must license the entire work, as a whole, under this + License to anyone who comes into possession of a copy. This + License will therefore apply, along with any applicable section 7 + additional terms, to the whole of the work, and all its parts, + regardless of how they are packaged. This License gives no + permission to license the work in any other way, but it does not + invalidate such permission if you have separately received it. + + d) If the work has interactive user interfaces, each must display + Appropriate Legal Notices; however, if the Program has interactive + interfaces that do not display Appropriate Legal Notices, your + work need not make them do so. + + A compilation of a covered work with other separate and independent +works, which are not by their nature extensions of the covered work, +and which are not combined with it such as to form a larger program, +in or on a volume of a storage or distribution medium, is called an +"aggregate" if the compilation and its resulting copyright are not +used to limit the access or legal rights of the compilation's users +beyond what the individual works permit. Inclusion of a covered work +in an aggregate does not cause this License to apply to the other +parts of the aggregate. + + 6. Conveying Non-Source Forms. + + You may convey a covered work in object code form under the terms +of sections 4 and 5, provided that you also convey the +machine-readable Corresponding Source under the terms of this License, +in one of these ways: + + a) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by the + Corresponding Source fixed on a durable physical medium + customarily used for software interchange. + + b) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by a + written offer, valid for at least three years and valid for as + long as you offer spare parts or customer support for that product + model, to give anyone who possesses the object code either (1) a + copy of the Corresponding Source for all the software in the + product that is covered by this License, on a durable physical + medium customarily used for software interchange, for a price no + more than your reasonable cost of physically performing this + conveying of source, or (2) access to copy the + Corresponding Source from a network server at no charge. + + c) Convey individual copies of the object code with a copy of the + written offer to provide the Corresponding Source. This + alternative is allowed only occasionally and noncommercially, and + only if you received the object code with such an offer, in accord + with subsection 6b. + + d) Convey the object code by offering access from a designated + place (gratis or for a charge), and offer equivalent access to the + Corresponding Source in the same way through the same place at no + further charge. You need not require recipients to copy the + Corresponding Source along with the object code. If the place to + copy the object code is a network server, the Corresponding Source + may be on a different server (operated by you or a third party) + that supports equivalent copying facilities, provided you maintain + clear directions next to the object code saying where to find the + Corresponding Source. Regardless of what server hosts the + Corresponding Source, you remain obligated to ensure that it is + available for as long as needed to satisfy these requirements. + + e) Convey the object code using peer-to-peer transmission, provided + you inform other peers where the object code and Corresponding + Source of the work are being offered to the general public at no + charge under subsection 6d. + + A separable portion of the object code, whose source code is excluded +from the Corresponding Source as a System Library, need not be +included in conveying the object code work. + + A "User Product" is either (1) a "consumer product", which means any +tangible personal property which is normally used for personal, family, +or household purposes, or (2) anything designed or sold for incorporation +into a dwelling. In determining whether a product is a consumer product, +doubtful cases shall be resolved in favor of coverage. For a particular +product received by a particular user, "normally used" refers to a +typical or common use of that class of product, regardless of the status +of the particular user or of the way in which the particular user +actually uses, or expects or is expected to use, the product. A product +is a consumer product regardless of whether the product has substantial +commercial, industrial or non-consumer uses, unless such uses represent +the only significant mode of use of the product. + + "Installation Information" for a User Product means any methods, +procedures, authorization keys, or other information required to install +and execute modified versions of a covered work in that User Product from +a modified version of its Corresponding Source. The information must +suffice to ensure that the continued functioning of the modified object +code is in no case prevented or interfered with solely because +modification has been made. + + If you convey an object code work under this section in, or with, or +specifically for use in, a User Product, and the conveying occurs as +part of a transaction in which the right of possession and use of the +User Product is transferred to the recipient in perpetuity or for a +fixed term (regardless of how the transaction is characterized), the +Corresponding Source conveyed under this section must be accompanied +by the Installation Information. But this requirement does not apply +if neither you nor any third party retains the ability to install +modified object code on the User Product (for example, the work has +been installed in ROM). + + The requirement to provide Installation Information does not include a +requirement to continue to provide support service, warranty, or updates +for a work that has been modified or installed by the recipient, or for +the User Product in which it has been modified or installed. Access to a +network may be denied when the modification itself materially and +adversely affects the operation of the network or violates the rules and +protocols for communication across the network. + + Corresponding Source conveyed, and Installation Information provided, +in accord with this section must be in a format that is publicly +documented (and with an implementation available to the public in +source code form), and must require no special password or key for +unpacking, reading or copying. + + 7. Additional Terms. + + "Additional permissions" are terms that supplement the terms of this +License by making exceptions from one or more of its conditions. +Additional permissions that are applicable to the entire Program shall +be treated as though they were included in this License, to the extent +that they are valid under applicable law. If additional permissions +apply only to part of the Program, that part may be used separately +under those permissions, but the entire Program remains governed by +this License without regard to the additional permissions. + + When you convey a copy of a covered work, you may at your option +remove any additional permissions from that copy, or from any part of +it. (Additional permissions may be written to require their own +removal in certain cases when you modify the work.) You may place +additional permissions on material, added by you to a covered work, +for which you have or can give appropriate copyright permission. + + Notwithstanding any other provision of this License, for material you +add to a covered work, you may (if authorized by the copyright holders of +that material) supplement the terms of this License with terms: + + a) Disclaiming warranty or limiting liability differently from the + terms of sections 15 and 16 of this License; or + + b) Requiring preservation of specified reasonable legal notices or + author attributions in that material or in the Appropriate Legal + Notices displayed by works containing it; or + + c) Prohibiting misrepresentation of the origin of that material, or + requiring that modified versions of such material be marked in + reasonable ways as different from the original version; or + + d) Limiting the use for publicity purposes of names of licensors or + authors of the material; or + + e) Declining to grant rights under trademark law for use of some + trade names, trademarks, or service marks; or + + f) Requiring indemnification of licensors and authors of that + material by anyone who conveys the material (or modified versions of + it) with contractual assumptions of liability to the recipient, for + any liability that these contractual assumptions directly impose on + those licensors and authors. + + All other non-permissive additional terms are considered "further +restrictions" within the meaning of section 10. If the Program as you +received it, or any part of it, contains a notice stating that it is +governed by this License along with a term that is a further +restriction, you may remove that term. If a license document contains +a further restriction but permits relicensing or conveying under this +License, you may add to a covered work material governed by the terms +of that license document, provided that the further restriction does +not survive such relicensing or conveying. + + If you add terms to a covered work in accord with this section, you +must place, in the relevant source files, a statement of the +additional terms that apply to those files, or a notice indicating +where to find the applicable terms. + + Additional terms, permissive or non-permissive, may be stated in the +form of a separately written license, or stated as exceptions; +the above requirements apply either way. + + 8. Termination. + + You may not propagate or modify a covered work except as expressly +provided under this License. Any attempt otherwise to propagate or +modify it is void, and will automatically terminate your rights under +this License (including any patent licenses granted under the third +paragraph of section 11). + + However, if you cease all violation of this License, then your +license from a particular copyright holder is reinstated (a) +provisionally, unless and until the copyright holder explicitly and +finally terminates your license, and (b) permanently, if the copyright +holder fails to notify you of the violation by some reasonable means +prior to 60 days after the cessation. + + Moreover, your license from a particular copyright holder is +reinstated permanently if the copyright holder notifies you of the +violation by some reasonable means, this is the first time you have +received notice of violation of this License (for any work) from that +copyright holder, and you cure the violation prior to 30 days after +your receipt of the notice. + + Termination of your rights under this section does not terminate the +licenses of parties who have received copies or rights from you under +this License. If your rights have been terminated and not permanently +reinstated, you do not qualify to receive new licenses for the same +material under section 10. + + 9. Acceptance Not Required for Having Copies. + + You are not required to accept this License in order to receive or +run a copy of the Program. Ancillary propagation of a covered work +occurring solely as a consequence of using peer-to-peer transmission +to receive a copy likewise does not require acceptance. However, +nothing other than this License grants you permission to propagate or +modify any covered work. These actions infringe copyright if you do +not accept this License. Therefore, by modifying or propagating a +covered work, you indicate your acceptance of this License to do so. + + 10. Automatic Licensing of Downstream Recipients. + + Each time you convey a covered work, the recipient automatically +receives a license from the original licensors, to run, modify and +propagate that work, subject to this License. You are not responsible +for enforcing compliance by third parties with this License. + + An "entity transaction" is a transaction transferring control of an +organization, or substantially all assets of one, or subdividing an +organization, or merging organizations. If propagation of a covered +work results from an entity transaction, each party to that +transaction who receives a copy of the work also receives whatever +licenses to the work the party's predecessor in interest had or could +give under the previous paragraph, plus a right to possession of the +Corresponding Source of the work from the predecessor in interest, if +the predecessor has it or can get it with reasonable efforts. + + You may not impose any further restrictions on the exercise of the +rights granted or affirmed under this License. For example, you may +not impose a license fee, royalty, or other charge for exercise of +rights granted under this License, and you may not initiate litigation +(including a cross-claim or counterclaim in a lawsuit) alleging that +any patent claim is infringed by making, using, selling, offering for +sale, or importing the Program or any portion of it. + + 11. Patents. + + A "contributor" is a copyright holder who authorizes use under this +License of the Program or a work on which the Program is based. The +work thus licensed is called the contributor's "contributor version". + + A contributor's "essential patent claims" are all patent claims +owned or controlled by the contributor, whether already acquired or +hereafter acquired, that would be infringed by some manner, permitted +by this License, of making, using, or selling its contributor version, +but do not include claims that would be infringed only as a +consequence of further modification of the contributor version. For +purposes of this definition, "control" includes the right to grant +patent sublicenses in a manner consistent with the requirements of +this License. + + Each contributor grants you a non-exclusive, worldwide, royalty-free +patent license under the contributor's essential patent claims, to +make, use, sell, offer for sale, import and otherwise run, modify and +propagate the contents of its contributor version. + + In the following three paragraphs, a "patent license" is any express +agreement or commitment, however denominated, not to enforce a patent +(such as an express permission to practice a patent or covenant not to +sue for patent infringement). To "grant" such a patent license to a +party means to make such an agreement or commitment not to enforce a +patent against the party. + + If you convey a covered work, knowingly relying on a patent license, +and the Corresponding Source of the work is not available for anyone +to copy, free of charge and under the terms of this License, through a +publicly available network server or other readily accessible means, +then you must either (1) cause the Corresponding Source to be so +available, or (2) arrange to deprive yourself of the benefit of the +patent license for this particular work, or (3) arrange, in a manner +consistent with the requirements of this License, to extend the patent +license to downstream recipients. "Knowingly relying" means you have +actual knowledge that, but for the patent license, your conveying the +covered work in a country, or your recipient's use of the covered work +in a country, would infringe one or more identifiable patents in that +country that you have reason to believe are valid. + + If, pursuant to or in connection with a single transaction or +arrangement, you convey, or propagate by procuring conveyance of, a +covered work, and grant a patent license to some of the parties +receiving the covered work authorizing them to use, propagate, modify +or convey a specific copy of the covered work, then the patent license +you grant is automatically extended to all recipients of the covered +work and works based on it. + + A patent license is "discriminatory" if it does not include within +the scope of its coverage, prohibits the exercise of, or is +conditioned on the non-exercise of one or more of the rights that are +specifically granted under this License. You may not convey a covered +work if you are a party to an arrangement with a third party that is +in the business of distributing software, under which you make payment +to the third party based on the extent of your activity of conveying +the work, and under which the third party grants, to any of the +parties who would receive the covered work from you, a discriminatory +patent license (a) in connection with copies of the covered work +conveyed by you (or copies made from those copies), or (b) primarily +for and in connection with specific products or compilations that +contain the covered work, unless you entered into that arrangement, +or that patent license was granted, prior to 28 March 2007. + + Nothing in this License shall be construed as excluding or limiting +any implied license or other defenses to infringement that may +otherwise be available to you under applicable patent law. + + 12. No Surrender of Others' Freedom. + + If conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot convey a +covered work so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you may +not convey it at all. For example, if you agree to terms that obligate you +to collect a royalty for further conveying from those to whom you convey +the Program, the only way you could satisfy both those terms and this +License would be to refrain entirely from conveying the Program. + + 13. Remote Network Interaction; Use with the GNU General Public License. + + Notwithstanding any other provision of this License, if you modify the +Program, your modified version must prominently offer all users +interacting with it remotely through a computer network (if your version +supports such interaction) an opportunity to receive the Corresponding +Source of your version by providing access to the Corresponding Source +from a network server at no charge, through some standard or customary +means of facilitating copying of software. This Corresponding Source +shall include the Corresponding Source for any work covered by version 3 +of the GNU General Public License that is incorporated pursuant to the +following paragraph. + + Notwithstanding any other provision of this License, you have +permission to link or combine any covered work with a work licensed +under version 3 of the GNU General Public License into a single +combined work, and to convey the resulting work. The terms of this +License will continue to apply to the part which is the covered work, +but the work with which it is combined will remain governed by version +3 of the GNU General Public License. + + 14. Revised Versions of this License. + + The Free Software Foundation may publish revised and/or new versions of +the GNU Affero General Public License from time to time. Such new versions +will be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + + Each version is given a distinguishing version number. If the +Program specifies that a certain numbered version of the GNU Affero General +Public License "or any later version" applies to it, you have the +option of following the terms and conditions either of that numbered +version or of any later version published by the Free Software +Foundation. If the Program does not specify a version number of the +GNU Affero General Public License, you may choose any version ever published +by the Free Software Foundation. + + If the Program specifies that a proxy can decide which future +versions of the GNU Affero General Public License can be used, that proxy's +public statement of acceptance of a version permanently authorizes you +to choose that version for the Program. + + Later license versions may give you additional or different +permissions. However, no additional obligations are imposed on any +author or copyright holder as a result of your choosing to follow a +later version. + + 15. Disclaimer of Warranty. + + THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY +APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT +HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY +OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM +IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF +ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. Limitation of Liability. + + IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS +THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY +GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE +USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF +DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD +PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), +EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF +SUCH DAMAGES. + + 17. Interpretation of Sections 15 and 16. + + If the disclaimer of warranty and limitation of liability provided +above cannot be given local legal effect according to their terms, +reviewing courts shall apply local law that most closely approximates +an absolute waiver of all civil liability in connection with the +Program, unless a warranty or assumption of liability accompanies a +copy of the Program in return for a fee. + + END OF TERMS AND CONDITIONS + + How to Apply These Terms to Your New Programs + + If you develop a new program, and you want it to be of the greatest +possible use to the public, the best way to achieve this is to make it +free software which everyone can redistribute and change under these terms. + + To do so, attach the following notices to the program. It is safest +to attach them to the start of each source file to most effectively +state the exclusion of warranty; and each file should have at least +the "copyright" line and a pointer to where the full notice is found. + + Neural Network Equivalence (NNEQ) + Copyright (C) 2026 Eric Marin + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU Affero General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU Affero General Public License for more details. + + You should have received a copy of the GNU Affero General Public License + along with this program. If not, see . + +Also add information on how to contact you by electronic and paper mail. + + If your software can interact with users remotely through a computer +network, you should also make sure that it provides a way for users to +get its source. For example, if your program is a web application, its +interface could display a "Source" link that leads users to an archive +of the code. There are many ways you could offer source, and different +solutions will be better for different programs; see section 13 for the +specific requirements. + + You should also get your employer (if you work as a programmer) or school, +if any, to sign a "copyright disclaimer" for the program, if necessary. +For more information on this, and how to apply and follow the GNU AGPL, see +. diff --git a/README.md b/README.md index ce759eb..2425ab9 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,11 @@ +# Neural Network Equivalence (NNEQ) + Requires my [fork of Inpla](https://github.com/eric-marin/inpla). - Clone the fork - **make** the executable - Copy the **inpla** executable in NNEQ/ + +## License + +This project is licensed under the GNU Affero General Public License v3.0 - see the [LICENSE](LICENSE) file for details. diff --git a/examples/fashion_mnist/fashion_mnist.py b/examples/fashion_mnist/fashion_mnist.py new file mode 100644 index 0000000..1c9dcf7 --- /dev/null +++ b/examples/fashion_mnist/fashion_mnist.py @@ -0,0 +1,53 @@ +import torch, torch.nn as nn +from torchvision.datasets import FashionMNIST +from torch.utils.data import DataLoader +from torchvision import transforms + +class FashionMNIST_MLP(nn.Module): + def __init__(self, hidden_dim): + super().__init__() + self.layers = nn.Sequential( + nn.Flatten(), + nn.Linear(6 * 6, hidden_dim), + nn.ReLU(), + nn.Linear(hidden_dim, 2) + ) + def forward(self, x): + return self.layers(x) + +transform = transforms.Compose([ + transforms.Resize((6, 6)), + transforms.ToTensor(), +]) + +train_dataset = FashionMNIST('./', download=True, transform=transform, train=True) +tshirts_trousers = [id for id, data in enumerate(train_dataset.targets) if data.item() == 0 or data.item() == 1] +train_dataset = torch.utils.data.Subset(train_dataset, tshirts_trousers) + +trainloader = DataLoader(train_dataset, batch_size=128, shuffle=True) + +def train_model(name: str, dim): + net = FashionMNIST_MLP(hidden_dim=dim) + loss_fn = nn.CrossEntropyLoss() + optimizer = torch.optim.Adam(net.parameters(), lr=1e-4) + + print(f"Training {name}...") + for epoch in range(100): + global loss + for data in trainloader: + inputs, targets = data + optimizer.zero_grad() + outputs = net(inputs) + loss = loss_fn(outputs, targets) + loss.backward() + optimizer.step() + if (epoch + 1) % 10 == 0: + print(f" Epoch {epoch+1}, Loss: {loss.item():.4f}") + return net + +if __name__ == "__main__": + torch_net_a = train_model("Network A", 6).eval() + torch_net_b = train_model("Network B", 12).eval() + + torch.onnx.export(torch_net_a, (torch.randn(1, 1, 6, 6),), "fashion_mnist_a.onnx") + torch.onnx.export(torch_net_b, (torch.randn(1, 1, 6, 6),), "fashion_mnist_b.onnx") diff --git a/examples/fashion_mnist/fashion_mnist_argmax.vnnlib b/examples/fashion_mnist/fashion_mnist_argmax.vnnlib new file mode 100644 index 0000000..0c4412b --- /dev/null +++ b/examples/fashion_mnist/fashion_mnist_argmax.vnnlib @@ -0,0 +1,133 @@ +; Argmax Equivalence for reduced FashionMNIST + +; Constant declaration +(declare-const X_0 Real) +(declare-const X_1 Real) +(declare-const X_2 Real) +(declare-const X_3 Real) +(declare-const X_4 Real) +(declare-const X_5 Real) +(declare-const X_6 Real) +(declare-const X_7 Real) +(declare-const X_8 Real) +(declare-const X_9 Real) +(declare-const X_10 Real) +(declare-const X_11 Real) +(declare-const X_12 Real) +(declare-const X_13 Real) +(declare-const X_14 Real) +(declare-const X_15 Real) +(declare-const X_16 Real) +(declare-const X_17 Real) +(declare-const X_18 Real) +(declare-const X_19 Real) +(declare-const X_20 Real) +(declare-const X_21 Real) +(declare-const X_22 Real) +(declare-const X_23 Real) +(declare-const X_24 Real) +(declare-const X_25 Real) +(declare-const X_26 Real) +(declare-const X_27 Real) +(declare-const X_28 Real) +(declare-const X_29 Real) +(declare-const X_30 Real) +(declare-const X_31 Real) +(declare-const X_32 Real) +(declare-const X_33 Real) +(declare-const X_34 Real) +(declare-const X_35 Real) +(declare-const Y_0 Real) +(declare-const Y_1 Real) +(declare-const Y_2 Real) +(declare-const Y_3 Real) + +; Bounded inputs: X must be within [0, 1] +(assert (>= X_0 0.0)) +(assert (<= X_0 1.0)) +(assert (>= X_1 0.0)) +(assert (<= X_1 1.0)) +(assert (>= X_2 0.0)) +(assert (<= X_2 1.0)) +(assert (>= X_3 0.0)) +(assert (<= X_3 1.0)) +(assert (>= X_4 0.0)) +(assert (<= X_4 1.0)) +(assert (>= X_5 0.0)) +(assert (<= X_5 1.0)) +(assert (>= X_6 0.0)) +(assert (<= X_6 1.0)) +(assert (>= X_7 0.0)) +(assert (<= X_7 1.0)) +(assert (>= X_8 0.0)) +(assert (<= X_8 1.0)) +(assert (>= X_9 0.0)) +(assert (<= X_9 1.0)) +(assert (>= X_10 0.0)) +(assert (<= X_10 1.0)) +(assert (>= X_11 0.0)) +(assert (<= X_11 1.0)) +(assert (>= X_12 0.0)) +(assert (<= X_12 1.0)) +(assert (>= X_13 0.0)) +(assert (<= X_13 1.0)) +(assert (>= X_14 0.0)) +(assert (<= X_14 1.0)) +(assert (>= X_15 0.0)) +(assert (<= X_15 1.0)) +(assert (>= X_16 0.0)) +(assert (<= X_16 1.0)) +(assert (>= X_17 0.0)) +(assert (<= X_17 1.0)) +(assert (>= X_18 0.0)) +(assert (<= X_18 1.0)) +(assert (>= X_19 0.0)) +(assert (<= X_19 1.0)) +(assert (>= X_20 0.0)) +(assert (<= X_20 1.0)) +(assert (>= X_21 0.0)) +(assert (<= X_21 1.0)) +(assert (>= X_22 0.0)) +(assert (<= X_22 1.0)) +(assert (>= X_23 0.0)) +(assert (<= X_23 1.0)) +(assert (>= X_24 0.0)) +(assert (<= X_24 1.0)) +(assert (>= X_25 0.0)) +(assert (<= X_25 1.0)) +(assert (>= X_26 0.0)) +(assert (<= X_26 1.0)) +(assert (>= X_27 0.0)) +(assert (<= X_27 1.0)) +(assert (>= X_28 0.0)) +(assert (<= X_28 1.0)) +(assert (>= X_29 0.0)) +(assert (<= X_29 1.0)) +(assert (>= X_30 0.0)) +(assert (<= X_30 1.0)) +(assert (>= X_31 0.0)) +(assert (<= X_31 1.0)) +(assert (>= X_32 0.0)) +(assert (<= X_32 1.0)) +(assert (>= X_33 0.0)) +(assert (<= X_33 1.0)) +(assert (>= X_34 0.0)) +(assert (<= X_34 1.0)) +(assert (>= X_35 0.0)) +(assert (<= X_35 1.0)) + +; Violation of argmax equivalence +(assert (or + (and + (> Y_0 Y_1) + (or + (> Y_3 Y_2) + ) + ) + (and + (> Y_1 Y_0) + (or + (> Y_2 Y_3) + ) + ) +)) diff --git a/examples/fashion_mnist/fashion_mnist_epsilon.vnnlib b/examples/fashion_mnist/fashion_mnist_epsilon.vnnlib new file mode 100644 index 0000000..948e501 --- /dev/null +++ b/examples/fashion_mnist/fashion_mnist_epsilon.vnnlib @@ -0,0 +1,124 @@ +; Strict Equivalence for reduced FashionMNIST + +; Constant declaration +(declare-const X_0 Real) +(declare-const X_1 Real) +(declare-const X_2 Real) +(declare-const X_3 Real) +(declare-const X_4 Real) +(declare-const X_5 Real) +(declare-const X_6 Real) +(declare-const X_7 Real) +(declare-const X_8 Real) +(declare-const X_9 Real) +(declare-const X_10 Real) +(declare-const X_11 Real) +(declare-const X_12 Real) +(declare-const X_13 Real) +(declare-const X_14 Real) +(declare-const X_15 Real) +(declare-const X_16 Real) +(declare-const X_17 Real) +(declare-const X_18 Real) +(declare-const X_19 Real) +(declare-const X_20 Real) +(declare-const X_21 Real) +(declare-const X_22 Real) +(declare-const X_23 Real) +(declare-const X_24 Real) +(declare-const X_25 Real) +(declare-const X_26 Real) +(declare-const X_27 Real) +(declare-const X_28 Real) +(declare-const X_29 Real) +(declare-const X_30 Real) +(declare-const X_31 Real) +(declare-const X_32 Real) +(declare-const X_33 Real) +(declare-const X_34 Real) +(declare-const X_35 Real) +(declare-const Y_0 Real) +(declare-const Y_1 Real) +(declare-const Y_2 Real) +(declare-const Y_3 Real) + +; Bounded inputs: X must be within [0, 1] +(assert (>= X_0 0.0)) +(assert (<= X_0 1.0)) +(assert (>= X_1 0.0)) +(assert (<= X_1 1.0)) +(assert (>= X_2 0.0)) +(assert (<= X_2 1.0)) +(assert (>= X_3 0.0)) +(assert (<= X_3 1.0)) +(assert (>= X_4 0.0)) +(assert (<= X_4 1.0)) +(assert (>= X_5 0.0)) +(assert (<= X_5 1.0)) +(assert (>= X_6 0.0)) +(assert (<= X_6 1.0)) +(assert (>= X_7 0.0)) +(assert (<= X_7 1.0)) +(assert (>= X_8 0.0)) +(assert (<= X_8 1.0)) +(assert (>= X_9 0.0)) +(assert (<= X_9 1.0)) +(assert (>= X_10 0.0)) +(assert (<= X_10 1.0)) +(assert (>= X_11 0.0)) +(assert (<= X_11 1.0)) +(assert (>= X_12 0.0)) +(assert (<= X_12 1.0)) +(assert (>= X_13 0.0)) +(assert (<= X_13 1.0)) +(assert (>= X_14 0.0)) +(assert (<= X_14 1.0)) +(assert (>= X_15 0.0)) +(assert (<= X_15 1.0)) +(assert (>= X_16 0.0)) +(assert (<= X_16 1.0)) +(assert (>= X_17 0.0)) +(assert (<= X_17 1.0)) +(assert (>= X_18 0.0)) +(assert (<= X_18 1.0)) +(assert (>= X_19 0.0)) +(assert (<= X_19 1.0)) +(assert (>= X_20 0.0)) +(assert (<= X_20 1.0)) +(assert (>= X_21 0.0)) +(assert (<= X_21 1.0)) +(assert (>= X_22 0.0)) +(assert (<= X_22 1.0)) +(assert (>= X_23 0.0)) +(assert (<= X_23 1.0)) +(assert (>= X_24 0.0)) +(assert (<= X_24 1.0)) +(assert (>= X_25 0.0)) +(assert (<= X_25 1.0)) +(assert (>= X_26 0.0)) +(assert (<= X_26 1.0)) +(assert (>= X_27 0.0)) +(assert (<= X_27 1.0)) +(assert (>= X_28 0.0)) +(assert (<= X_28 1.0)) +(assert (>= X_29 0.0)) +(assert (<= X_29 1.0)) +(assert (>= X_30 0.0)) +(assert (<= X_30 1.0)) +(assert (>= X_31 0.0)) +(assert (<= X_31 1.0)) +(assert (>= X_32 0.0)) +(assert (<= X_32 1.0)) +(assert (>= X_33 0.0)) +(assert (<= X_33 1.0)) +(assert (>= X_34 0.0)) +(assert (<= X_34 1.0)) +(assert (>= X_35 0.0)) +(assert (<= X_35 1.0)) + +; Violation of epsilon equivalence (epsilon = 0.1) +(define-fun absolute ((x Real)) Real (if (>= x 0) x (- x))) +(assert (or + (> (absolute (- Y_0 Y_2)) 0.1) + (> (absolute (- Y_1 Y_3)) 0.1) +)) diff --git a/examples/fashion_mnist/fashion_mnist_strict.vnnlib b/examples/fashion_mnist/fashion_mnist_strict.vnnlib new file mode 100644 index 0000000..8242c34 --- /dev/null +++ b/examples/fashion_mnist/fashion_mnist_strict.vnnlib @@ -0,0 +1,123 @@ +; Strict Equivalence for reduced FashionMNIST + +; Constant declaration +(declare-const X_0 Real) +(declare-const X_1 Real) +(declare-const X_2 Real) +(declare-const X_3 Real) +(declare-const X_4 Real) +(declare-const X_5 Real) +(declare-const X_6 Real) +(declare-const X_7 Real) +(declare-const X_8 Real) +(declare-const X_9 Real) +(declare-const X_10 Real) +(declare-const X_11 Real) +(declare-const X_12 Real) +(declare-const X_13 Real) +(declare-const X_14 Real) +(declare-const X_15 Real) +(declare-const X_16 Real) +(declare-const X_17 Real) +(declare-const X_18 Real) +(declare-const X_19 Real) +(declare-const X_20 Real) +(declare-const X_21 Real) +(declare-const X_22 Real) +(declare-const X_23 Real) +(declare-const X_24 Real) +(declare-const X_25 Real) +(declare-const X_26 Real) +(declare-const X_27 Real) +(declare-const X_28 Real) +(declare-const X_29 Real) +(declare-const X_30 Real) +(declare-const X_31 Real) +(declare-const X_32 Real) +(declare-const X_33 Real) +(declare-const X_34 Real) +(declare-const X_35 Real) +(declare-const Y_0 Real) +(declare-const Y_1 Real) +(declare-const Y_2 Real) +(declare-const Y_3 Real) + +; Bounded inputs: X must be within [0, 1] +(assert (>= X_0 0.0)) +(assert (<= X_0 1.0)) +(assert (>= X_1 0.0)) +(assert (<= X_1 1.0)) +(assert (>= X_2 0.0)) +(assert (<= X_2 1.0)) +(assert (>= X_3 0.0)) +(assert (<= X_3 1.0)) +(assert (>= X_4 0.0)) +(assert (<= X_4 1.0)) +(assert (>= X_5 0.0)) +(assert (<= X_5 1.0)) +(assert (>= X_6 0.0)) +(assert (<= X_6 1.0)) +(assert (>= X_7 0.0)) +(assert (<= X_7 1.0)) +(assert (>= X_8 0.0)) +(assert (<= X_8 1.0)) +(assert (>= X_9 0.0)) +(assert (<= X_9 1.0)) +(assert (>= X_10 0.0)) +(assert (<= X_10 1.0)) +(assert (>= X_11 0.0)) +(assert (<= X_11 1.0)) +(assert (>= X_12 0.0)) +(assert (<= X_12 1.0)) +(assert (>= X_13 0.0)) +(assert (<= X_13 1.0)) +(assert (>= X_14 0.0)) +(assert (<= X_14 1.0)) +(assert (>= X_15 0.0)) +(assert (<= X_15 1.0)) +(assert (>= X_16 0.0)) +(assert (<= X_16 1.0)) +(assert (>= X_17 0.0)) +(assert (<= X_17 1.0)) +(assert (>= X_18 0.0)) +(assert (<= X_18 1.0)) +(assert (>= X_19 0.0)) +(assert (<= X_19 1.0)) +(assert (>= X_20 0.0)) +(assert (<= X_20 1.0)) +(assert (>= X_21 0.0)) +(assert (<= X_21 1.0)) +(assert (>= X_22 0.0)) +(assert (<= X_22 1.0)) +(assert (>= X_23 0.0)) +(assert (<= X_23 1.0)) +(assert (>= X_24 0.0)) +(assert (<= X_24 1.0)) +(assert (>= X_25 0.0)) +(assert (<= X_25 1.0)) +(assert (>= X_26 0.0)) +(assert (<= X_26 1.0)) +(assert (>= X_27 0.0)) +(assert (<= X_27 1.0)) +(assert (>= X_28 0.0)) +(assert (<= X_28 1.0)) +(assert (>= X_29 0.0)) +(assert (<= X_29 1.0)) +(assert (>= X_30 0.0)) +(assert (<= X_30 1.0)) +(assert (>= X_31 0.0)) +(assert (<= X_31 1.0)) +(assert (>= X_32 0.0)) +(assert (<= X_32 1.0)) +(assert (>= X_33 0.0)) +(assert (<= X_33 1.0)) +(assert (>= X_34 0.0)) +(assert (<= X_34 1.0)) +(assert (>= X_35 0.0)) +(assert (<= X_35 1.0)) + +; Violation of strict equivalence +(assert (or + (not (= Y_0 Y_2)) + (not (= Y_1 Y_3)) +)) diff --git a/examples/verify_fashion_mnist.py b/examples/verify_fashion_mnist.py new file mode 100644 index 0000000..4de0d1e --- /dev/null +++ b/examples/verify_fashion_mnist.py @@ -0,0 +1,50 @@ +# Copyright (C) 2026 Eric Marin +# +# This program is free software: you can redistribute it and/or modify +# it under the terms of the GNU Affero General Public License as +# published by the Free Software Foundation, either version 3 of the +# License, or (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU Affero General Public License for more details. +# +# You should have received a copy of the GNU Affero General Public License +# along with this program. If not, see . + +import sys, os +sys.path.append(os.path.dirname(os.path.dirname(os.path.abspath(__file__)))) + +import z3 +import nneq + +def check_property(onnx_a, onnx_b, vnnlib): + solver = nneq.Solver() + + print(f"--- Checking {vnnlib} ---") + + solver.load_onnx(onnx_a) + solver.load_onnx(onnx_b) + solver.load_vnnlib(vnnlib) + + result = solver.check() + + if result == z3.unsat: + print("VERIFIED (UNSAT): The networks are equivalent under this property.") + elif result == z3.sat: + print("FAILED (SAT): The networks are NOT equivalent.") + print("Counter-example input:") + print(solver.model()) + # m = solver.model() + # sorted_symbols = sorted([s for s in m.decls() if s.name().startswith("X_")], key=lambda s: s.name()) + # for s in sorted_symbols: + # print(f" {s.name()} = {m[s]}") + else: + print("UNKNOWN") + print("") + +if __name__ == "__main__": + check_property("./examples/fashion_mnist/fashion_mnist_a.onnx", "./examples/fashion_mnist/fashion_mnist_b.onnx", "./examples/fashion_mnist/fashion_mnist_strict.vnnlib") + check_property("./examples/fashion_mnist/fashion_mnist_a.onnx", "./examples/fashion_mnist/fashion_mnist_b.onnx", "./examples/fashion_mnist/fashion_mnist_epsilon.vnnlib") + check_property("./examples/fashion_mnist/fashion_mnist_a.onnx", "./examples/fashion_mnist/fashion_mnist_b.onnx", "./examples/fashion_mnist/fashion_mnist_argmax.vnnlib") diff --git a/examples/verify_xor.py b/examples/verify_xor.py new file mode 100644 index 0000000..f1de0cb --- /dev/null +++ b/examples/verify_xor.py @@ -0,0 +1,50 @@ +# Copyright (C) 2026 Eric Marin +# +# This program is free software: you can redistribute it and/or modify +# it under the terms of the GNU Affero General Public License as +# published by the Free Software Foundation, either version 3 of the +# License, or (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU Affero General Public License for more details. +# +# You should have received a copy of the GNU Affero General Public License +# along with this program. If not, see . + +import sys, os +sys.path.append(os.path.dirname(os.path.dirname(os.path.abspath(__file__)))) + +import z3 +import nneq + +def check_property(onnx_a, onnx_b, vnnlib): + solver = nneq.Solver() + + print(f"--- Checking {vnnlib} ---") + + solver.load_onnx(onnx_a) + solver.load_onnx(onnx_b) + solver.load_vnnlib(vnnlib) + + result = solver.check() + + if result == z3.unsat: + print("VERIFIED (UNSAT): The networks are equivalent under this property.") + elif result == z3.sat: + print("FAILED (SAT): The networks are NOT equivalent.") + print("Counter-example input:") + print(solver.model()) + # m = solver.model() + # sorted_symbols = sorted([s for s in m.decls() if s.name().startswith("X_")], key=lambda s: s.name()) + # for s in sorted_symbols: + # print(f" {s.name()} = {m[s]}") + else: + print("UNKNOWN") + print("") + +if __name__ == "__main__": + check_property("./examples/xor/xor_a.onnx", "./examples/xor/xor_b.onnx", "./examples/xor/xor_strict.vnnlib") + check_property("./examples/xor/xor_a.onnx", "./examples/xor/xor_b.onnx", "./examples/xor/xor_epsilon.vnnlib") + check_property("./examples/xor/xor_a.onnx", "./examples/xor/xor_b.onnx", "./examples/xor/xor_argmax.vnnlib") diff --git a/examples/xor/xor.py b/examples/xor/xor.py new file mode 100644 index 0000000..ebc5477 --- /dev/null +++ b/examples/xor/xor.py @@ -0,0 +1,40 @@ +import torch +import torch.nn as nn +import torch.onnx + +class xor_mlp(nn.Module): + def __init__(self, hidden_dim): + super().__init__() + self.layers = nn.Sequential( + nn.Linear(2, hidden_dim), + nn.ReLU(), + nn.Linear(hidden_dim, 1) + ) + def forward(self, x): + return self.layers(x) + +def train_model(name: str, dim): + X = torch.tensor([[0,0], [0,1], [1,0], [1,1]], dtype=torch.float32) + Y = torch.tensor([[0], [1], [1], [0]], dtype=torch.float32) + + net = xor_mlp(hidden_dim=dim) + loss_fn = nn.MSELoss() + optimizer = torch.optim.Adam(net.parameters(), lr=0.1) + + print(f"Training {name}...") + for epoch in range(1000): + optimizer.zero_grad() + out = net(X) + loss = loss_fn(out, Y) + loss.backward() + optimizer.step() + if (epoch+1) % 100 == 0: + print(f" Epoch {epoch+1}, Loss: {loss.item():.4f}") + return net + +if __name__ == "__main__": + torch_net_a = train_model("Network A", 8).eval() + torch_net_b = train_model("Network B", 16).eval() + + torch.onnx.export(torch_net_a, (torch.randn(1, 2),), "xor_a.onnx") + torch.onnx.export(torch_net_b, (torch.randn(1, 2),), "xor_b.onnx") diff --git a/examples/xor/xor_argmax.vnnlib b/examples/xor/xor_argmax.vnnlib new file mode 100644 index 0000000..d38bc31 --- /dev/null +++ b/examples/xor/xor_argmax.vnnlib @@ -0,0 +1,14 @@ +; Argmax Equivalence for XOR + +; Constant declaration +(declare-const X_0 Real) +(declare-const X_1 Real) +(declare-const Y_0 Real) +(declare-const Y_1 Real) + +; Bounded inputs: X must be 0 or 1 +(assert (or (= X_0 0) (= X_0 1))) +(assert (or (= X_1 0) (= X_1 1))) + +; Violation of argmax equivalence +(assert (not (= (> Y_0 0.5) (> Y_1 0.5)))) diff --git a/examples/xor/xor_epsilon.vnnlib b/examples/xor/xor_epsilon.vnnlib new file mode 100644 index 0000000..427243e --- /dev/null +++ b/examples/xor/xor_epsilon.vnnlib @@ -0,0 +1,15 @@ +; Epsilon Equivalence for XOR + +; Constant declaration +(declare-const X_0 Real) +(declare-const X_1 Real) +(declare-const Y_0 Real) +(declare-const Y_1 Real) + +; Bounded inputs: X must be 0 or 1 +(assert (or (= X_0 0) (= X_0 1))) +(assert (or (= X_1 0) (= X_1 1))) + +; Violation of epsilon equivalence (epsilon = 0.1) +(define-fun absolute ((x Real)) Real (if (>= x 0) x (- x))) +(assert (> (absolute (- Y_0 Y_1)) 0.1)) diff --git a/examples/xor/xor_strict.vnnlib b/examples/xor/xor_strict.vnnlib new file mode 100644 index 0000000..bead476 --- /dev/null +++ b/examples/xor/xor_strict.vnnlib @@ -0,0 +1,14 @@ +; Strict Equivalence for XOR + +; Constant declaration +(declare-const X_0 Real) +(declare-const X_1 Real) +(declare-const Y_0 Real) +(declare-const Y_1 Real) + +; Bounded inputs: X must be 0 or 1 +(assert (or (= X_0 0) (= X_0 1))) +(assert (or (= X_1 0) (= X_1 1))) + +; Violation of strict equivalence: outputs are different +(assert (not (= Y_0 Y_1))) diff --git a/fashion_mnist/fashion_mnist.py b/fashion_mnist/fashion_mnist.py deleted file mode 100644 index 1c9dcf7..0000000 --- a/fashion_mnist/fashion_mnist.py +++ /dev/null @@ -1,53 +0,0 @@ -import torch, torch.nn as nn -from torchvision.datasets import FashionMNIST -from torch.utils.data import DataLoader -from torchvision import transforms - -class FashionMNIST_MLP(nn.Module): - def __init__(self, hidden_dim): - super().__init__() - self.layers = nn.Sequential( - nn.Flatten(), - nn.Linear(6 * 6, hidden_dim), - nn.ReLU(), - nn.Linear(hidden_dim, 2) - ) - def forward(self, x): - return self.layers(x) - -transform = transforms.Compose([ - transforms.Resize((6, 6)), - transforms.ToTensor(), -]) - -train_dataset = FashionMNIST('./', download=True, transform=transform, train=True) -tshirts_trousers = [id for id, data in enumerate(train_dataset.targets) if data.item() == 0 or data.item() == 1] -train_dataset = torch.utils.data.Subset(train_dataset, tshirts_trousers) - -trainloader = DataLoader(train_dataset, batch_size=128, shuffle=True) - -def train_model(name: str, dim): - net = FashionMNIST_MLP(hidden_dim=dim) - loss_fn = nn.CrossEntropyLoss() - optimizer = torch.optim.Adam(net.parameters(), lr=1e-4) - - print(f"Training {name}...") - for epoch in range(100): - global loss - for data in trainloader: - inputs, targets = data - optimizer.zero_grad() - outputs = net(inputs) - loss = loss_fn(outputs, targets) - loss.backward() - optimizer.step() - if (epoch + 1) % 10 == 0: - print(f" Epoch {epoch+1}, Loss: {loss.item():.4f}") - return net - -if __name__ == "__main__": - torch_net_a = train_model("Network A", 6).eval() - torch_net_b = train_model("Network B", 12).eval() - - torch.onnx.export(torch_net_a, (torch.randn(1, 1, 6, 6),), "fashion_mnist_a.onnx") - torch.onnx.export(torch_net_b, (torch.randn(1, 1, 6, 6),), "fashion_mnist_b.onnx") diff --git a/fashion_mnist/fashion_mnist_argmax.vnnlib b/fashion_mnist/fashion_mnist_argmax.vnnlib deleted file mode 100644 index 0c4412b..0000000 --- a/fashion_mnist/fashion_mnist_argmax.vnnlib +++ /dev/null @@ -1,133 +0,0 @@ -; Argmax Equivalence for reduced FashionMNIST - -; Constant declaration -(declare-const X_0 Real) -(declare-const X_1 Real) -(declare-const X_2 Real) -(declare-const X_3 Real) -(declare-const X_4 Real) -(declare-const X_5 Real) -(declare-const X_6 Real) -(declare-const X_7 Real) -(declare-const X_8 Real) -(declare-const X_9 Real) -(declare-const X_10 Real) -(declare-const X_11 Real) -(declare-const X_12 Real) -(declare-const X_13 Real) -(declare-const X_14 Real) -(declare-const X_15 Real) -(declare-const X_16 Real) -(declare-const X_17 Real) -(declare-const X_18 Real) -(declare-const X_19 Real) -(declare-const X_20 Real) -(declare-const X_21 Real) -(declare-const X_22 Real) -(declare-const X_23 Real) -(declare-const X_24 Real) -(declare-const X_25 Real) -(declare-const X_26 Real) -(declare-const X_27 Real) -(declare-const X_28 Real) -(declare-const X_29 Real) -(declare-const X_30 Real) -(declare-const X_31 Real) -(declare-const X_32 Real) -(declare-const X_33 Real) -(declare-const X_34 Real) -(declare-const X_35 Real) -(declare-const Y_0 Real) -(declare-const Y_1 Real) -(declare-const Y_2 Real) -(declare-const Y_3 Real) - -; Bounded inputs: X must be within [0, 1] -(assert (>= X_0 0.0)) -(assert (<= X_0 1.0)) -(assert (>= X_1 0.0)) -(assert (<= X_1 1.0)) -(assert (>= X_2 0.0)) -(assert (<= X_2 1.0)) -(assert (>= X_3 0.0)) -(assert (<= X_3 1.0)) -(assert (>= X_4 0.0)) -(assert (<= X_4 1.0)) -(assert (>= X_5 0.0)) -(assert (<= X_5 1.0)) -(assert (>= X_6 0.0)) -(assert (<= X_6 1.0)) -(assert (>= X_7 0.0)) -(assert (<= X_7 1.0)) -(assert (>= X_8 0.0)) -(assert (<= X_8 1.0)) -(assert (>= X_9 0.0)) -(assert (<= X_9 1.0)) -(assert (>= X_10 0.0)) -(assert (<= X_10 1.0)) -(assert (>= X_11 0.0)) -(assert (<= X_11 1.0)) -(assert (>= X_12 0.0)) -(assert (<= X_12 1.0)) -(assert (>= X_13 0.0)) -(assert (<= X_13 1.0)) -(assert (>= X_14 0.0)) -(assert (<= X_14 1.0)) -(assert (>= X_15 0.0)) -(assert (<= X_15 1.0)) -(assert (>= X_16 0.0)) -(assert (<= X_16 1.0)) -(assert (>= X_17 0.0)) -(assert (<= X_17 1.0)) -(assert (>= X_18 0.0)) -(assert (<= X_18 1.0)) -(assert (>= X_19 0.0)) -(assert (<= X_19 1.0)) -(assert (>= X_20 0.0)) -(assert (<= X_20 1.0)) -(assert (>= X_21 0.0)) -(assert (<= X_21 1.0)) -(assert (>= X_22 0.0)) -(assert (<= X_22 1.0)) -(assert (>= X_23 0.0)) -(assert (<= X_23 1.0)) -(assert (>= X_24 0.0)) -(assert (<= X_24 1.0)) -(assert (>= X_25 0.0)) -(assert (<= X_25 1.0)) -(assert (>= X_26 0.0)) -(assert (<= X_26 1.0)) -(assert (>= X_27 0.0)) -(assert (<= X_27 1.0)) -(assert (>= X_28 0.0)) -(assert (<= X_28 1.0)) -(assert (>= X_29 0.0)) -(assert (<= X_29 1.0)) -(assert (>= X_30 0.0)) -(assert (<= X_30 1.0)) -(assert (>= X_31 0.0)) -(assert (<= X_31 1.0)) -(assert (>= X_32 0.0)) -(assert (<= X_32 1.0)) -(assert (>= X_33 0.0)) -(assert (<= X_33 1.0)) -(assert (>= X_34 0.0)) -(assert (<= X_34 1.0)) -(assert (>= X_35 0.0)) -(assert (<= X_35 1.0)) - -; Violation of argmax equivalence -(assert (or - (and - (> Y_0 Y_1) - (or - (> Y_3 Y_2) - ) - ) - (and - (> Y_1 Y_0) - (or - (> Y_2 Y_3) - ) - ) -)) diff --git a/fashion_mnist/fashion_mnist_epsilon.vnnlib b/fashion_mnist/fashion_mnist_epsilon.vnnlib deleted file mode 100644 index 948e501..0000000 --- a/fashion_mnist/fashion_mnist_epsilon.vnnlib +++ /dev/null @@ -1,124 +0,0 @@ -; Strict Equivalence for reduced FashionMNIST - -; Constant declaration -(declare-const X_0 Real) -(declare-const X_1 Real) -(declare-const X_2 Real) -(declare-const X_3 Real) -(declare-const X_4 Real) -(declare-const X_5 Real) -(declare-const X_6 Real) -(declare-const X_7 Real) -(declare-const X_8 Real) -(declare-const X_9 Real) -(declare-const X_10 Real) -(declare-const X_11 Real) -(declare-const X_12 Real) -(declare-const X_13 Real) -(declare-const X_14 Real) -(declare-const X_15 Real) -(declare-const X_16 Real) -(declare-const X_17 Real) -(declare-const X_18 Real) -(declare-const X_19 Real) -(declare-const X_20 Real) -(declare-const X_21 Real) -(declare-const X_22 Real) -(declare-const X_23 Real) -(declare-const X_24 Real) -(declare-const X_25 Real) -(declare-const X_26 Real) -(declare-const X_27 Real) -(declare-const X_28 Real) -(declare-const X_29 Real) -(declare-const X_30 Real) -(declare-const X_31 Real) -(declare-const X_32 Real) -(declare-const X_33 Real) -(declare-const X_34 Real) -(declare-const X_35 Real) -(declare-const Y_0 Real) -(declare-const Y_1 Real) -(declare-const Y_2 Real) -(declare-const Y_3 Real) - -; Bounded inputs: X must be within [0, 1] -(assert (>= X_0 0.0)) -(assert (<= X_0 1.0)) -(assert (>= X_1 0.0)) -(assert (<= X_1 1.0)) -(assert (>= X_2 0.0)) -(assert (<= X_2 1.0)) -(assert (>= X_3 0.0)) -(assert (<= X_3 1.0)) -(assert (>= X_4 0.0)) -(assert (<= X_4 1.0)) -(assert (>= X_5 0.0)) -(assert (<= X_5 1.0)) -(assert (>= X_6 0.0)) -(assert (<= X_6 1.0)) -(assert (>= X_7 0.0)) -(assert (<= X_7 1.0)) -(assert (>= X_8 0.0)) -(assert (<= X_8 1.0)) -(assert (>= X_9 0.0)) -(assert (<= X_9 1.0)) -(assert (>= X_10 0.0)) -(assert (<= X_10 1.0)) -(assert (>= X_11 0.0)) -(assert (<= X_11 1.0)) -(assert (>= X_12 0.0)) -(assert (<= X_12 1.0)) -(assert (>= X_13 0.0)) -(assert (<= X_13 1.0)) -(assert (>= X_14 0.0)) -(assert (<= X_14 1.0)) -(assert (>= X_15 0.0)) -(assert (<= X_15 1.0)) -(assert (>= X_16 0.0)) -(assert (<= X_16 1.0)) -(assert (>= X_17 0.0)) -(assert (<= X_17 1.0)) -(assert (>= X_18 0.0)) -(assert (<= X_18 1.0)) -(assert (>= X_19 0.0)) -(assert (<= X_19 1.0)) -(assert (>= X_20 0.0)) -(assert (<= X_20 1.0)) -(assert (>= X_21 0.0)) -(assert (<= X_21 1.0)) -(assert (>= X_22 0.0)) -(assert (<= X_22 1.0)) -(assert (>= X_23 0.0)) -(assert (<= X_23 1.0)) -(assert (>= X_24 0.0)) -(assert (<= X_24 1.0)) -(assert (>= X_25 0.0)) -(assert (<= X_25 1.0)) -(assert (>= X_26 0.0)) -(assert (<= X_26 1.0)) -(assert (>= X_27 0.0)) -(assert (<= X_27 1.0)) -(assert (>= X_28 0.0)) -(assert (<= X_28 1.0)) -(assert (>= X_29 0.0)) -(assert (<= X_29 1.0)) -(assert (>= X_30 0.0)) -(assert (<= X_30 1.0)) -(assert (>= X_31 0.0)) -(assert (<= X_31 1.0)) -(assert (>= X_32 0.0)) -(assert (<= X_32 1.0)) -(assert (>= X_33 0.0)) -(assert (<= X_33 1.0)) -(assert (>= X_34 0.0)) -(assert (<= X_34 1.0)) -(assert (>= X_35 0.0)) -(assert (<= X_35 1.0)) - -; Violation of epsilon equivalence (epsilon = 0.1) -(define-fun absolute ((x Real)) Real (if (>= x 0) x (- x))) -(assert (or - (> (absolute (- Y_0 Y_2)) 0.1) - (> (absolute (- Y_1 Y_3)) 0.1) -)) diff --git a/fashion_mnist/fashion_mnist_strict.vnnlib b/fashion_mnist/fashion_mnist_strict.vnnlib deleted file mode 100644 index 8242c34..0000000 --- a/fashion_mnist/fashion_mnist_strict.vnnlib +++ /dev/null @@ -1,123 +0,0 @@ -; Strict Equivalence for reduced FashionMNIST - -; Constant declaration -(declare-const X_0 Real) -(declare-const X_1 Real) -(declare-const X_2 Real) -(declare-const X_3 Real) -(declare-const X_4 Real) -(declare-const X_5 Real) -(declare-const X_6 Real) -(declare-const X_7 Real) -(declare-const X_8 Real) -(declare-const X_9 Real) -(declare-const X_10 Real) -(declare-const X_11 Real) -(declare-const X_12 Real) -(declare-const X_13 Real) -(declare-const X_14 Real) -(declare-const X_15 Real) -(declare-const X_16 Real) -(declare-const X_17 Real) -(declare-const X_18 Real) -(declare-const X_19 Real) -(declare-const X_20 Real) -(declare-const X_21 Real) -(declare-const X_22 Real) -(declare-const X_23 Real) -(declare-const X_24 Real) -(declare-const X_25 Real) -(declare-const X_26 Real) -(declare-const X_27 Real) -(declare-const X_28 Real) -(declare-const X_29 Real) -(declare-const X_30 Real) -(declare-const X_31 Real) -(declare-const X_32 Real) -(declare-const X_33 Real) -(declare-const X_34 Real) -(declare-const X_35 Real) -(declare-const Y_0 Real) -(declare-const Y_1 Real) -(declare-const Y_2 Real) -(declare-const Y_3 Real) - -; Bounded inputs: X must be within [0, 1] -(assert (>= X_0 0.0)) -(assert (<= X_0 1.0)) -(assert (>= X_1 0.0)) -(assert (<= X_1 1.0)) -(assert (>= X_2 0.0)) -(assert (<= X_2 1.0)) -(assert (>= X_3 0.0)) -(assert (<= X_3 1.0)) -(assert (>= X_4 0.0)) -(assert (<= X_4 1.0)) -(assert (>= X_5 0.0)) -(assert (<= X_5 1.0)) -(assert (>= X_6 0.0)) -(assert (<= X_6 1.0)) -(assert (>= X_7 0.0)) -(assert (<= X_7 1.0)) -(assert (>= X_8 0.0)) -(assert (<= X_8 1.0)) -(assert (>= X_9 0.0)) -(assert (<= X_9 1.0)) -(assert (>= X_10 0.0)) -(assert (<= X_10 1.0)) -(assert (>= X_11 0.0)) -(assert (<= X_11 1.0)) -(assert (>= X_12 0.0)) -(assert (<= X_12 1.0)) -(assert (>= X_13 0.0)) -(assert (<= X_13 1.0)) -(assert (>= X_14 0.0)) -(assert (<= X_14 1.0)) -(assert (>= X_15 0.0)) -(assert (<= X_15 1.0)) -(assert (>= X_16 0.0)) -(assert (<= X_16 1.0)) -(assert (>= X_17 0.0)) -(assert (<= X_17 1.0)) -(assert (>= X_18 0.0)) -(assert (<= X_18 1.0)) -(assert (>= X_19 0.0)) -(assert (<= X_19 1.0)) -(assert (>= X_20 0.0)) -(assert (<= X_20 1.0)) -(assert (>= X_21 0.0)) -(assert (<= X_21 1.0)) -(assert (>= X_22 0.0)) -(assert (<= X_22 1.0)) -(assert (>= X_23 0.0)) -(assert (<= X_23 1.0)) -(assert (>= X_24 0.0)) -(assert (<= X_24 1.0)) -(assert (>= X_25 0.0)) -(assert (<= X_25 1.0)) -(assert (>= X_26 0.0)) -(assert (<= X_26 1.0)) -(assert (>= X_27 0.0)) -(assert (<= X_27 1.0)) -(assert (>= X_28 0.0)) -(assert (<= X_28 1.0)) -(assert (>= X_29 0.0)) -(assert (<= X_29 1.0)) -(assert (>= X_30 0.0)) -(assert (<= X_30 1.0)) -(assert (>= X_31 0.0)) -(assert (<= X_31 1.0)) -(assert (>= X_32 0.0)) -(assert (<= X_32 1.0)) -(assert (>= X_33 0.0)) -(assert (<= X_33 1.0)) -(assert (>= X_34 0.0)) -(assert (<= X_34 1.0)) -(assert (>= X_35 0.0)) -(assert (<= X_35 1.0)) - -; Violation of strict equivalence -(assert (or - (not (= Y_0 Y_2)) - (not (= Y_1 Y_3)) -)) diff --git a/nneq.py b/nneq.py index 784002a..b919b17 100644 --- a/nneq.py +++ b/nneq.py @@ -1,3 +1,18 @@ +# Copyright (C) 2026 Eric Marin +# +# This program is free software: you can redistribute it and/or modify +# it under the terms of the GNU Affero General Public License as +# published by the Free Software Foundation, either version 3 of the +# License, or (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU Affero General Public License for more details. +# +# You should have received a copy of the GNU Affero General Public License +# along with this program. If not, see . + import z3 import re import numpy as np diff --git a/notes.norg b/notes.norg deleted file mode 100644 index ed823b3..0000000 --- a/notes.norg +++ /dev/null @@ -1,111 +0,0 @@ -@document.meta -title: Neural Network Equivalence -description: WIP tool to prove NNEQ using Interaction Nets as pre-processor fo my Batchelor's Thesis -authors: ericmarin -categories: research -created: 2026-03-14T09:21:24 -updated: 2026-03-25T09:32:43 -version: 1.1.1 -@end - -* TODO - - (!) Scalability: - Added cache for already processed NN. - Removed limits from Inpla, but it runs slow on big NN because of parsing overhead. - *I should write a Reduction Engine in Rust with a Work Stealing Queue to be more flexible.* - - - (x) Soundness of translated NN: - Translation from NN to IN and the Interaction Rules are proved {:proof.norg:}[here]. - - - (x) Compatibility with other types of NN: - Added support for ONNX format. - Operations: Gemm, ReLU, Flatten, Reshape, Matmul. - - - (+) Comparison with other tool ({https://github.com/NeuralNetworkVerification/Marabou}[Marabou], {https://github.com/guykatzz/ReluplexCav2017}[Reluplex]): - My tool is just a pre-processor that takes an NN, optimizes it using IN and converts in a format for SMT solvers. - Marabou and Reluplex are solvers and this tool could be used WITH them. - DeePoly/Marabou-Preprocessor: numeric bound tightening, lossy and heuristic. - ONNX-Simplifier: just folds constants. - Neurify: symbolic bound tightening (similar to the Range agent). Doesn't use a solver - - - (!) Add Range agent to enable ReLU optimization: - - - ( ) Merging Linear packets of the same variable when Adding: - - ~ Completare passo induttivo dimostrazione - ~ 2 Reti uguali NOTE - ~ 1 Rete grande NOTE - -* Agents -** Built-in - - Eraser: delete other agents recursively - - Dup: duplicates other agents recursively - -** Implemented - - Linear(x, float q, float r): represent "q*x + r" - - Concrete(float k): represent a concrete value k - - Symbolic(id): represent the variable id - - Add(out, b): represent the addition (has various steps AddCheckLinear/AddCheckConcrete) - - Mul(out, b): represent the multiplication (has various steps MulCheckLinear/MulCheckConcrete) - - ReLU(out): represent "IF x > 0 THEN x ELSE 0" - - Materialize(out): transforms a Linear packet into a final representation of TermAdd/TermMul - -* Rules -** Add - Linear(x, float q, float r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r); - - Concrete(float k) >< Add(out, b) - | k == 0 => out ~ b - | _ => b ~ AddCheckConcrete(out, k); - - Linear(y, float s, float t) >< AddCheckLinear(out, x, float q, float r) - | (q == 0) && (r == 0) && (s == 0) && (t == 0) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser - | (s == 0) && (t == 0) => out ~ Linear(x, q, r), y ~ Eraser - | (q == 0) && (r == 0) => out ~ (*L)Linear(y, s, t), x ~ Eraser - | _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermAdd(out_x, out_y), 1, 0); - - Concrete(float j) >< AddCheckLinear(out, x, float q, float r) => out ~ Linear(x, q, r + j); - - Linear(y, float s, float t) >< AddCheckConcrete(out, float k) => out ~ Linear(y, s, t + k); - - Concrete(float j) >< AddCheckConcrete(out, float k) - | j == 0 => out ~ Concrete(k) - | _ => out ~ Concrete(k + j); - -** Mul - Linear(x, float q, float r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r); - - Concrete(float k) >< Mul(out, b) - | k == 0 => b ~ Eraser, out ~ (*L)Concrete(0) - | k == 1 => out ~ b - | _ => b ~ MulCheckConcrete(out, k); - - Linear(y, float s, float t) >< MulCheckLinear(out, x, float q, float r) - | ((q == 0) && (r == 0)) || ((s == 0) && (t == 0)) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser - | _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermMul(out_x, out_y), 1, 0); - - Concrete(float j) >< MulCheckLinear(out, x, float q, float r) => out ~ Linear(x, q * j, r * j); - - Linear(y, float s, float t) >< MulCheckConcrete(out, float k) => out ~ Linear(y, s * k, t * k); - - Concrete(float j) >< MulCheckConcrete(out, float k) - | j == 0 => out ~ Concrete(0) - | j == 1 => out ~ Concrete(k) - | _ => out ~ Concrete(k * j); - -** ReLU - Linear(x, float q, float r) >< ReLU(out) => (*L)Linear(x, q, r) ~ Materialize(out_x), out ~ Linear(TermReLU(out_x), 1, 0); - - Concrete(float k) >< ReLU(out) - | k > 0 => out ~ (*L)Concrete(k) - | _ => out ~ Concrete(0); - -** Materialize - Linear(x, float q, float r) >< Materialize(out) - | (q == 0) => out ~ Concrete(r), x ~ Eraser - | (q == 1) && (r == 0) => out ~ x - | (q == 1) && (r != 0) => out ~ TermAdd(x, Concrete(r)) - | (q != 0) && (r == 0) => out ~ TermMul(Concrete(q), x) - | _ => out ~ TermAdd(TermMul(Concrete(q), x), Concrete(r)); - - Concrete(float k) >< Materialize(out) => out ~ (*L)Concrete(k); diff --git a/verify_fashion_mnist.py b/verify_fashion_mnist.py deleted file mode 100644 index 48c8bc1..0000000 --- a/verify_fashion_mnist.py +++ /dev/null @@ -1,32 +0,0 @@ -import z3 -import nneq - -def check_property(onnx_a, onnx_b, vnnlib): - solver = nneq.Solver() - - print(f"--- Checking {vnnlib} ---") - - solver.load_onnx(onnx_a) - solver.load_onnx(onnx_b) - solver.load_vnnlib(vnnlib) - - result = solver.check() - - if result == z3.unsat: - print("VERIFIED (UNSAT): The networks are equivalent under this property.") - elif result == z3.sat: - print("FAILED (SAT): The networks are NOT equivalent.") - print("Counter-example input:") - print(solver.model()) - # m = solver.model() - # sorted_symbols = sorted([s for s in m.decls() if s.name().startswith("X_")], key=lambda s: s.name()) - # for s in sorted_symbols: - # print(f" {s.name()} = {m[s]}") - else: - print("UNKNOWN") - print("") - -if __name__ == "__main__": - check_property("./fashion_mnist/fashion_mnist_a.onnx", "./fashion_mnist/fashion_mnist_b.onnx", "./fashion_mnist/fashion_mnist_strict.vnnlib") - check_property("./fashion_mnist/fashion_mnist_a.onnx", "./fashion_mnist/fashion_mnist_b.onnx", "./fashion_mnist/fashion_mnist_epsilon.vnnlib") - check_property("./fashion_mnist/fashion_mnist_a.onnx", "./fashion_mnist/fashion_mnist_b.onnx", "./fashion_mnist/fashion_mnist_argmax.vnnlib") diff --git a/verify_xor.py b/verify_xor.py deleted file mode 100644 index 90623a0..0000000 --- a/verify_xor.py +++ /dev/null @@ -1,32 +0,0 @@ -import z3 -import nneq - -def check_property(onnx_a, onnx_b, vnnlib): - solver = nneq.Solver() - - print(f"--- Checking {vnnlib} ---") - - solver.load_onnx(onnx_a) - solver.load_onnx(onnx_b) - solver.load_vnnlib(vnnlib) - - result = solver.check() - - if result == z3.unsat: - print("VERIFIED (UNSAT): The networks are equivalent under this property.") - elif result == z3.sat: - print("FAILED (SAT): The networks are NOT equivalent.") - print("Counter-example input:") - print(solver.model()) - # m = solver.model() - # sorted_symbols = sorted([s for s in m.decls() if s.name().startswith("X_")], key=lambda s: s.name()) - # for s in sorted_symbols: - # print(f" {s.name()} = {m[s]}") - else: - print("UNKNOWN") - print("") - -if __name__ == "__main__": - check_property("./xor/xor_a.onnx", "./xor/xor_b.onnx", "./xor/xor_strict.vnnlib") - check_property("./xor/xor_a.onnx", "./xor/xor_b.onnx", "./xor/xor_epsilon.vnnlib") - check_property("./xor/xor_a.onnx", "./xor/xor_b.onnx", "./xor/xor_argmax.vnnlib") diff --git a/xor/xor.py b/xor/xor.py deleted file mode 100644 index ebc5477..0000000 --- a/xor/xor.py +++ /dev/null @@ -1,40 +0,0 @@ -import torch -import torch.nn as nn -import torch.onnx - -class xor_mlp(nn.Module): - def __init__(self, hidden_dim): - super().__init__() - self.layers = nn.Sequential( - nn.Linear(2, hidden_dim), - nn.ReLU(), - nn.Linear(hidden_dim, 1) - ) - def forward(self, x): - return self.layers(x) - -def train_model(name: str, dim): - X = torch.tensor([[0,0], [0,1], [1,0], [1,1]], dtype=torch.float32) - Y = torch.tensor([[0], [1], [1], [0]], dtype=torch.float32) - - net = xor_mlp(hidden_dim=dim) - loss_fn = nn.MSELoss() - optimizer = torch.optim.Adam(net.parameters(), lr=0.1) - - print(f"Training {name}...") - for epoch in range(1000): - optimizer.zero_grad() - out = net(X) - loss = loss_fn(out, Y) - loss.backward() - optimizer.step() - if (epoch+1) % 100 == 0: - print(f" Epoch {epoch+1}, Loss: {loss.item():.4f}") - return net - -if __name__ == "__main__": - torch_net_a = train_model("Network A", 8).eval() - torch_net_b = train_model("Network B", 16).eval() - - torch.onnx.export(torch_net_a, (torch.randn(1, 2),), "xor_a.onnx") - torch.onnx.export(torch_net_b, (torch.randn(1, 2),), "xor_b.onnx") diff --git a/xor/xor_argmax.vnnlib b/xor/xor_argmax.vnnlib deleted file mode 100644 index d38bc31..0000000 --- a/xor/xor_argmax.vnnlib +++ /dev/null @@ -1,14 +0,0 @@ -; Argmax Equivalence for XOR - -; Constant declaration -(declare-const X_0 Real) -(declare-const X_1 Real) -(declare-const Y_0 Real) -(declare-const Y_1 Real) - -; Bounded inputs: X must be 0 or 1 -(assert (or (= X_0 0) (= X_0 1))) -(assert (or (= X_1 0) (= X_1 1))) - -; Violation of argmax equivalence -(assert (not (= (> Y_0 0.5) (> Y_1 0.5)))) diff --git a/xor/xor_epsilon.vnnlib b/xor/xor_epsilon.vnnlib deleted file mode 100644 index 427243e..0000000 --- a/xor/xor_epsilon.vnnlib +++ /dev/null @@ -1,15 +0,0 @@ -; Epsilon Equivalence for XOR - -; Constant declaration -(declare-const X_0 Real) -(declare-const X_1 Real) -(declare-const Y_0 Real) -(declare-const Y_1 Real) - -; Bounded inputs: X must be 0 or 1 -(assert (or (= X_0 0) (= X_0 1))) -(assert (or (= X_1 0) (= X_1 1))) - -; Violation of epsilon equivalence (epsilon = 0.1) -(define-fun absolute ((x Real)) Real (if (>= x 0) x (- x))) -(assert (> (absolute (- Y_0 Y_1)) 0.1)) diff --git a/xor/xor_strict.vnnlib b/xor/xor_strict.vnnlib deleted file mode 100644 index bead476..0000000 --- a/xor/xor_strict.vnnlib +++ /dev/null @@ -1,14 +0,0 @@ -; Strict Equivalence for XOR - -; Constant declaration -(declare-const X_0 Real) -(declare-const X_1 Real) -(declare-const Y_0 Real) -(declare-const Y_1 Real) - -; Bounded inputs: X must be 0 or 1 -(assert (or (= X_0 0) (= X_0 1))) -(assert (or (= X_1 0) (= X_1 1))) - -; Violation of strict equivalence: outputs are different -(assert (not (= Y_0 Y_1))) -- cgit v1.2.3