VoxLogicA2: A Spatial Model Checker for Neuro-symbolic Medical Imaging (extended version)

We present the tool VoxLogicA2, a spatial model checker aimed at Computer Vision, with applications in high-resolution 2D and 3D medical imaging. The new version of the tool combines logical primitives, non-logical primitives, and training and prediction primitives of state-of-the-art neural networks, freely interleaved with the symbolic tool functionality. The primary application field is neuro-symbolic medical image analysis. VoxLogicA2 is a fast, parallelising spatial model checker with a declarative domain-specific language, capable of describing both the learning procedures and the spatial logic procedures of an analysis in one program. We validate our approach by verifying its improved efficiency, and by using the new constructs of the language to describe case studies of previous work, which were based on Python, with a specification that uses VoxLogicA2 only