https://arxiv.org/api/LYppmoN0TriHBHKcUfEKDwFr7v4 2026-09-10T19:11:45Z 3239 45 15 http://arxiv.org/abs/2604.08849v3 2026-08-11T03:23:53Z

Many real-world retrieval and matching problems require more than topical relevance: a candidate must satisfy the specific constraints of one profile among many, not just be relevant to it. Clinical trials are a high-stakes instance of this challenge: they are central to evidence-based medicine, yet many struggle to meet enrollment targets, despite the availability of over half a million trials listed on ClinicalTrials.gov, which attracts approximately two million users monthly. Existing retrieval techniques, largely based on keyword and embedding-similarity matching, treat eligibility constraints as soft signals rather than binding requirements, resulting in low recall, low precision, and limited interpretability. We propose SatIR, a scalable, efficient, high-precision, high-recall, interpretable clinical trial retrieval method based on formal constraint satisfaction. Leveraging established medical ontologies, we use Large Language Models (LLMs) to convert informal reasoning -- regarding ambiguity, implicit clinical assumptions, and incomplete patient records -- into explicit, precise, controllable, and interpretable formal Satisfiability Modulo Theories (SMT) constraints. For scalable and efficient retrieval, we project the SMT matching problem onto relational algebra, enabling an efficient database implementation that retains high recall while sacrificing little precision. SatIR consistently improves eligibility-aware retrieval over similarity-based baselines on the SIGIR 2016 dataset and a benchmark derived from TREC 2022. Relative to TrialGPT-style retrieval, SatIR retrieves 32%-72% more relevant-and-eligible trials per patient on SIGIR 2016 and achieves 1.8-3.2x higher eligible-trial recall on the TREC benchmark. Retrieval is fast, requiring only 146 milliseconds per patient over 3,621 SIGIR trials.

2026-04-10T01:13:44Z Zikai Zhou Yufei Jin Yilin Xu Yu-Chiang Wang Chieh-Ju Chao Monica S. Lam http://arxiv.org/abs/2607.29191v2 2026-08-10T15:18:42Z

The Dittert conjecture states that the Dittert functional on nonnegative $n\times n$ matrices whose entries sum to $n$ is uniquely maximized by the uniform matrix. We prove the conjecture in dimension $4$. More precisely, let $K_4$ be the simplex of nonnegative $4\times4$ real matrices whose entries sum to $4$, let $U_4$ be the uniform matrix, and let $φ$ denote the Dittert functional. We establish $\frac{61}{32}-φ(A)\ge \frac{1}{52}\|A-U_4\|_F^2$ for every $A\in K_4$. Consequently, $U_4$ is the unique maximizer of $φ$ on $K_4$. 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 $LDL^T$ decompositions and coefficient comparison over $\mathbb{Q}$ certify the polynomial identity. The resulting exact certificate is formally verified using the Lean proof assistant.

2026-07-31T09:12:45Z Jinhui Li Beibei Xiong Zhengfeng Yang http://arxiv.org/abs/2508.04081v2 2026-08-10T01:18:43Z

Let $A_0,A_1\in\mathbf{F}^{n\times n}$ be square matrices over a finite field $\mathbf{F}$ and consider the matrix pencil $A_0+yA_1$ with indeterminate $y$. We observe that, once $A_0+λA_1$ is nonsingular for some $λ\in\mathbf{F}$, the polynomial $\det(A_0+yA_1)$ can be reconstructed by computing one determinant, one inverse matrix, and the characteristic polynomial of a single matrix. Consequently, this determinant polynomial can be computed in $\mathrm{O}(n^ω)$ field operations, avoiding the polylogarithmic overhead of a general polynomial-matrix determinant algorithm in this special setting. Applying this observation to random evaluation of the Tutte matrix of a graph, we obtain a matrix-multiplication-time randomized algorithm for the so-called exact matching problem. Specifically, one can decide, simultaneously for all $k$, whether a given $0/1$-weighted graph has a perfect matching of weight exactly $k$ in $\mathrm{O}(n^ω)$ field operations, where $n$ denotes the number of vertices in the graph. We also discuss the analogous extension to the exact linear matroid parity problem and its consequences for a perfect packing of Mader's $\mathcal{S}$-paths of minimum total length and for a shortest cycle through three specified vertices.

2025-08-06T04:51:07Z 20 pages Ryotaro Sato Yutaro Yamaguchi http://arxiv.org/abs/2608.04513v2 2026-08-09T10:41:13Z

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.

2026-08-05T06:49:28Z Address review comments, update affliations Soha Hussein Favonia Stephen McCamant Favonia Kelton OBrien Favonia Kuen-Bang Hou Favonia Michael Whalen Vaibhav Sharma http://arxiv.org/abs/2608.08118v1 2026-08-08T13:07:51Z

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 $\mathrm{Cay}(Γ, S)$ or a lexicographic product $C_5[K_3]$. 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.

2026-08-08T13:07:51Z David Seka Stefan Szeider http://arxiv.org/abs/2608.08017v1 2026-08-08T08:55:35Z

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.

2026-08-08T08:55:35Z 49 pages Peter Bro Miltersen http://arxiv.org/abs/2608.07626v1 2026-08-07T10:18:05Z

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.

2026-08-07T10:18:05Z Ali Hamza Malik Raja Hasnain Anwar Muhammad Taqi Raza http://arxiv.org/abs/2608.07058v1 2026-08-07T10:07:41Z

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.

2026-08-07T10:07:41Z 14 pages Kazuki Tanaka http://arxiv.org/abs/2608.06292v1 2026-08-06T17:16:28Z

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.

2026-08-06T17:16:28Z Jonas Gann Michael Gertz http://arxiv.org/abs/2608.05943v1 2026-08-06T12:10:09Z

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.

2026-08-06T12:10:09Z Edward Liem Clemens Dubslaff http://arxiv.org/abs/2608.05120v1 2026-08-05T17:48:45Z

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 $R^2>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.

2026-08-05T17:48:45Z Roberto Aliaga Medina Paulina Quintanilla Antonio del Rio Chanona http://arxiv.org/abs/2608.05254v1 2026-08-05T16:18:41Z

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.

2026-08-05T16:18:41Z 53 pages, 5 figures, 36 tables Hongbo Ma Bangji Yang Yunqian Selina Cheng Jiajun Fan Hanwen Zhang Ge Liu http://arxiv.org/abs/2606.07321v2 2026-08-05T13:10:14Z

We present a novel S-pair selection strategy called Homogeneity Entropy, for deciding the sequence of S-polynomials to construct in Buchberger's algorithm to compute a Groebner basis. The strategy uses an information theoretic measure derived from the distribution of degrees among the monomials of the S-polynomial: a very different approach to the classical heuristics such as Degree, Normal and Sugar, or indeed the more recent machine learning approaches to the problem. We implement this strategy and evaluate it on two different datasets: (1) variations of randomly generated polynomial systems with controlled numbers of variables, degrees, densities and number of polynomials per system; and (2) the PHCpack benchmark dataset sourced from real world problems. The Homogeneity Entropy strategy significantly outperforms classical strategies on random polynomial datasets, but on the PHCpack dataset the classical strategies perform better. This suggests the right strategy varies with the shape of the data and we explore this in several experiments. The new strategy offers practically meaningful gains on certain distributions, and represents the first use of such information-theoretic guidance in the optimisation of symbolic computation algorithms.

2026-06-05T14:39:35Z Uzma Shafiq Matthew England AmirHosein Sadeghimanesh Nayyar Zaidi http://arxiv.org/abs/2607.03376v2 2026-08-05T07:50:50Z

The Richelot $(2,2)$-step is the standard step of explicit genus-2 isogeny computation. We determine the exact stratification of its input space over a finite field $\mathbb{F}_q$ of odd characteristic: ordered factorizations $f=uvw$ of a square-free sextic into monic quadratics fall into three strata by the geometric type of the quotient, governed by the incidence geometry of the discriminant locus. This yields closed formulas for each stratum and, modulo affine coordinate changes, mass formulas of degree four in $q$ with a complete classification of stabilisers. The classification is decided by data the step already computes, at $5\mathrm{M}+6\mathrm{S}$ beyond the brackets, and an output post-check is provably redundant. On the decomposable stratum the square class of one resultant determines the field of definition of the elliptic factors and the shape of the Weil polynomial of the Jacobian; the two cases are counted exactly, and in the nonsplit case the curve $y^2=f$ has $q+1$ rational points. Exhaustive enumeration over small finite fields verifies every proved count.

2026-07-03T14:29:46Z Substantially revised and extended; supersedes v1, then titled "Derivative-free Richelot isogenies via subresultants with algebraic certification". Corrects v1 and adds exact stratification counts, affine mass formulas with a full stabiliser classification, and the base-field arithmetic of the decomposable stratum. 46 pages; verification scripts included as ancillary files Hung T. Dang Diep V. Nguyen http://arxiv.org/abs/2602.03592v3 2026-08-04T15:40:40Z

Transcendental Liouvillian extensions are differential fields, in which one can model poly-logarithmic, hyperexponential, and trigonometric functions, logarithmic integrals, and their (nested) rational expressions. For such an extension, we construct, over the subfield of constants, a complement of the subspace of derivatives, and develop an algorithm that decomposes any element of the field into the sum of a derivative and a component lying in the complement. Consequently, an element is a derivative if and only if its complementary component vanishes. Moreover, the algorithm enables us to determine elementary integrability over the extension by computing parametric logarithmic parts, and leads to a reduction-based approach to constructing telescopers for elements in the extension, provided that an a priori order bound is given.

2026-02-03T14:43:48Z 49pages Shaoshi Chen Hao Du Yiman Gao Hui huang Wenqiao Li Ziming Li