https://arxiv.org/api/lkOUVRVMlkPYOLr4dMx9eo67hsQ 2026-06-15T00:09:04Z 3138 525 15 http://arxiv.org/abs/2412.07939v2 2025-01-21T23:20:19Z

We define computational atoms named "actions" equipped primarily with three operations: reduction, collection, and inspection. We show how actions can be used for decision-making algorithms from simple axioms. We describe the encodings of typical data structures as actions, and provide a method of analysis for algorithms on the basis of data mutation.

2024-12-10T21:51:52Z 18 pages, 2 figures Sotirios Henning http://arxiv.org/abs/2411.16348v2 2025-01-20T12:07:57Z

Formal verification techniques based on computer algebra have proven highly effective for circuit verification. The circuit, given as an and-inverter graph, is encoded as a set of polynomials that automatically generates a Gröbner basis with respect to a lexicographic term ordering. Correctness of the circuit can be derived by computing the polynomial remainder of the specification. However, the main obstacle is the monomial blow-up during the rewriting of the specification, which leads to the development of dedicated heuristics to overcome this issue. In this paper, we investigate an orthogonal approach and focus the computational effort on rewriting the Gröbner basis itself. Our goal is to ensure the basis contains linear polynomials that can be effectively used to rewrite the linearized specification. We first prove the soundness and completeness of this technique and then demonstrate its practical application. Our implementation of this method shows promising results on benchmarks related to multiplier verification.

2024-11-25T12:55:49Z Accepted at 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2025 Daniela Kaufmann Jérémy Berthomieu http://arxiv.org/abs/2501.09729v1 2025-01-16T18:25:50Z

In physics, Lagrangians provide a systematic way to describe laws governing physical systems. In the context of particle physics, they encode the interactions and behavior of the fundamental building blocks of our universe. By treating Lagrangians as complex, rule-based constructs similar to linguistic expressions, we trained a transformer model -- proven to be effective in natural language tasks -- to predict the Lagrangian corresponding to a given list of particles. We report on the transformer's performance in constructing Lagrangians respecting the Standard Model $\mathrm{SU}(3)\times \mathrm{SU}(2)\times \mathrm{U}(1)$ gauge symmetries. The resulting model is shown to achieve high accuracies (over 90\%) with Lagrangians up to six matter fields, with the capacity to generalize beyond the training distribution, albeit within architectural constraints. We show through an analysis of input embeddings that the model has internalized concepts such as group representations and conjugation operations as it learned to generate Lagrangians. We make the model and training datasets available to the community. An interactive demonstration can be found at: \url{https://huggingface.co/spaces/JoseEliel/generate-lagrangians}.

2025-01-16T18:25:50Z 32 pages, 11 figues, 18 tables Yong Sheng Koay Rikard Enberg Stefano Moretti Eliel Camargo-Molina http://arxiv.org/abs/2501.09201v1 2025-01-15T23:24:32Z

The rise of automated code generation tools, such as large language models (LLMs), has introduced new challenges in ensuring the correctness and efficiency of scientific software, particularly in complex kernels, where numerical stability, domain-specific optimizations, and precise floating-point arithmetic are critical. We propose a stepwise semantics lifting approach using an extended SPIRAL framework with symbolic execution and theorem proving to statically derive high-level code semantics from LLM-generated kernels. This method establishes a structured path for verifying the source code's correctness via a step-by-step lifting procedure to high-level specification. We conducted preliminary tests on the feasibility of this approach by successfully lifting GPT-generated fast Fourier transform code to high-level specifications.

2025-01-15T23:24:32Z Accepted at the Theory and Practice of Static Analysis Workshop (TPSA), in conjunction with the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2025 Naifeng Zhang Sanil Rao Mike Franusich Franz Franchetti http://arxiv.org/abs/2501.08086v1 2025-01-14T12:55:48Z

While many physical and engineering processes are most effectively described by non-linear symbolic models, existing non-linear symbolic regression (SR) methods are restricted to a limited set of continuous algebraic functions, thereby limiting their applicability to discover higher order non-linear differential relations. In this work, we introduce the Neural Operator-based symbolic Model approximaTion and discOvery (NOMTO) method, a novel approach to symbolic model discovery that leverages Neural Operators to encompass a broad range of symbolic operations. We demonstrate that NOMTO can successfully identify symbolic expressions containing elementary functions with singularities, special functions, and derivatives. Additionally, our experiments demonstrate that NOMTO can accurately rediscover second-order non-linear partial differential equations. By broadening the set of symbolic operations available for discovery, NOMTO significantly advances the capabilities of existing SR methods. It provides a powerful and flexible tool for model discovery, capable of capturing complex relations in a variety of physical systems.

2025-01-14T12:55:48Z Sergei Garmaev Siddhartha Mishra Olga Fink http://arxiv.org/abs/2501.07123v1 2025-01-13T08:25:14Z

Machine learning is rapidly making its path into natural sciences, including high-energy physics. We present the first study that infers, directly from experimental data, a functional form of fragmentation functions. The latter represent a key ingredient to describe physical observables measured in high-energy physics processes that involve hadron production, and predict their values at different energy. Fragmentation functions can not be calculated in theory and have to be determined instead from data. Traditional approaches rely on global fits of experimental data using a pre-assumed functional form inspired from phenomenological models to learn its parameters. This novel approach uses a ML technique, namely symbolic regression, to learn an analytical model from measured charged hadron multiplicities. The function learned by symbolic regression resembles the Lund string function and describes the data well, thus representing a potential candidate for use in global FFs fits. This study represents an approach to follow in such QCD-related phenomenology studies and more generally in sciences.

2025-01-13T08:25:14Z Nour Makke Sanjay Chawla http://arxiv.org/abs/2501.06707v1 2025-01-12T04:23:34Z

ELIZA, created by Joseph Weizenbaum at MIT in the early 1960s, is usually considered the world's first chatbot. It was developed in MAD-SLIP on MIT's CTSS, the world's first time-sharing system, on an IBM 7094. We discovered an original ELIZA printout in Prof. Weizenbaum's archives at MIT, including an early version of the famous DOCTOR script, a nearly complete version of the MAD-SLIP code, and various support functions in MAD and FAP. Here we describe the reanimation of this original ELIZA on a restored CTSS, itself running on an emulated IBM 7094. The entire stack is open source, so that any user of a unix-like OS can run the world's first chatbot on the world's first time-sharing system.

2025-01-12T04:23:34Z In review Rupert Lane Anthony Hay Arthur Schwarz David M. Berry Jeff Shrager http://arxiv.org/abs/2501.06699v1 2025-01-12T03:32:12Z

Much has been discussed about how Large Language Models, Knowledge Graphs and Search Engines can be combined in a synergistic manner. A dimension largely absent from current academic discourse is the user perspective. In particular, there remain many open questions regarding how best to address the diverse information needs of users, incorporating varying facets and levels of difficulty. This paper introduces a taxonomy of user information needs, which guides us to study the pros, cons and possible synergies of Large Language Models, Knowledge Graphs and Search Engines. From this study, we derive a roadmap for future research.

2025-01-12T03:32:12Z Aidan Hogan Xin Luna Dong Denny Vrandečić Gerhard Weikum http://arxiv.org/abs/2501.05318v1 2025-01-09T15:39:39Z

The report is devoted to the concept of creating block-recursive matrix algorithms for computing on a supercomputer with distributed memory and dynamic decentralized control.

2025-01-09T15:39:39Z 6 paged 2019 Computer Science and Information Technologies (CSIT), Yerevan, Armenia, 2019, pp. 112-115 Gennadi Malaschonok 10.1109/CSITechnol.2019.8895255 http://arxiv.org/abs/2501.03381v1 2025-01-06T20:55:59Z

Complex systems are characterized by nonlinear dynamics, multi-level interactions, and emergent collective behaviors. Traditional analyses that focus solely on pairwise interactions often oversimplify these systems, neglecting the higher-order interactions critical for understanding their full collective dynamics. Recent advances in multivariate information theory provide a principled framework for quantifying these higher-order interactions, capturing key properties such as redundancy, synergy, shared randomness, and collective constraints. However, two major challenges persist: accurately estimating joint entropies and addressing the combinatorial explosion of interacting terms. To overcome these challenges, we introduce THOI (Torch-based High-Order Interactions), a novel, accessible, and efficient Python library for computing high-order interactions in continuous-valued systems. THOI leverages the well-established Gaussian copula method for joint entropy estimation, combined with state-of-the-art batch and parallel processing techniques to optimize performance across CPU, GPU, and TPU environments. Our results demonstrate that THOI significantly outperforms existing tools in terms of speed and scalability. For larger systems, where exhaustive analysis is computationally impractical, THOI integrates optimization strategies that make higher-order interaction analysis feasible. We validate THOI accuracy using synthetic datasets with parametrically controlled interactions and further illustrate its utility by analyzing fMRI data from human subjects in wakeful resting states and under deep anesthesia. Finally, we analyzed over 900 real-world and synthetic datasets, establishing a comprehensive framework for applying higher-order interaction (HOI) analysis in complex systems.

2025-01-06T20:55:59Z 22 pages, 6 figures Laouen Belloli Pedro Mediano Rodrigo Cofré Diego Fernandez Slezak Rubén Herzog http://arxiv.org/abs/2101.03482v3 2025-01-03T15:43:40Z

We define a new type of ideal basis called the proper basis that improves both Gröbner basis and Buchberger's algorithm. Let $x_1$ be the least variable of a monomial ordering in a polynomial ring $K[x_1,\dotsc,x_n]$ over a field $K$. The Gröbner basis of a zero-dimensional polynomial ideal contains a univariate polynomial in $x_1$. The proper basis is defined and computed in the variables $\tilde{\bm{x}}:=(x_2,\dotsc,x_n)$ with $x_1$ serving as a parameter in the algebra $K[x_1][\tilde{\bm{x}}]$. Its algorithm is more efficient than not only Buchberger's algorithm whose elimination of $\tilde{\bm{x}}$ unnecessarily involves the least variable $x_1$ but also Möller's algorithm due to its polynomial division mechanism. This is corroborated by a series of benchmark testings herein. The proper basis is in a modular form and neater than Gröbner basis and hence reduces its coefficient swell problem. It is expected that all the state of the art algorithms improving Buchberger's algorithm over the last decades can be further improved if we apply them to the proper basis.

2021-01-10T06:29:49Z 15 pages. The length of the previous version is shortened to 15 pages in its current form Sheng-Ming Ma http://arxiv.org/abs/2501.00563v1 2024-12-31T17:49:53Z

We present a new Python package called "motives", a symbolic manipulation package based on SymPy capable of handling and simplifying motivic expressions in the Grothendieck ring of Chow motives and other types of $λ$-rings. The package is able to manipulate and compare arbitrary expressions in $λ$-rings and, in particular, it contains explicit tools for manipulating motives of several types of commonly used moduli schemes and moduli stacks of decorated bundles on curves. We have applied this new tool to advance in the verification of Mozgovoy's conjectural formula for the motive of the moduli space of twisted Higgs bundles, proving that it holds in rank 2 and 3 for any curve of genus up to 18 and any twisting bundle of small degree.

2024-12-31T17:49:53Z 19 pages, 2 figures. The code of the library described in the paper is publicly hosted at https://github.com/CIAMOD/motives Daniel Sanchez David Alfaya Jaime Pizarroso http://arxiv.org/abs/2412.20973v1 2024-12-30T14:24:54Z

For the sake of reliability, the kernels of Interactive Theorem Provers (ITPs) are generally kept relatively small. On top of the kernel, additional symbols and inference rules are defined. This paper presents an analysis of how kernel extension reduces the size of proofs and impacts proof checking.

2024-12-30T14:24:54Z The paper was presented in the student session of the European Summer School in Logic, Language, and Information (ESSLLI) in 2016 Shuai Wang http://arxiv.org/abs/2412.20332v1 2024-12-29T03:19:21Z

In this paper, we tackle the parametric complete multiplicity problem for a univariate polynomial. Our approach to the parametric complete multiplicity problem has a significant difference from the classical method, which relies on repeated gcd computation. Instead, we introduce a novel technique that uses incremental gcds of the given polynomial and its high-order derivatives. This approach, formulated as non-nested subresultants, sidesteps the exponential expansion of polynomial degrees in the generated condition. We also uncover the hidden structure between the incremental gcds and pseudo-remainders. Our analysis reveals that the conditions produced by our new algorithm are simpler than those generated by the classical approach in most cases. Experiments show that our algorithm is faster than the one based on repeated gcd computation for problems with relatively big size.

2024-12-29T03:19:21Z Simin Qin Bican Xia Jing Yang http://arxiv.org/abs/2403.06294v3 2024-12-28T17:40:48Z

There are two main barriers to using large language models (LLMs) in clinical reasoning. Firstly, while LLMs exhibit significant promise in Natural Language Processing (NLP) tasks, their performance in complex reasoning and planning falls short of expectations. Secondly, LLMs use uninterpretable methods to make clinical decisions that are fundamentally different from the clinician's cognitive processes. This leads to user distrust. In this paper, we present a multi-agent framework called ArgMed-Agents, which aims to enable LLM-based agents to make explainable clinical decision reasoning through interaction. ArgMed-Agents performs self-argumentation iterations via Argumentation Scheme for Clinical Discussion (a reasoning mechanism for modeling cognitive processes in clinical reasoning), and then constructs the argumentation process as a directed graph representing conflicting relationships. Ultimately, use symbolic solver to identify a series of rational and coherent arguments to support decision. We construct a formal model of ArgMed-Agents and present conjectures for theoretical guarantees. ArgMed-Agents enables LLMs to mimic the process of clinical argumentative reasoning by generating explanations of reasoning in a self-directed manner. The setup experiments show that ArgMed-Agents not only improves accuracy in complex clinical decision reasoning problems compared to other prompt methods, but more importantly, it provides users with decision explanations that increase their confidence.

2024-03-10T19:47:00Z Shengxin Hong Liang Xiao Xin Zhang Jianxia Chen