Paper
Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits
Authors
Clemens Hofstadler, Daniela Kaufmann, Chen Chen
Abstract
Word-level verification of arithmetic circuits with large operands typically relies on arbitrary-precision arithmetic, which can lead to significant computational overhead as word sizes grow. In this paper, we present a hybrid algebraic verification technique based on polynomial reasoning that combines linear and nonlinear rewriting. Our approach relies on multimodular reasoning using homomorphic images, where computations are performed in parallel modulo different primes, thereby avoiding any large-integer arithmetic. We implement the proposed method in the verification tool TalisMan2.0 and evaluate it on a suite of multiplier benchmarks. Our results show that hybrid multimodular reasoning significantly improves upon existing approaches.
Metadata
Related papers
Cosmic Shear in Effective Field Theory at Two-Loop Order: Revisiting $S_8$ in Dark Energy Survey Data
Shi-Fan Chen, Joseph DeRose, Mikhail M. Ivanov, Oliver H. E. Philcox • 2026-03-30
Stop Probing, Start Coding: Why Linear Probes and Sparse Autoencoders Fail at Compositional Generalisation
Vitória Barin Pacela, Shruti Joshi, Isabela Camacho, Simon Lacoste-Julien, Da... • 2026-03-30
SNID-SAGE: A Modern Framework for Interactive Supernova Classification and Spectral Analysis
Fiorenzo Stoppa, Stephen J. Smartt • 2026-03-30
Acoustic-to-articulatory Inversion of the Complete Vocal Tract from RT-MRI with Various Audio Embeddings and Dataset Sizes
Sofiane Azzouz, Pierre-André Vuissoz, Yves Laprie • 2026-03-30
Rotating black hole shadows in metric-affine bumblebee gravity
Jose R. Nascimento, Ana R. M. Oliveira, Albert Yu. Petrov, Paulo J. Porfírio,... • 2026-03-30
Raw Data (Debug)
{
"raw_xml": "<entry>\n <id>http://arxiv.org/abs/2603.09501v1</id>\n <title>Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits</title>\n <updated>2026-03-10T11:05:47Z</updated>\n <link href='https://arxiv.org/abs/2603.09501v1' rel='alternate' type='text/html'/>\n <link href='https://arxiv.org/pdf/2603.09501v1' rel='related' title='pdf' type='application/pdf'/>\n <summary>Word-level verification of arithmetic circuits with large operands typically relies on arbitrary-precision arithmetic, which can lead to significant computational overhead as word sizes grow. In this paper, we present a hybrid algebraic verification technique based on polynomial reasoning that combines linear and nonlinear rewriting. Our approach relies on multimodular reasoning using homomorphic images, where computations are performed in parallel modulo different primes, thereby avoiding any large-integer arithmetic. We implement the proposed method in the verification tool TalisMan2.0 and evaluate it on a suite of multiplier benchmarks. Our results show that hybrid multimodular reasoning significantly improves upon existing approaches.</summary>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.SC'/>\n <published>2026-03-10T11:05:47Z</published>\n <arxiv:comment>Submitted to IJCAR 2026</arxiv:comment>\n <arxiv:primary_category term='cs.SC'/>\n <author>\n <name>Clemens Hofstadler</name>\n </author>\n <author>\n <name>Daniela Kaufmann</name>\n </author>\n <author>\n <name>Chen Chen</name>\n </author>\n </entry>"
}