3,211 papers in this slice of arXiv.
Rahul Nair, Bastian Lipka, Elizabeth Daly
In many practical applications of generative AI systems, from tax rules to airline baggage allowance, responses to natural language queries must respect written policies or rules. We present a hybrid symbolic approach that expresses policies in formal logic and at inference time exploits the representation power of language models for fact extraction to ground predicates, and an answer set solver for reasoning such that responses are interpretable, auditable, and as we show, accurate and robust under input perturbations. Specifically, we show this separation of extraction and reasoning steps outperforms policy-as-prompt and policy-as-code methods in most cases with ~10x reduction in token usage. The results point to the value of structured reasoning and symbolic solvers in conjunction with generative models to make robust decisions involving objective criteria.
Uma Ranjan, Kunal Tilaganji, Aditya Koul +9
Large language models (LLMs) often rely on shortcuts rather than systematic reasoning, raising safety concerns in medical applications. Allowing models to abstain when uncertain improves reliability but introduces a coverage accuracy tradeoff. We propose a two-stage framework for medical hypothesis verification in multiple-choice settings that manages this tradeoff through targeted ontology grounding, applied only when the model abstains. We show that abstention is not random but reflects genuine uncertainty, with abstained predictions associated with lower confidence. Across two frontier models (GPT-5.5, accessed via the Azure OpenAI API, and DeepSeek-R1), the proposed framework improves question-level accuracy by 9.6 percentage points (82.9% to 92.5%) and hypothesis-level accuracy by 4.2 percentage points (92.0% to 96.2%). Our experiments conducted on MedReason and MedQA show that abstention can be repurposed as a control signal for selective reasoning refinement, achieving knowledge-graph-level performance without explicit knowledge graph construction.
David Seka, Stefan Szeider
There are several methods for searching for graphs with prescribed properties, such as SAT solvers and specialized generators. These methods return the result as raw data: an adjacency matrix or a string encoding. The raw data certifies that the graph exists, but it does not reveal any structural properties of the graph. We ask whether one can automatically discover a short algebraic description if only this raw data is provided. We look for a description such as a Cayley graph Cay(Γ,S) or a lexicographic product C5[K3]. We address this question with a neurosymbolic approach. We propose an agent that runs on a general-purpose large language model with no fine-tuning or per-target training. The model interleaves reasoning with calls to the computer algebra system SageMath: it analyzes the target graph, proposes and tests candidate constructions, and revises them until the output matches the target. The agent communicates with SageMath through a Model Context Protocol (MCP) server, which we release as a general-purpose bridge. Whether a construction matches the target is checked by a single exact isomorphism test, and therefore rests on the symbolic side and not on the model. We test the approach on a benchmark of 100 highly symmetric graphs, namely two-orbit graphs on up to 25 vertices; the benchmark was fixed in advance. Our agent could find verified algebraic constructions for all of them, without falling back to raw encodings. A strong template-enumeration baseline reaches only about 20%, and a catalog lookup could not identify any of these graphs. However, construction quality declines when symmetry is removed. As a concrete application, we identify the smallest known counterexample to the Bernhart-Kainen dispersability conjecture, a 16-vertex graph that enumeration found as raw data. For this graph, our agent found an explicit algebraic construction.
Peter Bro Miltersen
In a finite recursive game in the sense of Everett, both players have stationary epsilon-optimal strategies for every epsilon>0. Frederiksen and Miltersen strengthened this result by showing that the strategies for all sufficiently small epsilon can be encoded by finitely many monomials: at every state, all but possibly one of the action probabilities are constants times integer powers of epsilon. The resulting finite symbolic object specifies a strategy for every sufficiently small accuracy. Their proof uses semialgebraic selection and Puiseux series. We give an alternative elementary proof of this regularity theorem for recursive games. We start with stationary strategies that guarantee vectors approaching the value through Everett's one-sided region. After fixing their support, we express, for each pure stationary reply, all absorption probabilities as quotients of directed-forest polynomials with nonnegative coefficients and a common positive denominator. Each payoff is a fixed signed linear combination of these quotients. We then compress the asymptotic orders of the finitely many forest monomials into one integer weight vector. This proof uses neither semialgebraic selection nor Puiseux series. Furthermore, for rational games with a fixed number N of active states, we present a deterministic polynomial-time algorithm that computes a monomial family exactly. It returns all algebraic coefficients in one ordered real univariate representation. The representation length and running time are at most L^{(N+1)^{O(N)}}, where L is the input length.
Ali Hamza Malik, Raja Hasnain Anwar, Muhammad Taqi Raza
Quantum Key Distribution (QKD) protocols provide information-theoretic security by using quantum mechanical principles. Yet QKD is fundamentally a hybrid protocol: its security depends on the correct integration of the quantum phase with classical post-processing. While ETSI and ITUT specifications standardize QKD architectures and interfaces, they evaluate protocol security in isolation, leaving cross-layer interactions as an underexplored attack surface. This paper introduces a formal verification framework that holistically models QKD protocols based on ETSI and ITUT QKD specifications. Our model is the first hybrid QKD protocol model that supports automated analysis of protocollevel security focusing on how classical operations influence the security guarantees provided by the quantum phase of the QKD protocol. We formalize a comprehensive symbolic model of QKD protocols, based on ETSI and ITU-T QKD specifications, in Tamarin, an automated protocol verifier. Applying this framework, we obtain formal evidence of three specification-level vulnerabilities in ETSI- and ITU-T-grounded protocol models under adversary Eve+: subverted entanglement injection, basis-deferred measurement, and message reflection. Each arises from a classical control-plane omission in the procedure text and is established under a symbolic abstraction rather than as a claim about all practical deployments. We introduce two protocol improvements: measurement commitment and identitybound message authentication codes (MACs). Tamarin verification confirms that these countermeasures eliminate the identified vulnerabilities under Eve+. We have communicated our results and recommendations to relevant standardization organizations.
Kazuki Tanaka
Matsumoto's algorithm for computing the radical of a polynomial ideal is generalized to the parametric setting within the framework of symbolic computation. The main tool is a comprehensive Gröbner system over a finite field, also known as a parametric Gröbner basis. As a result, an algorithm for computing the radical of a parametric ideal over a finite field is proposed.
Daniel Keren
The numerical bootstrap for quantum mechanics tests a candidate state's positivity only against sums of squares, whereas every physical state assigns nonnegative expectation to every pointwise nonnegative polynomial. In one dimension the two coincide; in two or more they do not. Whether this gap is realized depends sharply on which constraint set is imposed. For the stationary bootstrap, which imposes <[H,O]> = 0 and is the relaxation appropriate to thermal and mixed states, we exhibit a two-dimensional quartic double well and a moment vector that satisfies every level-three stationary constraint exactly, has a positive definite moment matrix, and yet assigns a negative expectation to a polynomial nonnegative on R^2; it is therefore the moment sequence of no state. All data are rational, and every step is verified in exact arithmetic. For the eigenstate bootstrap, which additionally imposes <OH> = E<O>, the same search finds no violation in any of five settings spanning two, three and five degrees of freedom and truncation levels three and four, tested against complete families of separating polynomials. The single exception occurs at a truncation so low that only one eigenstate constraint survives, and the theory presented here accounts for it. We identify the mechanism: the eigenstate constraints bound the high momentum moments, otherwise unbounded on the feasible set, and it is those unbounded directions that reach the region between the two cones. Finally, under the reflection symmetries of a typical potential the relevant obstruction is copositivity rather than nonnegativity, which, for the quartic witnesses available at the lowest truncation, places the first possible failure at five degrees of freedom. We conjecture that the eigenstate constraints imply an Archimedean-type bound on the momentum moments, and formulate the corresponding tightness statement.
Jonas Gann, Michael Gertz
Retrieval-augmented generation (RAG) improves question answering by grounding large language models (LLMs) in external knowledge such as text corpora. However, its reasoning process remains largely opaque: intermediate reasoning steps are difficult to verify and cannot be reliably attributed to specific evidence. Moreover, missing user-specific context is rarely detected systematically, often leading to incomplete or incorrect output. We propose NeSy-RAG, a modular neuro-symbolic RAG framework that synthesizes attributable Prolog modules from retrieved text chunks. For each chunk, the system generates semantically meaningful predicates that encode Boolean claims, which may depend on user facts. Using joint natural language-code embeddings, predicates are retrieved and composed into Prolog queries. To address incomplete user context, we introduce a symbolic knowledge-gap detection mechanism that identifies missing user facts whose truth values affect the query outcome and automatically triggers follow-up interactions. Executing the resulting Prolog queries yields deterministic answers together with transparent execution traces that link each reasoning step to its originating source. On the ShARC benchmark, without domain-specific training, NeSy-RAG achieves 61.1% accuracy, outperforming a same-model RAG baseline that achieves 42.8% accuracy.
Edward Liem, Clemens Dubslaff
Prime implicants (PIs) are central in computer science, with applications in logic minimization, diagnosis, explainable formal methods and AI. Algorithms for the computation of PIs were first-and-foremost considered on the full input space, not considering the case where the input space might be constrained by context or structural dependencies. To filter out those PIs that do not fulfill the constraints, existing methods rely on an explicit post-processing step after computing all PIs, which leads to scalability issues due to the number of PIs being exponential. We propose end-to-end symbolic algorithms that implicitly represent the set of PIs under side constraints. For this, we extend the prominent Coudert-Madre method based on decision diagrams and implement a modular tool chain that separates decision-diagram construction, PI computation, and filtering.
Roberto Aliaga Medina, Paulina Quintanilla, Antonio del Rio Chanona
Kinetic model discovery is a central challenge in chemical engineering, as accurate rate expressions are essential for understanding and controlling chemical and biological processes. Symbolic regression (SR) has emerged as a powerful data-driven approach for identifying interpretable kinetic models, but usually operates without domain knowledge, often exploring physicochemically implausible models. Large language models (LLMs) offer a promising avenue for injecting domain expertise into this search. Here, we introduce an LLM-guided SR framework, embedding an LLM module within an iterative SR algorithm for automated kinetic model discovery. The LLM performs two roles at each iteration: (1) a qualitative physicochemical critique of the best SR candidates, and (2) the proposal of new candidate rate expressions guided by the SR-generated models and embedded chemical knowledge. Our framework is evaluated on four in silico case studies of increasing complexity, spanning heterogeneous catalysis and bioprocess systems. Results show the LLM-guided framework reduces iterations to identify the ground-truth model by 41.7−79.3% versus a state-of-the-art SR framework, with the LLM directly proposing the correct model structure in over half of the guided runs. In practical settings, where each iteration typically requires a new wet-lab experiment, this translates into a substantial reduction in experimental effort. Predictive performance on an independent validation set is equivalent between both approaches, with R2>0.98 in all case studies. Ablation studies indicate that both the SR component and the LLM scale contribute to this performance, with a reduced-size LLM largely retaining discovery efficiency. These findings demonstrate that LLMs can effectively inject domain knowledge into scientific model discovery, paving the way toward fully automated, domain-aware kinetic modelling pipelines.
Hongbo Ma, Bangji Yang, Yunqian Selina Cheng +3
Large language models can derive a plausible mathematical object yet still violate explicit requirements--for example, by omitting a modular reduction, returning a non-integer, or using the wrong encoded answer form. We introduce Constraint-First Reasoning (CFR), a training-free two-stage prompting protocol: Stage 1 extracts and summarizes constraints entailed by the problem, and Stage 2 solves while checking intermediate and final results against that summary. Routed-CFR activates the two-stage protocol only when a text-only regex router detects restrictive cues; otherwise it uses direct chain-of-thought (CoT). Across AIME, CMIMC, BRUMO, and AIMO_AMC, the method improves direct CoT on multiple backbones. We further report convention-controlled routing experiments, matched prompting baselines, problem-level paired tests, decoding robustness, constraint-quality audits, total-token accounting, and an OlympiadBench evaluation. These analyses position CFR as a targeted test-time intervention whose benefit depends on recoverable constraints and reliable Stage 1 extraction, rather than as a general-purpose replacement for mathematical reasoning.
Soha Hussein, Stephen McCamant, Kelton OBrien +3
Symbolic execution plays a critical role in software reliability, as they are used to find bugs, generate test cases, and provide correctness guarantees, particularly for safety-critical systems. Yet their own correctness is rarely subject to formal scrutiny, as it is typically established empirically by evaluating tool behavior across many programs. This leaves open the possibility that the tools themselves introduce unsoundness, potentially invalidating the verification results they produce and undermining the very guarantees they are meant to provide. In this paper, we address this gap by providing the formal treatment of symbolic execution with path-merging, an optimization that improves path explosion by summarizing branching code regions into disjunctive constraints rather than exploring each path independently. Specifically, we target Java Ranger, a path-merging tool for Java programs that progressively transforms imperative Java code toward the language of formal logic through a series of code transformations. We formalize each of these transformations and prove their soundness with respect to a simplified version of the Java concrete semantics, establishing that Java Ranger's path-merging process preserves program semantics.
Xiaoxian Tang, Bican Xia, Tianqi Zhao
Given an algebraic statistical model, a challenging problem is classifying the data according to the number of positive critical points of the likelihood function. The positive critical points are the positive solutions to an algebraic system, say likelihood equations. So, identifying the number of positive critical points is a real root classification problem for the likelihood equations. A discriminant variety of a likelihood-equation system geometrically describes the data for which the number of real solutions becomes unusual. As an essential component of the discriminant variety, the nonproperness set collects the data such that the likelihood-equation system has a solution at infinity. So, the number of real solutions varies when the data passes the nonproperness set, and identifying the nonproperness set plays a crucial role in the real root classification. In this work, we develop a novel method for computing nonproperness sets of likelihood-equation systems. We prove the correctness of this method. We show experimentally that it is far more efficient than the known methods in the literature.
Itamar Nir
We give a deterministic algorithm for finding all integer roots of a square-free polynomial f∈Z[x] of degree n with ∥f∥∞<2b. The running time is O~(n3/2b), improving the O~(n2b) bound of Harvey and Hittmeir (Research in Number Theory, 2022). The algorithm follows the classical p-adic framework: find roots modulo a prime p, lift them modulo a high power of p, and verify the lifted candidates. The main new idea is to avoid searching for a prime for which fmodp is square-free. Instead, we find a prime for which the total multiplicity of repeated roots modulo p is small. This requires lifting repeated roots, which we handle using a weighted lifting tree. We also give a faster deterministic candidate-verification algorithm: given n candidate integers smaller in absolute value than 2b, we decide which are roots of f in O~(nb+min(n2,nb2)) bit operations. Together, these ingredients give the first deterministic subquadratic-in-n improvement for integer root finding in the square-free case.
M. Levent Doğan, Elias Tsigaridas, Zafeirakis Zafeirakopoulos
For a system of s homogeneous polynomials of degree d in n variables, say f=0, we consider the problem of constructing resultant systems. A resultant system is a finite set of polynomials in the coefficients of the input polynomials, the vanishing of which characterizes the systems f with a common non-zero solution. The classical approaches for constructing resultant systems rely either on maximal minors of large coefficient matrices or on the coefficients of a resultant of generic linear combinations of the input polynomials. Typically, they produce resultant systems containing a very large number of polynomials. We develop new constructions based on taking resultants of linear combinations of the input polynomials; this results in resultant systems of small cardinality. Our main results are: 1) We prove that a resultant system with (n−1d+n−1)s−n2+1 polynomials exists; each polynomial is the resultant of n linear combinations of the input polynomials. This improves the previously known upper bounds, even for systems of bivariate homogeneous polynomials. 2) Under the assumption that the input polynomials are non-zero, we construct explicit resultant systems with cardinality poly(s,d), when n is fixed.
Nick Palladinos
The matrix-multiplication SAT benchmark of Heule, Kauers, and Seidl asks, among other tasks, for solutions of ten known-satisfiable rank-23 formulas, proofs of unsatisfiability for ten formulas expected to be unsatisfiable, and a rank-23 scheme over F2 having a summand with no type-3 monomial. We give complete satisfying assignments for the 21 CNFs in the repository's top-level challenge1/, challenge2/, and challenge3/ directories at commit 150b2e2f. The principal finding is that all ten top-level Challenge-2 formulas are satisfiable. A direct audit shows that their hardcoded type-3 pairings are imposed by positive unit clauses on the 621 base variables: the formulas require selected incidences but do not forbid additional type-3 incidences. Starting from exact 23-summand schemes, we use the GL(3,2)3 isotropy action, cyclic trace symmetry, and perfect matching of transformed summands to constrained slots to construct witnesses for all ten files. For Challenge 3, we combine a locked semantic repair with a two-term identity over F2 to obtain a distinguished summand of type-3 count zero. Every semantic decomposition has zero residual in all 729 Brent equations. The accompanying DIMACS models assign all 26,541 variables of each formula and satisfy all 2,461,316 clauses across the 21 instances. A separate parser and clause evaluator rechecks the emitted models. A deterministic one-file Python reproducer regenerates the 21 certificates from the original CNFs in approximately nine seconds on the reported test host.
Jinhui Li, Beibei Xiong, Zhengfeng Yang
The Dittert conjecture states that the Dittert functional on nonnegative n×n matrices whose entries sum to n is uniquely maximized by the uniform matrix. We prove the conjecture in dimension 4. More precisely, let K4 be the simplex of nonnegative 4×4 real matrices whose entries sum to 4, let U4 be the uniform matrix, and let φ denote the Dittert functional. We establish 3261−φ(A)≥521∥A−U4∥F2 for every A∈K4. Consequently, U4 is the unique maximizer of φ on K4. The proof reduces the problem to an exact certification of the nonnegativity of a structured quartic polynomial in sixteen variables on a simplex. We develop a symbolic-numeric procedure for constructing an exact rational constrained sum-of-squares certificate. The procedure combines adaptive template selection with sequential rational recovery to handle singular Gram matrices and coupled SOS blocks arising from the constraint structure. The final certificate consists of a main SOS with 152 positively weighted rational squares and 136 smaller SOS blocks, each containing 16 such squares. Exact LDLT decompositions and coefficient comparison over Q certify the polynomial identity. The resulting exact certificate is formally verified using the Lean proof assistant.
Cosmin E. Oancea, Stephen M. Watt
We report on GPU implementations of block-level addition, subtraction, multiplication and division for midsize integers, with operands of 215 to 219 bits using the high-level functional language Futhark. Comparing with hand-written C++/CUDA versions and CGBN, we identify which functional constructs compile well, where memory placement and sequentialization are effective, and what compiler support is needed. The results show that high-level code can express the algorithms compactly while approaching competitive performance after certain compiler improvements. In particular, we find that automated placement of arrays in GPU register memory is critical for performance.
Jens Lehmann, Andrei Aioanei, Sahar Vahdati
ARC-AGI-3 turns abstraction into an interactive problem of skill acquisition. A player must infer an unfamiliar game's rules, hidden state, and goal while maintaining action efficiency because every move counts. We formalize these environments as parameterized rendered deterministic Moore machines and introduce Tycho, a coding-agent system that constructs and uses game-specific models during interaction. Tycho separates actionable observations from intermediate animation, level-completion, and game-over frames. From this structured history, an agent can model, test, plan with, repair, or bypass a free-form executable hypothesis. In one matched public-set run per policy, we compare four orchestration policies on all 25 public games using Claude Opus 4.8 under matched inference budgets. Actor-requested delegation to a model builder obtains the highest observed mean Relative Human Action Efficiency (RHAE), 88.49. With this selected policy, GPT-5.6 Sol and Opus 5 both reach 100.00 RHAE and complete all 183 levels. Their game-balanced first-run human-replay midranks are 98.5 and 100.0. Opus 5 uses 61% fewer scored actions than the aggregate official human baselines. Automatic repair after verification failures produces models that reproduce observed transitions much more accurately, yet reaches only 83.07 RHAE. Transition match indicates whether a simulator reproduces observed dynamics, not whether it has identified the objective or improves the next action. Strong play also requires deciding when to construct, repair, use, or bypass a model. We call this joint problem active abstraction: generating a testable model from costly interaction and deciding when acquiring or using it is worth its cost.
Stephan Schulz
In saturation-based theorem proving, selecting the next clause for processing is a major concern. Twee has successfully applied the idea of preferring clauses that share terms with the conjecture by adding equational definitions to transform the problem. In this paper, we apply the idea to the full first-order case, and offer an alternative implementation based on shared terms. Both approaches have complementary applications and show very promising results.