arXiv subjects

Ruichen Qiu

Publications and source records attributed to Ruichen Qiu.

15 recordsLinked to original sources

arXiv2026

MechMath Agent Team: LLM Driven Agents for Mathematical Research

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.

cs.AI↗

arXiv2026

Deterministic Polynomial-time Exact-root Computation for Sparse Polynomials with Bounded Total Degree

We study the problem of deterministically computing the exact root of a sparse polynomial in the multivariate setting. Let $f \in \F[x_1,\ldots,x_n]$ be a nonzero polynomial that is an exact $e$-th power, say $f = g^e$. Suppose $f$ is $s$-sparse, has an individual degree of at most $d$, and a total degree of $D = \tdeg(f)$. We prove a sparsity bound on the base polynomial $g$: \[ \|g\|_0 \le s^{D(2d+2)/e + 1}. \] Based on this bound, we develop a deterministic algorithm that computes the base $g$. % In contrast to the general deterministic factorization algorithm of Bhargava, Saraf, and Volkovich \cite{BhargavaSarafVolkovich2020}, which achieves only a quasi-polynomial dependence on the input parameters, our algorithm is \emph{polynomial-time} in the setting where the total degree $D$ is bounded. Specifically, the overall complexity is \[ \mathrm{poly}\left(s^{O(Dd)}, n, d, D\right) + s\cdot R(e), \] % where $R(e)$ denotes the cost of constructing a single $e$-th root of a scalar in the base field $\F$, and, when $\operatorname{char}(\F)\mid e$, the cost of computing a single Frobenius root of a scalar. % This term is field-dependent, and over finite fields, $\mathbb{Q}$, or number fields with a suitable representation, it is absorbed into the polynomial complexity bound. % Within the bounded total-degree regime, this yields a deterministic polynomial-time algorithm for exact-root computation.

cs.DS↗

arXiv2026

The Equivalence Problem for Generalized Airy Operators

In this paper, we establish degree obstructions to the equivalence of generalized Airy operators of the same type. As an application, we answer a question posed by Nicholas M. Katz in Inventiones Mathematicae (87, pp. 13-61,1987). The main results of Sections 3 and 4 were obtained through a close interactive collaboration between the authors and the artificial intelligence agent system MechMath Agent Team (MMAT).

math.RA↗

arXiv2026

Complexity of Low-Degree Skew Polynomial Multiplication over Finite Fields

In this note, we study the complexity of multiplication in skew polynomial rings over finite fields. We prove that the product of two elements in $\mathbb{F}_{q^n}[x;\sigma]$ of degree at most $d < n$ can be computed using $\widetilde O(d^{\omega_K-1}n)$ arithmetic operations over $\mathbb{F}_q$, where $\sigma$ is the $q$-Frobenius automorphism. This matches the conjectural upper bound of Caruso--Le Borgne~[ISSAC'17] and is quasi-optimal in view of the lower bound of Chen--Ye [ISSAC'24]. The proof reduces the finite-field case to the split algebra case using the equivariant multiplication theory of Couveignes--Ezome~[J.~Algebra, 2023], and then applies existing fast algorithms.

cs.SC↗

arXiv2026

Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number

In this paper, it is proved that any nonnegative integer can be written in the following form $$ x(x+1)/2 + y(3y+1)/2 + z(5z+1)/2, \qquad x,y,z \in \mathbb{N}. $$ This settles the conjecture recorded as OEIS A287616. All parts of the proof have been formalized in Lean 4, with the exception of two results: one externally cited theorem and one statement verified by symbolic computation. Both the natural-language proof and the Lean formalization were generated by the MechMath Agent Team developed by the authors.

math.NT↗

arXiv2026

A Greatest Common Divisor Criterion of Certain Binomial Coefficients

The binomial greatest common divisor (gcd) criterion recorded as OEIS A080170 is proven. The criterion also appears as conjecture (17) in Ralf Stephan's list of OEIS conjectures. For $k\geq 2$, put \[ D(k)=\gcd_{2\leq q\leq k+1}\binom{qk}{k}, \qquad n=k+1. \] If $P$ is the largest prime-power component $p^a$ exactly dividing $n$, then the criterion asserts \[ D(k)=1 \quad\Longleftrightarrow\quad \frac{n}{P}>P. \] The proof is formalized in Lean and the Lean artifact is accepted as part of the Formal Conjectures project. Both the natural-language proof and the Lean formalization are generated by the MechMath Agent Team, an AI agent developed by the authors.

math.NT↗

arXiv2026

Quasi-linear Time Multiplication of Sparse Polynomials with Integer Coefficients

Sparse polynomial multiplication is a fundamental problem in computer algebra and the theory of computation, and the development of a quasi-linear time output-sensitive multiplication algorithm has been posed as an open challenge. In this paper, a counterexample is provided to a previously claimed solution to this open problem for integer coefficients. By employing the existing quasi-linear modular-black-box interpolation algorithm, we are able to provide an algorithm with quasi-linear bit complexity for the integer coefficients setting. Furthermore, in the case of coefficients over a finite field, we obtain an algorithm whose bit complexity is linear in the number of terms, the logarithm of the degree, and the logarithm of the size of the finite field.

cs.SC↗

arXiv2026

Sparse Polynomial Divisibility Test over Finite Field is CoNP-hard

In this paper, we show that deciding whether a sparse polynomial does not divide another sparse polynomial exactly over finite fields is NP-hard under BPP many-one reductions. Equivalently, the sparse polynomial divisibility test over finite fields is CoNP-hard. This resolves the long-standing open problem concerning the computational complexity of the divisibility test for sparse polynomials in the setting of finite fields.

cs.SC↗

arXiv2026

Output-sensitive Sparse Polynomial GCD over Finite Fields is NP-hard

In this paper, we prove that output-sensitive sparse polynomial GCD computation over finite fields is NP-hard under BPP many-one reduction. More precisely, for two sparse univariate polynomials $f,g$ with finite field coefficients, there exists no randomized algorithm to compute $\mathrm{gcd}(f,g)$, which is polynomial-time in the sizes of $f,g,\gcd(f,g)$ under the standard complexity assumption $\mathrm{NP}\nsubseteq\mathrm{BPP}$. This settles the open problem posed as Challenge 5 in The Sparsity Challenges in the finite field setting. Furthermore, we show that the Roots of Unity Detection problem over finite fields is NP-hard; that is, determining whether the GCD of a sparse univariate polynomial and $x^n - 1$ has nonzero degree is NP-hard.

cs.SC↗

arXiv2026

A Finite Certificate for the Positive $n=9$ Vasc Inequality

We prove the positive-real $n=9$ case of the Vasc cyclic inequality. The proof was obtained with human-guided assistance from the AI agent MechMath Agent Team: the human-readable part reduces the rational inequality to a homogeneous polynomial inequality, fixes a cyclic maximum, and parametrizes each sorted fixed-maximum cone by cumulative gaps; the finite part is a certificate covering all $8!=40320$ sorted cones. MechMath Agent Team generated the certificate verification workflow through Python tool calls, including the case split, verification programs, and terminal classifications. The published certificate has $36815$ coefficient leaves, $2236$ ordinary Polya multiplier leaves, and $1269$ AM-GM midpoint overlay leaves. Human authors audited the mathematical reductions and verification logic, and a separate artifact contains the certificate, an independent verifier, and a from-source rebuild route.

cs.SC↗

arXiv2026

MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving

Recent advances in large language models (LLMs) and LLM-based agents have substantially improved the capabilities of automated theorem proving. However, for problems that require complex mathematical reasoning, current systems seldom succeed in their initial attempt, necessitating iterative adjustments to their proof strategies. Existing approaches for handling failed attempts typically either iteratively fix errors within the proof or discard the entire proof and regenerate it from scratch. The former leads to progressively longer contexts, which degrade the model's ability to attend to the remaining unresolved subproblems, while the latter is inefficient, as it may abandon mostly correct reasoning due to localized errors. To address this dilemma, we present MechMath, an agent system centered on a Sorrifier-driven formal decomposition paradigm. By leveraging the sorry placeholder in Lean to precisely isolate unresolved subgoals while preserving the surrounding verified proof structure, MechMath extracts each failed subproblem into a clean, self-contained context and resolves it independently. This avoids both the waste of full regeneration and the excessive context length induced by repeated repairs. Experimental results on challenging mathematical competition benchmarks, including IMO 2025, Putnam 2025, miniF2F, and a subset of ProverBench, demonstrate that our agent achieves significant advantages in proving efficiency.

cs.CL↗

arXiv2025

A Survey on Unlearning in Large Language Models

Large Language Models (LLMs) demonstrate remarkable capabilities, but their training on massive corpora poses significant risks from memorized sensitive information. To mitigate these issues and align with legal standards, unlearning has emerged as a critical technique to selectively erase specific knowledge from LLMs without compromising their overall performance. This survey provides a systematic review of over 180 papers on LLM unlearning published since 2021. First, it introduces a novel taxonomy that categorizes unlearning methods based on the phase in the LLM pipeline of the intervention. This framework further distinguishes between parameter modification and parameter selection strategies, thus enabling deeper insights and more informed comparative analysis. Second, it offers a multidimensional analysis of evaluation paradigms. For datasets, we compare 18 existing benchmarks from the perspectives of task format, content, and experimental paradigms to offer actionable guidance. For metrics, we move beyond mere enumeration by dividing knowledge memorization metrics into 10 categories to analyze their advantages and applicability, while also reviewing metrics for model utility, robustness, and efficiency. By discussing current challenges and future directions, this survey aims to advance the field of LLM unlearning and the development of secure AI systems.

cs.CL↗

arXiv2025

Circuit Diagram Retrieval Based on Hierarchical Circuit Graph Representation

In the domain of analog circuit design, the retrieval of circuit diagrams has drawn a great interest, primarily due to its vital role in the consultation of legacy designs and the detection of design plagiarism. Existing image retrieval techniques are adept at handling natural images, which converts images into feature vectors and retrieval similar images according to the closeness of these vectors. Nonetheless, these approaches exhibit limitations when applied to the more specialized and intricate domain of circuit diagrams. This paper presents a novel approach to circuit diagram retrieval by employing a graph representation of circuit diagrams, effectively reformulating the retrieval task as a graph retrieval problem. The proposed methodology consists of two principal components: a circuit diagram recognition algorithm designed to extract the circuit components and topological structure of the circuit using proposed GAM-YOLO model and a 2-step connected domain filtering algorithm, and a hierarchical retrieval strategy based on graph similarity and different graph representation methods for analog circuits. Our methodology pioneers the utilization of graph representation in the retrieval of circuit diagrams, incorporating topological features that are commonly overlooked by standard image retrieval methods. The results of our experiments substantiate the efficacy of our approach in retrieving circuit diagrams across of different types.

cs.AR↗

arXiv2024

PowerMLP: An Efficient Version of KAN

The Kolmogorov-Arnold Network (KAN) is a new network architecture known for its high accuracy in several tasks such as function fitting and PDE solving. The superior expressive capability of KAN arises from the Kolmogorov-Arnold representation theorem and learnable spline functions. However, the computation of spline functions involves multiple iterations, which renders KAN significantly slower than MLP, thereby increasing the cost associated with model training and deployment. The authors of KAN have also noted that ``the biggest bottleneck of KANs lies in its slow training. KANs are usually 10x slower than MLPs, given the same number of parameters.'' To address this issue, we propose a novel MLP-type neural network PowerMLP that employs simpler non-iterative spline function representation, offering approximately the same training time as MLP while theoretically demonstrating stronger expressive power than KAN. Furthermore, we compare the FLOPs of KAN and PowerMLP, quantifying the faster computation speed of PowerMLP. Our comprehensive experiments demonstrate that PowerMLP generally achieves higher accuracy and a training speed about 40 times faster than KAN in various tasks.

cs.LG↗

arXiv2024

Unlink to Unlearn: Simplifying Edge Unlearning in GNNs

As concerns over data privacy intensify, unlearning in Graph Neural Networks (GNNs) has emerged as a prominent research frontier in academia. This concept is pivotal in enforcing the \textit{right to be forgotten}, which entails the selective removal of specific data from trained GNNs upon user request. Our research focuses on edge unlearning, a process of particular relevance to real-world applications. Current state-of-the-art approaches like GNNDelete can eliminate the influence of specific edges yet suffer from \textit{over-forgetting}, which means the unlearning process inadvertently removes excessive information beyond needed, leading to a significant performance decline for remaining edges. Our analysis identifies the loss functions of GNNDelete as the primary source of over-forgetting and also suggests that loss functions may be redundant for effective edge unlearning. Building on these insights, we simplify GNNDelete to develop \textbf{Unlink to Unlearn} (UtU), a novel method that facilitates unlearning exclusively through unlinking the forget edges from graph structure. Our extensive experiments demonstrate that UtU delivers privacy protection on par with that of a retrained model while preserving high accuracy in downstream tasks, by upholding over 97.3\% of the retrained model's privacy protection capabilities and 99.8\% of its link prediction accuracy. Meanwhile, UtU requires only constant computational demands, underscoring its advantage as a highly lightweight and practical edge unlearning solution.

cs.LG↗