← All papers

Sparse Matrix Multiplication Exponent 1.5 in the Low-bandwidth Model

Chetan Gupta, Jukka Suomela, Hossein Vahidi

cs.DC Nov 11, 2026 · v1 cs.DS

formalization verification

Read PDF arXiv abstract Code

TL;DR

The paper's main results were formalized in Lean with AI assistance, and the formalization is published on Zenodo.

Abstract

We study sparse matrix multiplication in the low-bandwidth model: $n$ computers multiply two $n\times n$ matrices, and each computer can send and receive one $O(\log n)$-bit message per round. The input matrices are uniformly sparse, meaning that there are at most $d$ nonzero entries in each row and column, and the task is to compute a uniformly sparse part of their product. In prior work, Gupta et al. (SPAA 2022) presented an $O(d^{1.907})$-round algorithm over fields for this problem when the sparsity structure is globally known in advance (this is referred to as the supported setting). The upper bound was later improved to $O(d^{1.832})$ rounds. In this work, we give a deterministic algorithm that solves this problem in $O(d^{3/2})$ rounds in the supported setting, improving the previous bounds over fields and semirings.

Problem

Uniformly sparse n×n matrix multiplication in the low-bandwidth model, where each of n computers sends and receives one O(log n)-bit message per round, with the sparsity structure known in advance (the supported setting). The best prior bounds were O(d^{1.832}) rounds over fields and O(d^{1.867}) over semirings.

Approach

A deterministic algorithm partitions the requested output positions into clusters, each packing d^{3/2} positions within a d×d rectangle, plus a remainder with an extra sparsity structure. Clusters and remaining positions are processed separately under a balanced public output assignment. AI tools assisted with the algorithm design and proofs, and AI was used to produce a Lean formalization of the results.

Results

A deterministic O(d^{3/2})-round algorithm for supported uniformly sparse matrix multiplication over both fields and semirings, improving on prior bounds. The Lean formalization is publicly available.

Result	Semirings	Fields
Trivial	O(d^2)	O(d^2)
Gupta et al. (2022)	O(d^1.927)	O(d^1.907)
Gupta et al. (2025)	O(d^1.867)	O(d^1.832)
This work	O(d^1.5)	O(d^1.5)

Round complexity bounds for supported sparse matrix multiplication

Papers With

Sparse Matrix Multiplication Exponent 1.5 in the Low-bandwidth Model