REVIEW 6 cited by
Neural Network Verification with PyRAT
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Neural Network Verification with PyRAT
read the original abstract
As AI systems are becoming more and more popular and used in various critical domains (health, transport, energy, ...), the need to provide guarantees and trust of their safety is undeniable. To this end, we present PyRAT, a tool based on abstract interpretation to verify the safety and the robustness of neural networks. In this paper, we describe the different abstractions used by PyRAT to find the reachable states of a neural network starting from its input as well as the main features of the tool to provide fast and accurate analysis of neural networks. PyRAT has already been used in several collaborations to ensure safety guarantees, with its second place at the VNN-Comp 2024 showcasing its performance.
Forward citations
Cited by 6 Pith papers
-
Quantitative Linear Logic for Neuro-Symbolic Learning and Verification
QLL is a novel logic for neuro-symbolic learning that uses ML-native operations (sum, log-sum-exp) on logits to embed constraints, satisfying most linear logic properties and showing stronger correlation between empir...
-
Lipschitz-Based Robustness Certification Under Floating-Point Execution
Lipschitz-based robustness certificates that assume real arithmetic can be unsound under floating-point execution; a formal FP-aware theory and certifier close that gap for dense ReLU networks.
-
Lipschitz-Based Robustness Certification Under Floating-Point Execution
Classical Lipschitz robustness certificates are unsound under floating-point execution; this paper derives sound corrected conditions, a Rocq formalisation, and a practical certifier for dense ReLU networks.
-
IoUCert: Robustness Verification for Anchor-based Object Detectors
IoUCert derives exact IoU bounds over anchor-offset boxes via a coordinate transformation and uses them to formally verify single-object SSD, YOLOv2, and YOLOv3 models under brightness, contrast, and motion-blur pertu...
-
Quantitative Linear Logic for Neuro-Symbolic Learning and Verification
Quantitative Linear Logic interprets logical connectives via natural ML operations on logits to embed constraints in neural training while satisfying most linear logic laws and correlating performance with independent...
-
A Survey on the Verification of Reinforcement Learning Policies
A unifying taxonomy of post-training RL-policy verification methods along formal/probabilistic, step-wise/multi-step, and guarantee-strength axes, plus benchmark-based tool-selection guidance.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.