8 papers
Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs
Ido Pinto, Yizhak Yisrael Elboher, Haoze Wu +2
The synthesis of inductive loop invariants remains a critical bottleneck in automated program verification. While Large Language Models (LLMs) show promise in mitigating this issue…
Provably Explaining Neural Additive Models
Shahaf Bassan, Yizhak Yisrael Elboher, Tobias Ladner +4
Despite significant progress in post-hoc explanation methods for neural networks, many remain heuristic and lack provable guarantees. A key approach for obtaining explanations with…
Talking with Verifiers: Automatic Specification Generation for Neural Network Verification
Yizhak Y. Elboher, Reuven Peleg, Zhouxing Shi +2
Neural network verification tools currently support only a narrow class of specifications, typically expressed as low-level constraints over raw inputs and outputs. This limitation…
Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits
Yizhak Yisrael Elboher, Avraham Raviv, Amihay Elboher +4
Ensuring the safety and efficiency of AI systems is a central goal of modern research. Formal verification provides guarantees of neural network robustness, while early exits impro…
Abstraction-Based Proof Production in Formal Verification of Neural Networks
Yizhak Yisrael Elboher, Omri Isac, Guy Katz +2
Modern verification tools for deep neural networks (DNNs) increasingly rely on abstraction to scale to realistic architectures. In parallel, proof production is becoming a critical…
Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
Shahaf Bassan, Yizhak Yisrael Elboher, Tobias Ladner +2
Despite significant advancements in post-hoc explainability techniques for neural networks, many current methods rely on heuristics and do not provide formally provable guarantees…