https://arxiv.org/api/6XuFCjBXylW3J/mNvq9iv+lbE2I 2026-04-13T16:42:18Z 3075 600 15 http://arxiv.org/abs/2307.12712v3 2024-07-01T08:43:58Z

This paper deals with simultaneously fast and in-place algorithms for formulae where the result has to be linearly accumulated: some of the output variables are also input variables, linked by a linear dependency. Fundamental examples include the in-place accumulated multiplication of polynomials or matrices, C+=AB. The difficulty is to combine in-place computations with fast algorithms: those usually come at the expense of (potentially large) extra temporary space, but with accumulation the output variables are not even available to store intermediate values. We first propose a novel automatic design of fast and in-place accumulating algorithms for any bilinear formulae (and thus for polynomial and matrix multiplication) and then extend it to any linear accumulation of a collection of functions. For this, we relax the in-place model to any algorithm allowed to modify its inputs, provided that those are restored to their initial state afterwards. This allows us, in fine, to derive unprecedented in-place accumulating algorithms for fast polynomial multiplications and for Strassen-like matrix multiplications.

2023-07-24T11:47:29Z Proceedings of the 49th International Symposium on Symbolic and Algebraic Computation (ISSAC'24), ACM SIGSAM, Jul 2024, Raleigh, NC, United States Jean-Guillaume Dumas CASC Bruno Grenet CASC 10.1145/3666000.3669671 http://arxiv.org/abs/2406.20072v1 2024-06-28T17:30:20Z

Cryptographic hash functions play a crucial role in ensuring data security, generating fixed-length hashes from variable-length inputs. The hash function SHA-256 is trusted for data security due to its resilience after over twenty years of intense scrutiny. One of its critical properties is collision resistance, meaning that it is infeasible to find two different inputs with the same hash. Currently, the best SHA-256 collision attacks use differential cryptanalysis to find collisions in simplified versions of SHA-256 that are reduced to have fewer steps, making it feasible to find collisions. In this paper, we use a satisfiability (SAT) solver as a tool to search for step-reduced SHA-256 collisions, and dynamically guide the solver with the aid of a computer algebra system (CAS) used to detect inconsistencies and deduce information that the solver would otherwise not detect on its own. Our hybrid SAT + CAS solver significantly outperformed a pure SAT approach, enabling us to find collisions in step-reduced SHA-256 with significantly more steps. Using SAT + CAS, we find a 38-step collision of SHA-256 with a modified initialization vector -- something first found by a highly sophisticated search tool of Mendel, Nad, and Schläffer. Conversely, a pure SAT approach could find collisions for no more than 28 steps. However, our work only uses the SAT solver CaDiCaL and its programmatic interface IPASIR-UP.

2024-06-28T17:30:20Z To appear in the 2024 Proceedings of the International Workshop on Satisfiability Checking and Symbolic Computation Nahiyan Alamgir Saeed Nejati Curtis Bright http://arxiv.org/abs/2406.20071v1 2024-06-28T17:30:20Z

The difficulty of factoring large integers into primes is the basis for cryptosystems such as RSA. Due to the widespread popularity of RSA, there have been many proposed attacks on the factorization problem such as side-channel attacks where some bits of the prime factors are available. When enough bits of the prime factors are known, two methods that are effective at solving the factorization problem are satisfiability (SAT) solvers and Coppersmith's method. The SAT approach reduces the factorization problem to a Boolean satisfiability problem, while Coppersmith's approach uses lattice basis reduction. Both methods have their advantages, but they also have their limitations: Coppersmith's method does not apply when the known bit positions are randomized, while SAT-based methods can take advantage of known bits in arbitrary locations, but have no knowledge of the algebraic structure exploited by Coppersmith's method. In this paper we describe a new hybrid SAT and computer algebra approach to efficiently solve random leaked-bit factorization problems. Specifically, Coppersmith's method is invoked by a SAT solver to determine whether a partial bit assignment can be extended to a complete assignment. Our hybrid implementation solves random leaked-bit factorization problems significantly faster than either a pure SAT or pure computer algebra approach.

2024-06-28T17:30:20Z To appear in the 2024 Proceedings of the International Symposium on Symbolic and Algebraic Computation Yameen Ajani Curtis Bright 10.1145/3666000.3669712 http://arxiv.org/abs/2402.05630v2 2024-06-28T08:31:46Z

We propose a non-commutative algorithm for multiplying 2x2 matrices using 7 coefficient products. This algorithm reaches simultaneously a better accuracy in practice compared to previously known such fast algorithms, and a time complexity bound with the best currently known leading term (obtained via alternate basis sparsification). To build this algorithm, we consider matrix and tensor norms bounds governing the stability and accuracy of numerical matrix multiplication. First, we reduce those bounds by minimizing a growth factor along the unique orbit of Strassen's 2x2-matrix multiplication tensor decomposition. Second, we develop heuristics for minimizing the number of operations required to realize a given bilinear formula, while further improving its accuracy. Third, we perform an alternate basis sparsification that improves on the time complexity constant and mostly preserves the overall accuracy.

2024-02-08T12:36:35Z Jean-Guillaume Dumas CASC Clément Pernet CASC Alexandre Sedoglavic CRIStAL http://arxiv.org/abs/2406.18964v1 2024-06-27T07:49:03Z

Satisfiability modulo nonlinear real arithmetic theory (SMT(NRA)) solving is essential to multiple applications, including program verification, program synthesis and software testing. In this context, recently model constructing satisfiability calculus (MCSAT) has been invented to directly search for models in the theory space. Although following papers discussed practical directions and updates on MCSAT, less attention has been paid to the detailed implementation. In this paper, we present an efficient implementation of dynamic variable orderings of MCSAT, called dnlsat. We show carefully designed data structures and promising mechanisms, such as branching heuristic, restart, and lemma management. Besides, we also give a theoretical study of potential influences brought by the dynamic variablr ordering. The experimental evaluation shows that dnlsat accelerates the solving speed and solves more satisfiable instances than other state-of-the-art SMT solvers. Demonstration Video: https://youtu.be/T2Z0gZQjnPw Code: https://github.com/yogurt-shadow/dnlsat/tree/master/code Benchmark https://zenodo.org/records/10607722/files/QF_NRA.tar.zst?download=1

2024-06-27T07:49:03Z Zhonghan Wang http://arxiv.org/abs/2406.18930v1 2024-06-27T06:53:28Z

The purpose of this book is to provide an overview of AI research, ranging from basic work to interfaces and applications, with as much emphasis on results as on current issues. It is aimed at an audience of master students and Ph.D. students, and can be of interest as well for researchers and engineers who want to know more about AI. The book is split into three volumes.

2024-06-27T06:53:28Z Marquis, Pierre; Papini, Odile; Prade, Henri. A Guided Tour of Artificial Intelligence Research, 1 / 3, Springer International Publishing, pp.487-518, 2020, Knowledge Representation, Reasoning and Learning, 978-3-030-06163-0 Florence Dupin de Saint-Cyr IRIT-ADRIA, UT3 Andreas Herzig IRIT-LILaC, CNRS Jérôme Lang LAMSADE, PSL, IRIT-ADRIA Pierre Marquis CRIL 10.1007/978-3-030-06164-7_15 http://arxiv.org/abs/2406.17762v1 2024-06-25T17:47:13Z

In this work, we prove over 3000 previously ATP-unproved Mizar/MPTP problems by using several ATP and AI methods, raising the number of ATP-solved Mizar problems from 75\% to above 80\%. First, we start to experiment with the cvc5 SMT solver which uses several instantiation-based heuristics that differ from the superposition-based systems, that were previously applied to Mizar,and add many new solutions. Then we use automated strategy invention to develop cvc5 strategies that largely improve cvc5's performance on the hard problems. In particular, the best invented strategy solves over 14\% more problems than the best previously available cvc5 strategy. We also show that different clausification methods have a high impact on such instantiation-based methods, again producing many new solutions. In total, the methods solve 3021 (21.3\%) of the 14163 previously unsolved hard Mizar problems. This is a new milestone over the Mizar large-theory benchmark and a large strengthening of the hammer methods for Mizar.

2024-06-25T17:47:13Z Jan Jakubův Mikoláš Janota Josef Urban http://arxiv.org/abs/2406.17610v1 2024-06-25T14:55:35Z

In the standard circuit model of quantum computation, the number and quality of the quantum gates composing the circuit influence the runtime and fidelity of the computation. The fidelity of the decomposition of quantum algorithms, represented as unitary matrices, to bounded depth quantum circuits depends strongly on the set of gates available for the decomposition routine. To investigate this dependence, we explore the design space of discrete quantum gate sets and present a software tool for comparative analysis of quantum processing units and control protocols based on their native gates. The evaluation is conditioned on a set of unitary transformations representing target use cases on the quantum processors. The cost function considers three key factors: (i) the statistical distribution of the decomposed circuits' depth, (ii) the statistical distribution of process fidelities for the approximate decomposition, and (iii) the relative novelty of a gate set compared to other gate sets in terms of the aforementioned properties. The developed software, YAQQ (Yet Another Quantum Quantizer), enables the discovery of an optimized set of quantum gates through this tunable joint cost function. To identify these gate sets, we use the novelty search algorithm, circuit decomposition techniques, and stochastic optimization to implement YAQQ within the Qiskit quantum simulator environment. YAQQ exploits reachability tradeoffs conceptually derived from quantum algorithmic information theory. Our results demonstrate the pragmatic application of identifying gate sets that are advantageous to popularly used quantum gate sets in representing quantum algorithms. Consequently, we demonstrate pragmatic use cases of YAQQ in comparing transversal logical gate sets in quantum error correction codes, designing optimal quantum instruction sets, and compiling to specific quantum processors.

2024-06-25T14:55:35Z Aritra Sarkar Akash Kundu Matthew Steinberg Sibasish Mishra Sebastiaan Fauquenot Tamal Acharya Jarosław A. Miszczak Sebastian Feld http://arxiv.org/abs/2406.17224v1 2024-06-25T02:18:15Z

The trade-off between expressiveness and interpretability remains a core challenge when building human-centric predictive models for classification and decision-making. While symbolic rules offer interpretability, they often lack expressiveness, whereas neural networks excel in performance but are known for being black boxes. In this paper, we show a combination of Large Language Models (LLMs) and symbolic programs can bridge this gap. In the proposed LLM-based Symbolic Programs (LSPs), the pretrained LLM with natural language prompts provides a massive set of interpretable modules that can transform raw input into natural language concepts. Symbolic programs then integrate these modules into an interpretable decision rule. To train LSPs, we develop a divide-and-conquer approach to incrementally build the program from scratch, where the learning process of each step is guided by LLMs. To evaluate the effectiveness of LSPs in extracting interpretable and accurate knowledge from data, we introduce IL-Bench, a collection of diverse tasks, including both synthetic and real-world scenarios across different modalities. Empirical results demonstrate LSP's superior performance compared to traditional neurosymbolic programs and vanilla automatic prompt tuning methods. Moreover, as the knowledge learned by LSP is a combination of natural language descriptions and symbolic rules, it is easily transferable to humans (interpretable), and other LLMs, and generalizes well to out-of-distribution samples.

2024-06-25T02:18:15Z Preliminary Version, Code at [this url](https://github.com/ruocwang/llm-symbolic-program) Ruochen Wang Si Si Felix Yu Dorothea Wiesmann Cho-Jui Hsieh Inderjit Dhillon http://arxiv.org/abs/2309.13920v3 2024-06-23T06:17:12Z

In emergency situations, the high-speed movement of an ambulance through the city streets can be hindered by vehicular traffic. This work presents a method for detecting emergency vehicle sirens in real time. To obtain the audio fingerprint of a Hi-Lo siren, DSP and signal symbolization techniques were applied, which were contrasted against an audio classifier based on a deep neural network, using the same 280 audios of ambient sounds and 52 Hi-Lo siren audios dataset. In both methods, some classification accuracy metrics were evaluated based on its confusion matrix, resulting in the DSP algorithm having a slightly lower accuracy than the DNN model, however, it offers a self-explanatory, adjustable, portable, high performance and lower energy and consumption that makes it a more viable lower cost ADAS implementation to identify Hi-Lo sirens in real time.

2023-09-25T07:40:19Z in Spanish language Revista Electro, Vol. 45, pp. 184-189, 2023 Alberto Pacheco-Gonzalez Raymundo Torres Raul Chacon Isidro Robledo http://arxiv.org/abs/2406.15782v1 2024-06-22T08:22:34Z

MaxSAT modulo theories (MaxSMT) is an important generalization of Satisfiability modulo theories (SMT) with various applications. In this paper, we focus on MaxSMT with the background theory of Linear Integer Arithmetic, denoted as MaxSMT(LIA). We design the first local search algorithm for MaxSMT(LIA) called PairLS, based on the following novel ideas. A novel operator called pairwise operator is proposed for integer variables. It extends the original local search operator by simultaneously operating on two variables, enriching the search space. Moreover, a compensation-based picking heuristic is proposed to determine and distinguish the pairwise operations. Experiments are conducted to evaluate our algorithm on massive benchmarks. The results show that our solver is competitive with state-of-the-art MaxSMT solvers. Furthermore, we also apply the pairwise operation to enhance the local search algorithm of SMT, which shows its extensibility.

2024-06-22T08:22:34Z Xiang He Bohan Li Mengyu Zhao Shaowei Cai http://arxiv.org/abs/2401.13343v2 2024-06-20T10:32:20Z

Symbolic Computation algorithms and their implementation in computer algebra systems often contain choices which do not affect the correctness of the output but can significantly impact the resources required: such choices can benefit from having them made separately for each problem via a machine learning model. This study reports lessons on such use of machine learning in symbolic computation, in particular on the importance of analysing datasets prior to machine learning and on the different machine learning paradigms that may be utilised. We present results for a particular case study, the selection of variable ordering for cylindrical algebraic decomposition, but expect that the lessons learned are applicable to other decisions in symbolic computation. We utilise an existing dataset of examples derived from applications which was found to be imbalanced with respect to the variable ordering decision. We introduce an augmentation technique for polynomial systems problems that allows us to balance and further augment the dataset, improving the machine learning results by 28\% and 38\% on average, respectively. We then demonstrate how the existing machine learning methodology used for the problem $-$ classification $-$ might be recast into the regression paradigm. While this does not have a radical change on the performance, it does widen the scope in which the methodology can be applied to make choices.

2024-01-24T10:12:43Z Mathematics in Computer Science, vol 18, article number 17. Springer, 2024 Tereso del Río Matthew England 10.1007/s11786-024-00591-0 http://arxiv.org/abs/2305.00702v3 2024-06-17T16:06:36Z

We are concerned with the arithmetic of solutions to ordinary or partial nonlinear differential equations which are algebraic in the indeterminates and their derivatives. We call these solutions D-algebraic functions, and their equations are algebraic (ordinary or partial) differential equations (ADEs). The general purpose is to find ADEs whose solutions contain specified rational expressions of solutions to given ADEs. For univariate D-algebraic functions, we show how to derive an ADE of smallest possible order. In the multivariate case, we introduce a general algorithm for these computations and derive conclusions on the order bound of the resulting algebraic PDE. Using our accompanying Maple software, we discuss applications in physics, statistics, and symbolic integration.

2023-05-01T08:01:34Z 28 pages. To appear in the Journal of Symbolic Computation Bertrand Teguia Tabuguia http://arxiv.org/abs/2406.11631v1 2024-06-17T15:13:36Z

There has been a growing need to devise processes that can create comprehensive datasets in the world of Computer Algebra, both for accurate benchmarking and for new intersections with machine learning technology. We present here a method to generate integrands that are guaranteed to be integrable, dubbed the LIOUVILLE method. It is based on Liouville's theorem and the Parallel Risch Algorithm for symbolic integration. We show that this data generation method retains the best qualities of previous data generation methods, while overcoming some of the issues built into that prior work. The LIOUVILLE generator is able to generate sufficiently complex and realistic integrands, and could be used for benchmarking or machine learning training tasks related to symbolic integration.

2024-06-17T15:13:36Z To appear in proc. CASC (2024) F. Boulier, C. Mou, T.M. Sadykov, and E.V. Vorozhtsov, eds. Computer Algebra in Scientific Computing (Proc. CASC '24), pp. 47-62. (Lecture Notes in Computer Science, vol 14938). Springer International, 2024 Rashid Barket Matthew England Jürgen Gerhard 10.1007/978-3-031-69070-9_4 http://arxiv.org/abs/2405.10578v3 2024-06-17T03:42:18Z

The classical theory of Kosambi-Cartan-Chern (KCC) developed in differential geometry provides a powerful method for analyzing the behaviors of dynamical systems. In the KCC theory, the properties of a dynamical system are described in terms of five geometrical invariants, of which the second corresponds to the so-called Jacobi stability of the system. Different from that of the Lyapunov stability that has been studied extensively in the literature, the analysis of the Jacobi stability has been investigated more recently using geometrical concepts and tools. It turns out that the existing work on the Jacobi stability analysis remains theoretical and the problem of algorithmic and symbolic treatment of Jacobi stability analysis has yet to be addressed. In this paper, we initiate our study on the problem for a class of ODE systems of arbitrary dimension and propose two algorithmic schemes using symbolic computation to check whether a nonlinear dynamical system may exhibit Jacobi stability. The first scheme, based on the construction of the complex root structure of a characteristic polynomial and on the method of quantifier elimination, is capable of detecting the existence of the Jacobi stability of the given dynamical system. The second algorithmic scheme exploits the method of semi-algebraic system solving and allows one to determine conditions on the parameters for a given dynamical system to have a prescribed number of Jacobi stable fixed points. Several examples are presented to demonstrate the effectiveness of the proposed algorithmic schemes.

2024-05-17T07:05:21Z Proceedings of the 2024 International Symposium on Symbolic and Algebraic Computation (ISSAC 2024) Bo Huang Dongming Wang Jing Yang 10.1145/3666000.3669689