Symbolic Computation
Roughly includes material in ACM Subject Class I.1.
sort pith recommended most recent
Linear-relation machinery puts Eckart–Young, pseudoinverse, and restricted low-rank problems under one theorem.
· “Least-Squares and Low-Rank Approximation for Linear Relations Using a Diagrammatic Language”
The exact finite-length joint law of the uniform car-parking process is resolved into jamming cells with rational densities, evaluable in…
· “Exact Finite-Length Theory of Uniform Car Parking: Spatial Laws, Absorption, and Aggregation”
Volume tracking reaches $\widetilde{O}(d^{\omega(2)}\log\|B\|)$ bit operations, nearing randomized speeds.
· “Computing the Determinant via the Generalized Euclidean Algorithm”
Open-source package for graded superspace expressions outruns established systems on tested operations.
· “Alakazam: Symbolic Tensor Algebra for Field Theory in Julia”
Trained action memories become compressed kernel expansions whose bit errors decay exponentially with dimension.
Handing back the minimal conflicting rule set stops weaker models from deleting real constraints and inventing solutions.
· “From Errors to Proofs: Minimal-Core-Guided Repair for Neuro-Symbolic Constraint Solving”
A neuro-symbolic pipeline scores every episode against eight SSC rules and pinpoints the Hour-1 bundle.
On airline, tax, and salary-cap rules, a solver pipeline beats prompts while using 10x fewer tokens.
A frozen LLM, with a computer algebra system as exact judge, beat a 20% template baseline.
· “Neurosymbolic Discovery of Algebraic Graph Constructions”
Fixed-state rational games now admit one exact, polynomial-time-computable strategy family for all fine accuracies.
· “Existence and computation of monomial families of near-optimal strategies for recursive games”
A symbolic model of ETSI and ITU-T procedures traces them to timing and message-order gaps in classical control.
· “Beyond the Quantum Promise: A Security Analysis of Classical Control in Quantum Key Distribution”
A new algorithm gives radical generators on every parameter region, closing a gap in computational algebra.
· “On the Radical Computation of Parametric Ideals over Finite Fields”
Exact rational proof: a moment vector passes every level-three stationarity test yet matches no physical state.
· “Stationarity is not enough: tightness of the quantum mechanical bootstrap and the copositive cone”
Source-attributed Prolog rules and targeted follow-ups lift accuracy and explainability over pure LLM RAG.
· “NeSy-RAG: Neuro-Symbolic RAG for Explainable Question Answering”
Three symbolic filters on meta-product BDDs keep only the prime implicants that respect side constraints.
Each saved iteration is one MBDoE-designed experiment not run; validation R2 stays above 0.98.
· “DASyR-LLM: Domain-Aware Symbolic Regression with LLMs for Kinetic Model Discovery”
Writing the answer's constraints into the prompt cuts modular and format errors on AIME-style problems.
Formal proofs cover every transformation, so summaries handed to the solver match real program behavior.
· “Technical Report: A Formal Semantics for Java Symbolic Evaluation using Large-Block Encoding”
It splits the generator into factors and interpolates each one, beating standard Gröbner methods by orders of magnitude.
A weighted lifting tree that tolerates repeated roots cuts the previous quadratic-in-degree bound.
· “Faster Deterministic Integer Root Finding for Integer Polynomials”
New construction yields polynomially many resultants that detect common zeros, improving all known bounds for n>2.
Complete assignments satisfy all 2,461,316 clauses; the formulas only require type-3 incidences, not exact cores.
Futhark addition matches or beats CUDA, and register placement closes most of the speed gap.
Optional executable world models hit perfect public-set scores; always-on repair replayed better but played worse.
· “Tycho: Active Abstraction with Programmatic World Models for ARC-AGI-3”
Constructive division, GCDs, LCMs and Riccati–Newton factoring turn LODO into routine computer-algebra objects
Independent checkers backed by proof assistants are fast enough for competitions and have exposed real unsoundness.
Mixed cells give both solution counts and eliminant Newton polytopes for sparse systems from geometry and chemistry
A learned rule table verifies each reasoning step, fixes only what is broken, and lets the model finish — biggest gains on the longest chain
· “Reason Popper-ly: Patching In-Context Reasoning with Inductive Logic Programming”
A solver, not the LLM, does the reasoning: millisecond answers, zero token cost, far fewer false alarms.
A strict division of labor lets a hallucination-prone AI find soft network invariants with formal guarantees.
A Lean 4 formalization proves correctness and a fixed polynomial arithmetic bit-cost bound for the Kannan–Bachem Smith normal form…
· “Machine-Checked Arithmetic Bit Complexity of the Kannan-Bachem Smith Normal Form in Lean 4”
Three-phase algorithm returns the well-founded model, an inconsistency flag, or a no-model verdict.
· “Hybrid MKNF with Classical Negation in the Rule Component”
A key-value database answers 'what happens from this position?' across a 10-million-game corpus on one desktop.
· “Chess\_db: A framework for working with large chess game datasets”
A human writes the proof skeleton; the LLM fills in the lemmas; every faulty step is rejected before the result is accepted.
· “Case study: proving sqrt(2) irrational with LPTP and an LLM”
The fifth-order recurrence is now a theorem, proved by creative telescoping, residues, and graph recurrences.
Under non-degeneracy, solutions bunch into countably many near-2π-periodic sequences on algebraic-exponential curves.
Coefficient determinants alone yield a µ-basis; the implicit equation follows by a resultant.
· “Explicit Formulas for μ-Bases of Planar Rational Quartic Curves”
One precomputed Gröbner system yields the exact parameter intervals where joint solutions exist.
Open-source tool also checks MACs and dot-products by treating fixed heuristics as configs
· “Arisca: A Parameterized Symbolic Algebra Framework for Arithmetic Circuit Verification”
Six constraint patterns turn slot values into a solvable puzzle that also suggests the minimal fixes.
· “Towards Detecting Inconsistencies in End-to-end Generated TODs”
Two-phase Proper-Cover algorithm returns proper bases for zero-dimensional ideals with proven termination
· “Beyond F5 and GVW: The Proper-Cover Algorithm for Fast Ideal Basis Computation”
Moderately sparse multiplication matrices make classical Gaussian elimination competitive for large polynomial systems
· “Fast Rational Univariate Representation via Gaussian Elimination”
A learn-once, apply-many F4 variant reuses one computation's structure across primes and evaluations.
A Monte Carlo black-box algorithm recovers the three invariants in expected Õ(n^{2.27}) ring ops
· “Computing Smith Forms Modulo p² of Sparse Matrices Faster Than Matrix Multiplication”
ClassicLogic separates perception, rule-following, and multi-step planning—and finds neuro-symbolic systems collapse below 25% on the last.
Degree-2/3 systems finish two orders of magnitude faster and reach longer paths.
· “Algebraic Modelings of the Supersingular Isogeny Problem”
A three-plane harness plus Lean 4 turns informal proofs into certified results across five domains.
· “MechMath Agent Team: LLM Driven Agents for Mathematical Research”
Controller role beats equation authoring and full generative search at a fraction of the token cost
· “Language models guide symbolic equation discovery by controlling search”
Closed forms for every non-invertible root; same geometry for MA(2), AR, and composite likelihood
· “Likelihood Geometry of Moving Average and Autoregressive Processes”
Central bounds plus modular reduction decide factorization once constants split; over cyclotomics the search may still fail
· “On Factoring Quantum-Plane Skew Polynomials over mathbb{Q}(ω)(t)”
When residual characteristic is zero or high, approximate roots cut factorization cost by the discriminant valuation factor.
· “Local polynomial factorisation: improving the Montes algorithm”
Bin-packing tests show quadratic breakers boost some solvers but linearization and large sets hurt others overall.
· “When Algebraic Symmetry Breaking Meets Solvers: An Experimental Study”
A reduction to split algebras yields the conjectured complexity and meets the known lower bound for d less than n.
· “Complexity of Low-Degree Skew Polynomial Multiplication over Finite Fields”
A circulant determinant of degree at most n(n-1) marks all bad parameters, enabling a fully deterministic search at the stated cost.
· “Fast Deterministic Normal Bases and Circulant Polynomial Determinants”
Separating formal logic from local document interpretation makes reviews inspectable, updatable, and testable on tasks like NDA clause evalu
· “PolicyGuard: From Organizational Policies to Neuro-SymbolicCompliance Review Engines”
Theory-neutral working memory and AI-assisted experiment generation from paper methods lower the barrier for new users.
· “Rapid Prototyping of Event-Driven Contextual Memory in the ACT-Up Cognitive Architecture”
It runs in polynomial time whenever the ideal norm is coprime to the index, covering every ideal in monogenic fields.
· “Deterministic and Efficient Ideal Arithmetic via Two-Element Representations”
The explicit three-term sum settles the OEIS A287616 conjecture for all nonnegative integers.
· “Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number”
Small sensor programs with random inputs obtain precise probability calculations by decomposing the input space into integrable cells.
· “Exact Evaluation of Probabilistic Programs with Cylindrical Algebraic Decomposition”
Version-aware layers turn replace and rollback into ordered MeMo primitive transactions on sequences and tokens.
· “Towards Version-aware Operations and Transaction Memories for Multi-layer MeMo”
Attention isolates features for KAN to expose mobility-load links in three U.S. markets
Basis conjugation operations produce closed-form expressions for all odd-dimensional cases by reduction to the even case.
Tree compositions of the exp-minus-log function match functions with bounded weak derivatives up to order k to any accuracy.
First speedup by a positive power of log N over the Eratosthenes sieve via fast polynomial arithmetic over finite fields.
SATURN builds approximate 3D scenes and applies soft predicates to handle changing perspectives, gaining 14 points over baselines on MindCub
· “SATURN: Symbolic Spatial Reasoning for Multi-Perspective Grounding”
ForEx translates model rationales into Lean4 and shows formal success and human agreement are largely independent.
Accuracy is gained by extending runtime of the same network rather than changing its weights or size, matching polynomial rates.
· “Recurrent neural networks approximate continuous functions”
Store numbers as numerator/denominator pairs, divide once at the end, deep gradients stay exact within 2^53.
No randomized algorithm runs in time polynomial in input and output sizes unless NP is contained in BPP.
· “Output-sensitive Sparse Polynomial GCD over Finite Fields is NP-hard”
Proves non-divisibility is NP-hard via BPP reductions, resolving open complexity question for exact tests.
· “Sparse Polynomial Divisibility Test over Finite Field is CoNP-hard”
Reduction to an existing modular black-box interpolation routine delivers the bound after a prior claim is disproved by counterexample.
· “Quasi-linear Time Multiplication of Sparse Polynomials with Integer Coefficients”
REO framework isolates persistent problems that determine which governing laws can be recovered from data.
· “Data-driven discovery of governing differential equations across physical systems”
One frozen Scheme evaluator lets LLM-proposed code structures receive exact parameter calibration against data.
· “Compile Once, Differentiate Everywhere: A Differentiable Meta-Circular Interpreter”
Optimization over symbolic models uses only the governing equation and boundary conditions to match analytical solutions for algebraic and d
· “A Data-Free Symbolic Regression Approach for Solving Equations”
Integer-only Newton method fills the large-precision gap left by existing CUDA libraries.
· “On GPU Implementation for Multi-Precision Integer Division”
Gaussian-mixture messages that transform under rotations and translations deliver fast accurate inference on molecules and robots where stan
It covers every one of the 40320 sorted cones with verified Polya and AM-GM multipliers.
· “A Finite Certificate for the Positive n=9 Vasc Inequality”
Mimics exact sequential structure to cut error in half on standard cases and succeed where belief propagation fails on frustrated graphs.
Prefix-suffix-middle training with symbolic verification reaches state-of-the-art results while cutting token use 31 percent.
· “Imbuing Large Language Models with Bidirectional Logic for Robust Chain Repair”
Bombieri-Pila and Coppersmith techniques cut the cost of building correctly rounded math libraries for binary128.
· “Integer points close to a transcendental curve: an algorithmic approach”