https://arxiv.org/api/XMBGhH4FgREGfSCUUeQ6ytEjOR0 2026-04-09T09:42:33Z 3074 120 15 http://arxiv.org/abs/2601.12711v1 2026-01-19T04:24:49Z

Large language models (LLMs) can be adapted either through numerical updates that alter model parameters or symbolic manipulations that work on discrete prompts or logical constraints. While numerical fine-tuning excels at injecting new factual knowledge, symbolic updates offer flexible control of style and alignment without retraining. We introduce a neurosymbolic LoRA framework that dynamically combines these two complementary strategies. Specifically, we present a unified monitoring signal and a reward-based classifier to decide when to employ LoRA for deeper factual reconstruction and when to apply TextGrad for token-level edits. Our approach remains memory-efficient by offloading the symbolic transformations to an external LLM only when needed. Additionally, the refined prompts produced during symbolic editing serve as high-quality, reusable training data, an important benefit in data-scarce domains like mathematical reasoning. Extensive experiments across multiple LLM backbones show that neurosymbolic LoRA consistently outperforms purely numerical or purely symbolic baselines, demonstrating superior adaptability and improved performance. Our findings highlight the value of interleaving numerical and symbolic updates to unlock a new level of versatility in language model fine-tuning.

2026-01-19T04:24:49Z Kevin Wang Neel P. Bhatt Cong Liu Junbo Li Runjin Chen Yihan Xi Timothy Barclay Alvaro Velasquez Ufuk Topcu Zhangyang Wang http://arxiv.org/abs/2510.05178v3 2026-01-18T11:38:26Z

AI for health will only scale when models are not only accurate but also readable, auditable, and governable. Many clinical and public-health decisions hinge on numeric thresholds -- cut-points that trigger alarms, treatment, or follow-up -- yet most machine-learning systems bury those thresholds inside opaque scores or smooth response curves. We introduce logistic-gated operators (LGO) for symbolic regression, which promote thresholds to first-class, unit-aware parameters inside equations and map them back to physical units for direct comparison with guidelines. On public ICU and population-health cohorts (MIMIC-IV ICU, eICU, NHANES), LGO recovers clinically plausible gates on MAP, lactate, GCS, SpO2, BMI, fasting glucose, and waist circumference while remaining competitive with established scoring systems (AutoScore) and explainable boosting machines (EBM). The gates are sparse and selective: they appear when regime switching is supported by the data and are pruned on predominantly smooth tasks, yielding compact formulas that clinicians can inspect, stress-test, and revise. As a standalone symbolic model or a safety overlay on black-box systems, LGO helps translate observational data into auditable, unit-aware rules for medicine and other threshold-driven domains.

2025-10-05T16:04:47Z Ou Deng Ruichen Cong Jianting Xu Shoji Nishimura Atsushi Ogihara Qun Jin http://arxiv.org/abs/2509.19859v3 2026-01-16T14:21:50Z

We propose a novel symbolic control framework for enforcing temporal logic specifications in Euler-Lagrange systems that addresses the key limitations of traditional abstraction-based approaches. Unlike existing methods that require exact system models and provide guarantees only at discrete sampling instants, our approach relies only on bounds on system parameters and input constraints, and ensures correctness for the full continuous-time trajectory. The framework combines scalable abstraction of a simplified virtual system with a closed-form, model-free controller that guarantees trajectories satisfy the original specification while respecting input bounds and remaining robust to unknown but bounded disturbances. We provide feasibility conditions for the construction of confinement regions and analyze the trade-off between efficiency and conservatism. Case studies on pendulum dynamics, a two-link manipulator, and multi-agent systems, including hardware experiments, demonstrate that the proposed approach ensures both correctness and safety while significantly reducing computational time and memory requirements. These results highlight its scalability and practicality for real-world robotic systems where precise models are unavailable and continuous-time guarantees are essential.

2025-09-24T07:57:36Z Ratnangshu Das Shubham Sawarkar Pushpak Jagtap http://arxiv.org/abs/2601.00312v2 2026-01-16T04:32:07Z

In this paper, we address the complexity barrier inherent in Fourier-Motzkin elimination (FME) and cylindrical algebraic decomposition (CAD) when eliminating a block of (existential) quantifiers. To mitigate this, we propose exploiting structural sparsity in the variable dependency graph of quantified formulas. Utilizing tools from parameterized algorithms, we investigate the role of treewidth, a parameter that measures the graph's tree-likeness, in the process of quantifier elimination. A novel dynamic programming framework, structured over a tree decomposition of the dependency graph, is developed for applying FME and CAD, and is also extensible to general quantifier elimination procedures. Crucially, we prove that when the treewidth is a constant, the framework achieves a significant exponential complexity improvement for both FME and CAD, reducing the worst-case complexity bound from doubly exponential to single exponential. Preliminary experiments on sparse linear real arithmetic (LRA) and nonlinear real arithmetic (NRA) benchmarks confirm that our algorithm outperforms the existing popular heuristic-based approaches on instances exhibiting low treewidth.

2026-01-01T11:20:30Z To appear at TACAS 2026 Hao Wu Jiyu Zhu Amir Kafshdar Goharshady Jie An Bican Xia Naijun Zhan http://arxiv.org/abs/2410.10336v2 2026-01-15T13:23:01Z

Mathematical reasoning remains a significant challenge for large language models (LLMs), despite progress in prompting techniques such as Chain-of-Thought (CoT). We present **Chain of Mathematically Annotated Thought (CoMAT)**, which enhances reasoning through two stages: *Symbolic Conversion* (converting natural language queries into symbolic form) and *Reasoning Execution* (deriving answers from symbolic representations). CoMAT operates entirely with a single LLM and without external solvers. Across four LLMs, CoMAT outperforms traditional CoT on six out of seven benchmarks, achieving gains of 4.48% on MMLU-Redux (MATH) and 4.58% on GaoKao MCQ. In addition to improved performance, CoMAT ensures faithfulness and verifiability, offering a transparent reasoning process for complex mathematical tasks

2024-10-14T09:48:41Z 9 pages, 12 figures Proc. EMNLP 2025, pp. 20245-20274 Joshua Ong Jun Leang Aryo Pradipta Gema Shay B. Cohen 10.18653/v1/2025.emnlp-main.1024 http://arxiv.org/abs/2601.09795v1 2026-01-14T19:02:02Z

Cylindrical Algebraic Decompositions (CADs) endowed with additional topological properties have found applications beyond their original logical setting, including algorithmic optimizations in CAD construction, robot motion planning, and the algorithmic study of the topology of semi-algebraic sets. In this paper, we construct explicit examples of CADs and CAD cells that refute several conjectures and open questions of J. H. Davenport, A. Locatelli, and G. K. Sankaran concerning these topological assumptions.

2026-01-14T19:02:02Z Lucas Michel http://arxiv.org/abs/2601.09548v1 2026-01-14T15:07:50Z

We consider cylindrical algebraic decompositions (CADs) as a tool for representing semi-algebraic subsets of $\mathbb{R}^n$. In this framework, a CAD $\mathscr{C}$ is adapted to a given set $S$ if $S$ is a union of cells of $\mathscr{C}$. Different algorithms computing an adapted CAD may produce different outputs, usually with redundant cell divisions. In this paper we analyse the possibility to remove the superfluous data. We thus consider the set $\text{CAD}^r(\mathcal{F})$ of CADs of class $C^r$ ($r \in \mathbb{N} \cup \{\infty, ω\}$) that are adapted to a finite family $\mathcal{F}$ of semi-algebraic sets of $\mathbb{R}^n$, endowed with the refinement partial order and we study the existence of minimal and minimum element in $\text{CAD}^r(\mathcal{F})$. We show that for every such $\mathcal{F}$ and every $\mathscr{C} \in \text{CAD}^r(\mathcal{F})$, there is a minimal CAD of class $C^r$ adapted to $\mathcal{F}$ and smaller (i.e. coarser) than or equal to $\mathscr{C}$. In dimension $n=1$ or $n=2$, this result is strengthened by proving the existence of a minimum element in $\text{CAD}^r(\mathcal{F})$. In contrast, for any $n \geq 3$, we provide explicit examples of semi-algebraic sets whose associated poset of adapted CADs does not admit a minimum. We then introduce a reduction relation on $\text{CAD}^r(\mathcal{F})$ in order to define an algorithm for the computation of minimal CADs and we characterise those semi-algebraic sets $\mathcal{F}$ for which $\text{CAD}^r(\mathcal{F})$ has a minimum by means of confluence of the associated reduction system. We finally provide practical criteria for deciding if a semi-algebraic set does admit a minimum CAD and apply them to describe various concrete examples of semi-algebraic sets, along with their minimum CAD of class $C^r$.

2026-01-14T15:07:50Z Expanded version of the following paper : https://dl.acm.org/doi/10.1145/3666000.3669704 Lucas Michel Pierre Mathonet Naïm Zénaïdi http://arxiv.org/abs/2601.08522v1 2026-01-13T13:05:06Z

Linear differential equations and recurrences reveal many properties about their solutions. Therefore, these equations are well-suited for representing solutions and computing with special functions. We identify a large class of existing algorithms that compute such representations as a linear relation between the iterates of an elementary operator known as a \emph{pseudo-linear map}. Algorithms of this form have been designed and used for solving various computational problems, in different contexts, including effective closure properties for linear differential or recurrence equations, the computation of a differential equation satisfied by an algebraic function, and many others. We propose a unified approach for establishing precise degree bounds on the solutions of all these problems. This approach relies on a common structure shared by all the specific instances of the class. For each problem, the obtained bound is tight. It either improves or recovers the previous best known bound that was derived by \emph{ad hoc} methods.

2026-01-13T13:05:06Z Louis Gaillard http://arxiv.org/abs/2304.07083v2 2026-01-10T20:59:03Z

In this article, we present a fast algorithm performing an instance of the Guruswami-Sudan list decoder for algebraic geometry codes. We show that any such code can be decoded in $\tilde{O}(s^2\ell^{ω-1}μ^{ω-1}(n+g) + \ell^ωμ^ω)$ operations in the underlying finite field, where $n$ is the code length, $g$ is the genus of the function field used to construct the code, $s$ is the multiplicity parameter, $\ell$ is the designed list size and $μ$ is the smallest positive element in the Weierstrass semigroup of some chosen place.

2023-04-14T12:18:35Z 13 pages (two-column format), 2 algorithms Peter Beelen Vincent Neiger 10.1109/TIT.2025.3550750 http://arxiv.org/abs/2601.05026v2 2026-01-09T09:29:32Z

We introduce monomial divisibility diagrams (MDDs), a data structure for monomial ideals that supports insertion of new generators and fast membership tests. MDDs stem from a canonical tree representation by maximally sharing equal subtrees, yielding a directed acyclic graph. We establish basic complexity bounds for membership and insertion, and study empirically the size of MDDs. As an application, we integrate MDDs into the signature Gröbner basis implementation of the Julia package AlgebraicSolving.jl. Membership tests in monomial ideals are used to detect some reductions to zero, and the use of MDDs leads to substantial speed-ups.

2026-01-08T15:33:58Z Pierre Lairez Rafael Mohr Théo Ternier http://arxiv.org/abs/2601.04901v1 2026-01-08T12:56:55Z

We describe a practical algorithm for computing the Stokes multipliers of a linear differential equation with polynomial coefficients at an irregular singular point of single level one. The algorithm follows a classical approach based on Borel summation and numerical ODE solving, but avoids a large amount of redundant work compared to a direct implementation. It applies to differential equations of arbitrary order, with no genericity assumption, and is suited to high-precision computations. In addition, we present an open-source implementation of this algorithm in the SageMath computer algebra system and illustrate its use with several examples. Our implementation supports arbitrary-precision computations and automatically provides rigorous error bounds. The article assumes minimal prior knowledge of the asymptotic theory of meromorphic differential equations and provides an elementary introduction to the linear Stokes phenomenon that may be of independent interest.

2026-01-08T12:56:55Z Michèle Loday-Richaud LMO Marc Mezzarobba LIX Pascal Remy LMV http://arxiv.org/abs/2412.14043v2 2026-01-07T12:32:53Z

Loop invariants are properties of a program loop that hold both before and after each iteration of the loop. They are often used to verify programs and ensure that algorithms consistently produce correct results during execution. Consequently, generating invariants becomes a crucial task for loops. We specifically focus on polynomial loops, where both the loop conditions and the assignments within the loop are expressed as polynomials. Although computing polynomial invariants for general loops is undecidable, efficient algorithms have been developed for certain classes of loops. For instance, when all assignments within a while loop involve linear polynomials, the loop becomes solvable. In this work, we study the more general case, where the polynomials can have arbitrary degrees. Using tools from algebraic geometry, we present two algorithms designed to generate all polynomial invariants within a given vector subspace, for a branching loop with nondeterministic conditional statements. These algorithms combine linear algebraic subroutines with computations on polynomial ideals. They differ depending on whether the initial values of the loop variables are specified or treated as parameters. Additionally, we present a much more efficient algorithm for generating polynomial invariants of a specific form, applicable to all initial values. This algorithm avoids expensive ideal computations.

2024-12-18T16:58:48Z 44 pages, 1 figure Journal of Symbolic Computation Vol. 135, 2026, p.102551 Erdenebayar Bayarmagnai Fatemeh Mohammadi Rémi Prébet 10.1016/j.jsc.2025.102551 http://arxiv.org/abs/2601.02703v1 2026-01-06T04:29:30Z

We present a unified constructive digit-by-digit framework for exact root extraction using only integer arithmetic. The core contribution is a complete correctness theory for the fractional square root algorithm, proving that each computed decimal digit is exact and final, together with a sharp truncation error bound of $10^{-k}$ after $k$ digits. We further develop an invariant-based framework for computing the integer $e$-th root $\lfloor N^{1/e} \rfloor$ of a non-negative integer $N$ for arbitrary fixed exponents $e \ge 2$, derived directly from the binomial theorem. This method generalizes the classical long-division square root algorithm, preserves a constructive remainder invariant throughout the computation, and provides an exact decision procedure for perfect $e$-th power detection. We also explain why exact digit-by-digit fractional extraction with non-revisable digits is structurally possible only for square roots ($e=2$), whereas higher-order roots ($e \ge 3$) exhibit nonlinear coupling that prevents digit stability under scaling. All proofs are carried out in a constructive, algorithmic manner consistent with Bishop-style constructive mathematics, yielding explicit algorithmic witnesses, decidable predicates, and guaranteed termination. The resulting algorithms require no division or floating-point operations and are well suited to symbolic computation, verified exact arithmetic, educational exposition, and digital hardware implementation.

2026-01-06T04:29:30Z Suresan Pareth http://arxiv.org/abs/2601.03298v1 2026-01-06T01:01:04Z

This is a brief description of a project that has already autoformalized a large portion of the general topology from the Munkres textbook (which has in total 241 pages in 7 chapters and 39 sections). The project has been running since November 21, 2025 and has as of January 4, 2026, produced 160k lines of formalized topology. Most of it (about 130k lines) have been done in two weeks,from December 22 to January 4, for an LLM subscription cost of about \$100. This includes a 3k-line proof of Urysohn's lemma, a 2k-line proof of Urysohn's Metrization theorem, over 10k-line proof of the Tietze extension theorem, and many more (in total over 1.5k lemmas/theorems). The approach is quite simple and cheap: build a long-running feedback loop between an LLM and a reasonably fast proof checker equipped with a core foundational library. The LLM is now instantiated as ChatGPT (mostly 5.2) or Claude Sonnet (4.5) run through the respective Codex or Claude Code command line interfaces. The proof checker is Chad Brown's higher-order set theory system Megalodon, and the core library is Brown's formalization of basic set theory and surreal numbers (including reals, etc). The rest is some prompt engineering and technical choices which we describe here. Based on the fast progress, low cost, virtually unknown ITP/library, and the simple setup available to everyone, we believe that (auto)formalization may become quite easy and ubiquitous in 2026, regardless of which proof assistant is used.

2026-01-06T01:01:04Z Josef Urban http://arxiv.org/abs/2601.02283v1 2026-01-05T17:11:53Z

The integration of command-line tools into the Galaxy platform is crucial for making complex computational methods accessible to a broader audience and ensuring reproducible research. However, the manual development of tool wrappers is a time-consuming, error-prone, and knowledge-intensive process. This bottleneck significantly affects the rapid deployment of new and updated tools, creating a gap between tool development and its availability to the scientific community. We have developed a novel, automated approach that directly translates Python tool interfaces into Galaxy-compliant tool wrappers. Our method leverages the argparse library, a standard for command-line argument parsing in Python. By embedding structured metadata within the metavar attribute of input and output arguments, our system programmatically parses the tool's interface to extract all necessary information. This includes parameter types, data formats, help text, and input/output definitions. The system then uses this information to automatically generate a complete and valid Galaxy tool XML wrapper, requiring no manual intervention. To validate the scalability and effectiveness of our approach, we applied it to the anvi'o framework, a comprehensive and complex bioinformatics platform comprising hundreds of individual programs. Our method successfully parsed the argparse definitions for the entire anvi'o suite and generated functional Galaxy tool wrappers. The resulting integration allows for the seamless execution of anvi'o workflows within the Galaxy environment. This work presents a significant advancement in the automation of tool integration for scientific workflow systems. By establishing a convention-based approach using Python's argparse library, we have created a scalable and generalizable solution that dramatically reduces the effort required to make command-line tools available in Galaxy.

2026-01-05T17:11:53Z 26 pages, 5 figures Fabio Cumbo Jayadev Joshi Daniel Blankenberg