https://arxiv.org/api/e8v1w/WeAHLRt4m3ysX1iHgvlNA 2026-04-09T20:08:28Z 3074 225 15 http://arxiv.org/abs/2509.25662v1 2025-09-30T01:58:59Z

Artificial intelligence (AI) systems in high-stakes domains raise concerns about proxy discrimination, unfairness, and explainability. Existing audits often fail to reveal why unfairness arises, particularly when rooted in structural bias. We propose a novel framework using formal abductive explanations to explain proxy discrimination in individual AI decisions. Leveraging background knowledge, our method identifies which features act as unjustified proxies for protected attributes, revealing hidden structural biases. Central to our approach is the concept of aptitude, a task-relevant property independent of group membership, with a mapping function aligning individuals of equivalent aptitude across groups to assess fairness substantively. As a proof of concept, we showcase the framework with examples taken from the German credit dataset, demonstrating its applicability in real-world cases.

2025-09-30T01:58:59Z Accepted at AJCAI 2025 AI 2025: Advances in Artificial Intelligence Belona Sonna Alban Grastien 10.1007/978-981-95-4969-6_20 http://arxiv.org/abs/2509.25114v1 2025-09-29T17:41:16Z

Ensuring software correctness remains a fundamental challenge in formal program verification. One promising approach relies on finding polynomial invariants for loops. Polynomial invariants are properties of a program loop that hold before and after each iteration. Generating such invariants is a crucial task in loop analysis, but it is undecidable in the general case. Recently, an alternative approach to this problem has emerged, focusing on synthesizing loops from invariants. However, existing methods only synthesize affine loops without guard conditions from polynomial invariants. In this paper, we address a more general problem, allowing loops to have polynomial update maps with a given structure, inequations in the guard condition, and polynomial invariants of arbitrary form. We use algebraic geometry tools to design and implement an algorithm that computes a finite set of polynomial equations whose solutions correspond to all nondeterministic branching loops satisfying the given invariants. Furthermore, we introduce a new class of invariants for which we present a significantly more efficient algorithm. In other words, we reduce the problem of synthesizing loops to find solutions of multivariate polynomial systems with rational entries. This final step is handled in our software using an SMT solver.

2025-09-29T17:41:16Z Erdenebayar Bayarmagnai Fatemeh Mohammadi Rémi Prébet http://arxiv.org/abs/2406.02122v4 2025-09-26T20:04:14Z

The Model-Constructing Satisfiability Calculus (MCSAT) framework has been applied to SMT problems over various arithmetic theories. NLSAT, an implementation using cylindrical algebraic decomposition (CAD) for explanation, is especially competitive for nonlinear real arithmetic (NRA) constraints. However, current Conflict-Driven Clause Learning (CDCL)-style algorithms only consider literal information when making decisions, and thus ignore the influence of clauses on arithmetic variables. This limitation may lead NLSAT to encounter unnecessary conflicts due to suboptimal literal choices. To address this issue, we analyze conflicts caused by literal decisions and incorporate clause-level information that directly affects arithmetic variables. We propose two main algorithmic improvements: a clause-level feasible-set-based look-ahead mechanism and an arithmetic propagation-based branching heuristic. We implement our solver, named clauseSMT, based on a dynamic variable ordering framework. Experiments indicate that clauseSMT is competitive on nonlinear real arithmetic problems compared with existing SMT solvers (CVC5, Z3, YICES2), and it outperforms all of them on satisfiable instances of SMT(QF_NRA) in SMT-LIB. We also evaluate the effectiveness of our proposed methods.

2024-06-04T09:05:09Z Final version of ASE'2025 Zhonghan Wang http://arxiv.org/abs/2310.03598v3 2025-09-26T13:20:15Z

Symbolic Execution is a formal method that can be used to verify the behavior of computer programs and detect software vulnerabilities. Compared to other testing methods such as fuzzing, Symbolic Execution has the advantage of providing formal guarantees about the program. However, despite advances in performance in recent years, Symbolic Execution is too slow to be applied to real-world software. This is primarily caused by the \emph{path explosion problem} as well as by the computational complexity of SMT solving. In this paper, we present a divide-and-conquer approach for symbolic execution by executing individual slices and later combining the side effects. This way, the overall problem size is kept small, reducing the impact of computational complexity on large problems.

2023-10-05T15:21:10Z Christopher Scherb Luc Bryan Heitz Hermann Grieder Olivier Mattmann http://arxiv.org/abs/2509.20534v2 2025-09-26T01:51:02Z

Symbolic computation systems suffer from memory inefficiencies due to redundant storage of structurally identical subexpressions, commonly known as expression swell, which degrades performance in both classical computer algebra and emerging AI-driven mathematical reasoning tools. In this paper, we present the first integration of hash consing into JuliaSymbolics, a high-performance symbolic toolkit in Julia, by employing a global weak-reference hash table that canonicalizes expressions and eliminates duplication. This approach reduces memory consumption and accelerates key operations such as differentiation, simplification, and code generation, while seamlessly integrating with Julia's metaprogramming and just-in-time compilation infrastructure. Benchmark evaluations across different computational domains reveal substantial improvements: symbolic computations are accelerated by up to 3.2 times, memory usage is reduced by up to 2 times, code generation is up to 5 times faster, function compilation up to 10 times faster, and numerical evaluation up to 100 times faster for larger models. While certain workloads with fewer duplicate unknown-variable expressions show more modest gains or even slight overhead in initial computation stages, downstream processing consistently benefits significantly. These findings underscore the importance of hash consing in scaling symbolic computation and pave the way for future work integrating hash consing with e-graphs for enhanced equivalence-aware expression sharing in AI-driven pipelines.

2025-09-24T20:06:56Z Bowen Zhu Aayush Sabharwal Songchen Tan Yingbo Ma Alan Edelman Christopher Rackauckas http://arxiv.org/abs/2509.20932v1 2025-09-25T09:17:27Z

This paper uses category theory to develop an entirely new approach to approximate game theory. Game theory is the study of how different agents within a multi-agent system take decisions. At its core, game theory asks what an optimal decision is in a given scenario. Thus approximate game theory asks what is an approximately optimal decision in a given scenario. This is important in practice as -- just like in much of computing -- exact answers maybe too difficult to compute or even impossible to compute given inherent uncertainty in input. We consider first "Selection Functions" which are functions and develop a simple yet robust model of approximate equilibria. We develop the algebraic properties of approximation wrt selection functions and also relate approximation to the compositional structure of selection functions. We then repeat this process successfully for Open Games -- a more advanced model of game theory.

2025-09-25T09:17:27Z In Proceedings ACT 2024, arXiv:2509.18357 EPTCS 429, 2025, pp. 190-202 Neil Ghani MSP Group, University of Strathclyde 10.4204/EPTCS.429.10 http://arxiv.org/abs/2509.19479v1 2025-09-23T18:39:15Z

Despite the prevalence of symmetry in scientific linear systems, these structural properties are often underutilized by standard computational software. This paper introduces PySymmetry, an open-source Sage/Python framework that implements classical representation theory to simplify G-equivariant linear systems. PySymmetry uses projection operators to generate symmetry-adapted bases, transforming equivariant operators into a more efficient block-diagonal form. Its functionalities include defining and reducing representations, calculating multiplicities, and obtaining the explicit block structure. We demonstrate PySymmetry's versatility through three case studies: a chemistry application, a numerical benchmark on the non-Hermitian Schrödinger equation that achieved a performance increase of over 17x compared to standard methods, and a symbolic investigation that enabled the first complete analytical classification of a challenging problem in celestial mechanics. Designed for seamless integration with libraries like NumPy and SciPy, PySymmetry offers a powerful, user-friendly tool for exploring symmetries in theoretical and applied contexts. ```

2025-09-23T18:39:15Z Leon D. da Silva Marcelo P. Santos http://arxiv.org/abs/2404.10839v2 2025-09-22T18:48:27Z

We design polynomial size, constant depth (namely, $\mathsf{AC}^0$) arithmetic formulae for the greatest common divisor (GCD) of two polynomials, as well as the related problems of the discriminant, resultant, Bézout coefficients, squarefree decomposition, and the inversion of structured matrices like Sylvester and Bézout matrices. Our GCD algorithm extends to any number of polynomials. Previously, the best known arithmetic formulae for these problems required super-polynomial size, regardless of depth. These results are based on new algorithmic techniques to compute various symmetric functions in the roots of polynomials, as well as manipulate the multiplicities of these roots, without having access to them. These techniques allow $\mathsf{AC}^0$ computation of a large class of linear and polynomial algebra problems, which include the above as special cases. We extend these techniques to problems whose inputs are multivariate polynomials, which are represented by $\mathsf{AC}^0$ arithmetic circuits. Here too we solve problems such as computing the GCD and squarefree decomposition in $\mathsf{AC}^0$.

2024-04-16T18:25:34Z v2: Incorporates feedback from referees Robert Andrews Avi Wigderson 10.1109/FOCS61266.2024.00138 10.1137/24M1708085 http://arxiv.org/abs/2509.03953v2 2025-09-22T11:45:16Z

In automated planning, control parameters extend standard action representations through the introduction of continuous numeric decision variables. Existing state-of-the-art approaches have primarily handled control parameters as embedded constraints alongside other temporal and numeric restrictions, and thus have implicitly treated them as additional constraints rather than as decision points in the search space. In this paper, we propose an efficient alternative that explicitly handles control parameters as true decision points within a systematic search scheme. We develop a best-first, heuristic search algorithm that operates over infinite decision spaces defined by control parameters and prove a notion of completeness in the limit under certain conditions. Our algorithm leverages the concept of delayed partial expansion, where a state is not fully expanded but instead incrementally expands a subset of its successors. Our results demonstrate that this novel search algorithm is a competitive alternative to existing approaches for solving planning problems involving control parameters.

2025-09-04T07:27:27Z Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence. 2025. Main Track. Pages 8456-8464 Ángel Aso-Mollar Diego Aineto Enrico Scala Eva Onaindia 10.24963/ijcai.2025/940 http://arxiv.org/abs/2509.15441v1 2025-09-18T21:27:43Z

Neural networks are important tools in machine learning. Representing piecewise linear activation functions with tropical arithmetic enables the application of tropical geometry. Algorithms are presented to compute regions where the neural networks are linear maps. Through computational experiments, we provide insights on the difficulty to train neural networks, in particular on the problems of overfitting and on the benefits of skip connections.

2025-09-18T21:27:43Z Accepted for publication in the proceedings in Computer Algebra in Scientific Computing 2025 Johnny Joyce Jan Verschelde http://arxiv.org/abs/2507.15665v2 2025-09-17T12:49:43Z

Koutschan, Krattenthaler and Schlosser recently considered a family of binomial determinants. In this work, we give combinatorial interpretations of two subclasses of these determinants in terms of domino tilings and nonintersecting lattice paths, thereby partially answering a question of theirs. Furthermore, the determinant evaluations established by Koutschan, Krattenthaler and Schlosser produce many product formulas for our weighted enumerations of domino tilings and nonintersecting lattice paths. However, there are still two enumerations left corresponding to conjectural formulas made by the three. We hereby prove the two conjectures using the principle of holonomic Ansatz plus the approach of modular reduction for creative telescoping, and hence fill the gap.

2025-07-21T14:26:10Z Typo in Thm. 1.4, eq. (1.21) fixed Qipin Chen Shane Chern Atsuro Yoshida http://arxiv.org/abs/2501.04194v2 2025-09-15T00:45:51Z

Signal Temporal Logic (STL) offers a concise yet expressive framework for specifying and reasoning about spatio-temporal behaviors of robotic systems. Attractively, STL admits the notion of robustness, the degree to which an input signal satisfies or violates an STL specification, thus providing a nuanced evaluation of system performance. In particular, the differentiability of STL robustness enables direct integration to robotic workflows that rely on gradient-based optimization, such as trajectory optimization and deep learning. However, existing approaches to evaluating and differentiating STL robustness rely on recurrent computations, which become inefficient with longer sequences, limiting their use in time-sensitive applications. In this paper, we present STLCG++, a masking-based approach that parallelizes STL robustness evaluation and backpropagation across timesteps, \revised{achieving more than 1000$\times$ faster computation time than the recurrent approach (STLCG++).}{achieving significant speed-ups compared to a recurrent approach.} We also introduce a smoothing technique to enable the differentiation of time interval bounds, thereby expanding STL's applicability in gradient-based optimization tasks involving spatial and temporal variables. Finally, we demonstrate STLCG++'s benefits through three robotics use cases and provide JAX and PyTorch libraries for seamless integration into modern robotics workflows. Project website with demo and code: https://uw-ctrl.github.io/stlcg/.

2025-01-08T00:06:43Z ©2025 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works Parv Kapoor Kazuki Mizuta Eunsuk Kang Karen Leung 10.1109/LRA.2025.3588389 http://arxiv.org/abs/2502.17026v2 2025-09-15T00:12:59Z

Understanding the uncertainty in large language model (LLM) explanations is important for evaluating their faithfulness and reasoning consistency, and thus provides insights into the reliability of LLM's output regarding a question. In this work, we propose a novel framework that quantifies uncertainty in LLM explanations through a reasoning topology perspective. By designing a structural elicitation strategy, we guide the LLMs to frame the explanations of an answer into a graph topology. This process decomposes the explanations into the knowledge related sub-questions and topology-based reasoning structures, which allows us to quantify uncertainty not only at the semantic level but also from the reasoning path. It further brings convenience to assess knowledge redundancy and provide interpretable insights into the reasoning process. Our method offers a systematic way to interpret the LLM reasoning, analyze limitations, and provide guidance for enhancing robustness and faithfulness. This work pioneers the use of graph-structured uncertainty measurement in LLM explanations and demonstrates the potential of topology-based quantification.

2025-02-24T10:28:21Z 28 pages, 9 figures; accepted at COLM'25 Longchao Da Xiaoou Liu Jiaxin Dai Lu Cheng Yaqing Wang Hua Wei http://arxiv.org/abs/2209.04807v5 2025-09-14T09:08:38Z

An effective exact method is proposed for computing generalized eigenspaces of a matrix of integers or rational numbers. Keys of our approach are the use of minimal annihilating polynomials and the concept of the Jourdan-Krylov basis. A new method, called Jordan-Krylov elimination, is introduced to design an algorithm for computing Jordan-Krylov basis. The resulting algorithm outputs generalized eigenspaces as a form of Jordan chains. Notably, in the output, components of generalized eigenvectors are expressed as polynomials in the associated eigenvalue as a variable.

2022-09-11T08:00:32Z 35 pages. The title has been revised to better reflect the scope and contributions of the paper Shinichi Tajima Katsuyoshi Ohara Akira Terui http://arxiv.org/abs/2509.08433v1 2025-09-10T09:26:50Z

This article proposes a paraconsistent framework for evaluating similarity in knowledge bases. Unlike classical approaches, this framework explicitly integrates contradictions, enabling a more robust and interpretable similarity measure. A new measure $ S^* $ is introduced, which penalizes inconsistencies while rewarding shared properties. Paraconsistent super-categories $ Ξ_K^* $ are defined to hierarchically organize knowledge entities. The model also includes a contradiction extractor $ E $ and a repair mechanism, ensuring consistency in the evaluations. Theoretical results guarantee reflexivity, symmetry, and boundedness of $ S^* $. This approach offers a promising solution for managing conflicting knowledge, with perspectives in multi-agent systems.

2025-09-10T09:26:50Z in French language, 19{è}mes Journ{é}es d'Intelligence Artificielle Fondamentale et 20{è}mes Journ{é}es Francophones sur la Planification, la D{é}cision et l'Apprentissage pour la conduite de syst{è}mes, JIAF-JFPDA 2025, Coll{è}ge Repr{é}sentation et Raisonnement de l'AFIA, Jul 2025, Dijon, France José-Luis Vilchis Medina ENSTA Bretagne, Lab-STICC, Lab-STICC_ROBEX