Pith. sign in

REVIEW 4 cited by

Neural Network Verification with PyRAT

Not yet reviewed by Pith; the record is open.

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

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

arxiv 2410.23903 v2 pith:S4XIRCW4 submitted 2024-10-31 cs.AI cs.LG

Augustin Lemesle , Julien Lehmann , Tristan Le Gall This is my paper · ORCID
classification cs.AIcs.LG
keywords neuralpyratsafetyusedguaranteesnetworknetworkstool
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 4 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Lipschitz-Based Robustness Certification Under Floating-Point Execution

    cs.LG 2026-03 conditional novelty 7.0 of 10 partial

    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.

  2. IoUCert: Robustness Verification for Anchor-based Object Detectors

    cs.LG 2026-03 conditional novelty 7.0 of 10

    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...

  3. Efficient Certified Reasoning for Binarized Neural Networks

    cs.LG 2025-06 unverdicted novelty 6.0 of 10

    A native BNN-aware solver and proof-checking pipeline certifies 99% of qualitative and 86% of quantitative robustness queries, with 9x and 218x speedups over prior certified baselines.

  4. A Survey on the Verification of Reinforcement Learning Policies

    cs.AI 2026-05 conditional novelty 4.0 of 10

    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.

Pith tools