2 Search Results for "Shkedy, Ziv"

Document
DOI: 10.4230/LIPIcs.SAT.2025.32
Efficient Certified Reasoning for Binarized Neural Networks

Authors: Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Neural networks have emerged as essential components in safety-critical applications - these use cases demand complex, yet trustworthy computations. Binarized Neural Networks (BNNs) are a type of neural network where each neuron is constrained to a Boolean value; they are particularly well-suited for safety-critical tasks because they retain much of the computational capacities of full-scale (floating-point or quantized) deep neural networks, but remain compatible with satisfiability solvers for qualitative verification and with model counters for quantitative reasoning. However, existing methods for BNN analysis suffer from either limited scalability or susceptibility to soundness errors, which hinders their applicability in real-world scenarios. In this work, we present a scalable and trustworthy approach for both qualitative and quantitative verification of BNNs. Our approach introduces a native representation of BNN constraints in a custom-designed solver for qualitative reasoning, and in an approximate model counter for quantitative reasoning. We further develop specialized proof generation and checking pipelines with native support for BNN constraint reasoning, ensuring trustworthiness for all of our verification results. Empirical evaluations on a BNN robustness verification benchmark suite demonstrate that our certified solving approach achieves a 9× speedup over prior certified CNF and PB-based approaches, and our certified counting approach achieves a 218× speedup over the existing CNF-based baseline. In terms of coverage, our pipeline produces fully certified results for 99% and 86% of the qualitative and quantitative reasoning queries on BNNs, respectively. This is in sharp contrast to the best existing baselines which can fully certify only 62% and 4% of the queries, respectively.
Cite as

Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel. Efficient Certified Reasoning for Binarized Neural Networks. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.SAT.2025.32,
  author =	{Yang, Jiong and Tan, Yong Kiam and Soos, Mate and Myreen, Magnus O. and Meel, Kuldeep S.},
  title =	{{Efficient Certified Reasoning for Binarized Neural Networks}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{32:1--32:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.32},
  URN =		{urn:nbn:de:0030-drops-237665},
  doi =		{10.4230/LIPIcs.SAT.2025.32},
  annote =	{Keywords: Neural network verification, proof certification, SAT solving, approximate model counting}
}
Document
DOI: 10.4230/DagRep.3.5.78
Computational Methods Aiding Early-Stage Drug Design (Dagstuhl Seminar 13212)

Authors: Andreas Bender, Hinrich Göhlmann, Sepp Hochreiter, and Ziv Shkedy

Published in: Dagstuhl Reports, Volume 3, Issue 5 (2013)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13212 "Computational Methods Aiding Early-Stage Drug Design". The aim of the seminar was to bring scientists working on various aspects of drug discovery, genomic technologies and computational science (e.g., bioinformatics, chemoinformatics, machine learning, and statistics) together to explore how high dimensional data sets created by genomic technologies can be integrated to identify functional manifestations of drug actions on living cells early in the drug discovery process.
Cite as

Andreas Bender, Hinrich Göhlmann, Sepp Hochreiter, and Ziv Shkedy. Computational Methods Aiding Early-Stage Drug Design (Dagstuhl Seminar 13212). In Dagstuhl Reports, Volume 3, Issue 5, pp. 78-94, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{bender_et_al:DagRep.3.5.78,
  author =	{Bender, Andreas and G\"{o}hlmann, Hinrich and Hochreiter, Sepp and Shkedy, Ziv},
  title =	{{Computational Methods Aiding Early-Stage Drug Design (Dagstuhl Seminar 13212)}},
  pages =	{78--94},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{3},
  number =	{5},
  editor =	{Bender, Andreas and G\"{o}hlmann, Hinrich and Hochreiter, Sepp and Shkedy, Ziv},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.5.78},
  URN =		{urn:nbn:de:0030-drops-41791},
  doi =		{10.4230/DagRep.3.5.78},
  annote =	{Keywords: Bioinformatics, Chemoinformatics, Machine learning, Statistics, Interdisciplinary applications}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2013

  • Refine by Author
  • 1 Bender, Andreas
  • 1 Göhlmann, Hinrich
  • 1 Hochreiter, Sepp
  • 1 Meel, Kuldeep S.
  • 1 Myreen, Magnus O.
  • Show More...

  • Refine by Series/Journal
  • 1 LIPIcs
  • 1 DagRep

  • Refine by Classification
  • 1 Computing methodologies → Artificial intelligence
  • 1 Computing methodologies → Neural networks
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 Bioinformatics
  • 1 Chemoinformatics
  • 1 Interdisciplinary applications
  • 1 Machine learning
  • 1 Neural network verification
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact