https://arxiv.org/api/eyHbIMb1lBfjiTGmhsWmZMumGMo 2026-04-10T01:40:38Z 3074 285 15 http://arxiv.org/abs/2507.15449v1 2025-07-21T10:01:42Z

We consider the multivariate scheme Pesto, which was introduced by Calderini, Caminata, and Villa. In this scheme, the public polynomials are obtained by applying a CCZ transformation to a set of quadratic secret polynomials. As a consequence, the public key consists of polynomials of degree 4. In this work, we show that the public degree 4 polynomial system can be efficiently reduced to a system of quadratic polynomials. This seems to suggest that the CCZ transformation may not offer a significant increase in security, contrary to what was initially believed.

2025-07-21T10:01:42Z are welcome! Alessio Caminata Elisa Gorla Madison Mabe Martina Vigorito Irene Villa http://arxiv.org/abs/2502.12721v2 2025-07-21T08:13:58Z

The MinRank problem is a simple linear algebra problem: given matrices with coefficients in a field, find a non trivial linear combination of the matrices that has a small rank. There are several algebraic modeling of the problem. The main ones are: the Kipnis-Shamir modeling, the Minors modeling and the Support-Minors modeling. The Minors modeling has been studied by Faug{è}re et al. in 2010, where the authors provide an analysis of the complexity of computing a Gr{ö}bner basis of the modeling, through the computation of the exact Hilbert Series for a generic instance. For the Support-Minors modeling, the first terms of the Hilbert Series are given by Bardet et al. in 2020 based on an heuristic and experimental work. In this work, we provide a formula and a proof for the complete Hilbert Series of the Support Minors modeling for generic instances. This is done by adapting well known results on determinantal ideals to an ideal generated by a particular subset of the set of all minors of a matrix of variables. We then show that this ideal is generated by

2025-02-18T10:38:06Z Magali Bardet CA - LITIS Alban Gilard CA - LITIS http://arxiv.org/abs/2306.15375v2 2025-07-18T07:57:21Z

We present a new design for an algebraic simplification library structured around concepts from universal algebra: theories, models, homomorphisms, and universal properties of free algebras and free extensions of algebras. The library's dependently typed interface guarantees that both built-in and user-defined simplification modules are terminating, sound, and complete with respect to a well-specified class of equations. We have implemented the design in the Idris 2 and Agda dependently typed programming languages and shown that it supports modular extension to new theories, proof extraction and certification, goal extraction via reflection, and interactive development.

2023-06-27T10:47:22Z Proc. ACM Program. Lang. 9, ICFP, Article 237 (August 2025), 36 pages Guillaume Allais Edwin Brady Nathan Corbyn Ohad Kammar Jeremy Yallop 10.1145/3747506 http://arxiv.org/abs/2507.12366v1 2025-07-16T16:09:51Z

Neuro-symbolic artificial intelligence (neuro-symbolic AI) excels in logical analysis and reasoning. Hyperdimensional Computing (HDC), a promising brain-inspired computational model, is integral to neuro-symbolic AI. Various HDC models have been proposed to represent class-instance and class-class relations, but when representing the more complex class-subclass relation, where multiple objects associate different levels of classes and subclasses, they face challenges for factorization, a crucial task for neuro-symbolic AI systems. In this article, we propose FactorHD, a novel HDC model capable of representing and factorizing the complex class-subclass relation efficiently. FactorHD features a symbolic encoding method that embeds an extra memorization clause, preserving more information for multiple objects. In addition, it employs an efficient factorization algorithm that selectively eliminates redundant classes by identifying the memorization clause of the target class. Such model significantly enhances computing efficiency and accuracy in representing and factorizing multiple objects with class-subclass relation, overcoming limitations of existing HDC models such as "superposition catastrophe" and "the problem of 2". Evaluations show that FactorHD achieves approximately 5667x speedup at a representation size of 10^9 compared to existing HDC models. When integrated with the ResNet-18 neural network, FactorHD achieves 92.48% factorization accuracy on the Cifar-10 dataset.

2025-07-16T16:09:51Z 7 pages, 5 figures, 2 tables, to be published in the 62nd DAC (Design Automation Conference) proceedings Yifei Zhou Xuchu Huang Chenyu Ni Min Zhou Zheyu Yan Xunzhao Yin Cheng Zhuo http://arxiv.org/abs/2507.11987v1 2025-07-16T07:37:23Z

Neural certificates have emerged as a powerful tool in cyber-physical systems control, providing witnesses of correctness. These certificates, such as barrier functions, often learned alongside control policies, once verified, serve as mathematical proofs of system safety. However, traditional formal verification of their defining conditions typically faces scalability challenges due to exhaustive state-space exploration. To address this challenge, we propose a lightweight runtime monitoring framework that integrates real-time verification and does not require access to the underlying control policy. Our monitor observes the system during deployment and performs on-the-fly verification of the certificate over a lookahead region to ensure safety within a finite prediction horizon. We instantiate this framework for ReLU-based control barrier functions and demonstrate its practical effectiveness in a case study. Our approach enables timely detection of safety violations and incorrect certificates with minimal overhead, providing an effective but lightweight alternative to the static verification of the certificates.

2025-07-16T07:37:23Z Accepted at RV'25 Thomas A. Henzinger Konstantin Kueffner Emily Yu http://arxiv.org/abs/2507.10407v1 2025-07-14T15:53:58Z

I discuss a seemingly unlikely confluence of topics in algebra, numerical computation, and computer vision. The motivating problem is that of solving multiples instances of a parametric family of systems of algebraic (polynomial or rational function) equations. No doubt already of interest to ISSAC attendees, this problem arises in the context of robust model-fitting paradigms currently utilized by the computer vision community (namely "Random Sampling and Consensus", aka "RanSaC".) This talk will give an overview of work in the last 5+ years that aspires to measure the intrinsic difficulty of solving such parametric systems, and makes strides towards practical solutions.

2025-07-14T15:53:58Z abstract accompanying invited tutorial at ISSAC 2025; 10 pages w/ references Timothy Duff http://arxiv.org/abs/2506.18392v3 2025-07-14T08:45:47Z

The Peterson hit problem in algebraic topology is to explicitly determine the dimension of the quotient space $Q\mathcal P_k = \mathbb F_2\otimes_{\mathcal A}\mathcal P_k$ in positive degrees, where $\mathcal{P}_k$ denotes the polynomial algebra in $k$ variables over the field $\mathbb{F}_2$, considered as an unstable module over the Steenrod algebra $\mathcal{A}$. Current approaches to this problem still rely heavily on manual computations, which are highly prone to errors due to the intricate nature of the underlying calculations. To date, no efficient algorithm implemented in any computer algebra system has been made publicly available to tackle this problem in a systematic manner. Motivated by the above, in this work, which is considered as Part I of our project, we first establish a criterion based entirely on linear algebra for determining whether a given homogeneous polynomial is "hit". Accordingly, we describe the dimensions of the hit spaces. This leads to a practical and reliable computational method for determining the dimension of $Q\mathcal{P}_k$ for arbitrary $k$ and any positive degrees, with the support of a computer algebra system. We then give a concrete implementation of the obtained results as novel algorithms in \textsc{SageMath}. As an application, our algorithm demonstrates that the manually computed result presented in the recent work of Sum and Tai [15] for the dimension of $Q\mathcal{P}_5$ in degree $2^{6}$ is not correct. Furthermore, our algorithm determines that $\dim(Q\mathcal{P}_5)_{2^{7}} = 1985,$ which falls within the range $1984 \leq \dim(Q\mathcal{P}_5)_{2^{7}} \leq 1990$ as estimated in [15].

2025-06-23T08:27:44Z 47 pages. This version includes updated references and improved algorithms for enhanced execution efficiency. We welcome constructive comments and feedback on theoretical and practical aspects. We also welcome international collaboration in developing and extending our algorithms, particularly through implementation on the SageMath computer algebra system Dang Vo Phuc http://arxiv.org/abs/2507.00557v2 2025-07-11T15:40:25Z

In this paper, we propose a hybrid framework for Satisfiability Modulo the Theory of Nonlinear Real Arithmetic (SMT-NRA for short). First, we introduce a two-dimensional cell-jump move, called \emph{$2d$-cell-jump}, generalizing the key operation, cell-jump, of the local search method for SMT-NRA. Then, we propose an extended local search framework, named \emph{$2d$-LS} (following the local search framework, LS, for SMT-NRA), integrating the model constructing satisfiability calculus (MCSAT) framework to improve search efficiency. To further improve the efficiency of MCSAT, we implement a recently proposed technique called \emph{sample-cell projection operator} for MCSAT, which is well suited for CDCL-style search in the real domain and helps guide the search away from conflicting states. Finally, we present a hybrid framework for SMT-NRA integrating MCSAT, $2d$-LS and OpenCAD, to improve search efficiency through information exchange. The experimental results demonstrate improvements in local search performance, highlighting the effectiveness of the proposed methods.

2025-07-01T08:27:29Z Tianyi Ding Haokun Li Xinpeng Ni Bican Xia Tianqi Zhao http://arxiv.org/abs/2507.08138v1 2025-07-10T19:56:14Z

Ratios of D-finite sequences and their limits -- known as Apéry limits -- have driven much of the work on irrationality proofs since Apéry's 1979 breakthrough proof of the irrationality of $ζ(3)$. We extend ratios of D-finite sequences to a high-dimensional setting by introducing the Conservative Matrix Field (CMF). We demonstrate how classical Apéry limits are included by this object as special cases. A useful construction of CMFs is provided, drawing a connection to gauge transformations and to representations of shift operators in finite dimensional modules of Ore algebras. Finally, numerical experiments on these objects reveal surprising arithmetic and dynamical phenomena, which are formulated into conjectures. If established, these conjectures would extend Poincaré--Perron asymptotics to higher dimensions, potentially opening the door to optimization-based searches for new irrationality proofs.

2025-07-10T19:56:14Z 26 pages, 5 figures Shachar Weinbaum Elyasheev Leibtag Rotem Kalisch Michael Shalyt Ido Kaminer http://arxiv.org/abs/2504.21058v2 2025-07-10T08:06:57Z

Let $m,n,d > 1$ be integers such that $n=md$. In this paper, we present an efficient change of level algorithm that takes as input $(B, \mathscr{M}, Θ_\mathscr{M})$ a marked abelian variety of level $m$ over the base field $k$ of odd characteristic and returns $(B, \mathscr{M}^d, Θ_{\mathscr{M}^d})$ a marked abelian variety of level $n$ at the expense of $O(m^g d^{2g})$ operations in $k$. A similar algorithm allows to compute $d$-isogenies: from $(B, \mathscr{M}, Θ_\mathscr{M})$ a marked abelian variety of level $m$, $K\subset B[d]$ isotropic for the Weil pairing isomorphic to $(\mathbb{Z}/d\mathbb{Z})^g$ defined over $k$, the isogeny algorithm returns $(A, \mathscr{L}, Θ_\mathscr{L})$ of level $m$ such that $A=B/K$ with $O(m^g d^g)$ operations in $k$. Our algorithms extend previous known results in the case that $d \wedge m=1$ and $d$ odd. In this paper, we lift theses restrictions. We use the same general approach as in the literature in conjunction with the notion of symmetric compatible that we introduce, study and link to previous results of Mumford. For practical computation, most of the time $m$ is $2$ or $4$ so that our algorithms allows in particular to compute $2^e$-isogenies which are important for the theory of theta functions but also for computational applications such as isogeny based cryptography.

2025-04-29T08:02:59Z Antoine Dequay IRMAR David Lubicz DGA.MI, IRMAR http://arxiv.org/abs/2507.06681v1 2025-07-09T09:18:51Z

We describe a complete algorithm to compute millions of coefficients of classical modular forms in a few seconds. We also review operations on Euler products and illustrate our methods with a computation of triple product L-function of large conductor.

2025-07-09T09:18:51Z Pascal Molin IMJ-PRG http://arxiv.org/abs/2307.05102v3 2025-07-08T18:06:09Z

In this paper, we give an algorithm for finding general rational solutions of a given first-order ODE with parametric coefficients that occur rationally. We present an analysis, complete modulo Hilbert's irreducibility problem, of the existence of rational solutions of the differential equation, with parametric coefficients, when the parameters are specialized.

2023-07-11T08:24:25Z Bulletin des Sciences Mathématiques, Volume 205, 2025, paper 103694 Sebastian Falkensteiner Rafael Sendra 10.1016/j.bulsci.2025.103694 http://arxiv.org/abs/2505.07685v2 2025-07-08T15:12:18Z

We provide an algorithm for computing a basis of homology of fibre products of elliptic surfaces over $\mathbb P^1$, along with the corresponding intersection product and period matrices. We use this data to investigate the Gamma conjecture for Calabi-Yau threefolds obtained in this manner. We find a formula that works for all operators of a list of 105 fibre products, as well as for fourth order operators of the Calabi-Yau database. This algorithm comes with a SageMath implementation.

2025-05-12T15:48:24Z 39 pages, 4 figures Eric Pichon-Pharabod http://arxiv.org/abs/2507.05017v1 2025-07-07T14:00:05Z

The volume and diversity of digital information have led to a growing reliance on Machine Learning techniques, such as Natural Language Processing, for interpreting and accessing appropriate data. While vector and graph embeddings represent data for similarity tasks, current state-of-the-art pipelines lack guaranteed explainability, failing to determine similarity for given full texts accurately. These considerations can also be applied to classifiers exploiting generative language models with logical prompts, which fail to correctly distinguish between logical implication, indifference, and inconsistency, despite being explicitly trained to recognise the first two classes. We present a novel pipeline designed for hybrid explainability to address this. Our methodology combines graphs and logic to produce First-Order Logic representations, creating machine- and human-readable representations through Montague Grammar. Preliminary results indicate the effectiveness of this approach in accurately capturing full text similarity. To the best of our knowledge, this is the first approach to differentiate between implication, inconsistency, and indifference for text classification tasks. To address the limitations of existing approaches, we use three self-contained datasets annotated for the former classification task to determine the suitability of these approaches in capturing sentence structure equivalence, logical connectives, and spatiotemporal reasoning. We also use these data to compare the proposed method with language models pre-trained for detecting sentence entailment. The results show that the proposed method outperforms state-of-the-art models, indicating that natural language understanding cannot be easily generalised by training over extensive document corpora. This work offers a step toward more transparent and reliable Information Retrieval from extensive textual data.

2025-07-07T14:00:05Z Oliver Robert Fox Giacomo Bergami Graham Morgan http://arxiv.org/abs/2502.06055v2 2025-07-07T03:07:45Z

The Ramsey problem $R(3, k)$ seeks to determine the smallest value of $n$ such that any red/blue edge coloring of the complete graph on $n$ vertices must either contain a blue triangle (3-clique) or a red clique of size $k$. Despite its significance, many previous computational results for the Ramsey $R(3, k)$ problem such as $R(3, 8)$ and $R(3, 9)$ lack formal verification. To address this issue, we use the software MathCheck to generate certificates for Ramsey problems $R(3, 8)$ and $R(3, 9)$ (and symmetrically $R(8, 3)$ and $R(9, 3)$) by integrating a Boolean satisfiability (SAT) solver with a computer algebra system (CAS). Our SAT+CAS approach significantly outperforms traditional SAT-only methods, demonstrating an improvement of several orders of magnitude in runtime. For instance, our SAT+CAS approach solves $R(3, 8)$ (resp., $R(8, 3)$) sequentially in 59 hours (resp., in 11 hours), while a SAT-only approach using state-of-the-art CaDiCaL solver times out after 7 days. Additionally, in order to be able to scale to harder Ramsey problems $R(3, 9)$ and $R(9, 3)$ we further optimized our SAT+CAS tool using a parallelized cube-and-conquer approach. Our results provide the first independently verifiable certificates for these Ramsey numbers, ensuring both correctness and completeness of the exhaustive search process of our SAT+CAS tool.

2025-02-09T22:24:37Z To appear at IJCAI 2025 Zhengyu Li Conor Duggan Curtis Bright Vijay Ganesh 10.24963/ijcai.2025/292