2 Search Results for "Stroobandt, Dirk"

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/DagSemProc.07041.8
Energy Scalability and the RESUME Scalable Video Codec

Authors: Harald Devos, Hendrik Eeckhaut, Mark Christiaens, and Dirk Stroobandt

Published in: Dagstuhl Seminar Proceedings, Volume 7041, Power-aware Computing Systems (2007)

Abstract
In the context of the RESUME-project a scalable wavelet-based video decoder was built to demonstrate the benefits of reconfigurable hardware for scalable applications. emph{Scalable} video means that the quality of service (QoS), i.e., the frame rate, resolution, color depth, ldots of the decoded video can easily be changed by only decoding those parts of the video stream that contribute to the desired QoS. With the emergence of high-performance FPGAs (Field Programmable Gate Array), both the required performance for real-time decoding and flexibility, by allowing reconfiguration, are offered. Since the amount of calculations scales with the QoS, energy dissipation is expected to scale similarly. To investigate the relation between QoS and energy dissipation we actually measured the energy dissipation of a scalable video decoder implementation on a FPGA. The measurements show how dissipation effectively scales with the QoS, but also depends on the decoded data and the used design method. This is illustrated by comparing two different implementations of the inverse discrete wavelet transform (IDWT).
Cite as

Harald Devos, Hendrik Eeckhaut, Mark Christiaens, and Dirk Stroobandt. Energy Scalability and the RESUME Scalable Video Codec. In Power-aware Computing Systems. Dagstuhl Seminar Proceedings, Volume 7041, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{devos_et_al:DagSemProc.07041.8,
  author =	{Devos, Harald and Eeckhaut, Hendrik and Christiaens, Mark and Stroobandt, Dirk},
  title =	{{Energy Scalability and the RESUME Scalable Video Codec}},
  booktitle =	{Power-aware Computing Systems},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7041},
  editor =	{Luca Benini and Naehyuck Chang and Ulrich Kremer and Christian W. Probst},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07041.8},
  URN =		{urn:nbn:de:0030-drops-11120},
  doi =		{10.4230/DagSemProc.07041.8},
  annote =	{Keywords: Wavelet-based Scalable Video, Energy Measurement, Hardware Generation, FPGA}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2007

  • Refine by Author
  • 1 Christiaens, Mark
  • 1 Devos, Harald
  • 1 Eeckhaut, Hendrik
  • 1 Meel, Kuldeep S.
  • 1 Myreen, Magnus O.
  • Show More...

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

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

  • Refine by Keyword
  • 1 Energy Measurement
  • 1 FPGA
  • 1 Hardware Generation
  • 1 Neural network verification
  • 1 SAT solving
  • 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact