We present Prophecy, a tool for automatically inferring formal properties of neural networks. Prophecy is based on the observation that a significant part of the logic of neural networks is captured in the activation status of the neurons at inner layers. Prophecy works by extracting rules based on neuron activations (values or on/off statuses) as preconditions that imply certain desirable output property, e.g., the prediction being a certain class. We present the architecture of the tool, highlight its features and demonstrate its usage on different types of models and output properties. We also present an overview of its applications, such as inferring and proving formal explanations of neural networks, compositional verification, run-time monitoring, repair, and others. We also show novel results highlighting its potential in the era of large vision- language models. Demo: https://youtu.be/3mobcm0OQcI
| Prophecy: Inferring Formal Properties from Neuron Activations (Presentation Slides) (ICSE 2026 Prophecy Slides.pptx) | 7.6MiB |
Fri 17 AprDisplayed time zone: Brasilia, Distrito Federal, Brazil change
11:00 - 12:30 | Dependability and Security 9Research Track / Demonstrations / SE In Practice (SEIP) at Oceania VII Chair(s): Jieke Shi Singapore Management University | ||
11:00 15mTalk | Prophecy: Inferring Formal Properties from Neuron Activations Demonstrations Divya Gopinath KBR; NASA Ames, Corina S. Păsăreanu Carnegie Mellon University, Muhammad Usman University of Texas at Austin, USA Media Attached File Attached | ||
11:15 15mTalk | Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification Research Track Paschal Amusuo Purdue University, Owen Cochell Michigan State University, Taylor Le Lievre Purdue University, Parth Vinod Patil Purdue University, Aravind Machiry Purdue University, James C. Davis Purdue University Pre-print | ||
11:30 15mTalk | Accurate Inference of Termination ConditionsDistinguished Paper Award Research Track | ||
11:45 15mTalk | Verification of Multi-Model Stochastic Systems Research Track Radu Calinescu University of York, UK, Simos Gerasimou Cyprus University of Technology, Sinem Getir Yaman University of York, UK, Gricel Vázquez University of York, UK, Micah Bassett University of York, UK Pre-print | ||
12:00 15mTalk | Accelerating IC3 Verification by Exploiting Unsatisfiable Cores and Satisfying ModelsDistinguished Paper Award Research Track Xinyi Gong National University of Defense Technology, Liangze Yin National University of Defense Technology, Yuhan Li National University of Defense Technology, Ke Kang National University of Defense Technology, Wei Dong National University of Defense Technology, Shanshan Li National University of Defense Technology, Ji Wang National University of Defense Technology | ||
12:15 15mTalk | Agentic Taxation Optimization via LLM SMT-Constraint Reasoning SE In Practice (SEIP) Ting Chien Hwang National Chengchi University, Fang Yu National Chengchi University, Jie-Hong Roland Jiang National Taiwan University | ||