https://arxiv.org/api/93aaFGlP9M14ZA01Yiw5PtyPAvA 2026-04-09T14:27:02Z 3074 165 15 http://arxiv.org/abs/2512.07520v1 2025-12-08T12:58:35Z

Verifying the security of masked hardware and software implementations, under advanced leakage models, remains a significant challenge, especially then accounting for glitches, transitions and CPU micro-architectural specifics. Existing verification approaches are either restricted to small hardware gadgets, small programs on CPUs such as Sboxes, limited leakage models, or require hardware-specific prior knowledge. In this work, we present aLEAKator, an open-source framework for the automated formal verification of masked cryptographic accelerators and software running on CPUs from their HDL descriptions. Our method introduces mixed-domain simulation, enabling precise modeling and verification under various (including robust and relaxed) 1-probing leakage models, and supports variable signal granularity without being restricted to 1-bit wires. aLEAKator also supports verification in the presence of lookup tables, and does not require prior knowledge of the target CPU architecture. Our approach is validated against existing tools and real-world measurements while providing innovative results such as the verification of a full, first-order masked AES on various CPUs

2025-12-08T12:58:35Z Noé Amiot ALSOC Quentin L. Meunier ALSOC Karine Heydemann ALSOC Emmanuelle Encrenaz ALSOC http://arxiv.org/abs/2512.07018v1 2025-12-07T21:57:53Z

Motivated by functional synthesis in sequential circuit construction and quantified boolean formulas (QBF), boolean synthesis serves as one of the core problems in Formal Methods. Recent advances show that decision diagrams (DD) are particularly competitive in symbolic approaches for boolean synthesis, among which zero-suppressed decision diagram (ZDD) is a relatively new algorithmic approach, but is complementary to the industrial portfolio, where binary decision diagrams (BDDs) are more often applied. We propose a new dynamic-programming ZDD-based framework in the context of boolean synthesis, show solutions to theoretical challenges, develop a tool, and investigate the experimental performance. We also propose an idea of magic number that functions as the upper bound of planning-phase time and treewidth, showing how to interpret the exploration-exploitation dilemma in planning-execution synthesis framework. The algorithm we propose shows its strengths in general, gives inspiration for future needs to determine industrial magic numbers, and justifies that the framework we propose is an appropriate addition to the industrial synthesis solvers portfolio.

2025-12-07T21:57:53Z Yi Lin Moshe Y. Vardi http://arxiv.org/abs/2504.16632v2 2025-12-04T15:49:45Z

Matroid theory provides a unifying framework for studying dependence across combinatorics, geometry, and applications ranging from rigidity to statistics. In this work, we study circuit varieties of matroids, defined by their minimal dependencies, which play a central role in modeling determinantal varieties, rigidity problems, and conditional independence relations. We introduce an efficient computational strategy for decomposing the circuit variety of a given matroid $M$, based on an algorithm that identifies its maximal degenerations. These degenerations correspond to the largest matroids lying below $M$ in the weak order. Our framework yields explicit and computable decompositions of circuit varieties that were previously out of reach for symbolic or numerical algebra systems. We apply our strategy to several classical configurations, including the Vámos matroid, the unique Steiner quadruple system $S(3,4,8)$, projective and affine planes, the dual of the Fano matroid, and the dual of the graphic matroid of $K_{3,3}$. In each case, we successfully compute the minimal irreducible decomposition of their circuit varieties.

2025-04-23T11:47:56Z Emiliano Liwski Fatemeh Mohammadi Rémi Prébet http://arxiv.org/abs/2512.03864v1 2025-12-03T15:14:34Z

Smart manufacturing can significantly improve efficiency and reduce energy consumption, yet the energy demands of AI models may offset these gains. This study utilizes in-situ sensing-based prediction of geometric quality in smart machining to compare the energy consumption, accuracy, and speed of common AI models. HyperDimensional Computing (HDC) is introduced as an alternative, achieving accuracy comparable to conventional models while drastically reducing energy consumption, 200$\times$ for training and 175 to 1000$\times$ for inference. Furthermore, HDC reduces training times by 200$\times$ and inference times by 300 to 600$\times$, showcasing its potential for energy-efficient smart manufacturing.

2025-12-03T15:14:34Z Danny Hoang Anandkumar Patel Ruimen Chen Rajiv Malhotra Farhad Imani http://arxiv.org/abs/2512.02898v1 2025-12-02T16:04:51Z

Debugging is one of the most time-consuming and expensive tasks in software development and circuit design. Several formula-based fault localisation (FBFL) methods have been proposed, but they fail to guarantee a set of diagnoses across all failing tests or may produce redundant diagnoses that are not subset-minimal, particularly for programs/circuits with multiple faults. This paper introduces CFaults, a novel fault localisation tool for C software and Boolean circuits with multiple faults. CFaults leverages Model-Based Diagnosis (MBD) with multiple observations and aggregates all failing test cases into a unified Maximum Satisfiability (MaxSAT) formula. Consequently, our method guarantees consistency across observations and simplifies the fault localisation procedure. Experimental results on three benchmark sets, two of C programs, TCAS and C-Pack-IPAs, and one of Boolean circuits, ISCAS85, show that CFaults is faster at localising faults in C software than other FBFL approaches such as BugAssist, SNIPER, and HSD. On the ISCAS85 benchmark, CFaults is generally slower than HSD; however, it localises faults in only 6% fewer circuits, demonstrating that it remains competitive in this domain. Furthermore, CFaults produces only subset-minimal diagnoses of faulty statements, whereas the other approaches tend to enumerate redundant diagnoses (e.g., BugAssist and SNIPER).

2025-12-02T16:04:51Z 50 pages, 9 figures, 6 tables, 5 listings Pedro Orvalho Marta Kwiatkowska Mikoláš Janota Vasco Manquinho http://arxiv.org/abs/2410.17498v2 2025-12-02T00:32:57Z

Large Language Models (LLMs) have demonstrated impressive abilities in symbol processing through in-context learning (ICL). This success flies in the face of decades of critiques asserting that artificial neural networks cannot master abstract symbol manipulation. We seek to understand the mechanisms that can enable robust symbol processing in transformer networks, illuminating both the unanticipated success, and the significant limitations, of transformers in symbol processing. Borrowing insights from symbolic AI and cognitive science on the power of Production System architectures, we develop a high-level Production System Language, PSL, that allows us to write symbolic programs to do complex, abstract symbol processing, and create compilers that precisely implement PSL programs in transformer networks which are, by construction, 100% mechanistically interpretable. The work is driven by study of a purely abstract (semantics-free) symbolic task that we develop, Templatic Generation (TGT). Although developed through study of TGT, PSL is, we demonstrate, highly general: it is Turing Universal. The new type of transformer architecture that we compile from PSL programs suggests a number of paths for enhancing transformers' capabilities at symbol processing. We note, however, that the work we report addresses computability, and not learnability, by transformer networks. Note: The first section provides an extended synopsis of the entire paper.

2024-10-23T01:38:10Z Journal of Artificial Intelligence Research, 84(23) 2025 Paul Smolensky Roland Fernandez Zhenghao Herbert Zhou Mattia Opper Adam Davies Jianfeng Gao 10.1613/jair.1.17469 http://arxiv.org/abs/2512.01467v1 2025-12-01T09:50:04Z

We investigate whether continuous-control policies can be represented and learned as discrete logic circuits instead of continuous neural networks. We introduce Differentiable Weightless Controllers (DWCs), a symbolic-differentiable architecture that maps real-valued observations to actions using thermometer-encoded inputs, sparsely connected boolean lookup-table layers, and lightweight action heads. DWCs can be trained end-to-end by gradient-based techniques, yet compile directly into FPGA-compatible circuits with few- or even single-clock-cycle latency and nanojoule-level energy cost per action. Across five MuJoCo benchmarks, including high-dimensional Humanoid, DWCs achieve returns competitive with weight-based policies (full precision or quantized neural networks), matching performance on four tasks and isolating network capacity as the key limiting factor on HalfCheetah. Furthermore, DWCs exhibit structurally sparse and interpretable connectivity patterns, enabling a direct inspection of which input thresholds influence control decisions.

2025-12-01T09:50:04Z 16 pages, 11 figures, 10 tables Fabian Kresse Christoph H. Lampert http://arxiv.org/abs/2512.01355v1 2025-12-01T07:10:08Z

We establish the first complexity analysis for Krawczyk-based certified homotopy tracking. It consists of explicit a priori stepsize bounds ensuring the success of the Krawczyk test, and an iteration count bound proportional to the weighted length of the solution path. Our a priori bounds reduce the overhead of interval arithmetic, resulting in fewer iterations than previous methods. Experiments using a proof-of-concept implementation validate the results.

2025-12-01T07:10:08Z 16 pages, 1 figure, 3 tables Kisun Lee http://arxiv.org/abs/2507.19361v2 2025-12-01T06:55:00Z

We introduce Speech-based Intelligence Quotient (SIQ) as a new form of human cognition-inspired evaluation pipeline for voice understanding large language models, LLM Voice, designed to assess their voice understanding ability. Moving beyond popular voice understanding metrics such as word error rate (WER), SIQ examines LLM Voice across three cognitive levels motivated by Bloom's Taxonomy: (1) Remembering (i.e., WER for verbatim accuracy); (2) Understanding (i.e., similarity of LLM's interpretations); and (3) Application (i.e., QA accuracy for simulating downstream tasks). We demonstrate that SIQ not only quantifies voice understanding abilities but also provides unified comparisons between cascaded methods (e.g., ASR LLM) and end-to-end models, identifies annotation errors in existing benchmarks, and detects hallucinations in LLM Voice. Our framework represents a first-of-its-kind intelligence examination that bridges cognitive principles with voice-oriented benchmarks, while exposing overlooked challenges in multi-modal training. Our code and data will be open source to encourage future studies.

2025-07-25T15:12:06Z ACL 2025 main. Our Speech-IQ leaderboard is hosted at huggingface.co/spaces/nvidia/Speech-IQ-leaderboard. Speech-IQ Calculator: https://github.com/YukinoWan/SpeechIQ Zhen Wan Chao-Han Huck Yang Yahan Yu Jinchuan Tian Sheng Li Ke Hu Zhehuai Chen Shinji Watanabe Fei Cheng Chenhui Chu Sadao Kurohashi 10.18653/v1/2025.acl-long.1466 http://arxiv.org/abs/2501.08561v3 2025-11-30T17:42:09Z

In this paper, we propose an Adaptive Neuro-Symbolic Learning and Reasoning Framework for digital twin technology called "ANSR-DT." Digital twins in industrial environments often struggle with interpretability, real-time adaptation, and human input integration. Our approach addresses these challenges by combining CNN-LSTM dynamic event detection with reinforcement learning and symbolic reasoning to enable adaptive intelligence with interpretable decision processes. This integration enhances environmental understanding while promoting continuous learning, leading to more effective real-time decision-making in human-machine collaborative applications. We evaluated ANSR-DT on synthetic industrial data, observing significant improvements over traditional approaches, with up to 99.5% accuracy for dynamic pattern recognition. The framework demonstrated superior adaptability with extended reinforcement learning training, improving explained variance from 0.447 to 0.547. Future work aims at scaling to larger datasets to test rule management beyond the current 14 rules. Our open-source implementation promotes reproducibility and establishes a foundation for future research in adaptive, interpretable digital twins for industrial applications.

2025-01-15T04:04:57Z Code available at https://github.com/sbhakim/ansr-dt Safayat Bin Hakim Muhammad Adil Alvaro Velasquez Houbing Herbert Song http://arxiv.org/abs/2511.10786v2 2025-11-30T05:32:21Z

We give explicit low-rank bilinear non-commutative schemes for multiplying structured $n \times n$ matrices with $2 \leq n \leq 5$, which serve as building blocks for recursive algorithms with improved multiplicative factors in asymptotic complexity. Our schemes are discovered over $\mathbb{F}_2$ or $\mathbb{F}_3$ and lifted to $\mathbb{Z}$ or $\mathbb{Q}$. Using a flip graph search over tensor decompositions, we derive schemes for general, upper-triangular, lower-triangular, symmetric, and skew-symmetric inputs, as well as products of a structured matrix with its transpose. These schemes improve asymptotic constants for 13 of 15 structured formats. In particular, we obtain $4 \times 4$ rank-34 schemes for both multiplying a general matrix by its transpose and an upper-triangular matrix by a general matrix, improving the asymptotic factor from 8/13 (0.615) to 22/37 (0.595). Additionally, using $\mathbb{F}_3$ flip graphs, we discover schemes over $\mathbb{Q}$ that fundamentally require the inverse of 2, including a $2 \times 2$ symmetric-symmetric multiplication of rank 5 and a $3 \times 3$ skew-symmetric-general multiplication of rank 14 (improving upon AlphaTensor's 15).

2025-11-13T20:19:05Z Kirill Khoruzhii Patrick Gelß Sebastian Pokutta http://arxiv.org/abs/2511.20317v2 2025-11-29T15:36:19Z

Matrix multiplication optimization remains a fundamental challenge in computational mathematics. This work introduces a novel approach that discovers matrix multiplication schemes whose coefficients are restricted to the set $\{-1, 0, 1\}$ (denoted $Z_T$), minimizing naive additive complexity for efficient hardware implementation. The core of the method is a GPU-accelerated meta flip graph algorithm that maintains ternary safety through specialized arithmetic operations and sign symmetry breaking. Key results include new best ranks for the formats $4 \times 5 \times 12$, $5 \times 6 \times 10$, and $6 \times 7 \times 9$, the independent discovery of 32 schemes in $Z_T$ that match known optimal ranks (including 8 previously known only with rational coefficients), and 30 rank improvements in the binary field. The analysis of 164 known schemes shows that 92 admit a ternary-coefficient implementation, while 72 could not be found under this constraint, defining the current boundaries of the approach. All software, results, and discovered schemes are provided as open-source.

2025-11-25T13:53:17Z A. I. Perminov http://arxiv.org/abs/2512.05133v1 2025-11-28T17:31:44Z

We review the definition and main properties of differential subresultants in order to achieve their implementation in Maple, using the DEtools package. The focus is on computing GCRDs of ordinary differential operators with non necessarily rational coefficients. Determinant expressions provide explicit control, enabling the treatment of coefficients with parameters. Applications to commuting ordinary differential operators illustrate the effectiveness of the method.

2025-11-28T17:31:44Z 10 pages, 0 figures M. Cabellos S. L. Rueda http://arxiv.org/abs/2406.17122v2 2025-11-27T20:36:51Z

We describe two new algorithms for the computation of Whitney stratifications of real and complex algebraic varieties. The first algorithm is a modification of the algorithm of Helmer and Nanda (HN), but is made more efficient by using techniques for equidimensional decomposition rather than computing the set of associated primes of a polynomial ideal at a key step in the HN algorithm. We note that this modified algorithm may fail to produce a minimal Whitney stratification even when the HN algorithm would produce a minimal stratification. The second algorithm coarsens a given Whitney stratification of a complex variety to the unique minimal Whitney stratification; we refer to this as the minimization of a stratification. The theoretical basis for our approach is a classical result of Teissier. To our knowledge this yields the first algorithm for computing a minimal Whitney stratification.

2024-06-24T20:17:06Z Martin Helmer Rafael Mohr http://arxiv.org/abs/2511.21509v1 2025-11-26T15:44:54Z

In the past two decades, significant research and development effort went into the development of verification tools for individual languages, such asC, C++, and Java. Many of the used verification approaches are in fact language-agnostic and it would be beneficial for the technology transfer to allow for using the implementations also for other programming and modeling languages. To address the problem, we propose SV-LIB, an exchange format and intermediate language for software-verification tasks, including programs, specifications, and verification witnesses. SV-LIBis based on well-known concepts from imperative programming languages and uses SMT-LIB to represent expressions and sorts used in the program. This makes it easy to parse and to build into existing infrastructure, since many verification tools are based on SMT solvers already. Furthermore, SV-LIBdefines a witness format for both correct and incorrect SV-LIB programs, together with means for specifying witness-validation tasks. This makes it possible both to implement independent witness validators and to reuse some verifiers also as validators for witnesses. This paper presents version 1.0 of the SV-LIBformat, including its design goals, the syntax, and informal semantics. Formal semantics and further extensions to concurrency are planned for future versions.

2025-11-26T15:44:54Z Dirk Beyer Gidon Ernst Martin Jonáš Marian Lingsch-Rosenfeld