pith. sign in

arxiv: 2401.14461 · v2 · pith:QUFBICWYnew · submitted 2024-01-25 · 💻 cs.AI · cs.LG· cs.LO

Marabou 2.0: A Versatile Formal Analyzer of Neural Networks

Haoze Wu , Omri Isac , Aleksandar Zelji\'c , Teruhiro Tagomori , Matthew Daggitt , Wen Kokke , Idan Refaeli , Guy Amir
show 9 more authors
Kyle Julian Shahaf Bassan Pei Huang Ori Lahav Min Wu Min Zhang Ekaterina Komendantskaya Guy Katz Clark Barrett
This is my paper
classification 💻 cs.AI cs.LGcs.LO
keywords formalmarabounetworksneuralanalysisanalyzerarchitecturalcomponents
0
0 comments X
read the original abstract

This paper serves as a comprehensive system description of version 2.0 of the Marabou framework for formal analysis of neural networks. We discuss the tool's architectural design and highlight the major features and components introduced since its initial release.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 5 Pith papers

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

  1. Quantitative Linear Logic for Neuro-Symbolic Learning and Verification

    cs.LO 2026-05 unverdicted novelty 7.0

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

  2. Scaling Neural Network Verification with Tensor Parallelism and Fully Sharded Data Parallelism

    cs.LG 2026-06 unverdicted novelty 6.0

    Adapts TP and FSDP to bound-propagation verification, with FSDP delivering bitwise-identical bounds and 80-90% baseline memory reduction while TP trades some tightness for ~2x peak-memory savings.

  3. Quantitative Linear Logic for Neuro-Symbolic Learning and Verification

    cs.LO 2026-05 unverdicted novelty 6.0

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

  4. Analyzing Adversarial Inputs in Deep Reinforcement Learning

    cs.LG 2024-02 unverdicted novelty 5.0

    Introduces the Adversarial Rate metric and associated tools to systematically evaluate and visualize the impact of adversarial inputs on DRL policies using formal verification.

  5. The Luna Bound Propagator for Formal Analysis of Neural Networks

    cs.LG 2026-03 conditional novelty 4.0

    Luna delivers a C++ bound propagator supporting interval, DeepPoly/CROWN, and alpha-CROWN analyses that reports tighter bounds and higher speed than the leading Python alpha-CROWN implementation on VNN-COMP 2025 benchmarks.