https://arxiv.org/api/5cAOXs0eZEEs+bWTh9b3TpG4uBI 2026-09-10T22:25:51Z 3239 90 15 http://arxiv.org/abs/2605.07323v2 2026-07-15T14:08:36Z

Discovering governing differential equations from observational data is a fundamental challenge in scientific machine learning. Existing symbolic regression approaches rely primarily on quantitative metrics; however, real-world differential equation modeling also requires incorporating domain knowledge to ensure physical plausibility. To address this gap, we propose DoLQ, a method for discovering ordinary differential equations with LLM-based qualitative and quantitative evaluation. DoLQ employs a multi-agent architecture: a Sampler Agent proposes dynamic system candidates, a Parameter Optimizer refines equations for accuracy, and a Scientist Agent leverages an LLM to conduct both qualitative and quantitative evaluations and synthesize their results to iteratively guide the search. Experiments on multi-dimensional ordinary differential equation benchmarks demonstrate that DoLQ achieves superior performance compared to existing methods, not only attaining higher success rates but also more accurately recovering the correct symbolic terms of ground truth equations. Our code is available at https://github.com/Bon99yun/DoLQ.

2026-05-08T06:29:58Z Accepted at ICML 2026 International Conference on Machine Learning 2026 Sum Kyun Song Bong Gyun Shin Jae Yong Lee http://arxiv.org/abs/2608.11211v1 2026-07-13T18:42:21Z

Conway's 99-graph problem asks whether a strongly regular graph with parameters $\mathrm{srg}(99,14,1,2)$ exists. We report a systematic, fully reproducible attack by an autonomous AI research agent, scored under the track's partial-credit metric. Our verifiable contributions are: (1) an exhaustive proof that no circulant graph on $\mathbb{Z}/99$ satisfies more than $3366/4950=68.0\%$ of the constraints ($33$ of $49$ difference-classes), with the same ceiling for the other abelian group of order $99$; (2) a forced-structure reduction: $λ=1$ makes each neighbourhood a perfect matching and $μ=2$ puts the outer vertices in bijection with non-matched neighbour-pairs, collapsing existence to a $12$-regular graph on $84$ vertices, encoded for CP-SAT and validated by recovering the unique $\mathrm{srg}(9,4,1,2)$; (3) a validated prescribed-automorphism orbit-existence framework (fixed-point-free and single-fixed-point actions, checked on $\mathrm{srg}(9,4,1,2)$ and the Paley graph $\mathrm{srg}(13,6,2,3)$), and (4) a best verified artifact at $69.43\%$, with evidence that this is a robust frontier (fourteen distinct methods, none exceeding it) entangled with the open question, since any provable bound below $4950$ is a non-existence proof.

2026-07-13T18:42:21Z This paper is accepted to the first Conference For AI Scientists (CAISc) Aalok Thakkar http://arxiv.org/abs/2604.16232v2 2026-07-13T18:09:31Z

Understanding natural and engineered systems often relies on symbolic formulations, such as differential equations, which provide interpretability and transferability beyond black-box models. We introduce Latent Grammar Flow (LGF), a neuro-symbolic generative framework for discovering ordinary differential equations from data. LGF embeds equations as grammar-based representations into a discrete latent space and forces semantically similar equations to be positioned closer together with a behavioural loss. Then, a discrete flow model guides the sampling process to recursively generate candidate equations that best fit the observed data. Domain knowledge and constraints, such as stability, can be either embedded into the rules or used as conditional predictors.

2026-04-17T16:46:23Z Accepted to the Structured Probabilistic Inference & Generative Modeling Workshop at ICML 2026 in Seoul, South Korea Karin Yu Eleni Chatzi Georgios Kissas http://arxiv.org/abs/2607.11657v1 2026-07-13T15:05:31Z

We propose an algorithm and its implementation for trajectory planning and certification for 3-DOF robot manipulators. The method uses Real Quantifier Elimination (QE) based on Comprehensive Gröbner Systems (CGS), also known as the CGS-QE method. The main advantage of the proposed method is its efficiency in trajectory planning and solution certification. This efficiency comes from the effective use of the CGS. First, for trajectory planning, we solve the inverse kinematics problem at each point along the trajectory via Gröbner basis computation. This usually requires recalculating the Gröbner basis at every point, which is time-consuming. We avoid this by computing the CGS for a parametric system. Here, the end-effector coordinates are parameters. This approach streamlines the algorithm. Second, for solution certification, the CGS-QE method certifies that an inverse kinematics solution exists at any point along the end-effector's trajectory. Our method also certifies solutions for trajectories composed of line segments and cubic natural splines. The algorithm is implemented within the computer algebra system Risa/Asir.

2026-07-13T15:05:31Z Yu Nakai Akira Terui Masahiko Mikawa http://arxiv.org/abs/2606.06386v2 2026-07-11T16:12:02Z

This paper presents the issues arising in implementing a fast integer division algorithm on general purpose GPUs. The algorithm uses a Newton iteration based on the shifted inverse operation, keeping all arithmetic in the integer domain and relying on data-parallel operators. The principal contribution is an efficient GPU/CUDA implementation for integer precisions from $2^{15}$ to $2^{18}$ -- sizes not supported by \cgbn{} division. We propose algorithmic refinements, define a cost model in terms of multiplications, build on prefix sums and previous work on multi-precision multiplication, and present an evaluation showing near-optimal performance relative to the model for the target precision.

2026-06-04T16:51:22Z Martin B. Marchioro Aske N. Raahauge Marc I. Løvenskjold Cosmin E. Oancea Stephen M. Watt http://arxiv.org/abs/2607.10257v1 2026-07-11T10:58:48Z

Formal verification of highly optimized arithmetic circuits at the gate-level remains a significant challenge due to the state space explosion problem. Although Symbolic Computer Algebra (SCA) offers a scalable theoretical foundation by modeling circuits as multivariate polynomials, practical implementations frequently suffer from the explosion of the size of intermediate polynomials. State-of-the-art SCA tools typically rely on fixed heuristics and restrict their application to standard multipliers. A fixed heuristic is insufficient for structurally diverse arithmetic circuits, as it often fails to generalize across all cases. In this paper, we introduce Arisca, an open-source parameterized verification framework for \textbf{Ari}thmetic circuits using \textbf{S}ymbolic \textbf{C}omputer \textbf{A}lgebra. Arisca establishes a generalized parameter space that unifies previously isolated state-of-the-art (SOTA) techniques as specific configurations within a broader algebraic reduction theory. To fundamentally transplant and elevate previous methods, we propose several algorithmic improvements, such as an HA-preserving extraction strategy, density-based vanishing detection, and conservative polynomial size estimation. In addition, Arisca expands the verification scope to encompass general arithmetic circuits with any combination of addition and multiplication, such as multiply-accumulators and dot-product units. Extensive evaluations demonstrate that Arisca achieves SOTA performance in a comprehensive suite of multiplier benchmarks and a diverse array of practical arithmetic cases.

2026-07-11T10:58:48Z Kezhi Li Min Li Qiang Xu http://arxiv.org/abs/2607.06397v2 2026-07-11T00:32:37Z

In this note, we present RationalUnivariateRepresentation$.$jl (https://newrur.gitlabpages.inria.fr/RationalUnivariateRepresentation.jl/), a Julia package for computing rational univariate representations of zero-dimensional polynomial systems. The package uses dense linear algebra and Gaussian elimination for the FGLM-like stage. The purpose of this contribution is to advocate for this choice and explain the implementation details that turn the algorithm into practical software. In particular, we show that our implementation can compute guaranteedly correct parametrizations of ideals with thousands of solutions within seconds.

2026-07-07T15:29:14Z In proceedings of ICMS 2026 Alexander Demin Fabrice Rouillier http://arxiv.org/abs/2607.09338v1 2026-07-10T12:19:59Z

Generative AI is profoundly transforming the core technologies behind conversational systems, shifting from component-based to end-to-end approaches. However, Large Language Models (LLMs) may still generate inconsistencies, a critical issue particularly in Task-Oriented Dialogues (TODs), where system responses must strictly adhere to information from a domain knowledge base (e.g., restaurants in a city). A single hallucination (e.g., suggesting a non-existent restaurant) can lead to severe task failures. We investigate a method for automatically detecting inconsistencies by conceptualizing TODs as a Constraint Satisfaction Problem (CSP), where variables represent dialogue segments referencing the conversational domain, and constraints among variables capture dialogue properties such as turn coherence and adherence to domain knowledge. We propose a pipeline that first identifies variables in a target dialogue and then applies a CSP solver to identify valid solutions. By comparing the target dialogue with valid variable assignments, we can detect inconsistencies and suggest minimal changes to ensure dialogue consistency. We demonstrate the high accuracy of the CSP-based approach in detecting inconsistencies, and provide a detailed analysis of our findings.

2026-07-10T12:19:59Z arXiv admin note: substantial text overlap with arXiv:2407.11857 Tiziano Labruna Giovanni Bonetta Bernardo Magnini http://arxiv.org/abs/2607.09163v1 2026-07-10T07:34:57Z

Gröbner basis computation incurs heavy computational overhead, especially under lexicographic order. F5 and its GVW variant dominate efficient field-based Gröbner basis solving. The proper basis algorithm offers a parameterized ideal computation framework without leveraging modern signature-based optimizations. This work presents the Proper-Cover algorithm for zero-dimensional polynomial ideals by combining GVW's cover optimization over signature with the proper basis theory. We generalize signature, cover, POT ordering, reduction and S-pair concepts to parameterized coefficients, design a two-phase algorithm with compatible factor construction and hungry refinement, and rigorously prove termination and output correctness. Accordingly, we propose a new framework for the efficient computation of polynomial ideal bases. Benchmark results show that Proper-Cover surpasses F5 under all monomial orderings and delivers clear speedups over GVW for lexicographic (plex) order.

2026-07-10T07:34:57Z 15 pages Sheng-Ming Ma Yi Liu Zheng-Lin Jiao http://arxiv.org/abs/2503.21535v2 2026-07-10T07:11:17Z

The Deligne-Ogus-Shioda theorem guarantees the existence of isomorphisms between products of supersingular elliptic curves over finite fields. In this paper, we present methods for explicitly computing these isomorphisms in polynomial time, given the endomorphism rings of the curves involved. Our approach leverages the Deuring correspondence, enabling us to reformulate computational isogeny problems into algebraic problems in quaternions. Specifically, we reduce the computation of isomorphisms to solving systems of quadratic and linear equations over the integers derived from norm equations. We develop $\ell$-adic techniques for solving these equations when we have access to a low discriminant subring. Combining these results leads to the description of an efficient probabilistic Las Vegas algorithm for computing the desired isomorphisms. Under GRH, it is proved to run in expected polynomial time.

2025-03-27T14:26:31Z Accepted at ANTS 2026 Pierrick Gaudry Julien Soumier Pierre-Jean Spaenlehauer http://arxiv.org/abs/2607.05800v1 2026-07-07T03:54:21Z

Let $p$ be a prime and $R=\mathbb{Z}/p^2\mathbb{Z}$ the ring of integers modulo $p^2$. Any $A\in R^{n\times n}$ is unimodularly equivalent to its Smith form \[ S=diag\bigl(\underbrace{1,\ldots,1}_{r_0}, \underbrace{p,\ldots,p}_{r_1}, \underbrace{0,\ldots,0}_{r_2}\bigr) \in R^{n\times n}, \] i.e., there exist $U,V\in R^{n\times n}$ such that $UAV=S$, with $\det U,\det V\in R^*$ (where $R^*$ is the set of units in $R$, elements not equivalent to $0\bmod p$). Our goal in this paper is to determine $r_0,r_1,r_2$ quickly when $A$ is sparse or structured. By ``sparse'' we mean $A$ is given by a black box such that for any $v\in R^{n\times 1}$ we can compute $v\mapsto Av$ with $\tilde{O}(n)$ operations in $R$, which captures having few nonzero elements or a multiplicative structure (e.g., Hankel or Toeplitz matrices). We present a randomized algorithm which requires an expected number of \[ \tilde{O}\left(n^{3-1/(ω-1)}\right) \] operations in $R$ to compute the Smith form, where $ω$ is the exponent of dense matrix multiplication. Using standard cubic matrix multiplication ($ω=3$) our algorithm thus requires $\tilde{O}(n^{2.5})$ operations in $R$, while using the current asymptotically fastest matrix multiplication, with $ω<2.371339$, our algorithm requires $\tilde{O}(n^{2.270786})$ operations in $R$. Our algorithm is probabilistic of the Monte Carlo type, meaning it fails on any invocation with controllably small probability. We employ iterative block-Wiedemann-style matrix techniques and structured preconditioners. To our knowledge, this is the first algorithm to compute the modular Smith Normal Form modulo $p^2$ requiring fewer than $\tilde{O}(n^ω)$ operations in $R$, i.e., faster than any dense algorithm.

2026-07-07T03:54:21Z Mark Giesbrecht http://arxiv.org/abs/2607.05185v1 2026-07-06T15:02:23Z

Compositional generalization, the ability to understand and produce novel combinations of known components, remains a fundamental challenge for modern artificial intelligence. While few benchmarks exist, many focus on linguistic tasks and lack complex, explicit compositional structures. We introduce ClassicLogic, a new benchmark suite designed to evaluate an agent's ability to learn and compose problem-solving strategies. The benchmark consists of four classic logic puzzles: Sudoku, KenKen, Kakuro, and Futoshiki. Its core innovation is a hierarchical, explicit knowledge base for each game, where complex solving strategies are formally defined as compositions of simpler, foundational strategies. This structure allows for fine-grained evaluation of an agent's reasoning capabilities, from learning basic rules to applying multi-step compositional strategies to solve puzzles of increasing, mathematically validated difficulty. The open-source benchmark provides a challenging new testbed for advancing neuro-symbolic and other advanced AI reasoning systems.

2026-07-06T15:02:23Z Mahnoor Shahid Hannes Rothe http://arxiv.org/abs/2607.05160v1 2026-07-06T14:45:17Z

We present a new algebraic modeling of the Supersingular Isogeny Problem as a system of multivariate polynomial equations, in the case where the elliptic curves are connected by an isogeny whose degree is a power of $2$ or $3$. This modeling relies on Renes formulas for elliptic curves in Montgomery form (degree $2$) or triangular form (degree $3$). We investigate several algebraic properties of these systems: we prove that they are zero-dimensional, compute the dimension of their highest degree part, and show that they are not in generic coordinates. Experimental results show that solving these systems via Gröbner basis techniques is significantly faster than solving the algebraic modeling with modular polynomials.

2026-07-06T14:45:17Z 24 pages, 0 figures Alessio Caminata Andrea Sanguineti Silvia Sconza http://arxiv.org/abs/2607.04394v1 2026-07-05T16:37:40Z

AI reasoning has become a central focus in contemporary artificial intelligence, largely driven by the success of large language models. However, mathematical research, which is characterized by non-linear derivation paths, rigorous logical requirements, and protracted exploration cycles, poses severe challenges for existing reasoning systems. To overcome these limitations, we present the MechMath Agent Team (MMAT), which is a large language model driven agent designed to serve as a co-pilot throughout the full cycle of mathematical research. We design a tripartite Harness Architecture that decouples system responsibilities into Control, Execution, and Augmentation planes, thereby reconciling rigorous logical control with the agility demanded by open-ended research. Building upon this framework, we instantiate three specialized agents: a Knowledge Base Manager, a Natural Language Prover, and a Formal Language Prover, all operating in a closed loop to produce formally certified mathematical proofs. We evaluate MMAT on open problems in Number Theory, Algebraic Complexity Theory, Differential Algebra, Operator Algebra, and Inequalities. Across a two-month deployment, 11 problems have been solved, demonstrating its capacity to act as a co-pilot throughout the entire research cycle. The contributions are threefold: a general decoupled Harness Architecture for multi-agent mathematical reasoning, its concrete instantiation in the MMAT system, and empirical validation on a diverse suite of open problems.

2026-07-05T16:37:40Z Yichuan Cao Ruichen Qiu Junqi Liu Jiaqi Wang Dakai Guo Ruyong Feng Lihong Zhi Xiao-Shan Gao http://arxiv.org/abs/2607.04156v1 2026-07-05T07:50:08Z

Scientific equation discovery must combine broad domain priors with strict numerical testing. Symbolic regression supplies numerical grounding but faces a combinatorial search space, whereas many language-model systems ask the model to propose or select formulas directly. We test a different division of labour. We compare role specifications in which the language model acts as equation author, candidate decider or search controller, alongside end-to-end language-model and purely numerical baselines. In the controller setting we propose here, implemented as LLM-PySR, language models specify variables, operators, transformations and search depth; symbolic regression enumerates and fits expressions; and deterministic metrics govern retention. Across 74 AI-Feynman equations and seven complex formula-recovery tasks, search control achieved the strongest observed balance of accuracy, complexity, stability and cost. On an independent battery dataset, LLM-PySR identified a compact piecewise-linear relation between early voltage-curve displacement and cycle life. The results suggest that language models should shape hypothesis exploration rather than decide which equations survive.

2026-07-05T07:50:08Z Zikai Xie Wenmei Li Man Luo Jun Jiang Linjiang Chen