Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2603.09501 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914533153439744 |
|---|---|
| author | Hofstadler, Clemens Kaufmann, Daniela Chen, Chen |
| author_facet | Hofstadler, Clemens Kaufmann, Daniela Chen, Chen |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_09501 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits Hofstadler, Clemens Kaufmann, Daniela Chen, Chen Symbolic Computation 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. |
| title | Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits |
| topic | Symbolic Computation |
| url | https://arxiv.org/abs/2603.09501 |