arXiv subjects

Mirco Tribastone

Publications and source records attributed to Mirco Tribastone.

At least 19 recordsLinked to original sources

arXiv2026

Scaling Weisfeiler-Leman Expressiveness Analysis to Massive Graphs with GPUs

The stable coloring of the Weisfeiler-Leman (1-WL) test is a cornerstone of Graph Neural Networks because it provides an upper bound to the expressive power of message-passing architectures. Unfortunately, computing it presents two fundamental bottlenecks. First, classic algorithms are inherently sequential and cannot exploit modern massively parallel hardware. Second, these are \emph{global} algorithms, i.e., they require availability in memory of the full graph, severely limiting applicability to real-world instances. We leverage a linear-algebraic interpretation of 1-WL stable coloring and introduce two key contributions: (i)~a randomized refinement algorithm with tight probabilistic guarantees and (ii)~a correctness-preserving batching scheme that decomposes the graph into independently processable subgraphs while provably returning a stable coloring of the original graph. This approach maps directly to GPU-efficient primitives. In numerical experiments, our CUDA implementation delivers speedups up to two orders of magnitude over classical CPU-based partition refinement and, for the first time, successfully computes stable colorings on web-scale graphs with over 30 billion edges, where CPU baselines time out or fail.

cs.DC↗

arXiv2026

Neural Network Compression by Approximate Differential Equivalence

Neural network compression is commonly achieved by pruning parameters based on local importance scores, e.g., magnitude-based pruning. We propose a complementary approach that compresses models by aggregating neurons with similar functional behavior rather than removing weights independently. Our method encodes a trained network as a polynomial ODE system and applies a lumping method called Approximate Forward Differential Equivalence to identify neurons with approximately matching induced dynamics. A single tolerance parameter, $\varepsilon$, controls the compression level and induces a smooth trade-off between model size and predictive accuracy. We evaluate the method on synthetic datasets derived from nonlinear dynamical systems with known ground-truth behavior and on public regression benchmarks. Across both settings, the proposed approach achieves substantial parameter reduction while preserving accuracy, and consistently compares favorably with magnitude-based pruning and Wanda at similar compression levels. These results suggest that differential equivalence-based aggregation is a principled and effective alternative to conventional weight-centric pruning.

cs.LG↗

arXiv2026

RAwR: Role-Aware Rewiring via Approximate Equitable Partition

While Graph Neural Networks (GNNs) have demonstrated significant efficacy in node classification tasks, where predictions rely on local neighborhood information, the performance of GNNs often drops when prediction tasks depend on long-range interactions. These limitations are attributed to phenomena such as oversquashing, where structural bottlenecks restrict signal propagation across the network topology. To address this challenge, we introduce RAwR, a computationally efficient rewiring framework that augments the input graph with a quotient graph derived from equitable partitions. This approach facilitates accelerated communication between nodes that share identical structural roles, as identified by the Weisfeiler-Leman graph coloring, and thereby reduces the total effective resistance of the system. Furthermore, by employing an approximate definition of the equitable partition, RAwR enables a controllable reduction of the quotient graph, which, in its most condensed state, recovers the conventional Master Node rewiring technique. Empirical evaluations across a diverse suite of benchmarks -- including homophilic, heterophilic, and synthetic long-range datasets -- demonstrate that RAwR achieves state-of-the-art results. Our contribution is further supported by an analytical investigation using a teacher-student model of linear GNNs, which elucidates the theoretical foundations of role-based rewiring. This analysis leads to the formulation of Spectral Role Lift (SRL), a metric designed to identify the optimal approximate equitable partition for maximizing predictive performance.

cs.LG↗

arXiv2026

DeGAS: Gradient-Based Optimization of Probabilistic Programs without Sampling

We present DeGAS, a differentiable Gaussian approximate semantics for loopless probabilistic programs that enables sample-free, gradient-based optimization in models with both continuous and discrete components. DeGAS evaluates programs under a Gaussian-mixture semantics and replaces measure-zero predicates and discrete branches with a vanishing smoothing, yielding closed-form expressions for posterior and path probabilities. We prove differentiability of these quantities with respect to program parameters, enabling end-to-end optimization via standard automatic differentiation, without Monte Carlo estimators. On thirteen benchmark programs, DeGAS achieves accuracy and runtime competitive with variational inference and MCMC. Importantly, it reliably tackles optimization problems where sampling-based baselines fail to converge due to conditioning involving continuous variables.

cs.PL↗

arXiv2025

Certified Inductive Synthesis for Online Mixed-Integer Optimization

In fields such as autonomous and safety-critical systems, online optimization plays a crucial role in control and decision-making processes, often requiring the integration of continuous and discrete variables. These tasks are frequently modeled as mixed-integer programming (MIP) problems, where feedback data are incorporated as parameters. However, solving MIPs within strict time constraints is challenging due to their $\mathcal{NP}$-complete nature. A promising solution to this challenge involves leveraging the largely invariant structure of these problems to perform most computations offline, thus enabling efficient online solving even on platforms with limited hardware capabilities. In this paper we present a novel implementation of this strategy that uses counterexample-guided inductive synthesis to split the MIP solution process into two stages. In the offline phase, we construct a mapping that provides feasible assignments for binary variables based on parameter values within a specified range. In the online phase, we solve the remaining continuous part of the problem by fixing the binary variables to the values predicted by this mapping. Our numerical evaluation demonstrates the efficiency and solution quality of this approach compared to standard mixed-integer solvers, highlighting its potential for real-time applications in resource-constrained environments.

math.OC↗

arXiv2024

Efficient Network Embedding by Approximate Equitable Partitions

Structural network embedding is a crucial step in enabling effective downstream tasks for complex systems that aims to project a network into a lower-dimensional space while preserving similarities among nodes. We introduce a simple and efficient embedding technique based on approximate variants of equitable partitions. The approximation consists in introducing a user-tunable tolerance parameter relaxing the otherwise strict condition for exact equitable partitions that can be hardly found in real-world networks. We exploit a relationship between equitable partitions and equivalence relations for Markov chains and ordinary differential equations to develop a partition refinement algorithm for computing an approximate equitable partition in polynomial time. We compare our method against state-of-the-art embedding techniques on benchmark networks. We report comparable -- when not superior -- performance for visualization, classification, and regression tasks at a cost between one and three orders of magnitude smaller using a prototype implementation, enabling the embedding of large-scale networks which could not be efficiently handled by most of the competing techniques.

cs.SI↗

arXiv2024

Forward and Backward Constrained Bisimulations for Quantum Circuits using Decision Diagrams

Efficient methods for the simulation of quantum circuits on classic computers are crucial for their analysis due to the exponential growth of the problem size with the number of qubits. Here we study lumping methods based on bisimulation, an established class of techniques that has been proven successful for (classic) stochastic and deterministic systems such as Markov chains and ordinary differential equations. Forward constrained bisimulation yields a lower-dimensional model which exactly preserves quantum measurements projected on a linear subspace of interest. Backward constrained bisimulation gives a reduction that is valid on a subspace containing the circuit input, from which the circuit result can be fully recovered. We provide an algorithm to compute the constraint bisimulations yielding coarsest reductions in both cases, using a duality result relating the two notions. As applications, we provide theoretical bounds on the size of the reduced state space for well-known quantum algorithms for search, optimization, and factorization. Using a prototype implementation, we report significant reductions on a set of benchmarks. In particular, we show that constrained bisimulation can boost decision-diagram-based quantum circuit simulation by several orders of magnitude, allowing thus for substantial synergy effects.

quant-ph↗

arXiv2023

Proper Lumping for Positive Bilinear Control Systems

Positive systems naturally arise in situations where the model tracks physical quantities. Although the linear case is well understood, analysis and controller design for nonlinear positive systems remain challenging. Model reduction methods can help tame this problem. Here we propose a notion of model reduction for a class of positive bilinear systems with (bounded) matrix and exogenous controls. Our reduction, called proper positive lumping, aggregates the original system such that states of the corresponding reduced model represent non-negative linear combinations of original state variables. We prove a characterization result showing that the reductions by proper positive lumping are exactly those preserving the optimality of a suitable class of value functions. Moreover, we provide an efficient polynomial-time algorithm for the computation of the minimal lumping. We numerically evaluate our approach by applying it to a number of benchmark case studies.

math.OC↗

arXiv2023

Coarse-graining Complex Networks for Control Equivalence

The ability to control complex networks is of crucial importance across a wide range of applications in natural and engineering sciences. However, issues of both theoretical and numerical nature introduce fundamental limitations to controlling large-scale networks. In this paper, we cope with this problem by introducing a coarse-graining algorithm. It leads to an aggregated network which satisfies control equivalence, i.e., such that the optimal control values for the original network can be exactly recovered from those of the aggregated one. The algorithm is based on a partition refinement method originally devised for systems of ordinary differential equations, here extended and applied to linear dynamics on complex networks. Using a number of benchmarks from the literature we show considerable reductions across a variety of networks from biology, ecology, engineering, and social sciences.

eess.SY↗

arXiv2023

Certification of the proximal gradient method under fixed-point arithmetic for box-constrained QP problems

In safety-critical applications that rely on the solution of an optimization problem, the certification of the optimization algorithm is of vital importance. Certification and suboptimality results are available for a wide range of optimization algorithms. However, a typical underlying assumption is that the operations performed by the algorithm are exact, i.e., that there is no numerical error during the mathematical operations, which is hardly a valid assumption in a real hardware implementation. This is particularly true in the case of fixed-point hardware, where computational inaccuracies are not uncommon. This article presents a certification procedure for the proximal gradient method for box-constrained QP problems implemented in fixed-point arithmetic. The procedure provides a method to select the minimal fractional precision required to obtain a certain suboptimality bound, indicating the maximum number of iterations of the optimization method required to obtain it. The procedure makes use of formal verification methods to provide arbitrarily tight bounds on the suboptimality guarantee. We apply the proposed certification procedure on the implementation of a non-trivial model predictive controller on 32-bit fixed-point hardware.

math.OC↗

arXiv2023

Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures

Computing the posterior distribution of a probabilistic program is a hard task for which no one-fit-for-all solution exists. We propose Gaussian Semantics, which approximates the exact probabilistic semantics of a bounded program by means of Gaussian mixtures. It is parametrized by a map that associates each program location with the moment order to be matched in the approximation. We provide two main contributions. The first is a universal approximation theorem stating that, under mild conditions, Gaussian Semantics can approximate the exact semantics arbitrarily closely. The second is an approximation that matches up to second-order moments analytically in face of the generally difficult problem of matching moments of Gaussian mixtures with arbitrary moment order. We test our second-order Gaussian approximation (SOGA) on a number of case studies from the literature. We show that it can provide accurate estimates in models not supported by other approximation methods or when exact symbolic techniques fail because of complex expressions or non-simplified integrals. On two notable classes of problems, namely collaborative filtering and programs involving mixtures of continuous and discrete distributions, we show that SOGA significantly outperforms alternative techniques in terms of accuracy and computational time.

cs.PL↗

arXiv2023

Minimization of Dynamical Systems over Monoids

Quantitative notions of bisimulation are well-known tools for the minimization of dynamical models such as Markov chains and ordinary differential equations (ODEs). In \emph{forward bisimulations}, each state in the quotient model represents an equivalence class and the dynamical evolution gives the overall sum of its members in the original model. Here we introduce generalized forward bisimulation (GFB) for dynamical systems over commutative monoids and develop a partition refinement algorithm to compute the coarsest one. When the monoid is $(\mathbb{R}, +)$, we recover probabilistic bisimulation for Markov chains and more recent forward bisimulations for nonlinear ODEs. Using $(\mathbb{R}, \cdot)$ we get nonlinear reductions for discrete-time dynamical systems and ODEs where each variable in the quotient model represents the product of original variables in the equivalence class. When the domain is a finite set such as the Booleans $\mathbb{B}$, we can apply GFB to Boolean networks (BN), a widely used dynamical model in computational biology. Using a prototype implementation of our minimization algorithm for GFB, we find disjunction- and conjunction-preserving reductions on 60 BN from two well-known repositories, and demonstrate the obtained analysis speed-ups. We also provide the biological interpretation of the reduction obtained for two selected BN, and we show how GFB enables the analysis of a large one that could not be analyzed otherwise. Using a randomized version of our algorithm we find product-preserving (therefore non-linear) reductions on 21 dynamical weighted networks from the literature that could not be handled by the exact algorithm.

cs.LO↗

arXiv2023

Optimality-preserving Reduction of Chemical Reaction Networks

Across many disciplines, chemical reaction networks (CRNs) are an established population model defined as a system of coupled nonlinear ordinary differential equations. In many applications, for example, in systems biology and epidemiology, CRN parameters such as the kinetic reaction rates can be used as control inputs to steer the system toward a given target. Unfortunately, the resulting optimal control problem is nonlinear, therefore, computationally very challenging. We address this issue by introducing an optimality-preserving reduction algorithm for CRNs. The algorithm partitions the original state variables into a reduced set of macro-variables for which one can define a reduced optimal control problem from which one can exactly recover the solution of the original control problem. Notably, the reduction algorithm runs with polynomial time complexity in the size of the CRN. We use this result to reduce reachability and control problems of large-scale protein-interaction networks and vaccination models with hundreds of thousands of state variables.

eess.SY↗

arXiv2021

Reducing Boolean Networks with Backward Boolean Equivalence

Boolean Networks (BNs) are established models to qualitatively describe biological systems. The analysis of BNs might be infeasible for medium to large BNs due to the state-space explosion problem. We propose a novel reduction technique called \emph{Backward Boolean Equivalence} (BBE), which preserves some properties of interest of BNs. In particular, reduced BNs provide a compact representation by grouping variables that, if initialized equally, are always updated equally. The resulting reduced state space is a subset of the original one, restricted to identical initialization of grouped variables. The corresponding trajectories of the original BN can be exactly restored. We show the effectiveness of BBE by performing a large-scale validation on the whole GINsim BN repository. In selected cases, we show how our method enables analyses that would be otherwise intractable. Our method complements, and can be combined with, other reduction methods found in the literature.

cs.CE↗

arXiv2021

Improved estimations of stochastic chemical kinetics by finite state expansion

Stochastic reaction networks are a fundamental model to describe interactions between species where random fluctuations are relevant. The master equation provides the evolution of the probability distribution across the discrete state space consisting of vectors of population counts for each species. However, since its exact solution is often elusive, several analytical approximations have been proposed. The deterministic rate equation (DRE) gives a macroscopic approximation as a compact system of differential equations that estimate the average populations for each species, but it may be inaccurate in the case of nonlinear interaction dynamics. Here we propose finite state expansion (FSE), an analytical method mediating between the microscopic and the macroscopic interpretations of a stochastic reaction network by coupling the master equation dynamics of a chosen subset of the discrete state space with the mean population dynamics of the DRE. An algorithm translates a network into an expanded one where each discrete state is represented as a further distinct species. This translation exactly preserves the stochastic dynamics, but the DRE of the expanded network can be interpreted as a correction to the original one. The effectiveness of FSE is demonstrated in models that challenge state-of-the-art techniques due to intrinsic noise, multi-scale populations, and multi-stability.

q-bio.MN↗

arXiv2021

Efficient Local Computation of Differential Bisimulations via Coupling and Up-to Methods

We introduce polynomial couplings, a generalization of probabilistic couplings, to develop an algorithm for the computation of equivalence relations which can be interpreted as a lifting of probabilistic bisimulation to polynomial differential equations, a ubiquitous model of dynamical systems across science and engineering. The algorithm enjoys polynomial time complexity and complements classical partition-refinement approaches because: (a) it implements a local exploration of the system, possibly yielding equivalences that do not necessarily involve the inspection of the whole system of differential equations; (b) it can be enhanced by up-to techniques; and (c) it allows the specification of pairs which ought not to be included in the output. Using a prototype, these advantages are demonstrated on case studies from systems biology for applications to model reduction and comparison. Notably, we report four orders of magnitude smaller runtimes than partition-refinement approaches when disproving equivalences between Markov chains.

cs.LO↗

arXiv2021

Exact maximal reduction of stochastic reaction networks by species lumping

Motivation: Stochastic reaction networks are a widespread model to describe biological systems where the presence of noise is relevant, such as in cell regulatory processes. Unfortu-nately, in all but simplest models the resulting discrete state-space representation hinders analytical tractability and makes numerical simulations expensive. Reduction methods can lower complexity by computing model projections that preserve dynamics of interest to the user. Results: We present an exact lumping method for stochastic reaction networks with mass-action kinetics. It hinges on an equivalence relation between the species, resulting in a reduced network where the dynamics of each macro-species is stochastically equivalent to the sum of the original species in each equivalence class, for any choice of the initial state of the system. Furthermore, by an appropriate encoding of kinetic parameters as additional species, the method can establish equivalences that do not depend on specific values of the parameters. The method is supported by an efficient algorithm to compute the largest species equivalence, thus the maximal lumping. The effectiveness and scalability of our lumping technique, as well as the physical interpretability of resulting reductions, is demonstrated in several models of signaling pathways and epidemic processes on complex networks. Availability: The algorithms for species equivalence have been implemented in the software tool ERODE, freely available for download from https://www.erode.eu.

q-bio.QM↗

arXiv2020

CLUE: Exact maximal reduction of kinetic models by constrained lumping of differential equations

Motivation: Detailed mechanistic models of biological processes can pose significant challenges for analysis and parameter estimations due to the large number of equations used to track the dynamics of all distinct configurations in which each involved biochemical species can be found. Model reduction can help tame such complexity by providing a lower-dimensional model in which each macro-variable can be directly related to the original variables. Results: We present CLUE, an algorithm for exact model reduction of systems of polynomial differential equations by constrained linear lumping. It computes the smallest dimensional reduction as a linear mapping of the state space such that the reduced model preserves the dynamics of user-specified linear combinations of the original variables. Even though CLUE works with nonlinear differential equations, it is based on linear algebra tools, which makes it applicable to high-dimensional models. Using case studies from the literature, we show how CLUE can substantially lower model dimensionality and help extract biologically intelligible insights from the reduction. Availability: An implementation of the algorithm and relevant resources to replicate the experiments herein reported are freely available for download at https://github.com/pogudingleb/CLUE. Supplementary information: enclosed.

q-bio.MN↗