Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _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 |