https://arxiv.org/api/d6Lf8LB0pH2HIUc/NDZmZ4kCN9A 2026-09-10T21:18:40Z 3239 75 15 http://arxiv.org/abs/2607.23622v1 2026-07-26T12:12:06Z

Engineered Complete Intersections (ECI's) are a class of sparse polynomial systems frequently arising in a number of contexts, both in pure mathematics (e.g. enumerative geometry) and applications (e.g. chemical reaction networks). Based on theoretical results given by the first author, we give several contributions. First we give a new effective technique to tropicalize such systems by generalizing the classical notion of mixed subdivisions introduced by Huber and Sturmfels (1995) to ECI's with the particular goal to efficiently count solutions of square systems of equations in ECI form. We further design a tropical homotopy continuation algorithm for computing such mixed subdivisions, inspired by Jensen (2016), Malajovich (2017) and Daisey and Ren (2024). Our techniques can be used to numerically solve such systems by coupling them with the algorithms introduced by Helminck, Henriksson and Ren (2024). Finally, we give an algorithm to compute Newton polytopes of eliminants of ECI's. This gives a new way to compute, for example, Newton polytopes of so-called $A$-discriminants. Coupled with evaluation-interpolation paradigms our algorithm gives an efficient approach to compute such eliminants. We implemented our algorithms in the form of a software package which we use to demonstrate their practical feasibility on a range of examples.

2026-07-26T12:12:06Z 34 pages, 1 figure Alexander Esterov Rafael Mohr Yulia Mukhina http://arxiv.org/abs/2501.08561v5 2026-07-25T18:09:57Z

Digital twins are increasingly used to monitor and optimize industrial systems, yet many existing frameworks remain difficult to interpret, slow to adapt, and limited in their ability to incorporate explicit domain knowledge. This paper presents ANSR-DT, an adaptive neuro-symbolic framework that unifies temporal anomaly detection, symbolic reasoning, and reinforcement-learning-based decision support within a single digital twin pipeline. ANSR-DT combines a CNN-LSTM model for multivariate pattern recognition with Prolog-based reasoning that converts learned signals into explicit rules, enabling transparent diagnoses and traceable decision paths. A PPO-based adaptation layer further refines operational responses under changing conditions while preserving interpretability. Experiments against eight baselines show that ANSR-DT delivers competitive predictive performance together with stable rule extraction, scalable symbolic reasoning, and actionable explanations. Additional validation on the Skoltech Anomaly Benchmark (SKAB) further indicates that the framework transfers beyond synthetic settings. These findings position ANSR-DT as a practical foundation for trustworthy, adaptive, and explainable industrial digital twins.

2025-01-15T04:04:57Z Code available at https://github.com/sbhakim/ansr-dt Safayat Bin Hakim Muhammad Adil Alvaro Velasquez Houbing Herbert Song http://arxiv.org/abs/2607.23019v1 2026-07-25T03:24:05Z

Chain-of-thought (CoT) prompting enables large language models (LLMs) to tackle multi-step reasoning tasks, yet the generated intermediate steps are not guaranteed to be logically sound. We present Reason Popper-ly, a neurosymbolic framework that uses inductive logic programming (ILP) to learn relation composition rules from reasoning traces and deploys them as an online verifier for step-level correction. Given an LLM-generated trace, the method checks each inferred step against the learned rule table, diagnoses the violation type, rewrites incorrect steps with symbolically derived repairs, and regenerates the remaining suffix so that the model can produce its final answer conditioned on a verified trace. We evaluate on CLUTRR, a multi-hop kinship reasoning benchmark, using five language models over reasoning chains of 2 to 10 hops. Across all models, Reason Popper-ly consistently improves terminal accuracy over standard CoT, with gains of up to 48 percentage points for small models and 15 points for frontier models on the longest chains. Compared with a fully exogenous symbolic pipeline, our method performs better on harder instances by preserving the model's successful grounding while correcting only verifiable reasoning failures. In addition, step-level ILP verification yields a fine-grained error taxonomy that provides diagnostic insight beyond final-answer accuracy.

2026-07-25T03:24:05Z Accepted at the 20th Conference on Neurosymbolic Learning and Reasoning Zirong Chen Meiyi Ma http://arxiv.org/abs/2607.22947v1 2026-07-24T23:17:23Z

A formal model enables verifying reachability, localizing an outage, or anticipating the blast radius of a change. Yet, virtually no production network has one, since writing a model by hand demands rare expertise and is hard to keep current as the network changes frequently. At its core, network modeling is a typographical exercise: it translates network artifacts (e.g., configurations, topology, and routing state) into rules in formal logic. Translation of this kind is what large language models (LLMs) nowadays do well. Unlike free-form AI reasoning, such translation can be formally verified. Once modeling is no longer the bottleneck, trusting AI to reason over large, complex networks no longer makes sense. Our position therefore cuts against the prevailing race to put autonomous AI agents in charge end-to-end. We instead confine AI to translation and rely on a solver for reliable long-horizon reasoning, building a reusable formal model of general network behavior that can then be specialized to specific tasks, e.g., root-cause analysis (RCA). We build TypoNet that constructs and validates a symbolic model of an emulated production-scale WAN from the network's own artifacts. Our preliminary evaluation shows TypoNet helps in two ways. On its own, TypoNet answers operational questions (e.g., reachability verification and change-impact analysis) faster, more cheaply, and more reliably than an LLM. As a tool for an AI agent, TypoNet boosts fault localization at lower cost. The result makes the case for AI that builds verifiable network models and relies on a solver for reliable long-horizon reasoning.

2026-07-24T23:17:23Z 8 pages, 3 figures, 1 table Hongyu Hè Maria Apostolaki http://arxiv.org/abs/2607.22944v1 2026-07-24T23:07:31Z

Invariants, the relations expected to hold among measured signals of a network, underpin applications from verification to traffic generation, telemetry imputation, and input validation, yet writing them by hand demands rare expertise in both formal logic and networking. Automatic miners can help but fall short on two fronts: they still require the hardest input (the grammar of admissible invariants) and they learn only exact, ``hard'' rules, struggling with real-world approximation caused by inherent noise in data. LLMs are tools that can provide semantic reasoning over data, but are non-deterministic and opaque in their learning. Our key idea is to partition the invariant search problem into an AI-driven grammar ``discovery'' problem, followed by a statistics-driven ``search'' problem within the learned grammar. Taken together, this allows non-deterministic, hallucination-prone AI to help produce auditable invariants with formal guarantees. We design and implement such a system, Autogram, and evaluate it on both public and production telemetry data, recovering expert-derived invariants with high coverage and low false positives. We close with discussion on open problems on the path toward fully open-ended discovery.

2026-07-24T23:07:31Z 8 pages, 4 figures, 1 table Hongyu Hè Alexander Krentsel Sylvia Ratnasamy Maria Apostolaki http://arxiv.org/abs/2601.13731v2 2026-07-24T15:55:39Z

Symbolic computation, powered by modern computer algebra systems, has important applications in mathematical reasoning through exact deep computations. The efficiency of symbolic computation is largely constrained by such deep computations in high dimension. This creates a fundamental barrier on labelled data acquisition if leveraging supervised deep learning to accelerate symbolic computation. Cylindrical algebraic decomposition (CAD) is a pillar symbolic computation method for reasoning with first-order logic formulas over reals with many applications in formal verification and automatic theorem proving. Variable orderings have a huge impact on its efficiency. Impeded by the difficulty to acquire abundant labelled data, existing learning-based approaches are only competitive with the best expert-based heuristics. In this work, we address this problem by designing a series of intimately connected tasks for which a large amount of annotated data can be easily obtained. We pre-train a Transformer model with these data and then fine-tune it on the datasets for CAD ordering. Experiments on publicly available CAD ordering datasets show that on average the orderings predicted by the new model are significantly better than those suggested by the best heuristic methods.

2026-01-20T08:40:35Z Rui-Juan Jing Yuegang Zhao Changbo Chen http://arxiv.org/abs/2607.21205v1 2026-07-23T11:21:06Z

The formal analysis of real-time systems must address two dimensions of infiniteness: an unbounded number of agents and messages, and a potentially infinite state space induced by dense time. We present a novel narrowing-based verification method that deals with both dimensions. Our approach integrates (i) rewriting modulo SMT for symbolic representation of timing constraints, (ii) narrowing with logical variables to reason about systems with an unknown number of agents, and (iii) a constraint store over partially instantiated terms, in the style of constraint logic programming. We further introduce a folding mechanism that, under certain conditions, ensures termination of the symbolic analysis. The method has been implemented as an extension of the Maude rewriting engine. We evaluate the approach by verifying the correctness of a timed mutual exclusion protocol without imposing bounds on the number of participating processes. Moreover, we show that the framework uniformly supports the analysis of other real-time models, including parametric timed automata with unspecified components that our method can synthesize. Our results suggest that the proposed framework provides a sound and expressive basis for the symbolic verification of real-time rewrite theories.

2026-07-23T11:21:06Z In Proceedings ICLP 2026, arXiv:2607.17707 EPTCS 450, 2026, pp. 430-443 Santiago Escobar VRAIN, Universitat Politècnica de València, Spain Raúl López-Rueda VRAIN, Universitat Politècnica de València, Spain Carlos Olarte LIPN, CNRS UMR 7030, Université Sorbonne Paris Nord, France 10.4204/EPTCS.450.31 http://arxiv.org/abs/2607.21202v1 2026-07-23T11:20:15Z

Hybrid MKNF knowledge bases under the well-founded semantics integrate Description Logics with Logic Programming. However, they do not support classical negation in the rule component, limiting their ability to represent explicit negative knowledge. This limitation is particularly significant in safety-critical applications, where reasoning often requires explicit negative information rather than interpreting the absence of information as evidence of absence. To address this issue, we introduce an extension of Hybrid MKNF that supports classical negation in the rule component. We formally define the syntax and semantics of the extended language and present a general procedure for computing its well-founded model.

2026-07-23T11:20:15Z In Proceedings ICLP 2026, arXiv:2607.17707 EPTCS 450, 2026, pp. 374-402 Arun Raveendran Nair Sheela Université Clermont Auvergne, LIMOS Laboratory, Thales Christophe Rey Université Clermont Auvergne, LIMOS, CNRS, France Florence De Grancey Thales 10.4204/EPTCS.450.28 http://arxiv.org/abs/2607.21195v1 2026-07-23T11:17:41Z

Chess is a two player strategic game that is embedded in classical AI culture as it was once the frontier for intelligent behaviour. There was the silent assumption that the advent of computer engines that play better than the best humans will extinguish interest in the game. However, the opposite has come to pass, with a growing following for the game. A lot of the computational resources are now centered around training of players, where the engine output is just one aspect. Access to past games is also an essential part, both in knowing what games a specific player has played previously, and also which continuations at a certain position have led to victory more often for each of the two colour players. We present Chess_db a suite of logic programming tools that can effectively manipulate games both in memory and via creating back end databases. In particular, we provide versatile code that creates databases from PGN (portable game notation) game files and explore the suitability of open source key-value databases for storing position tables that provide near-instant access to information pertaining to substantially large number of games.

2026-07-23T11:17:41Z In Proceedings ICLP 2026, arXiv:2607.17707 EPTCS 450, 2026, pp. 196-208 Nicos Angelopoulos University College & Imperial College, London UK Jan Wielemaker SWI-Prolog solutions 10.4204/EPTCS.450.16 http://arxiv.org/abs/2607.21187v1 2026-07-23T11:15:38Z

We present the interactions with an LLM (Large Language Model) aiming at proving that the square root of 2 is not a rational number in an LP (Logic Programming) context. We start from a few basic pure logic programming predicate definitions. We rely on the LPTP (Logic Program Theorem Prover) system for stating and proving properties about logic programs. As the proof language of LPTP is based on natural deduction, the proofs are human readable. In our case study, we sketch in LPTP the usual proof showing the irrationality of the square root of 2. Then we describe the interactions we had with the LLM. We end up with a complete formal proof, partially generated by an LLM and fully proof-checked by LPTP.

2026-07-23T11:15:38Z In Proceedings ICLP 2026, arXiv:2607.17707 EPTCS 450, 2026, pp. 67-80 Fred Mesnard Étienne Payet Wim Vanhoof 10.4204/EPTCS.450.5 http://arxiv.org/abs/2607.21184v1 2026-07-23T11:15:02Z

Inductive Logic Programming (ILP) originated within the Logic Programming community in the Nineties as a framework for combining symbolic learning with declarative knowledge representation. Nowadays, mature ILP frameworks exist and they are capable of learning complex, non-monotonic hypotheses, thus broadening both the modeling capabilities and the scope of real-world applications of ILP. This work is primarily based on the FastLAS2 framework and aims to generate simple, interpretable hypotheses to help clarify the weather bulletins issued by OSMER FVG, the Regional Meteorological Observatory of the Italian region of Friuli Venezia-Giulia. In this paper we present a pipeline that, starting from simulated meteorological raw data and from OSMERs' bulletins (used as ground truth), extracts data as ASP facts and generates ILP examples. From such examples an explanatory hypothesis is then inferred via FastLAS2. Such a hypothesis (translated into natural language) explains the weather forecast issued by human experts, and in particular the rationale behind experts' choices of specific symbols in the bulletin pictogram (the symbol-annotated meteorological map of the forecast). The proposed approach is general, not specific to any particular region and it can equally be applied to bulletins from other sources and to different regions.

2026-07-23T11:15:02Z In Proceedings ICLP 2026, arXiv:2607.17707 EPTCS 450, 2026, pp. 15-28 Enrico Santi University of Udine, DMIF Alessandro Dal Palù University of Parma, SMFI Agostino Dovier University of Udine, DMIF Talissa Dreossi University of Udine, DMIF Andrea Formisano University of Udine, DMIF 10.4204/EPTCS.450.2 http://arxiv.org/abs/2607.20299v1 2026-07-22T15:47:54Z

Sequence A339987 of the OEIS counts (3,1)-regular graphs having one more vertex than edges by half the number of vertices. A recurrence relation satisfied by this sequence was guessed by Kauers and Koutschan in 2023. We confirm it in three ways: first, by a representation as the diagonal of a triple sum and an elaborate variant of traditional creative telescoping that makes an a posteriori validation possible; second, by a residue representation and a direct calculation by reduction-based creative telescoping; third, by a combinatorial recurrence on graph families and a calculation by differential elimination. Each of those three approaches leads to a formally complete proof and involves a computer calculation in one way or another.

2026-07-22T15:47:54Z Frédéric Chyzak Hui Huang Manuel Kauers http://arxiv.org/abs/2607.17349v1 2026-07-19T17:18:09Z

A bivariate exponential-trigonometric polynomial (BETP) equation with separated variables is of the form g(x, e^x, y, sin y, cos y) = 0 with g a polynomial and x, y real variables. Solving BETP equations with separated variables is useful in engineering. Besides, the problems of computing complex roots of rational-coefficient mixed-trigonometric polynomials and exponential polynomials, which occur frequently in dynamic systems, can both be reduced to solving a system containing two BETP equations with separated variables: g(x, e^x, y, sin y, cos y) = 0 h(x, e^x, y, sin y, cos y) = 0 In this paper, the theory of the analytic algebraic exponential polynomials is developed. Based on which we show that if some non-degenerate conditions hold for the system above, then there are N>0 and M>0 such that all solutions of that system in the quarter {(x, y)| x>N, y>M } lie on the curves of finitely many analytic algebraic exponential polynomials which are increasing and tend to infinity. These solutions consist of finitely many bunches of so-called semi-periodic solutions, and each bunch is entirely distributed along a certain curve. Finally, effective algorithms have been implemented to find those curves and to count those bunches of semi-periodic roots.

2026-07-19T17:18:09Z Tao Zheng Hao yuan http://arxiv.org/abs/2607.15571v1 2026-07-17T02:29:24Z

The $μ$-basis is an algebraic tool originating from the theory of moving curves and moving surfaces, and it is widely used in the study of rational curves and surfaces. In this paper, we give the explicit formulas for the $μ$-basis of planar quartic rational parametric curves based on redefined vector polynomials, and several illustrative examples are provided. Meanwhile, we also discuss the corresponding cases for quadratic and cubic curves.

2026-07-17T02:29:24Z 10 pages Weizhen Han Weikun Sun http://arxiv.org/abs/2507.08138v2 2026-07-15T15:40:14Z

We present the Conservative Matrix Field (CMF) as a tool for the analysis and computation of D-finite functions. We use conservative matrix fields to establish asymptotic properties of families of linear forms in periods, including (but not limited to) multivariate Mellin integrals, via a discrete Levinson-type framework due to Benzaid and Lutz. Finally, we present an experimental analysis of the families of linear forms generated by these objects and formalize the resulting observations as conjectures on their continuous asymptotic and arithmetic properties.

2025-07-10T19:56:14Z Revised structure and exposition. Added a proof of a statement previously formulated as a conjecture. This version has been submitted for publication Shachar Weinbaum Elyasheev Leibtag Rotem Kalisch Michael Shalyt Ido Kaminer