arXiv subjects

Elisabetta De Maria

Publications and source records attributed to Elisabetta De Maria.

8 recordsLinked to original sources

arXiv2026

A Formal Tool for Verification of Probabilistic Spiking Neural Networks Based on Quotient Abstractions

Spiking Neural Networks (SNNs) model biological neural dynamics more faithfully than classical artificial networks, but their stochastic, event-driven computation -- rooted in ion-channel noise and unreliable synaptic vesicle release -- demands probabilistic models for which deterministic abstractions are mathematically inadequate. Formal verification of such models via probabilistic model checking faces a fundamental barrier: the state space explosion problem, where the Discrete-Time Markov Chain (DTMC) encoding grows exponentially with the number of neurons. General-purpose quotient model abstractions [1] can in principle mitigate this growth by partitioning membrane potentials into equivalence classes, but a na\"ive application to SNNs discards synaptic weight information, limiting the properties that can be verified. This paper introduces a weight-discretized quotient model abstraction that maps continuous synaptic weights to a compact integer range while preserving the relative contribution of each synapse, and presents CogSpike, a unified workbench that integrates SNN design, simulation, and PRISM-based formal verification within a single isomorphic tool chain. The discretization is accompanied by formal correctness guarantees: a two-sided fidelity theorem confines any firing disagreement to a bounded gray zone around threshold, and an Asymptotic Silence theorem gives the exact limit guarantee that unforced neurons fall permanently silent. A topology-dependent scaling analysis shows that the state space reduction compounds exponentially -- approximately $17\times$ per neuron for discretization parameter $W = 3$ -- enabling verification of networks that are otherwise intractable, as confirmed empirically across seven canonical topologies.

cs.NE↗

arXiv2026

A Probabilistic Model-Checking Framework for Cognitive Assessment and Training

Serious games have proven to be effective tools for screening cognitive impairments and supporting diagnosis in patients with neurodegenerative diseases like Alzheimer's and Parkinson's. They also offer cognitive training benefits. According to the DSM-5 classification, cognitive disorders are categorized as Mild Neurocognitive Disorders (mild NCDs) and Major Neurocognitive Disorders (Major NCDs). In this study, we focus on three patient groups: healthy, mild NCD, and Major NCD. We employ Discrete Time Markov Chains to model the behavior exhibited by each group while interacting with serious games. By applying model-checking techniques, we can identify discrepancies between expected and actual gameplay behavior. The primary contribution of this work is a novel theoretical framework designed to assess how a practitioner's confidence level in diagnosing a patient's Alzheimer's stage evolves with each game session (diagnosis support). Additionally, we propose an experimental protocol where the difficulty of subsequent game sessions is dynamically adjusted based on the patient's observed behavior in previous sessions (training support).

cs.FL↗

arXiv2025

Probabilistic Modeling of Spiking Neural Networks with Contract-Based Verification

Spiking Neural Networks (SNN) are models for "realistic" neuronal computation, which makes them somehow different in scope from "ordinary" deep-learning models widely used in AI platforms nowadays. SNNs focus on timed latency (and possibly probability) of neuronal reactive activation/response, more than numerical computation of filters. So, an SNN model must provide modeling constructs for elementary neural bundles and then for synaptic connections to assemble them into compound data flow network patterns. These elements are to be parametric patterns, with latency and probability values instantiated on particular instances (while supposedly constant "at runtime"). Designers could also use different values to represent "tired" neurons, or ones impaired by external drugs, for instance. One important challenge in such modeling is to study how compound models could meet global reaction requirements (in stochastic timing challenges), provided similar provisions on individual neural bundles. A temporal language of logic to express such assume/guarantee contracts is thus needed. This may lead to formal verification on medium-sized models and testing observations on large ones. In the current article, we make preliminary progress at providing a simple model framework to express both elementary SNN neural bundles and their connecting constructs, which translates readily into both a model-checker and a simulator (both already existing and robust) to conduct experiments.

cs.AI↗

arXiv2025

Large Language Model Meets Constraint Propagation

Large Language Models (LLMs) excel at generating fluent text but struggle to enforce external constraints because they generate tokens sequentially without explicit control mechanisms. GenCP addresses this limitation by combining LLM predictions with Constraint Programming (CP) reasoning, formulating text generation as a Constraint Satisfaction Problem (CSP). In this paper, we improve GenCP by integrating Masked Language Models (MLMs) for domain generation, which allows bidirectional constraint propagation that leverages both past and future tokens. This integration bridges the gap between token-level prediction and structured constraint enforcement, leading to more reliable and constraint-aware text generation. Our evaluation on COLLIE benchmarks demonstrates that incorporating domain preview via MLM calls significantly improves GenCP's performance. Although this approach incurs additional MLM calls and, in some cases, increased backtracking, the overall effect is a more efficient use of LLM inferences and an enhanced ability to generate feasible and meaningful solutions, particularly in tasks with strict content constraints.

cs.CL↗

arXiv2025

Modelling and Verifying Neuronal Archetypes in Rocq

Formal verification has become increasingly important because of the kinds of guarantees that it can provide for software systems. Verification of models of biological and medical systems is a promising application of formal verification. Human neural networks have recently been emulated and studied as a biological system. In this paper, we provide a model of some crucial neuronal circuits, called "archetypes", in the Coq Proof Assistant and prove properties concerning their dynamic behavior. Understanding the behavior of these modules is crucial because they constitute the elementary building blocks of bigger neuronal circuits. We consider seven fundamental archetypes (simple series, series with multiple outputs, parallel composition, positive loop, negative loop, inhibition of a behavior, and contralateral inhibition), and prove an important representative property for six of them. In building up to our model of archetypes, we also provide a general model of "neuronal circuits", and prove a variety of general properties about neurons and circuits. In addition, we have defined our model with a longer term goal of modelling the composition of basic archetypes into larger networks, and structured our libraries with definitions and lemmas useful for proving the properties in this paper as well as those to be proved as future work.

cs.LO↗

arXiv2024

Combining Constraint Programming Reasoning with Large Language Model Predictions

Constraint Programming (CP) and Machine Learning (ML) face challenges in text generation due to CP's struggle with implementing "meaning'' and ML's difficulty with structural constraints. This paper proposes a solution by combining both approaches and embedding a Large Language Model (LLM) in CP. The LLM handles word generation and meaning, while CP manages structural constraints. This approach builds on GenCP, an improved version of On-the-fly Constraint Programming Search (OTFS) using LLM-generated domains. Compared to Beam Search (BS), a standard NLP method, this combined approach (GenCP with LLM) is faster and produces better results, ensuring all constraints are satisfied. This fusion of CP and ML presents new possibilities for enhancing text generation under constraints.

cs.CL↗

arXiv2018

Spiking Neural Networks modelled as Timed Automata with parameter learning

In this paper we present a novel approach to automatically infer parameters of spiking neural networks. Neurons are modelled as timed automata waiting for inputs on a number of different channels (synapses), for a given amount of time (the accumulation period). When this period is over, the current potential value is computed considering current and past inputs. If this potential overcomes a given threshold, the automaton emits a broadcast signal over its output channel , otherwise it restarts another accumulation period. After each emission, the automaton remains inactive for a fixed refractory period. Spiking neural networks are formalised as sets of automata, one for each neuron, running in parallel and sharing channels according to the network structure. Such a model is formally validated against some crucial properties defined via proper temporal logic formulae. The model is then exploited to find an assignment for the synaptical weights of neural networks such that they can reproduce a given behaviour. The core of this approach consists in identifying some correcting actions adjusting synaptical weights and back-propagating them until the expected behaviour is displayed. A concrete case study is discussed.

q-bio.NC↗

arXiv2014

A Logical Framework for Systems Biology

We propose a novel approach for the formal verification of biological systems based on the use of a modal linear logic. We show how such a logic can be used, with worlds as instants of time, as an unified framework to encode both biological systems and temporal properties of their dynamic behaviour. To illustrate our methodology, we consider a model of the P53/Mdm2 DNA-damage repair mechanism. We prove several properties that are important for such a model to satisfy and serve to illustrate the promise of our approach. We formalize the proofs of these properties in the Coq Proof Assistant, with the help of a Lambda Prolog prover for partial automation of the proofs.

cs.LO↗