QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking
QNNVerifier is the first open-source tool for verifying implementations of neural networks that takes into account the finite word-length (i.e. quantization) of their operands. The novel support for quantization is achieved by employing state-of-the-art software model checking (SMC) techniques. It translates the implementation of neural networks to a decidable fragment of first-order logic based on satisfiability modulo theories (SMT). The effects of fixed- and floating-point operations are represented through direct implementations given a hardware-determined precision. Furthermore, QNNVerifier allows to specify bespoke safety properties and verify the resulting model with different verification strategies (incremental and k-induction) and SMT solvers. Finally, QNNVerifier is the first tool that combines invariant inference via interval analysis and discretization of non-linear activation functions to speed up the verification of neural networks by orders of magnitude. A video presentation of QNNVerifier is available at https://youtu.be/7jMgOL41zTY
Code (0)
등록된 구현이 없습니다.
Tasks
QuantizationMethods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Evaluating open-source Large Language Models for automated fact-checking
The increasing prevalence of online misinformation has heightened the demand for automated fact-checking solutions. Large Language Models (LLMs) have emerged as potential tools for assisting in this task, but their effec…
Fact CheckingMisinformationTensor Probabilistic Model Checking of Finite-Horizon Markov Chains (Extended Version)
We reexamine the problem of verifying Markov chains with respect to step-bounded reachability probabilities. Prevailing approaches rely on encoding the state-transition matrix using either explicit or symbolic representa…
T-REX: Table -- Refute or Entail eXplainer
Verifying textual claims against structured tabular data is a critical yet challenging task in Natural Language Processing with broad real-world impact. While recent advances in Large Language Models (LLMs) have enabled …
Loki: An Open-Source Tool for Fact Verification
We introduce Loki, an open-source tool designed to address the growing problem of misinformation. Loki adopts a human-centered approach, striking a balance between the quality of fact-checking and the cost of human invol…
Claim VerificationFact CheckingFact VerificationMisinformationHerO at AVeriTeC: The Herd of Open Large Language Models for Verifying Real-World Claims
To tackle the AVeriTeC shared task hosted by the FEVER-24, we introduce a system that only employs publicly available large language models (LLMs) for each step of automated fact-checking, dubbed the Herd of Open LLMs fo…
Fact CheckingLanguage ModelingLanguage ModellingQuestion Generation+2