https://arxiv.org/api/OxbUVZExc7qzen7yoFFpkYphLtE2026-04-13T03:43:23Z307548015http://arxiv.org/abs/2412.15121v1Folding One Polyhedral Metric Graph into Another2024-12-19T18:01:35ZWe analyze the problem of folding one polyhedron, viewed as a metric graph of its edges, into the shape of another, similar to 1D origami. We find such foldings between all pairs of Platonic solids and prove corresponding lower bounds, establishing the optimal scale factor when restricted to integers. Further, we establish that our folding problem is also NP-hard, even if the source graph is a tree. It turns out that the problem is hard to approximate, as we obtain NP-hardness even for determining the existence of a scale factor 1.5-ε. Finally, we prove that, in general, the optimal scale factor has to be rational. This insight then immediately results in NP membership. In turn, verifying whether a given scale factor is indeed the smallest possible, requires two independent calls to an NP oracle, rendering the problem DP-complete.2024-12-19T18:01:35ZLily ChungErik D. DemaineMartin L. DemaineMarkus HecherRebecca LinJayson LynchChie Narahttp://arxiv.org/abs/2412.14814v1Answer Set Networks: Casting Answer Set Programming into Deep Learning2024-12-19T13:09:06ZAlthough Answer Set Programming (ASP) allows constraining neural-symbolic (NeSy) systems, its employment is hindered by the prohibitive costs of computing stable models and the CPU-bound nature of state-of-the-art solvers. To this end, we propose Answer Set Networks (ASN), a NeSy solver. Based on Graph Neural Networks (GNN), ASNs are a scalable approach to ASP-based Deep Probabilistic Logic Programming (DPPL). Specifically, we show how to translate ASPs into ASNs and demonstrate how ASNs can efficiently solve the encoded problem by leveraging GPU's batching and parallelization capabilities. Our experimental evaluations demonstrate that ASNs outperform state-of-the-art CPU-bound NeSy systems on multiple tasks. Simultaneously, we make the following two contributions based on the strengths of ASNs. Namely, we are the first to show the finetuning of Large Language Models (LLM) with DPPLs, employing ASNs to guide the training with logic. Further, we show the "constitutional navigation" of drones, i.e., encoding public aviation laws in an ASN for routing Unmanned Aerial Vehicles in uncertain environments.2024-12-19T13:09:06Z16 pages, 9 figuresArseny SkryaginDaniel OchsPhillip DeibertSimon KohautDevendra Singh DhamiKristian Kerstinghttp://arxiv.org/abs/2412.13306v1Invariants: Computation and Applications2024-12-17T20:18:03ZInvariants withstand transformations and, therefore, represent the essence of objects or phenomena. In mathematics, transformations often constitute a group action. Since the 19th century, studying the structure of various types of invariants and designing methods and algorithms to compute them remains an active area of ongoing research with an abundance of applications. In this incredibly vast topic, we focus on two particular themes displaying a fruitful interplay between the differential and algebraic invariant theories. First, we show how an algebraic adaptation of the moving frame method from differential geometry leads to a practical algorithm for computing a generating set of rational invariants. Then we discuss the notion of differential invariant signature, its role in solving equivalence problems in geometry and algebra, and some successes and challenges in designing algorithms based on this notion.2024-12-17T20:18:03ZThis is a tutorial paper that appeared in the proceedings of International Symposium on Symbolic and Algebraic Computation 2023 (ISSAC 2023), July 24-27, 2023, Tromsø, Norway. ACM, New York, NY, USA, https://doi.org/10.1145/3597066.3597149 . This is the author's version of the work. It is posted here for your personal use. Not for redistributionISSAC '23: Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation, Pages 31 - 40Irina A. Kogan10.1145/3597066.3597149http://arxiv.org/abs/2412.08576v1Positivity Proofs for Linear Recurrences through Contracted Cones2024-12-11T17:47:49ZDeciding the positivity of a sequence defined by a linear recurrence with polynomial coefficients and initial condition is difficult in general. Even in the case of recurrences with constant coefficients, it is known to be decidable only for order up to~5. We consider a large class of linear recurrences of arbitrary order, with polynomial coefficients, for which an algorithm decides positivity for initial conditions outside of a hyperplane. The underlying algorithm constructs a cone, contracted by the recurrence operator, that allows a proof of positivity by induction. The existence and construction of such cones relies on the extension of the classical Perron-Frobenius theory to matrices leaving a cone invariant.2024-12-11T17:47:49Z26 pagesAlaa IbrahimBruno Salvyhttp://arxiv.org/abs/2412.08235v1The B2Scala Tool: Integrating Bach in Scala with Security in Mind2024-12-11T09:32:11ZProcess algebras have been widely used to verify security protocols in a formal manner. However they mostly focus on synchronous communication based on the exchange of messages. We present an alternative approach relying on asynchronous communication obtained through information available on a shared space. More precisely this paper first proposes an embedding in Scala of a Linda-like language, called Bach. It consists of a Domain Specific Language, internal to Scala, that allows us to experiment programs developed in Bach while benefiting from the Scala eco-system, in particular from its type system as well as program fragments developed in Scala. Moreover, we introduce a logic that allows to restrict the executions of programs to those meeting logic formulae. Our work is illustrated on the Needham-Schroeder security protocol, for which we manage to automatically rediscover the man-in-the-middle attack first put in evidence by G. Lowe.2024-12-11T09:32:11ZIn Proceedings ICE 2024, arXiv:2412.07570EPTCS 414, 2024, pp. 58-76Doha OuardiUniversity of NamurManel BarkallahUniversity of NamurJean-Marie JacquetUniversity of Namur10.4204/EPTCS.414.4http://arxiv.org/abs/2409.09359v3Symbolic Regression with a Learned Concept Library2024-12-10T16:24:48ZWe present a novel method for symbolic regression (SR), the task of searching for compact programmatic hypotheses that best explain a dataset. The problem is commonly solved using genetic algorithms; we show that we can enhance such methods by inducing a library of abstract textual concepts. Our algorithm, called LaSR, uses zero-shot queries to a large language model (LLM) to discover and evolve concepts occurring in known high-performing hypotheses. We discover new hypotheses using a mix of standard evolutionary steps and LLM-guided steps (obtained through zero-shot LLM queries) conditioned on discovered concepts. Once discovered, hypotheses are used in a new round of concept abstraction and evolution. We validate LaSR on the Feynman equations, a popular SR benchmark, as well as a set of synthetic tasks. On these benchmarks, LaSR substantially outperforms a variety of state-of-the-art SR approaches based on deep learning and evolutionary algorithms. Moreover, we show that LaSR can be used to discover a novel and powerful scaling law for LLMs.2024-09-14T08:17:30ZNeurIPS version; 10 pages; no checklist; added more experiment detailsArya GrayeliAtharva SehgalOmar Costilla-ReyesMiles CranmerSwarat Chaudhurihttp://arxiv.org/abs/2412.05586v1Towards Learning to Reason: Comparing LLMs with Neuro-Symbolic on Arithmetic Relations in Abstract Reasoning2024-12-07T08:45:39ZThis work compares large language models (LLMs) and neuro-symbolic approaches in solving Raven's progressive matrices (RPM), a visual abstract reasoning test that involves the understanding of mathematical rules such as progression or arithmetic addition. Providing the visual attributes directly as textual prompts, which assumes an oracle visual perception module, allows us to measure the model's abstract reasoning capability in isolation. Despite providing such compositionally structured representations from the oracle visual perception and advanced prompting techniques, both GPT-4 and Llama-3 70B cannot achieve perfect accuracy on the center constellation of the I-RAVEN dataset. Our analysis reveals that the root cause lies in the LLM's weakness in understanding and executing arithmetic rules. As a potential remedy, we analyze the Abductive Rule Learner with Context-awareness (ARLC), a neuro-symbolic approach that learns to reason with vector-symbolic architectures (VSAs). Here, concepts are represented with distributed vectors s.t. dot products between encoded vectors define a similarity kernel, and simple element-wise operations on the vectors perform addition/subtraction on the encoded values. We find that ARLC achieves almost perfect accuracy on the center constellation of I-RAVEN, demonstrating a high fidelity in arithmetic rules. To stress the length generalization capabilities of the models, we extend the RPM tests to larger matrices (3x10 instead of typical 3x3) and larger dynamic ranges of the attribute values (from 10 up to 1000). We find that the LLM's accuracy of solving arithmetic rules drops to sub-10%, especially as the dynamic range expands, while ARLC can maintain a high accuracy due to emulating symbolic computations on top of properly distributed representations. Our code is available at https://github.com/IBM/raven-large-language-models.2024-12-07T08:45:39ZMichael HerscheGiacomo CamposampieroRoger WattenhoferAbu SebastianAbbas Rahimihttp://arxiv.org/abs/2412.04928v1Hahn series and Mahler equations: Algorithmic aspects2024-12-06T10:32:37ZMany articles have recently been devoted to Mahler equations, partly because of their links with other branches of mathematics such as automata theory. Hahn series (a generalization of the Puiseux series allowing arbitrary exponents of the indeterminate as long as the set that supports them is well-ordered) play a central role in the theory of Mahler equations. In this paper, we address the following fundamental question: is there an algorithm to calculate the Hahn series solutions of a given linear Mahler equation? What makes this question interesting is the fact that the Hahn series appearing in this context can have complicated supports with infinitely many accumulation points. Our (positive) answer to the above question involves among other things the construction of a computable well-ordered receptacle for the supports of the potential Hahn series solutions.2024-12-06T10:32:37ZJournal of the London Mathematical Society, 2024, 110 (1)C. FaverjonICJ, CTNJulien RoquesICJ, CTN10.1112/jlms.12945http://arxiv.org/abs/2412.03127v1Summa Summarum: Moessner's Theorem without Dynamic Programming2024-12-04T08:44:02ZSeventy years on, Moessner's theorem and Moessner's process -- i.e., the additive computation of integral powers -- continue to fascinate. They have given rise to a variety of elegant proofs, to an implementation in hardware, to generalizations, and now even to a popular video, "The Moessner Miracle.'' The existence of this video, and even more its title, indicate that while the "what'' of Moessner's process is understood, its "how'' and even more its "why'' are still elusive. And indeed all the proofs of Moessner's theorem involve more complicated concepts than both the theorem and the process. This article identifies that Moessner's process implements an additive function with dynamic programming. A version of this implementation without dynamic programming (1) gives rise to a simpler statement of Moessner's theorem and (2) can be abstracted and then instantiated into related additive computations. The simpler statement also suggests a simpler and more efficient implementation to compute integral powers as well as simple additive functions to compute, e.g., Factorial numbers. It also reveals the source of -- to quote John Conway and Richard Guy -- Moessner's magic.2024-12-04T08:44:02ZIn Proceedings PT 2024, arXiv:2412.01856EPTCS 413, 2024, pp. 57-92Olivier DanvyNational University of Singapore10.4204/EPTCS.413.5http://arxiv.org/abs/2412.02257v1Asymptotics for the reciprocal and shifted quotient of the partition function2024-12-03T08:32:37ZLet $p(n)$ denote the partition function. In this paper our main goal is to derive an asymptotic expansion up to order $N$ (for any fixed positive integer $N$) along with estimates for error bounds for the shifted quotient of the partition function, namely $p(n+k)/p(n)$ with $k\in \mathbb{N}$, which generalizes a result of Gomez, Males, and Rolen. In order to do so, we derive asymptotic expansions with error bounds for the shifted version $p(n+k)$ and the multiplicative inverse $1/p(n)$, which is of independent interest.2024-12-03T08:32:37ZKoustav BanerjeePeter PauleCristian-Silviu RaduCarsten Schneiderhttp://arxiv.org/abs/2412.01181v1Training Stiff Neural Ordinary Differential Equations with Explicit Exponential Integration Methods2024-12-02T06:40:08ZStiff ordinary differential equations (ODEs) are common in many science and engineering fields, but standard neural ODE approaches struggle to accurately learn these stiff systems, posing a significant barrier to widespread adoption of neural ODEs. In our earlier work, we addressed this challenge by utilizing single-step implicit methods for solving stiff neural ODEs. While effective, these implicit methods are computationally costly and can be complex to implement. This paper expands on our earlier work by exploring explicit exponential integration methods as a more efficient alternative. We evaluate the potential of these explicit methods to handle stiff dynamics in neural ODEs, aiming to enhance their applicability to a broader range of scientific and engineering problems. We found the integrating factor Euler (IF Euler) method to excel in stability and efficiency. While implicit schemes failed to train the stiff Van der Pol oscillator, the IF Euler method succeeded, even with large step sizes. However, IF Euler's first-order accuracy limits its use, leaving the development of higher-order methods for stiff neural ODEs an open research problem.2024-12-02T06:40:08ZColby FronkLinda Petzoldhttp://arxiv.org/abs/2412.00963v1Semantics of Division for Polynomial Solvers2024-12-01T20:40:51ZHow to handle division in systems that compute with logical formulas involving what would otherwise be polynomial constraints over the real numbers is a surprisingly difficult question. This paper argues that existing approaches from both the computer algebra and computational logic communities are unsatisfactory for systems that consider the satisfiability of formulas with quantifiers or that perform quantifier elimination. To address this, we propose the notion of the fair-satisfiability of a formula, use it to characterize formulas with divisions that are well-defined, meaning that they adequately guard divisions against division by zero, and provide a translation algorithm that converts a formula with divisions into a purely polynomial formula that is satisfiable if and only if the original formula is fair-satisfiable. This provides a semantics for division with some nice properties, which we describe and prove in the paper.2024-12-01T20:40:51ZChristopher W. Brownhttp://arxiv.org/abs/2412.00962v1LLMs as mirrors of societal moral standards: reflection of cultural divergence and agreement across ethical topics2024-12-01T20:39:42ZLarge language models (LLMs) have become increasingly pivotal in various domains due the recent advancements in their performance capabilities. However, concerns persist regarding biases in LLMs, including gender, racial, and cultural biases derived from their training data. These biases raise critical questions about the ethical deployment and societal impact of LLMs. Acknowledging these concerns, this study investigates whether LLMs accurately reflect cross-cultural variations and similarities in moral perspectives. In assessing whether the chosen LLMs capture patterns of divergence and agreement on moral topics across cultures, three main methods are employed: (1) comparison of model-generated and survey-based moral score variances, (2) cluster alignment analysis to evaluate the correspondence between country clusters derived from model-generated moral scores and those derived from survey data, and (3) probing LLMs with direct comparative prompts. All three methods involve the use of systematic prompts and token pairs designed to assess how well LLMs understand and reflect cultural variations in moral attitudes. The findings of this study indicate overall variable and low performance in reflecting cross-cultural differences and similarities in moral values across the models tested, highlighting the necessity for improving models' accuracy in capturing these nuances effectively. The insights gained from this study aim to inform discussions on the ethical development and deployment of LLMs in global contexts, emphasizing the importance of mitigating biases and promoting fair representation across diverse cultural perspectives.2024-12-01T20:39:42ZMijntje MeijerHadi MohammadiAyoub Bagherihttp://arxiv.org/abs/2412.00956v1Large Language Models as Mirrors of Societal Moral Standards2024-12-01T20:20:35ZPrior research has demonstrated that language models can, to a limited extent, represent moral norms in a variety of cultural contexts. This research aims to replicate these findings and further explore their validity, concentrating on issues like 'homosexuality' and 'divorce'. This study evaluates the effectiveness of these models using information from two surveys, the WVS and the PEW, that encompass moral perspectives from over 40 countries. The results show that biases exist in both monolingual and multilingual models, and they typically fall short of accurately capturing the moral intricacies of diverse cultures. However, the BLOOM model shows the best performance, exhibiting some positive correlations, but still does not achieve a comprehensive moral understanding. This research underscores the limitations of current PLMs in processing cross-cultural differences in values and highlights the importance of developing culturally aware AI systems that better align with universal human values.2024-12-01T20:20:35ZEvi PapadopoulouHadi MohammadiAyoub Bagherihttp://arxiv.org/abs/2411.17066v1Relations, Negations, and Numbers: Looking for Logic in Generative Text-to-Image Models2024-11-26T03:06:52ZDespite remarkable progress in multi-modal AI research, there is a salient domain in which modern AI continues to lag considerably behind even human children: the reliable deployment of logical operators. Here, we examine three forms of logical operators: relations, negations, and discrete numbers. We asked human respondents (N=178 in total) to evaluate images generated by a state-of-the-art image-generating AI (DALL-E 3) prompted with these `logical probes', and find that none reliably produce human agreement scores greater than 50\%. The negation probes and numbers (beyond 3) fail most frequently. In a 4th experiment, we assess a `grounded diffusion' pipeline that leverages targeted prompt engineering and structured intermediate representations for greater compositional control, but find its performance is judged even worse than that of DALL-E 3 across prompts. To provide further clarity on potential sources of success and failure in these text-to-image systems, we supplement our 4 core experiments with multiple auxiliary analyses and schematic diagrams, directly quantifying, for example, the relationship between the N-gram frequency of relational prompts and the average match to generated images; the success rates for 3 different prompt modification strategies in the rendering of negation prompts; and the scalar variability / ratio dependence (`approximate numeracy') of prompts involving integers. We conclude by discussing the limitations inherent to `grounded' multimodal learning systems whose grounding relies heavily on vector-based semantics (e.g. DALL-E 3), or under-specified syntactical constraints (e.g. `grounded diffusion'), and propose minimal modifications (inspired by development, based in imagery) that could help to bridge the lingering compositional gap between scale and structure. All data and code is available at https://github.com/ColinConwell/T2I-Probology2024-11-26T03:06:52ZColin ConwellRupert Tawiah-QuashieTomer Ullman