https://arxiv.org/api/vZuFWBZk1Lxoi/K1qOWdDHCnvCo 2026-04-12T21:22:18Z 3074 420 15 http://arxiv.org/abs/2410.21205v2 2025-03-11T11:07:49Z

Microkinetic models are key for evaluating industrial processes' efficiency and chemicals' environmental impact. Manual construction of these models is difficult and time-consuming, prompting a shift to automated methods. This study introduces SiMBA (Simplest Mechanism Builder Algorithm), a novel approach for generating microkinetic models from kinetic data. SiMBA operates through four phases: mechanism generation, mechanism translation, parameter estimation, and model comparison. Our approach systematically proposes reaction mechanisms, using matrix representations and a parallelized backtracking algorithm to manage complexity. These mechanisms are then translated into microkinetic models represented by ordinary differential equations, and optimized to fit available data. Models are compared using information criteria to balance accuracy and complexity, iterating until convergence to an optimal model is reached. Case studies on an aldol condensation reaction, and the dehydration of fructose demonstrate SiMBA's effectiveness in distilling complex kinetic behaviors into simple yet accurate models. While SiMBA predicts intermediates correctly for all case studies, it does not chemically identify intermediates, requiring expert input for complex systems. Despite this, SiMBA significantly enhances mechanistic exploration, offering a robust initial mechanism that accelerates the development and modeling of chemical processes.

2024-10-28T16:51:50Z Miguel Ángel de Carvalho Servia Mimi King Kuok Mimi Hii Klaus Hellgardt Dongda Zhang Ehecatl Antonio del Rio Chanona http://arxiv.org/abs/2303.16799v3 2025-03-10T20:01:27Z

Given a single (differential-algebraic) input-output equation, we present a method for finding different representations of the associated system in the form of rational realizations; these are dynamical systems with rational right-hand sides. It has been shown that in the case where the input-output equation is of order one, rational realizations can be computed, if they exist. In this work, we focus first on the existence and actual computation of the so-called observable rational realizations, and secondly on rational realizations with real coefficients. The study of observable realizations allows to find every rational realization of a given first order input-output equation, and the necessary field extensions in this process. We show that for first order input-output equations the existence of a rational realization is equivalent to the existence of an observable rational realization. Moreover, we give a criterion to decide the existence of real rational realizations. The computation of observable and real realizations of first order input-output equations is fully algorithmic. We also present partial results for the case of higher order input-output equations.

2023-03-29T15:42:01Z Systems & Control Letters, 198 (2025): 106059 Sebastian Falkensteiner Dmitrii Pavlov Rafael Sendra 10.1016/j.sysconle.2025.106059 http://arxiv.org/abs/2503.07342v1 2025-03-10T13:54:42Z

In this work, we introduce a novel variant of the multivariate quadratic problem, which is at the core of one of the most promising post-quantum alternatives: multivariate cryptography. In this variant, the solution of a given multivariate quadratic system must also be regular, i.e. if it is split into multiple blocks of consecutive entries with the same fixed length, then each block has only one nonzero entry. We prove the NP-completeness of this variant and show similarities and differences with other computational problems used in cryptography. Then we analyze its hardness by reviewing the most common solvers for polynomial systems over finite fields, derive asymptotic formulas for the corresponding complexities and compare the different approaches.

2025-03-10T13:54:42Z Antoine Joux Rocco Mora http://arxiv.org/abs/2501.14951v2 2025-03-09T20:31:19Z

Vector representations have been pivotal in advancing natural language processing (NLP), with prior research focusing on embedding techniques for mathematical expressions using mathematically equivalent formulations. While effective, these approaches are constrained by the size and diversity of training data. In this work, we address these limitations by introducing E-Gen, a novel e-graph-based dataset generation scheme that synthesizes large and diverse mathematical expression datasets, surpassing prior methods in size and operator variety. Leveraging this dataset, we train embedding models using two strategies: (1) generating mathematically equivalent expressions, and (2) contrastive learning to explicitly group equivalent expressions. We evaluate these embeddings on both in-distribution and out-of-distribution mathematical language processing tasks, comparing them against prior methods. Finally, we demonstrate that our embedding-based approach outperforms state-of-the-art large language models (LLMs) on several tasks, underscoring the necessity of optimizing embedding methods for the mathematical data modality. The source code and datasets are available at https://github.com/MLPgroup/E-Gen.

2025-01-24T22:39:08Z Hongbo Zheng Suyuan Wang Neeraj Gangwar Nickvash Kani http://arxiv.org/abs/2503.05924v1 2025-03-07T20:46:38Z

Techniques that rigorously bound the overall rounding error exhibited by a numerical program are of significant interest for communities developing numerical software. However, there are few available tools today that can be used to rigorously bound errors in programs that employ conditional statements (a basic need) as well as mixed-precision arithmetic (a direction of significant future interest) employing global optimization in error analysis. In this paper, we present a new tool that fills this void while also employing an abstraction-guided optimization approach to allow designers to trade error-bound tightness for gains in analysis time -- useful when searching for design alternatives. We first present the basic rigorous analysis framework of Satire and then show how to extend it to incorporate abstractions, conditionals, and mixed-precision arithmetic. We begin by describing Satire's design and its performance on a collection of benchmark examples. We then describe these aspects of Satire: (1) how the error-bound and tool execution time vary with the abstraction level; (2) the additional machinery to handle conditional expression branches, including defining the concepts of instability jumps and instability window widths and measuring these quantities; and (3) how the error changes when a mix of precision values are used. To showcase how \satire can add value during design, we start with a Conjugate Gradient solver and demonstrate how its step size and search direction are affected by different precision settings. Satire is freely available for evaluation, and can be used during the design of numerical routines to effect design tradeoffs guided by rigorous empirical error guarantees.

2025-03-07T20:46:38Z 22 pgs, 8 figures, 4 tables Tanmay Tirpankar Arnab Das Ganesh Gopalakrishnan http://arxiv.org/abs/2501.13680v2 2025-03-04T13:44:11Z

For a polynomial dynamical system, we study the problem of computing the minimal differential equation satisfied by a chosen coordinate (in other words, projecting the system on the coordinate). This problem can be viewed as a special case of the general elimination problem for systems of differential equations and appears in applications to modeling and control. We give a bound for the Newton polytope of such minimal equation and show that our bound is sharp in "more than half of the cases". We further use this bound to design an algorithm for computing the minimal equation following the evaluation-interpolation paradigm. We demonstrate that our implementation of the algorithm can tackle problems which are out of reach for the state-of-the-art software for differential elimination.

2025-01-23T14:07:11Z Yulia Mukhina Gleb Pogudin http://arxiv.org/abs/2503.02512v1 2025-03-04T11:20:19Z

We present a framework for verifying Memoryful Neural Multi-Agent Systems (MN-MAS) against full Linear Temporal Logic (LTL) specifications. In MN-MAS, agents interact with a non-deterministic, partially observable environment. Examples of MN-MAS include multi-agent systems based on feed-forward and recurrent neural networks or state-space models. Different from previous approaches, we support the verification of both bounded and unbounded LTL specifications. We leverage well-established bounded model checking techniques, including lasso search and invariant synthesis, to reduce the verification problem to that of constraint solving. To solve these constraints, we develop efficient methods based on bound propagation, mixed-integer linear programming, and adaptive splitting. We evaluate the effectiveness of our algorithms in single and multi-agent environments from the Gymnasium and PettingZoo libraries, verifying unbounded specifications for the first time and improving the verification time for bounded specifications by an order of magnitude compared to the SoA.

2025-03-04T11:20:19Z 11 pages, 2 figures, accepted at AAMAS 2025 conference Mehran Hosseini Alessio Lomuscio Nicola Paoletti http://arxiv.org/abs/2503.04810v1 2025-03-04T08:58:53Z

This article introduces a novel methodology, Network Simulator-centric Compositional Testing (NSCT), to enhance the verification of network protocols with a particular focus on time-varying network properties. NSCT follows a Model-Based Testing (MBT) approach. These approaches usually struggle to test and represent time-varying network properties. NSCT also aims to achieve more accurate and reproducible protocol testing. It is implemented using the Ivy tool and the Shadow network simulator. This enables online debugging of real protocol implementations. A case study on an implementation of QUIC (picoquic) is presented, revealing an error in its compliance with a time-varying specification. This error has subsequently been rectified, highlighting NSCT's effectiveness in uncovering and addressing real-world protocol implementation issues. The article underscores NSCT's potential in advancing protocol testing methodologies, offering a notable contribution to the field of network protocol verification.

2025-03-04T08:58:53Z Tom Rousseaux Christophe Crochet John Aoga Axel Legay 10.1007/978-3-031-62645-6_10 http://arxiv.org/abs/2502.05834v3 2025-03-04T08:57:58Z

In this article, we show that a flat morphism of $k$-varieties ($\mathop{\mathrm{char}} k=0$) with locally constant geometric fibers becomes finite étale after reduction. When $k$ is a real closed field, we prove that such a morphism induces a covering map on the rational points. We further give a triviality result different from Hardt's and a new interpretation of the construction of cylindrical algebraic decomposition as applications.

2025-02-09T09:50:17Z 17 pages, 5 figures. Submitted version Rizeng Chen http://arxiv.org/abs/2503.02413v1 2025-03-04T08:56:03Z

In this paper, we introduce PANTHER, a modular framework for testing network protocols and formally verifying their specification. The framework incorporates a plugin architecture to enhance flexibility and extensibility for diverse testing scenarios, facilitate reproducible and scalable experiments leveraging Ivy and Shadow, and improve testing efficiency by enabling automated workflows through YAML-based configuration management. Its modular design validates complex protocol properties, adapts to dynamic behaviors, and facilitates seamless plugin integration for scalability. Moreover, the framework enables a stateful fuzzer plugin to enhance implementation robustness checks.

2025-03-04T08:56:03Z Christophe Crochet John Aoga Axel Legay http://arxiv.org/abs/2503.01389v1 2025-03-03T10:39:38Z

We develop a self-learning approach for conjecturing of induction predicates on a dataset of 16197 problems derived from the OEIS. These problems are hard for today's SMT and ATP systems because they require a combination of inductive and arithmetical reasoning. Starting from scratch, our approach consists of a feedback loop that iterates between (i) training a neural translator to learn the correspondence between the problems solved so far and the induction predicates useful for them, (ii) using the trained neural system to generate many new induction predicates for the problems, (iii) fast runs of the z3 prover attempting to prove the problems using the generated predicates, (iv) using heuristics such as predicate size and solution speed on the proved problems to choose the best predicates for the next iteration of training. The algorithm discovers on its own many interesting induction predicates, ultimately solving 5565 problems, compared to 2265 problems solved by CVC5, Vampire or Z3 in 60 seconds.

2025-03-03T10:39:38Z Thibault Gauthier Josef Urban http://arxiv.org/abs/2503.00727v1 2025-03-02T04:43:08Z

In this paper, we propose AUKAI, an Adaptive Unified Knowledge-Action Intelligence for embodied cognition that seamlessly integrates perception, memory, and decision-making via multi-scale error feedback. Interpreting AUKAI as an embedded world model, our approach simultaneously predicts state transitions and evaluates intervention utility. The framework is underpinned by rigorous theoretical analysis drawn from convergence theory, optimal control, and Bayesian inference, which collectively establish conditions for convergence, stability, and near-optimal performance. Furthermore, we present a hybrid implementation that combines the strengths of neural networks with symbolic reasoning modules, thereby enhancing interpretability and robustness. Finally, we demonstrate the potential of AUKAI through a detailed application in robotic navigation and obstacle avoidance, and we outline comprehensive experimental plans to validate its effectiveness in both simulated and real-world environments.

2025-03-02T04:43:08Z Maijunxian Wang http://arxiv.org/abs/2501.00364v3 2025-02-28T17:13:11Z

Reward machines (RMs) are an effective approach for addressing non-Markovian rewards in reinforcement learning (RL) through finite-state machines. Traditional RMs, which label edges with propositional logic formulae, inherit the limited expressivity of propositional logic. This limitation hinders the learnability and transferability of RMs since complex tasks will require numerous states and edges. To overcome these challenges, we propose First-Order Reward Machines ($\texttt{FORM}$s), which use first-order logic to label edges, resulting in more compact and transferable RMs. We introduce a novel method for $\textbf{learning}$ $\texttt{FORM}$s and a multi-agent formulation for $\textbf{exploiting}$ them and facilitate their transferability, where multiple agents collaboratively learn policies for a shared $\texttt{FORM}$. Our experimental results demonstrate the scalability of $\texttt{FORM}$s with respect to traditional RMs. Specifically, we show that $\texttt{FORM}$s can be effectively learnt for tasks where traditional RM learning approaches fail. We also show significant improvements in learning speed and task transferability thanks to the multi-agent learning framework and the abstraction provided by the first-order language.

2024-12-31T09:31:15Z AAMAS'25 Leo Ardon Daniel Furelos-Blanco Roko Parac Alessandra Russo http://arxiv.org/abs/2502.19944v1 2025-02-27T10:13:42Z

Statistics and Optimization are foundational to modern Machine Learning. Here, we propose an alternative foundation based on Abstract Algebra, with mathematics that facilitates the analysis of learning. In this approach, the goal of the task and the data are encoded as axioms of an algebra, and a model is obtained where only these axioms and their logical consequences hold. Although this is not a generalizing model, we show that selecting specific subsets of its breakdown into algebraic atoms obtained via subdirect decomposition gives a model that generalizes. We validate this new learning principle on standard datasets such as MNIST, FashionMNIST, CIFAR-10, and medical images, achieving performance comparable to optimized multilayer perceptrons. Beyond data-driven tasks, the new learning principle extends to formal problems, such as finding Hamiltonian cycles from their specifications and without relying on search. This algebraic foundation offers a fresh perspective on machine intelligence, featuring direct learning from training data without the need for validation dataset, scaling through model additivity, and asymptotic convergence to the underlying rule in the data.

2025-02-27T10:13:42Z Fernando Martin-Maroto Nabil Abderrahaman David Mendez Gonzalo G. de Polavieja http://arxiv.org/abs/2312.17380v2 2025-02-25T10:38:32Z

Consider a sparse polynomial in several variables given explicitly as a sum of non-zero terms with coefficients in an effective field. In this paper, we present several algorithms for factoring such polynomials and related tasks (such as gcd computation, square-free factorization, content-free factorization, and root extraction). Our methods are all based on sparse interpolation, but follow two main lines of attack: iteration on the number of variables and more direct reductions to the univariate or bivariate case. We present detailed probabilistic complexity bounds in terms of the complexity of sparse interpolation and evaluation.

2023-12-28T22:06:11Z Alexander Demin Joris van der Hoeven