PV3 ⊧ VerifAIchecks built-in and user-defined properties of system modelsToolkit for formal design and analysis for systems that include artificial intelligence and machine learning components.
- Artificial intelligence
- Machine learning
Type of toolFramework?
- Simulatable model of the system, including code for one or more controllers and perception components, and a dynamical model of the system being controlled
- Probabilistic model of the environment, specifying constraints on the workspace, locations of agents and objects, and the dynamical behavior of agents
- Property over the composition of the system and its environment
- System model: Any executable code, invoked by the simulator
- Environment model: Typically a definition in the simulator of the different types of agents, plus a description of their initial conditions and other parameters using the Scenic probabilistic programming language.
- Property: Metric Temporal Logic (MTL), objective functions or arbitrary code monitoring the property
Expected outputDepends on what analysis is used.
- Falsification will return one or more counterexamples for simulation traces that violate the property
- Fuzz testing: Traces samples from the distribution of behaviors induced by the environment model
- Data augmentation: Generates additional data for training and testing an ML component
- Error table analysis: Identifies features that are correlated with property failures
- Hyper-parameter or model parameter synthesis: Generates a parameter evaluation that satisfies the specified property.
InternalsVerifAI offers the following analyses:
- temporal-logic falsification,
- model-based fuzz testing,
- counterexample-guided data augmentation,
- counterexample (error table) analysis,
- hyper-parameter synthesis, and
- model parameter synthesis