https://arxiv.org/api/d6Lf8LB0pH2HIUc/NDZmZ4kCN9A 2026-06-13T16:15:50Z 3138 75 15 http://arxiv.org/abs/2602.15603v2 2026-04-27T17:59:03Z

Models based on partial differential equations (PDEs) are powerful for describing a wide range of complex phenomena in the natural sciences. Accurately identifying the PDE model, which represents the underlying physical law, is essential for a proper understanding of the problem. This reconstruction typically relies on indirect and noisy measurements of the system's state and, without specifically tailored methods, rarely yields symbolic expressions, thereby limiting interpretability. In this work, we address this limitation by considering neural network architectures based on rational functions for the symbolic representation of physical laws. These networks combine the approximation power of rational functions with the flexibility to represent arithmetic operations, and generalize ParFam and EQL-type architectures used in symbolic regression for physical law learning. We further establish regularity results for these symbolic networks. Our main contribution is a reconstruction result showing that, if there exists an admissible physical law that is expressible within the symbolic network architecture, then in the limit of noiseless and complete measurements, symbolic networks recover a physical law within the PDE model that is representable by the architecture. Moreover, the recovered law corresponds to a regularization-minimizing parameterization, promoting interpretability and sparsity in case of $L^1$-regularization. Under an additional identifiability condition, the unique true physical law is recovered. These reconstruction and regularity results are derived at the continuous level prior to discretization due to a formulation in function space. Empirical results using the ParFam architecture are consistent with the theoretical findings and suggest the feasibility of reconstructing interpretable physical laws in practice.

2026-02-17T14:20:36Z Erion Morina Philipp Scholl Martin Holler http://arxiv.org/abs/2604.24504v1 2026-04-27T14:07:27Z

Equivalence checking of quantum circuits is a central verification task in quantum computing, ensuring the correctness of circuit optimizations, hardware mappings, and compilation pipelines. Among the primary symbolic methods for this purpose, the path-sum formalism provides a compact representation with powerful reduction rules that yield a canonical form for the classically simulable Clifford fragment, but confluence fails beyond the Clifford fragment. We introduce a new weighted model counting (WMC) encoding for path-sums and combine it with the existing path-sum reductions to obtain a verifier that is both complete and efficient. Our method applies reductions whenever possible and invokes the WMC-based decision procedure on the residual path-sum, yielding a complete semantic check up to a global phase. We implement the approach and evaluate it on standard benchmarks. Results show that the hybrid method outperforms either component in isolation and competes with state-of-the-art tools.

2026-04-27T14:07:27Z TACAS 2026 Wei-Jia Huang Christophe Chareton Yu-Fang Chen Kai-Min Chung Min-Hsiu Hsieh Alfons Laarman Jingyi Mei 10.1007/978-3-032-22749-2_21 http://arxiv.org/abs/2604.24379v1 2026-04-27T12:10:06Z

Safety-critical applications are required to perform as expected in normal operations. Image processing functions are often required to be insensitive to small geometric perturbations such as rotation, scaling, shearing or translation. This paper addresses the formal verification of neural networks against geometric perturbations on their image dataset. Our method Super-DeepG improves the reasoning used in linear relaxation techniques and Lipschitz optimization, and provides an implementation that leverages GPU hardware. By doing so, Super-DeepG achieves both precision and computational efficiency of robustness certification, to an extent that outperforms prior work. Super-DeepG is shared as an open-source tool on GitHub.

2026-04-27T12:10:06Z ICCPS / HSCC 2026, CPS IoT Week, May 2026, Saint Malo (Palais du Grand Large), France Noémie Cohen Airbus CR\&T Mélanie Ducoffe Airbus CR\&T Christophe Gabreau Claire Pagetti Xavier Pucel http://arxiv.org/abs/2604.23972v1 2026-04-27T02:35:10Z

Knowledge graphs (KGs) are increasingly used to support large lan guage model (LLM) reasoning, but standard triplet-based KGs treat each relation as globally valid. In many settings, whether a relation should count as evidence depends on the context. We therefore formulate triplet validity as a triplet-specific function of context and refer to this formulation as a Quantum Knowledge Graph (QKG). We instantiate QKG in medicine using a diabetes-centered PrimeKG subgraph, whose 68,651 context-sensitive relations are further annotated with patient-group-specific constraints. We evaluate it in a reasoner--validator pipeline for medical question answering on a KG-grounded subset of MedReason containing 2,788 questions. With Haiku-4.5 as both the Reasoner and the Validator, KG-backed validation significantly improves over a no-validator baseline ($+0.61$ pp), and QKG with context matching yields the largest gain, outperforming both KG validation without context matching ($+0.79$ pp) and the no-validator baseline ($+1.40$ pp; paired McNemar, all $p<0.05$). Under a stronger validator (Qwen-3.6-Plus), the raw QKG gain over the no-validator baseline grows from $+1.40$ pp to $+5.96$ pp; the context-matching gap is non-significant ($p=0.73$) on the raw set but becomes borderline significant ($p=0.05$) after adjustment for knowledge leakage and suspicious questions, consistent with a benchmark-gold ceiling rather than a QKG limitation. Taken together, the results support the view that the value of a KG in LLM-based clinical reasoning lies not merely in storing medically related facts, but in representing whether those facts are applicable to the specific patient context. For reproducibility and further research, we release the curated QKG datasets and source code.\footnote{https://github.com/HKAI-Sci/QKG}

2026-04-27T02:35:10Z 15 pages main text, 6 pages appendix, 5 figures, preprint Yao Wang Zixu Geng Jun Yan http://arxiv.org/abs/2604.23893v1 2026-04-26T21:35:19Z

The binary EML operator yields all (transcendental) elementary functions by recursive application, or a binary tree. The structure of the operator itself carries two distinct ingredients: that of an abelian group, and of functional inverse, which reveal a constructive path to many distinct functional families.

2026-04-26T21:35:19Z 5 pages Tomasz Stachowiak http://arxiv.org/abs/2401.00109v3 2026-04-26T21:20:28Z

As time-series applications grow larger, there is increasing demand for symbolic representations that are compact, accurate, and scalable across many signals and computing resources. Current ABBA-based symbolic approximation methods produce high-quality, shape-preserving representations, but they handle each time series separately and sequentially. This means they do not ensure consistent symbols across different series and cannot fully exploit modern multicore systems and distributed-memory systems. This paper presents a joint symbolic time-series approximation method for large-scale time series. The proposed method decouples local compression from global digitization: (i) time series are partitioned into independent domains that can be compressed in parallel, and (ii) the resulting pieces are digitized using a shared global dictionary. To further improve scalability, we introduce a two-stage parallel digitization scheme, in which aggregation is first performed locally and then merged globally without requiring a full-data reassignment step. Extensive experiments on time-series datasets and large synthetic benchmarks show that our approach maintains competitive reconstruction quality while substantially reducing runtime. These results show that joint symbolic approximation can serve as an efficient, high-level parallel tool for analyzing large-scale temporal data.

2023-12-30T01:16:22Z Xinye Chen http://arxiv.org/abs/2604.22673v1 2026-04-24T15:49:50Z

Equivalence class partitioning is a well-established test design technique mandated by safety standards such as ISO~26262 for systematic testing of safety software. In industrial practice, however, its application to legacy undocumented embedded firmware is often hindered by incomplete or outdated functional specifications. This paper proposes a binary-level methodology for inferring output-oriented equivalence classes directly from compiled firmware, without relying on source-level annotations or external documentation. The approach combines control-flow reconstruction and guided symbolic execution to analyze individual functions and group execution paths according to indistinguishable observable behavior, including return values and output parameters. An optional post-processing step produces human-readable representations to support comprehension and documentation. The methodology is evaluated in an industrial automotive context through a practitioner-based study assessing correctness and interpretability. Results indicate strong alignment with expert expectations and a positive perception of readability and usefulness for supporting function understanding and test design. These findings demonstrate the feasibility and practical relevance of binary-level equivalence class inference for systematic testing of legacy undocumented safety-embedded software.

2026-04-24T15:49:50Z Paper Accepted at EASE 26 Marco De Luca Domenico Francesco De Angelis Domenico Amalfitano Pasquale Cimmino Anna Rita Fasolino http://arxiv.org/abs/2604.22256v1 2026-04-24T05:58:30Z

Goal recognition aims to infer an agent's goal from observations of its behaviour. In realistic settings, recognition can benefit from exploiting hierarchical task structure and reasoning under uncertainty. Planning-based goal recognition has made substantial progress over the past decade, but to the best of our knowledge no existing approach jointly integrates hierarchical task structure with probabilistic inference. In this paper, we introduce the first planning-based probabilistic framework for hierarchical goal recognition over Hierarchical Task Networks (HTNs). We instantiate the framework by exploiting an HTN planner with a three-stage generative model for likelihood estimation, yielding posterior distributions over goal hypotheses. Empirical results show improved recognition performance over the existing HTN-based recognizer on HTN benchmarks. Overall, the framework lays a foundation for probabilistic goal recognition grounded in hierarchical planning structure, moving goal recognition toward more practical settings.

2026-04-24T05:58:30Z Accepted by KR 2026 Chenyuan Zhang Katherine Ip Hamid Rezatofighi Buser Say Mor Vered http://arxiv.org/abs/2604.21961v1 2026-04-23T16:03:12Z

Optimization problems are fundamental in diverse fields, such as engineering, economics, and scientific computing. However, current algorithms are mostly designed for specific problem types and exhibit limited generality in solving multiple types of optimization problems. To enhance generality, we propose an automated reduction method named OP-to-MaxSAT reduction and a general optimization solver based on OP-to-MaxSAT reduction (GORED). GORED unifies the solving of multiple types of optimization problems by reducing the problems from optimization problems to MaxSAT instances in polynomial time and solving them using the state-of-the-art MaxSAT solver. The generality and solution quality of GORED are validated through experiments on 136 instances across 11 types of optimization problems. Experimental results demonstrate that GORED not only successfully solves a wide range of optimization problems but also yields solutions comparable in quality to those from existing methods, with no statistically significant differences observed. By introducing automated reduction, this work shifts the paradigm of optimization solvers from designing specialized algorithms for each problem type to employing a single algorithm for diverse problems. As a result, advances in this single algorithm can now drive progress in a wide range of optimization problems across various domains.

2026-04-23T16:03:12Z Yuxin Zhao Han Huang Zhifeng Hao http://arxiv.org/abs/2604.18792v2 2026-04-23T12:23:22Z

Model transformations are central to MDE, but formal verification is difficult because mainstream transformation languages are undecidable. DSLTrans was designed to be Turing-incomplete to improve verifiability, yet earlier verification based on path-condition enumeration still suffered exponential blow-up and did not scale to realistic cases. We present a tractable verification workflow for DSLTrans and formalize when it is complete. The method combines three contributions: (i) a Cutoff Theorem proving that bounded model checking is complete for a precise DSLTrans fragment and positive existence/traceability properties, turning an infinite search into a finite computable bound; (ii) composable, soundness-preserving optimizations (per-class bounds, CEGAR-based fragment verification, and trace-aware dependency analysis) that reduce SMT encoding size; and (iii) a Z3-based implementation evaluated on realistic transformations from the ATL Zoo and related benchmarks. On 29 concrete transformations and 899 properties spanning compiler lowering, schema translation, behavioral modeling, graph mapping, and stress tests, 552 properties are proved, 345 produce concrete counterexamples (including intentional negative and boundary cases), and only 2 remain undecided within timeout. For properties beyond the tractability budget, we introduce tractability-driven refinement (precondition specialization, postcondition decomposition, and transformation instrumentation), achieving up to 112x speedup while eliminating spurious counterexamples. The workflow is supported by a web IDE and a concrete execution engine for runtime validation.

2026-04-20T19:57:45Z 41 pages, 4 figures Levi Lucio http://arxiv.org/abs/2505.08149v4 2026-04-21T09:24:59Z

Inequalities among symmetric functions are fundamental in various branches of mathematics, thus motivating a systematic study of their structure. Majorization has been shown to characterize inequalities among commonly used symmetric functions, except for complete homogeneous symmetric functions (shortened as CHs). In 2011, Cuttler, Greene, and Skandera posed a natural question: Can majorization also characterize inequalities among CHs? Their work demonstrated that majorization characterizes inequalities among CHs up to degree 7 and suggested exploring its validity for higher degrees. In this paper, we show that, for every degree greater than 7, majorization does not characterize inequalities among CHs.

2025-05-13T00:51:14Z 15 pages European Journal of Combinatorics (2026) Jia Xu Yong Yao 10.1016/j.ejc.2026.104389 http://arxiv.org/abs/2604.19227v1 2026-04-21T08:34:14Z

We introduce SignatureTensors.jl, a new package for computing signature tensors of paths in julia. We present its core functionality and demonstrate its use through illustrative examples. The package is compatible with the computer algebra system OSCAR, enabling both exact and numerical computations with signatures.

2026-04-21T08:34:14Z Gabriel Riffo Leonard Schmitz http://arxiv.org/abs/2604.17275v1 2026-04-19T06:07:47Z

Stochastic constraints, which incorporate both deterministic parameters and random variables, extend classical deterministic constraints by explicitly accounting for uncertainty. These constraints are increasingly prevalent in data science, artificial intelligence, and bioinformatics; however, solving them requires addressing quantitative satisfaction problems that remain a significant challenge in computer science. In this paper, we propose a novel framework for deciding deterministic parameters that maximize the satisfaction probability. Our approach features a unique synergy between stochastic optimization and symbolic techniques: at the high level, it employs \emph{oracle-based stochastic gradient descent} to identify high-quality parameter candidates, while at the low level, it utilizes \emph{interval arithmetic} to compute rigorously certified lower bounds. This framework produces a sequence of sound and increasingly tight lower bounds for the true maximum satisfaction probability, supported by a high-probability convergence guarantee. We demonstrate the effectiveness and efficiency of our approach through its application to Stochastic Satisfiability Modulo Theories (SSMT) problems and a stochastic trajectory planning task.

2026-04-19T06:07:47Z Xiakun Li Hao Wu Bican Xia Tengshun Yang Naijun Zhan http://arxiv.org/abs/2604.16232v1 2026-04-17T16:46:23Z

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 Karin Yu Eleni Chatzi Georgios Kissas http://arxiv.org/abs/2604.15402v1 2026-04-16T14:09:50Z

Classical symbolic protocol verification under Dolev--Yao uses binary attacker knowledge (known/unknown). This abstraction misses cumulative side-channel settings, where repeated noisy observations progressively improve attacker knowledge. We model this process with a graded attacker view \(μ_K\in[0,1]\), product T-norm leak updates, and finite-grid explicit-state execution in Modified Murphi. The method is optimised with exact concept-lattice attribute reducts and exposes threshold-driven safe-to-fail transitions that are not represented in corresponding binary runs under the same bounded assumptions. Executed results on symmetric and asymmetric protocols, including Needham--Schroeder--Lowe (NSL), show that baseline models passing under crisp semantics can fail once cumulative side-channel leakage is enabled.

2026-04-16T14:09:50Z Murat Moran