https://arxiv.org/api/iE6peqgUqfGT+Ag7FkKWIxCuPxI 2026-04-10T00:13:50Z 3074 270 15 http://arxiv.org/abs/2508.04590v1 2025-08-06T16:09:11Z

Physics-Informed Neural Network (PINN) is a deep learning framework that integrates the governing equations underlying data into a loss function. In this study, we consider the problem of estimating state variables and parameters in epidemiological models governed by ordinary differential equations using PINNs. In practice, not all trajectory data corresponding to the population described by models can be measured. Learning PINNs to estimate the unmeasured state variables and epidemiological parameters using partial measurements is challenging. Accordingly, we introduce the concept of algebraic observability of the state variables. Specifically, we propose augmenting the unmeasured data based on algebraic observability analysis. The validity of the proposed method is demonstrated through numerical experiments under three scenarios in the context of epidemiological modelling. Specifically, given noisy and partial measurements, the accuracy of unmeasured states and parameter estimation of the proposed method is shown to be higher than that of the conventional methods. The proposed method is also shown to be effective in practical scenarios, such as when the data corresponding to certain variables cannot be reconstructed from the measurements.

2025-08-06T16:09:11Z Mizuka Komatsu http://arxiv.org/abs/2508.04081v1 2025-08-06T04:51:07Z

Initiated by Mulmuley, Vazirani, and Vazirani (1987), many algebraic algorithms have been developed for matching and related problems. In this paper, we review basic facts and discuss possible improvements with the aid of fast computation of the characteristic polynomial of a matrix. In particular, we show that the so-called exact matching problem can be solved with high probability in asymptotically the same time order as matrix multiplication. We also discuss its extension to the linear matroid parity problem.

2025-08-06T04:51:07Z 12 pages Ryotaro Sato Yutaro Yamaguchi http://arxiv.org/abs/2508.03366v1 2025-08-05T12:14:32Z

General logical reasoning, defined as the ability to reason deductively on domain-agnostic tasks, continues to be a challenge for large language models (LLMs). Current LLMs fail to reason deterministically and are not interpretable. As such, there has been a recent surge in interest in neurosymbolic AI, which attempts to incorporate logic into neural networks. We first identify two main neurosymbolic approaches to improving logical reasoning: (i) the integrative approach comprising models where symbolic reasoning is contained within the neural network, and (ii) the hybrid approach comprising models where a symbolic solver, separate from the neural network, performs symbolic reasoning. Both contain AI systems with promising results on domain-specific logical reasoning benchmarks. However, their performance on domain-agnostic benchmarks is understudied. To the best of our knowledge, there has not been a comparison of the contrasting approaches that answers the following question: Which approach is more promising for developing general logical reasoning? To analyze their potential, the following best-in-class domain-agnostic models are introduced: Logic Neural Network (LNN), which uses the integrative approach, and LLM-Symbolic Solver (LLM-SS), which uses the hybrid approach. Using both models as case studies and representatives of each approach, our analysis demonstrates that the hybrid approach is more promising for developing general logical reasoning because (i) its reasoning chain is more interpretable, and (ii) it retains the capabilities and advantages of existing LLMs. To support future works using the hybrid approach, we propose a generalizable framework based on LLM-SS that is modular by design, model-agnostic, domain-agnostic, and requires little to no human input.

2025-08-05T12:14:32Z Accepted to NeSy 2025 Michael K. Chen http://arxiv.org/abs/2508.02918v1 2025-08-04T21:48:47Z

We study central configurations when the set of positions is symmetric. We use a theorem from representation theory of finite groups to explore the symmetry properties of equations for central configurations. This approach simplifies equations for central configurations by considering arbitrary numbers of bodies, symmetry groups, and dimensions. We discuss how to use this theorem to obtain a more refined decomposition of the equations than that given before. The decomposition presented here uses the symmetry-adapted basis method. As an application, we give a complete description of the existence and which masses are possible for central configurations of two nested regular tetrahedrons, two nested regular octahedrons, and two nested regular cubes. To do this, we employ some methods of rational parameterizations and isolation of zeros of multivariate polynomials. The decomposition obtained allows symbolic calculations to be used to study the expressions. This way, we summarize previous discussions and extend them by completing the analysis on the cube case, for both the inverse and direct problems.

2025-08-04T21:48:47Z Marcelo P. Santos Federal Rural University of Pernambuco Leon D. da Silva Federal Rural University of Pernambuco http://arxiv.org/abs/2508.00153v2 2025-08-04T03:57:25Z

Green computing represents a critical pathway to decarbonize the digital economy while maintaining technological progress. This article examines how sustainable IT strategies including energy-efficient hardware, AI-optimized data centres, and circular e-waste systems can transform computing into a net carbon sink. Through analysis of industry best practices and emerging technologies like quantum computing and biodegradable electronics, we demonstrate achievable reductions of 40-60% in energy consumption without compromising performance. The study highlights three key findings: (1) current solutions already deliver both environmental and economic benefits, with typical payback periods of 3-5 years; (2) systemic barriers including cost premiums and policy fragmentation require coordinated action; and (3) next-generation innovations promise order-of-magnitude improvements in efficiency. We present a practical framework for stakeholders from corporations adopting renewable-powered cloud services to individuals extending device lifespans to accelerate the transition. The research underscores computing's unique potential as a climate solution through its rapid innovation cycles and measurable impacts, concluding that strategic investments in green IT today can yield disproportionate sustainability dividends across all sectors tomorrow. This work provides both a compelling case for urgent action and a clear roadmap to realize computing's potential as a powerful carbon destruction tool in the climate crisis era.

2025-07-31T20:28:29Z 26 Pages, 6 Tables Sayed Mahbub Hasan Amiri Prasun Goswami Md. Mainul Islam Mohammad Shakhawat Hossen Marzana Mithila Naznin Akter http://arxiv.org/abs/2201.07127v3 2025-08-03T03:48:42Z

Let $(u(n))_{n\in\mathbb{N}}$ be an arithmetic progression of natural integers in base $b\in\mathbb{N}\setminus \{0,1\}$. We consider the following sequences: $s(n)=\overline{u(0)u(1)\cdots u(n) }^b$ formed by concatenating the first $n+1$ terms of $(u(n))_{n\in\mathbb{N}}$ in base $b$ from the right; $s_g(n) = \overline{u(n)u(n-1)\cdots u(0)}^b$; and $(s_*(n))_{n\in\mathbb{N}}$, given by $s_*(0)=u(0)$, $s_*(n)=\overline{s(n)s_g(n-1)}^b, n\geq 1$. We construct explicit formulae for these sequences and use basic concepts of linear difference operators to prove they are not P-recursive (holonomic). We also present an alternative proof that follows directly from their definitions. We implemented $(s(n))_{n\in\mathbb{N}}$ and $(s_g(n))_{n\in\mathbb{N}}$ in the decimal base when $(u(n))_{n\in\mathbb{N}}=\mathbb{N}\setminus \{0\}$.

2022-01-14T07:53:47Z Definitions 1, 2, and 3 are new. More details about "holonomicity per range'' have been added Florian Luca Bertrand Teguia Tabuguia http://arxiv.org/abs/2508.00512v1 2025-08-01T10:45:24Z

The cylindrical algebraic decomposition (CAD) is the only complete method used in practice for solving problems like quantifier elimination or SMT solving related to real algebra, despite its doubly exponential complexity. Recent exploration-guided algorithms like NLSAT, NuCAD, and CAlC rely on CAD technology but reduce the computational effort heuristically. Single cell construction is a paradigm that is used in each of these algorithms. The central property on which the CAD algorithm is based is called delineability. Recently, we introduced a weaker notion called projective delineability which can require fewer computations to guarantee, but needs to be applied carefully. This paper adapts the single cell construction for exploiting projective delineability and reports on experimental results.

2025-08-01T10:45:24Z Jasper Nalbach Lucas Michel Erika Ábrahám Christopher W. Brown James H. Davenport Matthew England Pierre Mathonet Naïm Zénaïdi http://arxiv.org/abs/2508.00505v1 2025-08-01T10:33:03Z

The Cylindrical Algebraic Decomposition (CAD) method is currently the only complete algorithm used in practice for solving real-algebraic problems. To ameliorate its doubly-exponential complexity, different exploration-guided adaptations try to avoid some of the computations. The first such adaptation named NLSAT was followed by Non-uniform CAD (NuCAD) and the Cylindrical Algebraic Covering (CAlC). Both NLSAT and CAlC have been developed and implemented in SMT solvers for satisfiability checking, and CAlC was recently also adapted for quantifier elimination. However, NuCAD was designed for quantifier elimination only, and no complete implementation existed before this work. In this paper, we present a novel variant of NuCAD for both real quantifier elimination and SMT solving, provide an implementation, and evaluate the method by experimentally comparing it to CAlC.

2025-08-01T10:33:03Z Jasper Nalbach Erika Ábrahám http://arxiv.org/abs/2507.23557v1 2025-07-31T13:46:17Z

We consider a family of infinite sums of products of Catalan numbers, indexed by trees. We show that these sums are polynomials in $1/π$ with rational coefficients; the proof is effective and provides an algorithm to explicitly compute these sums. Along the way we introduce parametric liftings of our sums, and show that they are polynomials in the complete elliptic integrals of the first and second kind. Moreover, the degrees of these polynomials are at most half of the number of vertices of the tree. The computation of these tree-indexed sums is motivated by the study of large meandric systems, which are non-crossing configurations of loops in the plane.

2025-07-31T13:46:17Z 62 pages, 8 figures Alin Bostan Valentin Féray Paul Thévenin http://arxiv.org/abs/2507.22255v1 2025-07-29T22:09:35Z

The pursuit of general intelligence has traditionally centered on external objectives: an agent's control over its environments or mastery of specific tasks. This external focus, however, can produce specialized agents that lack adaptability. We propose representational empowerment, a new perspective towards a truly agent-centric learning paradigm by moving the locus of control inward. This objective measures an agent's ability to controllably maintain and diversify its own knowledge structures. We posit that the capacity -- to shape one's own understanding -- is an element for achieving better ``preparedness'' distinct from direct environmental influence. Focusing on internal representations as the main substrate for computing empowerment offers a new lens through which to design adaptable intelligent systems.

2025-07-29T22:09:35Z RLC Finding the Frame Workshop 2025 Hanqi Zhou Fryderyk Mantiuk David G. Nagy Charley M. Wu http://arxiv.org/abs/2507.20889v1 2025-07-28T14:40:07Z

In 1978, Frost and Storey asserted that a bivariate polynomial matrix is equivalent to its Smith normal form if and only if the reduced minors of all orders generate the unit ideal. In this paper, we first demonstrate by constructing an example that for any given positive integer s with s >= 2, there exists a square bivariate polynomial matrix M with the degree of det(M) in y equal to s, for which the condition that reduced minors of all orders generate the unit ideal is not a sufficient condition for M to be equivalent to its Smith normal form. Subsequently, we prove that for any square bivariate polynomial matrix M where the degree of det(M) in y is at most 1, Frost and Storey's assertion holds. Using the Quillen-Suslin theorem, we further extend our consideration of M to rank-deficient and non-square cases.

2025-07-28T14:40:07Z 16 pages Dong Lu Dingkang Wang Fanghui Xiao Xiaopeng Zheng http://arxiv.org/abs/2507.20491v1 2025-07-28T03:00:35Z

Recent advances in large language models (LLMs) have significantly enhanced question-answering (QA) capabilities, particularly in open-domain contexts. However, in closed-domain scenarios such as education, healthcare, and law, users demand not only accurate answers but also transparent reasoning and explainable decision-making processes. While neural-symbolic (NeSy) frameworks have emerged as a promising solution, leveraging LLMs for natural language understanding and symbolic systems for formal reasoning, existing approaches often rely on large-scale models and exhibit inefficiencies in translating natural language into formal logic representations. To address these limitations, we introduce Text-JEPA (Text-based Joint-Embedding Predictive Architecture), a lightweight yet effective framework for converting natural language into first-order logic (NL2FOL). Drawing inspiration from dual-system cognitive theory, Text-JEPA emulates System 1 by efficiently generating logic representations, while the Z3 solver operates as System 2, enabling robust logical inference. To rigorously evaluate the NL2FOL-to-reasoning pipeline, we propose a comprehensive evaluation framework comprising three custom metrics: conversion score, reasoning score, and Spearman rho score, which collectively capture the quality of logical translation and its downstream impact on reasoning accuracy. Empirical results on domain-specific datasets demonstrate that Text-JEPA achieves competitive performance with significantly lower computational overhead compared to larger LLM-based systems. Our findings highlight the potential of structured, interpretable reasoning frameworks for building efficient and explainable QA systems in specialized domains.

2025-07-28T03:00:35Z 8 pages, 3 figures. Accepted at the International Joint Conference on Neural Networks (IJCNN) 2025, Workshop on Trustworthiness and Reliability in Neuro-Symbolic AI. https://2025.ijcnn.org Tuan Bui Trong Le Phat Thai Sang Nguyen Minh Hua Ngan Pham Thang Bui Tho Quan http://arxiv.org/abs/2507.20267v1 2025-07-27T13:27:20Z

Proof certificates can be used to validate the correctness of algebraic derivations. However, in practice, we frequently observed that the exact same proof steps are repeated for different sets of variables, which leads to unnecessarily large proofs. To overcome this issue we extend the existing Practical Algebraic Calculus with linear combinations (LPAC) with two new proof rules that allow us to capture and reuse parts of the proof to derive a more condensed proof certificate. We integrate these rules into the proof checker Pacheck 2.0. Our experimental results demonstrate that the proposed extension helps to reduce both proof size and verification time.

2025-07-27T13:27:20Z 6 pages; 2 figures; 1 table Daniela Kaufmann Clemens Hofstadler http://arxiv.org/abs/2501.03837v2 2025-07-27T04:03:09Z

We adapt the theory of normal and special polynomials from symbolic integration to the summation setting, and then built up a general framework embracing both the usual shift case and the $q$-shift case. In the context of this general framework, we develop a unified reduction algorithm, and subsequently a creative telescoping algorithm, applicable to both hypergeometric terms and their $q$-analogues. Our algorithms allow to split up the usual shift case and the $q$-shift case only when it is really necessary, and thus instantly reveal the intrinsic differences between these two cases. Computational experiments are also provided.

2025-01-07T14:47:02Z Shaoshi Chen Hao Du Yiman Gao Hui Huang Ziming Li 10.1007/s11139-025-01164-w http://arxiv.org/abs/2507.19010v1 2025-07-25T07:07:28Z

We present an experimental, verified clause processor ctv-cp that fits into the framework used at Arm for formal verification of arithmetic hardware designs. This largely automates the ACL2 proof development effort for integer multiplier modules that exist in designs ranging from floating-point division to matrix multiplication.

2025-07-25T07:07:28Z In Proceedings ACL2 2025, arXiv:2507.18567 EPTCS 423, 2025, pp. 51-55 Mayank Manjrekar Arm Inc. 10.4204/EPTCS.423.5