https://arxiv.org/api//F9Fi1C0bjLutLWsmfkupEYRzWo 2026-04-13T19:55:11Z 3075 630 15 http://arxiv.org/abs/2305.01206v4 2024-06-04T15:11:50Z

Solving Constrained Horn Clauses (CHCs) is a fundamental challenge behind a wide range of verification and analysis tasks. Data-driven approaches show great promise in improving CHC solving without the painstaking manual effort of creating and tuning various heuristics. However, a large performance gap exists between data-driven CHC solvers and symbolic reasoning-based solvers. In this work, we develop a simple but effective framework, "Chronosymbolic Learning", which unifies symbolic information and numerical data points to solve a CHC system efficiently. We also present a simple instance of Chronosymbolic Learning with a data-driven learner and a BMC-styled reasoner. Despite its relative simplicity, experimental results show the efficacy and robustness of our tool. It outperforms state-of-the-art CHC solvers on a dataset consisting of 288 benchmarks, including many instances with non-linear integer arithmetics.

2023-05-02T05:12:48Z Ziyan Luo Xujie Si http://arxiv.org/abs/2404.08751v3 2024-06-03T11:20:12Z

We introduce the third major version of Metatheory.jl, a Julia library for general-purpose metaprogramming and symbolic computation. Metatheory.jl provides a flexible and performant implementation of e-graphs and Equality Saturation (EqSat) that addresses the two-language problem in high-level compiler optimizations, symbolics and metaprogramming. We present results from our ongoing optimization efforts, comparing the state-of-the-art egg Rust library's performance against our system and show that performant EqSat implementations are possible without sacrificing the comfort of a direct 1-1 integration with a dynamic, high-level and an interactive host programming language.

2024-04-12T18:24:44Z 8 pages, 5 figures, submission for 2024 PLDI e-graph workshop Alessandro Cheli Niklas Heim http://arxiv.org/abs/2406.00938v1 2024-06-03T02:24:01Z

The prevailing approaches in Network Intrusion Detection Systems (NIDS) are often hampered by issues such as high resource consumption, significant computational demands, and poor interpretability. Furthermore, these systems generally struggle to identify novel, rapidly changing cyber threats. This paper delves into the potential of incorporating Neurosymbolic Artificial Intelligence (NSAI) into NIDS, combining deep learning's data-driven strengths with symbolic AI's logical reasoning to tackle the dynamic challenges in cybersecurity, which also includes detailed NSAI techniques introduction for cyber professionals to explore the potential strengths of NSAI in NIDS. The inclusion of NSAI in NIDS marks potential advancements in both the detection and interpretation of intricate network threats, benefiting from the robust pattern recognition of neural networks and the interpretive prowess of symbolic reasoning. By analyzing network traffic data types and machine learning architectures, we illustrate NSAI's distinctive capability to offer more profound insights into network behavior, thereby improving both detection performance and the adaptability of the system. This merging of technologies not only enhances the functionality of traditional NIDS but also sets the stage for future developments in building more resilient, interpretable, and dynamic defense mechanisms against advanced cyber threats. The continued progress in this area is poised to transform NIDS into a system that is both responsive to known threats and anticipatory of emerging, unseen ones.

2024-06-03T02:24:01Z Alice Bizzarri Chung-En Yu Brian Jalaian Fabrizio Riguzzi Nathaniel D. Bastian http://arxiv.org/abs/2406.00695v1 2024-06-02T10:17:54Z

The rapid expansion of wind power worldwide underscores the critical significance of engineering-focused analytical wake models in both the design and operation of wind farms. These theoretically-derived ana lytical wake models have limited predictive capabilities, particularly in the near-wake region close to the turbine rotor, due to assumptions that do not hold. Knowledge discovery methods can bridge these gaps by extracting insights, adjusting for theoretical assumptions, and developing accurate models for physical processes. In this study, we introduce a genetic symbolic regression (SR) algorithm to discover an interpretable mathematical expression for the mean velocity deficit throughout the wake, a previously unavailable insight. By incorporating a double Gaussian distribution into the SR algorithm as domain knowledge and designing a hierarchical equation structure, the search space is reduced, thus efficiently finding a concise, physically informed, and robust wake model. The proposed mathematical expression (equation) can predict the wake velocity deficit at any location in the full-wake region with high precision and stability. The model's effectiveness and practicality are validated through experimental data and high-fidelity numerical simulations.

2024-06-02T10:17:54Z Ding Wang Yuntian Chen Shiyi Chen http://arxiv.org/abs/2405.20745v1 2024-05-31T10:17:46Z

Bigraphs are a versatile modelling formalism that allows easy expression of placement and connectivity relations in a graphical format. System evolution is user defined as a set of rewrite rules. This paper presents a practical, yet detailed guide to developing, executing, and reasoning about bigraph models, including recent extensions such as parameterised, instantaneous, prioritised and conditional rules, and probabilistic and stochastic rewriting.

2024-05-31T10:17:46Z 34 pages Blair Archibald Muffy Calder Michele Sevegnani http://arxiv.org/abs/2405.20319v2 2024-05-31T04:09:41Z

The ability to edit 3D assets from natural language presents a compelling paradigm to aid in the democratization of 3D content creation. However, while natural language is often effective at communicating general intent, it is poorly suited for specifying precise manipulation. To address this gap, we introduce ParSEL, a system that enables controllable editing of high-quality 3D assets from natural language. Given a segmented 3D mesh and an editing request, ParSEL produces a parameterized editing program. Adjusting the program parameters allows users to explore shape variations with a precise control over the magnitudes of edits. To infer editing programs which align with an input edit request, we leverage the abilities of large-language models (LLMs). However, while we find that LLMs excel at identifying initial edit operations, they often fail to infer complete editing programs, and produce outputs that violate shape semantics. To overcome this issue, we introduce Analytical Edit Propagation (AEP), an algorithm which extends a seed edit with additional operations until a complete editing program has been formed. Unlike prior methods, AEP searches for analytical editing operations compatible with a range of possible user edits through the integration of computer algebra systems for geometric analysis. Experimentally we demonstrate ParSEL's effectiveness in enabling controllable editing of 3D objects through natural language requests over alternative system designs.

2024-05-30T17:55:46Z Aditya Ganeshan Ryan Y. Huang Xianghao Xu R. Kenny Jones Daniel Ritchie http://arxiv.org/abs/2405.20130v1 2024-05-30T15:10:30Z

We present LinApart, a routine designed for efficiently performing the univariate partial fraction decomposition of large symbolic expressions. Our method is based on an explicit closed formula for the decomposition of rational functions with fully factorized denominators. We provide implementations in both the Wolfram Mathematica and C languages, made available at https://github.com/fekeshazy/LinApart . The routine can provide very significant performance gains over available tools such as the Apart command in Mathematica.

2024-05-30T15:10:30Z 22 pages, 5 figures Bakar Chargeishvili Levente Fekésházy Gábor Somogyi Sam Van Thurenhout http://arxiv.org/abs/2402.15649v2 2024-05-30T14:37:15Z

Separation bounds are a fundamental measure of the complexity of solving a zero-dimensional system as it measures how difficult it is to separate its zeroes. In the positive dimensional case, the notion of reach takes its place. In this paper, we provide bounds on the reach of a smooth algebraic variety in terms of several invariants of interest: the condition number, Smale's $γ$ and the bit-size. We also provide probabilistic bounds for random algebraic varieties under some general assumptions.

2024-02-23T23:21:35Z 9 pages in double column Chris La Valle Josué Tonelli-Cueto http://arxiv.org/abs/2402.07053v2 2024-05-29T23:16:33Z

We revisit the problem of certifying the correctness of approximate solution paths computed by numerical homotopy continuation methods. We propose a conceptually simple approach based on a parametric variant of the Krawczyk method from interval arithmetic. Unlike most previous methods for certified path-tracking, our approach is applicable in the general setting of parameter homotopies commonly used to solve polynomial systems of equations. We also describe a novel preconditioning strategy and give theoretical correctness and termination results. Experiments using a preliminary implementation of the method indicate that our approach is competitive with specialized methods appearing previously in the literature, in spite of our more general setting.

2024-02-10T21:53:06Z 19 pages, 4 figures, 4 tables. Accepted for the Proceedings of ISSAC 2024 Timothy Duff Kisun Lee http://arxiv.org/abs/2405.19223v1 2024-05-29T16:03:48Z

For a given ideal I in K[x_1,...,x_n,y_1,...,y_m] in a polynomial ring with n+m variables, we want to find all elements that can be written as f-g for some f in K[x_1,...,x_n] and some g in K[y_1,...,y_m], i.e., all elements of I that contain no term involving at the same time one of the x_1,...,x_n and one of the y_1,...,y_m. For principal ideals and for ideals of dimension zero, we give a algorithms that compute all these polynomials in a finite number of steps.

2024-05-29T16:03:48Z Manfred Buchacher Manuel Kauers 10.1145/3666000.366968 http://arxiv.org/abs/2405.18896v1 2024-05-29T08:57:00Z

When developing empirical equations, domain experts require these to be accurate and adhere to physical laws. Often, constants with unknown units need to be discovered alongside the equations. Traditional unit-aware genetic programming (GP) approaches cannot be used when unknown constants with undetermined units are included. This paper presents a method for dimensional analysis that propagates unknown units as ''jokers'' and returns the magnitude of unit violations. We propose three methods, namely evolutive culling, a repair mechanism, and a multi-objective approach, to integrate the dimensional analysis in the GP algorithm. Experiments on datasets with ground truth demonstrate comparable performance of evolutive culling and the multi-objective approach to a baseline without dimensional analysis. Extensive analysis of the results on datasets without ground truth reveals that the unit-aware algorithms make only low sacrifices in accuracy, while producing unit-adherent solutions. Overall, we presented a promising novel approach for developing unit-adherent empirical equations.

2024-05-29T08:57:00Z Submitted to Conference Proceedings of PPSN2024 Julia Reuter Viktor Martinek Roland Herzog Sanaz Mostaghim http://arxiv.org/abs/2405.18549v1 2024-05-28T19:36:55Z

We introduce an efficient method for learning linear models from uncertain data, where uncertainty is represented as a set of possible variations in the data, leading to predictive multiplicity. Our approach leverages abstract interpretation and zonotopes, a type of convex polytope, to compactly represent these dataset variations, enabling the symbolic execution of gradient descent on all possible worlds simultaneously. We develop techniques to ensure that this process converges to a fixed point and derive closed-form solutions for this fixed point. Our method provides sound over-approximations of all possible optimal models and viable prediction ranges. We demonstrate the effectiveness of our approach through theoretical and empirical analysis, highlighting its potential to reason about model and prediction uncertainty due to data quality issues in training data.

2024-05-28T19:36:55Z Jiongli Zhu Su Feng Boris Glavic Babak Salimi http://arxiv.org/abs/2405.01733v2 2024-05-26T22:01:23Z

We examine the consequences of having a total division operation $\frac{x}{y}$ on commutative rings. We consider two forms of binary division, one derived from a unary inverse, the other defined directly as a general operation; each are made total by setting $1/0$ equal to an error value $\bot$, which is added to the ring. Such totalised divisions we call common divisions. In a field the two forms are equivalent and we have a finite equational axiomatisation $E$ that is complete for the equational theory of fields equipped with common division, called common meadows. These equational axioms $E$ turn out to be true of commutative rings with common division but only when defined via inverses. We explore these axioms $E$ and their role in seeking a completeness theorem for the conditional equational theory of common meadows. We prove they are complete for the conditional equational theory of commutative rings with inverse based common division. By adding a new proof rule, we can prove a completeness theorem for the conditional equational theory of common meadows. Although, the equational axioms $E$ fail with common division defined directly, we observe that the direct division does satisfies the equations in $E$ under a new congruence for partial terms called eager equality.

2024-05-02T21:07:00Z Jan A Bergstra John V Tucker 10.1017/jsl.2024.88 http://arxiv.org/abs/2405.16179v1 2024-05-25T11:11:17Z

Phosphorylation networks, representing the mechanisms by which proteins are phosphorylated at one or multiple sites, are ubiquitous in cell signalling and display rich dynamics such as unlimited multistability. Dual-site phosphorylation networks are known to exhibit oscillations in the form of periodic trajectories, when phosphorylation and dephosphorylation occurs as a mixed mechanism: phosphorylation of the two sites requires one encounter of the kinase, while dephosphorylation of the two sites requires two encounters with the phosphatase. A still open question is whether a mechanism requiring two encounters for both phosphorylation and dephosphorylation also admits oscillations. In this work we provide evidence in favor of the absence of oscillations of this network by precluding Hopf bifurcations in any reduced network comprising three out of its four intermediate protein complexes. Our argument relies on a novel network reduction step that preserves the absence of Hopf bifurcations, and on a detailed analysis of the semi-algebraic conditions precluding Hopf bifurcations obtained from Hurwitz determinants of the characteristic polynomial of the Jacobian of the system. We conjecture that the removal of certain reverse reactions appearing in Michaelis-Menten-type mechanisms does not have an impact on the presence or absence of Hopf bifurcations. We prove an implication of the conjecture under certain favorable scenarios and support the conjecture with additional example-based evidence.

2024-05-25T11:11:17Z Elisenda Feliu Nidhi Kaihnsa http://arxiv.org/abs/2403.13798v2 2024-05-24T17:44:11Z

Action quality assessment (AQA) applies computer vision to quantitatively assess the performance or execution of a human action. Current AQA approaches are end-to-end neural models, which lack transparency and tend to be biased because they are trained on subjective human judgements as ground-truth. To address these issues, we introduce a neuro-symbolic paradigm for AQA, which uses neural networks to abstract interpretable symbols from video data and makes quality assessments by applying rules to those symbols. We take diving as the case study. We found that domain experts prefer our system and find it more informative than purely neural approaches to AQA in diving. Our system also achieves state-of-the-art action recognition and temporal segmentation, and automatically generates a detailed report that breaks the dive down into its elements and provides objective scoring with visual evidence. As verified by a group of domain experts, this report may be used to assist judges in scoring, help train judges, and provide feedback to divers. Annotated training data and code: https://github.com/laurenok24/NSAQA.

2024-03-20T17:55:21Z CVPR 2024 CVSports (Oral Presentation; 3/3 Strong Accepts) + Selected for CVPR 2024 Demos Lauren Okamoto Paritosh Parmar