Pith. sign in

REVIEW 3 major objections 3 minor 58 references

Efficient Certified Reasoning for Binarized Neural Networks

T0 review · 3 major / 3 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A native Boolean representation of BNN constraints, paired with proof-generating solving and counting, yields 9x faster certified solving and 218x faster certified counting than prior baselines.

desk verdict Native BNN proof rules and big speedups make this worth a referee, but the certified-coverage claims stand on a soundness proof I can't verify from the abstract. read the letter →

arxiv 2507.02916 v1 pith:EJPPPMVB submitted 2025-06-25 cs.LG cs.AIcs.LO

Jiong Yang , Yong Kiam Tan , Mate Soos , Magnus O. Myreen , Kuldeep S. Meel This is my paper · ORCID
classification cs.LGcs.AIcs.LO
keywords binarizedneuralnetworkscertifiedreasoningqualitativeverificationquantitativemodelcountingSATsolvingproofcheckingrobustness
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tackles a trust gap in verifying Binarized Neural Networks (BNNs): existing tools either scale poorly or give answers without independently checkable evidence. It claims a single pipeline, built on a native Boolean representation of BNN constraints, that answers qualitative queries (is there an adversarial input?) and quantitative queries (how many inputs violate a property?) while emitting machine-checkable proofs. The reported gains are a 9x speedup for certified solving and a 218x speedup for certified counting over prior certified baselines, with fully certified results for 99% of qualitative and 86% of quantitative benchmark queries, compared with 62% and 4% for the best baselines. This would make certified verification of BNNs practical enough for safety-critical use.

What carries the argument

The central object is a native constraint representation of BNN computations, plus proof rules that justify deductions directly on those constraints without flattening them into generic CNF or pseudo-Boolean form. This representation is shared by the two reasoning engines: a custom solver for yes/no qualitative queries and an approximate model counter for quantitative counting queries. The same native rules feed the proof-generation and proof-checking pipelines, which is what makes the results certifiable rather than merely reported.

What would settle it

Feed the proof checker certificates with deliberately corrupted proof steps, and compare certified model counts against exhaustive brute-force enumeration on small BNNs; an accepted bad certificate or any certified count that disagrees with brute force would refute the soundness claim.

Watch

Extended reading notes

Core claim

The central claim is that translating BNN constraints into generic Boolean clauses or pseudo-Boolean inequalities is the main bottleneck, and that treating BNN-specific constraints as first-class citizens inside both the solver and the proof system removes it. A custom solver handles qualitative reasoning over native constraints, and an approximate model counter uses the same native representation for quantitative reasoning. Around these sits a proof-generation and proof-checking pipeline whose rules are specialized for BNN constraints, so every answer carries a certificate that an independent checker can validate. The evaluation reports a 9x speedup in certified solving, a 218x speedup in certified counting, and certified coverage of 99% of qualitative and 86% of quantitative queries.

Load-bearing premise

The entire trustworthiness claim rests on the proof checker's native BNN rules being sound and complete for the exact property being verified, so no invalid certificate is ever accepted.

Editorial extensions

If this is right

  • Qualitative verification of a BNN can be answered with a formally checked certificate at 9x the speed of prior certified CNF and pseudo-Boolean approaches.
  • Quantitative queries, such as counting inputs that violate a robustness property, can be certified 218x faster than the existing CNF-based counting baseline.
  • Fully certified coverage rises to 99% of qualitative and 86% of quantitative benchmark queries, up from 62% and 4% for the best existing baselines.
  • Because the proof checker is separate from the solver, a user can trust the verified answer without trusting the solver implementation.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the native-constraint approach transfers, other structured network families such as ternary or quantized networks could receive similar certified pipelines without a generic translation step; the paper does not test this.
  • The 218x counting speedup suggests quantitative robustness analysis, bounding the fraction of failure-inducing inputs, could become a routine safety check rather than a research demonstration; this extrapolates beyond the reported benchmarks.
  • A natural stress test is whether the certified-coverage advantage over baselines persists on deeper and wider BNNs than the benchmark suite includes; the paper does not claim such generalization.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 3 minor

Summary. This paper proposes a certified reasoning pipeline for binarized neural networks (BNNs), combining a custom satisfiability solver and an approximate model counter that natively represent BNN constraints, together with proof generation and checking pipelines specialized to those constraints. The abstract reports that the certified solving approach achieves a 9x speedup over prior certified CNF and PB-based approaches and the certified counting approach achieves a 218x speedup over a CNF-based baseline, while fully certifying 99% and 86% of qualitative and quantitative reasoning queries, respectively, compared with 62% and 4% for the best existing baselines. The paper claims that the specialized proof checking ensures trustworthiness for all verification results.

Significance. If the reported results are reproducible and the proof checker is sound, this work would constitute a substantial practical advance in BNN verification, combining scalability with machine-checkable certificates and directly addressing a known soundness gap in prior BNN analysis tools. The explicit emphasis on proof generation and checking is a strength, and the reported coverage improvements are dramatic. However, the significance assessment is conditional on two things that cannot be established from the abstract alone: the soundness of the custom proof checker for the native BNN inference rules, and the fairness and statistical robustness of the benchmark comparisons.

major comments (3)
  1. [Abstract] The trustworthiness claim ('ensuring trustworthiness for all of our verification results') rests entirely on the soundness of the proof checker for the native BNN proof rules. The submitted material provides no formal specification of these rules, no soundness theorem, and no description or audit of the checker implementation. A single unsound inference rule accepted by the checker would invalidate every 'fully certified' result, including the 99% and 86% coverage numbers. This is load-bearing because the central contribution is certified reasoning.
  2. [Abstract] The empirical claims (9x speedup, 218x speedup, 99%/86% certified coverage) are stated without any experimental methodology: there is no benchmark suite description, hardware configuration, time or memory limit, number of runs, variance measure, or baseline configuration. As a result, the quantitative comparisons cannot be assessed for fairness or statistical significance. The absence of these details in the abstract alone is not disqualifying if the full manuscript provides them, but in the submitted material the headline numbers are unsupported.
  3. [Abstract] The abstract describes an 'approximate model counter' for quantitative reasoning yet reports 'fully certified' counting results. The relationship between approximation and certification is not explained: does the proof checker verify the approximate count, or does the approximation only prune the search space while the final count is exact? Without this clarification, the certified counting claim is ambiguous and the 86% certified coverage for quantitative queries is difficult to interpret.
minor comments (3)
  1. [Abstract] The terms 'qualitative reasoning' and 'quantitative reasoning' are used without definition; a single sentence clarifying that these correspond to satisfiability solving and model counting would help orient the reader.
  2. [Abstract] The baselines are described only as 'prior certified CNF and PB-based approaches' and an 'existing CNF-based baseline'; the full text should name the specific tools, versions, and configurations used.
  3. [Abstract] The phrase 'native support for BNN constraint reasoning' would be more informative with one concrete example of a BNN constraint, such as the binarized activation or weight constraint, to make clear what is meant by 'native representation.'

Circularity Check

0 steps flagged · score 0.0 of 10

No circular dependency found; the claimed speedups and coverage compare against external prior baselines, and the certification pipeline is an engineering soundness concern, not an input-output equivalence.

full rationale

The abstract's central claims (9x/218x speedups and 99%/86% certified coverage) are empirical comparisons against prior CNF- and PB-based certified approaches, i.e., external baselines rather than quantities defined by the paper's own outputs. The paper introduces a native BNN constraint representation and proof generation/checking pipelines; nothing in the provided text defines the solver's predicted results in terms of the benchmark answers or fits parameters to the target queries. The only substantive concern is that the phrase 'ensuring trustworthiness' presupposes soundness of the custom proof checker and native BNN inference rules, and no soundness theorem, formalization, or checker artifact is visible in the available text. That is a correctness and verification gap, not circularity: a proof checker that accepts invalid certificates would make the certified-coverage numbers wrong, but it would not make the derivation circular. No equation, self-citation, or fitted-input-as-prediction step is present in the available text, so under the hard rule requiring a quoted reduction, no circular step can be flagged.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

Only the abstract was available, so no free parameters or newly invented entities can be identified. The listed axioms are domain assumptions implicit in the abstract's claims.

assumptions (3)
  • domain assumption BNNs can be faithfully encoded as Boolean constraints in the custom solver and model counter.
    The solver's native representation and the counting results depend on this encoding being sound and complete for the robustness property under test; the abstract does not specify the encoding's formal correctness proof.
  • domain assumption The benchmark suite used for evaluation is representative of real BNN verification tasks.
    The claimed speedups and coverage are measured on this suite; if the suite is narrow or biased, the empirical claims will not generalize.
  • domain assumption The proof checker correctly implements the proof rules and certificate format.
    The 'fully certified' and 'trustworthiness' claims assume that any certificate accepted by the checker genuinely implies the verification result; a checker bug would invalidate the headline coverage numbers.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Efficient Certified Reasoning for Binarized Neural Networks." pith.science (2026). https://pith.science/paper/EJPPPMVB

@misc{pith2026250702916,
  author       = {Pith},
  title        = {Pith review of: Efficient Certified Reasoning for Binarized Neural Networks},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EJPPPMVB}},
  note         = {Machine review of arXiv:2507.02916}
}
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\times$ speedup over prior certified CNF and PB-based approaches, and our certified counting approach achieves a $218\times$ 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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

58 extracted references · 54 canonical work pages

  1. [1]

    An introduction to CORA 2015

    Matthias Althoff. An introduction to CORA 2015. In Goran Frehse and Matthias Althoff, editors, ARCH@CPSWeek , volume 34 of EPiC Series in Computing , pages 120--151. EasyChair, 2015

    work page 2015

  2. [2]

    Barrett, and Guy Katz

    Guy Amir, Haoze Wu, Clark W. Barrett, and Guy Katz. An SMT -based approach for verifying binarized neural networks. In Jan Friso Groote and Kim Guldstrand Larsen, editors, TACAS , volume 12652 of LNCS , pages 203--222. Springer, 2021

    work page 2021

  3. [3]

    Seulkee Baek, Mario Carneiro, and Marijn J. H. Heule. A flexible proof format for SAT solver-elaborator communication. Log. Methods Comput. Sci. , 18(2), 2022

    work page 2022

  4. [4]

    nnenum : Verification of ReLU neural networks with optimized abstraction refinement

    Stanley Bak. nnenum : Verification of ReLU neural networks with optimized abstraction refinement. In Aaron Dutle, Mariano M. Moscato, Laura Titolo, C \' e sar A. Mu \ n oz, and Ivan Perez, editors, NFM , volume 12673 of LNCS , pages 19--36. Springer, 2021

    work page 2021

  5. [5]

    Meel, and Prateek Saxena

    Teodora Baluta, Shiqi Shen, Shweta Shinde, Kuldeep S. Meel, and Prateek Saxena. Quantitative verification of neural networks and its security applications. In Lorenzo Cavallaro, Johannes Kinder, XiaoFeng Wang, and Jonathan Katz, editors, CCS , pages 1249--1264. ACM , 2019

    work page 2019

  6. [6]

    Nori, and Antonio Criminisi

    Osbert Bastani, Yani Ioannou, Leonidas Lampropoulos, Dimitrios Vytiniotis, Aditya V. Nori, and Antonio Criminisi. Measuring neural net robustness with constraints. In Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Roman Garnett, editors, NIPS , pages 2613--2621, 2016

    work page 2016

  7. [7]

    CaDiCaL 2.0

    Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0. In Arie Gurfinkel and Vijay Ganesh, editors, CAV , volume 14681 of LNCS , pages 133--152. Springer, 2024

    work page 2024

  8. [8]

    Certified dominance and symmetry breaking for combinatorial optimisation

    Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordstr \" o m. Certified dominance and symmetry breaking for combinatorial optimisation. J. Artif. Intell. Res. , 77:1539--1589, 2023

    work page 2023

Show all 58 references
  1. [9]

    Jackel, Mathew Monfort, Urs Muller, Jiakai Zhang, Xin Zhang, Jake Zhao, and Karol Zieba

    Mariusz Bojarski, Davide Del Testa, Daniel Dworakowski, Bernhard Firner, Beat Flepp, Prasoon Goyal, Lawrence D. Jackel, Mathew Monfort, Urs Muller, Jiakai Zhang, Xin Zhang, Jake Zhao, and Karol Zieba. End to end learning for self-driving cars. CoRR , abs/1604.07316, 2016. http...

    2016 arXiv

  2. [10]

    Johnson, and Haoze Wu

    Christopher Brix, Stanley Bak, Taylor T. Johnson, and Haoze Wu. The fifth international verification of neural networks competition (VNN-COMP 2024): Summary and results. CoRR , abs/2412.19985, 2024. https://arxiv.org/abs/2412.19985 arXiv:2412.19985

    2024 arXiv

  3. [11]

    Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn J

    Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn J. H. Heule. Certified knowledge compilation with application to formally verified model counting. J. Artif. Intell. Res. , 82, 2025

    2025

  4. [12]

    Meel, and Moshe Y

    Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. A scalable approximate model counter. In Christian Schulte, editor, CP , volume 8124 of LNCS , pages 200--216. Springer, 2013

    2013

  5. [13]

    NeVer2 : learning and verification of neural networks

    Stefano Demarchi, Dario Guidotti, Luca Pulina, and Armando Tacchella. NeVer2 : learning and verification of neural networks. Soft Comput. , 28(19):11647--11665, 2024

    2024

  6. [14]

    Passmore, Kathrin Stark, Ekaterina Komendantskaya, and Guy Katz

    Remi Desmartin, Omri Isac, Grant O. Passmore, Kathrin Stark, Ekaterina Komendantskaya, and Guy Katz. Towards a certified proof checker for deep neural network verification. In Robert Gl \" u ck and Bishoksan Kafle, editors, LOPSTR , volume 14330 of LNCS , pages 198--209. Sprin...

    2023

  7. [15]

    BERT: pre-training of deep bidirectional transformers for language understanding

    Jacob Devlin, Ming - Wei Chang, Kenton Lee, and Kristina Toutanova. BERT: pre-training of deep bidirectional transformers for language understanding. In Jill Burstein, Christy Doran, and Thamar Solorio, editors, NAACL-HLT , pages 4171--4186. Association for Computational Lingu...

    2019

  8. [16]

    Meel, Roger Paredes, and Moshe Y

    Leonardo Due \ n as - Osorio, Kuldeep S. Meel, Roger Paredes, and Moshe Y. Vardi. Counting-based reliability estimation for power-transmission grids. In Satinder Singh and Shaul Markovitch, editors, AAAI , pages 4488--4494. AAAI Press, 2017

    2017

  9. [17]

    Hai Duong, Dong Xu, ThanhVu Nguyen, and Matthew B. Dwyer. Harnessing neuron stability to improve DNN verification. Proc. ACM Softw. Eng. , 1( FSE ):859--881, 2024

    2024

  10. [18]

    Effective preprocessing in SAT through variable and clause elimination

    Niklas E \' e n and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In Fahiem Bacchus and Toby Walsh, editors, SAT , volume 3569 of LNCS , pages 61--75. Springer, 2005

    2005

  11. [19]

    Divide and conquer: Towards faster pseudo-boolean solving

    Jan Elffers and Jakob Nordstr \" o m. Divide and conquer: Towards faster pseudo-boolean solving. In J \' e r \^ o me Lang, editor, IJCAI , pages 1291--1299. ijcai.org, 2018

    2018

  12. [20]

    Proofs for propositional model counting

    Johannes Klaus Fichte, Markus Hecher, and Valentin Roland. Proofs for propositional model counting. In Kuldeep S. Meel and Ofer Strichman, editors, SAT , volume 236 of LIPIcs , pages 30:1--30:24. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2022

    2022

  13. [21]

    Andreas Gittis, Eric Vin, and Daniel J. Fremont. Randomized synthesis for diversity and cost constraints with control improvisation. In Sharon Shoham and Yakir Vizel, editors, CAV , volume 13372 of LNCS , pages 526--546. Springer, 2022

    2022

  14. [22]

    Deep sparse rectifier neural networks

    Xavier Glorot, Antoine Bordes, and Yoshua Bengio. Deep sparse rectifier neural networks. In Geoffrey J. Gordon, David B. Dunson, and Miroslav Dud \' k, editors, AISTATS , volume 15 of JMLR Proceedings , pages 315--323. JMLR.org, 2011

    2011

  15. [23]

    BiViT : Extremely compressed binary vision transformers

    Yefei He, Zhenyu Lou, Luoming Zhang, Jing Liu, Weijia Wu, Hong Zhou, and Bohan Zhuang. BiViT : Extremely compressed binary vision transformers. In ICCV , pages 5628--5640. IEEE , 2023

    2023

  16. [24]

    Hunt Jr., Matt Kaufmann, and Nathan Wetzler

    Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, and Nathan Wetzler. Efficient, verified checking of propositional proofs. In Mauricio Ayala - Rinc \' o n and C \' e sar A. Mu \ n oz, editors, ITP , volume 10499 of LNCS , pages 269--284. Springer, 2017

    2017

  17. [25]

    Safety verification of deep neural networks

    Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In Rupak Majumdar and Viktor Kuncak, editors, CAV , volume 10426 of LNCS , pages 3--29. Springer, 2017

    2017

  18. [26]

    Binarized neural networks

    Itay Hubara, Matthieu Courbariaux, Daniel Soudry, Ran El - Yaniv, and Yoshua Bengio. Binarized neural networks. In Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Roman Garnett, editors, NIPS , pages 4107--4115, 2016

    2016

  19. [27]

    Kai Jia and Martin C. Rinard. Efficient exact verification of binarized neural networks. In Hugo Larochelle, Marc'Aurelio Ranzato, Raia Hadsell, Maria - Florina Balcan, and Hsuan - Tien Lin, editors, NeurIPS , 2020

    2020

  20. [28]

    Johnson and Michael A

    David S. Johnson and Michael A. Trick, editors. Cliques, Coloring, and Satisfiability , volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science . DIMACS/AMS , 1996

    1996

  21. [29]

    Julian, Jessica Lopez, Jeffrey S

    Kyle D. Julian, Jessica Lopez, Jeffrey S. Brush, Michael P. Owen, and Mykel J. Kochenderfer. Policy Compression for Aircraft Collision Avoidance Systems . In DASC , pages 1--10, 2016

    2016

  22. [30]

    Barrett, David L

    Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In Rupak Majumdar and Viktor Kuncak, editors, CAV , volume 10426 of LNCS , pages 97--117. Springer, 2017

    2017

  23. [31]

    Alex Krizhevsky, Ilya Sutskever, and Geoffrey E. Hinton. ImageNet classification with deep convolutional neural networks. In Peter L. Bartlett, Fernando C. N. Pereira, Christopher J. C. Burges, L \' e on Bottou, and Kilian Q. Weinberger, editors, NIPS , pages 1106--1114, 2012

    2012

  24. [32]

    Efficient verified (UN)SAT certificate checking

    Peter Lammich. Efficient verified (UN)SAT certificate checking. J. Autom. Reason. , 64(3):513--532, 2020

    2020

  25. [33]

    Neural network verification with PyRAT

    Augustin Lemesle, Julien Lehmann, and Tristan Le Gall. Neural network verification with PyRAT . CoRR , abs/2410.23903, 2024. https://arxiv.org/abs/2410.23903 arXiv:2410.23903

    2024 arXiv

  26. [34]

    AWQ: activation-aware weight quantization for on-device LLM compression and acceleration

    Ji Lin, Jiaming Tang, Haotian Tang, Shang Yang, Wei - Ming Chen, Wei - Chen Wang, Guangxuan Xiao, Xingyu Dang, Chuang Gan, and Song Han. AWQ: activation-aware weight quantization for on-device LLM compression and acceleration. In Phillip B. Gibbons, Gennady Pekhimenko, and Chr...

    2024

  27. [35]

    Diego Manzanas Lopez, Sung Woo Choi, Hoang - Dung Tran, and Taylor T. Johnson. NNV 2.0: The neural network verification tool. In Constantin Enea and Akash Lal, editors, CAV , volume 13965 of LNCS , pages 397--412. Springer, 2023

    2023

  28. [36]

    McConnell, Kurt Mehlhorn, Stefan N \" a her, and Pascal Schweitzer

    Ross M. McConnell, Kurt Mehlhorn, Stefan N \" a her, and Pascal Schweitzer. Certifying algorithms. Comput. Sci. Rev. , 5(2):119--161, 2011

    2011

  29. [37]

    Duncan J. M. Moss, Eriko Nurvitadhi, Jaewoong Sim, Asit K. Mishra, Debbie Marr, Suchit Subhaschandra, and Philip Heng Wai Leong. High performance binary neural networks on the xeon+fpga platform. In Marco D. Santambrogio, Diana G \" o hringer, Dirk Stroobandt, Nele Mentens, an...

    2017

  30. [38]

    Verifying properties of binarized deep neural networks

    Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, and Toby Walsh. Verifying properties of binarized deep neural networks. In Sheila A. McIlraith and Kilian Q. Weinberger, editors, AAAI , pages 6615--6624. AAAI Press, 2018

    2018

  31. [39]

    In search for a SAT -friendly binarized neural network architecture

    Nina Narodytska, Hongce Zhang, Aarti Gupta, and Toby Walsh. In search for a SAT -friendly binarized neural network architecture. In ICLR . OpenReview.net, 2020

    2020

  32. [40]

    XNOR-Net : ImageNet classification using binary convolutional neural networks

    Mohammad Rastegari, Vicente Ordonez, Joseph Redmon, and Ali Farhadi. XNOR-Net : ImageNet classification using binary convolutional neural networks. In Bastian Leibe, Jiri Matas, Nicu Sebe, and Max Welling, editors, ECCV , volume 9908 of LNCS , pages 525--542. Springer, 2016

    2016

  33. [41]

    Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. GANAK: A scalable probabilistic exact model counter. In Sarit Kraus, editor, IJCAI , pages 1169--1176. ijcai.org, 2019

    2019

  34. [42]

    David Silver, Aja Huang, Chris J. Maddison, Arthur Guez, Laurent Sifre, George van den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Vedavyas Panneershelvam, Marc Lanctot, Sander Dieleman, Dominik Grewe, John Nham, Nal Kalchbrenner, Ilya Sutskever, Timothy P. Lillicrap,...

    2016

  35. [43]

    Mate Soos and Kuldeep S. Meel. Arjun: An efficient independent support computation technique and its applications to counting and sampling. In Tulika Mitra, Evangeline F. Y. Young, and Jinjun Xiong, editors, ICCAD , pages 71:1--71:9. ACM , 2022

    2022

  36. [44]

    Extending SAT solvers to cryptographic problems

    Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In Oliver Kullmann, editor, SAT , volume 5584 of LNCS , pages 244--257. Springer, 2009

    2009

  37. [45]

    Goodfellow, and Rob Fergus

    Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. Intriguing properties of neural networks. In Yoshua Bengio and Yann LeCun, editors, ICLR , 2014

    2014

  38. [46]

    Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen. Verified propagation redundancy and compositional UNSAT checking in CakeML . Int. J. Softw. Tools Technol. Transf. , 25(2):167--184, 2023

    2023

  39. [47]

    Myreen, Ramana Kumar, Anthony C

    Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, and Michael Norrish. The verified CakeML compiler backend. J. Funct. Program. , 29:e2, 2019

    2019

  40. [48]

    Approximate model counting

    Yong Kiam Tan and Jiong Yang. Approximate model counting. Archive of Formal Proofs , March 2024. https://isa-afp.org/entries/Approximate_Model_Counting.html, Formal proof development

    2024

  41. [49]

    Myreen, and Kuldeep S

    Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel. Formally certified approximate model counting. In Arie Gurfinkel and Vijay Ganesh, editors, CAV , volume 14681 of LNCS , pages 153--177. Springer, 2024

    2024

  42. [50]

    Bie Verbist, Günter Klambauer, Liesbet Vervoort, Willem Talloen, Ziv Shkedy, Olivier Thas, Andreas Bender, Hinrich W. H. Göhlmann, Sepp Hochreiter, and the QSTAR Consortium. Using transcriptomics to guide lead optimization in drug discovery projects: Lessons learned from the Q...

    2015

  43. [51]

    Zico Kolter

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho - Jui Hsieh, and J. Zico Kolter. Beta-CROWN : Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. CoRR , abs/2103.06624, 2021. https://arxiv.org/abs/21...

    2021 arXiv

  44. [52]

    Nathan Wetzler, Marijn Heule, and Warren A. Hunt Jr. DRAT-trim : Efficient checking and trimming using expressive clausal proofs. In Carsten Sinz and Uwe Egly, editors, SAT , volume 8561 of LNCS , pages 422--429. Springer, 2014

    2014

  45. [53]

    Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, and Clark W

    Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tagomori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, and Clark W. Barrett. Marabou 2.0: A versatile formal anal...

    2024

  46. [54]

    SmoothQuant : Accurate and efficient post-training quantization for large language models

    Guangxuan Xiao, Ji Lin, Micka \" e l Seznec, Hao Wu, Julien Demouth, and Song Han. SmoothQuant : Accurate and efficient post-training quantization for large language models. In Andreas Krause, Emma Brunskill, Kyunghyun Cho, Barbara Engelhardt, Sivan Sabato, and Jonathan Scarle...

    2023

  47. [55]

    Jiong Yang and Kuldeep S. Meel. Engineering an efficient PB-XOR solver. In Laurent D. Michel, editor, CP , volume 210 of LIPIcs , pages 58:1--58:20. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2021

    2021

  48. [56]

    Jiong Yang and Kuldeep S. Meel. Rounding meets approximate model counting. In Constantin Enea and Akash Lal, editors, CAV , volume 13965 of LNCS , pages 132--162. Springer, 2023

    2023

  49. [57]

    Suwei Yang and Kuldeep S. Meel. Engineering an exact pseudo- Boolean model counter. In Michael J. Wooldridge, Jennifer G. Dy, and Sriraam Natarajan, editors, AAAI , pages 8200--8208. AAAI Press, 2024

    2024

  50. [58]

    Binarized neural machine translation

    Yichi Zhang, Ankush Garg, Yuan Cao, Lukasz Lew, Behrooz Ghorbani, Zhiru Zhang, and Orhan Firat. Binarized neural machine translation. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, NeurIPS , 2023

    2023

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.