Large Language Models have transformed automated code generation across general programming domains. In the specialized field of operations research, however, translating natural language problem descriptions into executable optimization solver code remains difficult due to strict syntactic requirements. Existing methods relying on static retrieval or one-shot generation frequently fail to align human intent with rigid solver APIs, resulting in hallucinated constraints and execution errors. To address this, we introduce CHORUS++, an agentic framework that replaces fragile one-shot generation with a loop of hierarchical retrieval, multi-layer validation, and iterative self-correction. Our results show that this approach allows open-source models, such as Llama-3.3 (70B), to achieve an accuracy of 78.89 × despite extensive documentation changes. By closing the feedback loop between generation and execution, CHORUS++ provides a scalable, privacy-preserving method for utilizing advanced optimization technologies without reliance on costly proprietary models.
Lifted inference exploits indistinguishabilities in probabilistic graphical models by using a representative for indistinguishable objects, thereby speeding up query answering while maintaining exact answers. In this article, we show how lifting can be applied to efficiently compute causal effects in relational domains. More specifically, we introduce parametric causal factor graphs (PCFGs) to incorporate causal knowledge in lifted models and give a formal semantics of interventions therein. We further present the Lifted Causal Inference (LCI) algorithm to compute causal effects on a lifted level, thereby drastically speeding up causal inference compared to propositional inference, e.g., in causal Bayesian networks. In addition, we present partially directed parametric causal factor graphs (PD-PCFGs) as a generalisation of PCFGs to handle partial causal knowledge and extend LCI to perform lifted causal inference in a PD-PCFG, thereby extending the applicability of lifted causal inference to a broader range of models requiring less prior knowledge about causal relationships.
Least general generalization is the problem of finding the most specific term that can generate all given terms via substitutions. It is also known as anti-unification and is considered a dual of the most general unification. It is known that both the least general generalization problem and the unification problem can be solved in polynomial time; however the latter becomes NP-hard when commutative function symbols are allowed. In this paper, we study the complexity of the least general generalization problem with commutative functions, formulated as a minimization problem. In particular, we show that this problem is NP-hard even if both input and output terms are restricted so that each variable occurs only once. We also show that this restricted variant can be solved in polynomial time if both the maximum arity and the number of input terms are bounded by constants. For the general terms, we present exponential-time algorithms for finding the most specific term in some restricted cases and in the general case.
In this paper, we focus on the prediction phase of a random forest and study the problem of representing a bag of decision trees using a smaller bag of decision trees, where we only consider binary decision problems on the binary domain and simple decision trees in which an internal node is limited to querying the Boolean value of a single variable. As a main result, we show that given a constant integer c the majority function of an odd number n of variables can be represented by a bag of n-2c decision trees each of which has size polynomial in n. We also show that a general bag of n decision trees can be represented by another bag containing only n-2c polynomial-size decision trees, provided a small classification error is allowed. A related result on the k-out-of-n functions is presented as well.
As artificial intelligence (AI) systems increasingly make decisions that affect human lives, formal tools for reasoning about norms, preferences, and uncertainty become essential. This paper presents an algebraic extension of input/output (I/O) logic for normative reasoning under uncertainty. We generalize I/O logic over Boolean algebras and abstract logics, characterize a family of derivation systems, and explore how alternative closure operators can support reasoning in the presence of normative uncertainty. We incorporate preference models into the framework, providing a mechanism for filtering normative outputs based on conditional desirability. We further demonstrate how the resulting formalism can be embedded into classical higher-order logic (HOL), enabling implementation within the LogiKEy framework. While motivated by AI applications–particularly the design of systems sensitive to ethical and legal constraints–the primary contribution of this work is a general-purpose formal foundation for reasoning about norms and preferences in uncertain settings.
Surrogate-based multi-objective optimization has become a cornerstone technique for tackling expensive real-world problems in science and engineering. This survey focuses on surrogate-based algorithms that use the decision-maker’s preference information to guide the search toward the most preferred areas of the Pareto front. Considering such preferences not only facilitates the decision-making process for the user but also helps the analyst to save expensive computational budget. This extended survey provides the first comprehensive overview of both explicit and implicit preference modeling within surrogate-based multi-objective optimization. Explicit preferences refer to information directly provided by the decision maker, such as reference points, weights, or rankings, that can be incorporated into the optimization algorithm. Implicit preferences, in contrast, arise from structural properties of the Pareto front itself, such as knee regions, and can be used to guide the search even when the decision maker cannot articulate preferences. We provide an overview of the state-of-the-art, highlight the most important shortcomings in the literature, and present promising directions for further research.
Job shop scheduling problems address the routing and sequencing of tasks in a job shop setting. Despite significant interest from operations research and machine learning communities over the years, a comprehensive platform for testing and comparing solution methods has been notably lacking. To fill this gap, we introduce a unified implementation of job shop scheduling problems and their solution methods, addressing the long-standing need for a standardized benchmarking platform in this domain. Our platform supports classic Job Shop (JSP), Flow Shop (FSP), Flexible Job Shop (FJSP), and Assembly Job Shop (AJSP), as well as variants featuring Sequence-Dependent Setup Times (SDST), variants with online arrivals of jobs, and combinations of these problems (e.g., FJSP-SDST and FAJSP). The platform provides a wide range of scheduling solution methods, from heuristics, metaheuristics, and exact optimization to deep reinforcement learning. The implementation is available as an open-source GitHub repository ( https://github.com/ai-for-decision-making-tue/Job_Shop_Scheduling_Benchmark_Environments_and_Instances ), serving as a collaborative hub for researchers, practitioners, and those new to the field. Beyond enabling direct comparisons with existing methods on widely studied benchmark problems, this resource serves as a robust starting point for addressing constrained and complex problem variants. By establishing a comprehensive and unified foundation, this platform is designed to consolidate existing knowledge and to inspire the development of next-generation algorithms in job shop scheduling research.
Combinatorial optimization problems represent a critical class of challenges in the field of operations research and computer science. These problems involve making optimal choices from a finite set of possibilities, subject to specific constraints, with the aim of optimizing a certain objective function. Combinatorial optimization encompasses a diverse array of applications, ranging from resource allocation, scheduling, and network design to logistics, facility location, and circuit design. However, most combinatorial optimization problems are NP-hard, which necessitates the development of sophisticated algorithms and heuristics to find near-optimal solutions efficiently. Researchers in this area continuously strive to devise innovative approaches, such as integer programming, dynamic programming, and metaheuristics, to address these challenges effectively. This paper investigates various NP-hard optimization problems, such as MAXCUT, MAXNAE2SAT, Subset Sum, and 0-1 Knapsack problem, with a focus on deriving exact solutions. We apply the framework of dataless neural networks to derive differentiable functions for each of these problems. Building on recent insights that a single differentiable function within a dataless neural network can solve the Maximum Independent Set problem, we adapt this methodology to address a broader array of combinatorial optimization problems. Additionally, we provide a thorough validation of the correctness of our derived functions. To demonstrate practical applicability, we implement the proposed MAXNAE2SAT dNN and extend it to capture MAXNAE3SAT through a principled modification of the objective function. The resulting solver requires no training data or hyperparameter tuning. We empirically evaluate the implementation on randomly generated instances and compare its performance against state-of-the-art combinatorial optimization solvers, including CP-SAT and Gurobi. Experimental results show that dNNs achieve competitive approximate solutions with sub-millisecond runtimes and substantially lower memory consumption, highlighting their potential as memory-efficient solvers for large-scale combinatorial optimization.
Partial functions are ubiquitous in Knowledge Representation applications, ranging from practical, e.g., business applications, to more abstract, e.g., mathematical and programming applications. Expressing propositions about partial functions may lead to non/denoting terms. These result in undefinedness errors and ambiguity, causing subtle modeling and reasoning problems. In our approach, formulae are well-defined (true or false) and non/ambiguous in all structures. We develop a base extension of three-valued predicate logic, in which partial function terms are guarded by domain expressions, ensuring the well/definedness property despite the three-valued nature of the underlying logic. This property allows us to define the satisfaction relation of the new logic in terms of the standard two-valued logic of total functions. To tackle the verbosity of this core language, we propose different ways to increase convenience by means of disambiguating annotations and non-commutative connectives. As a practically relevant result, we prove that many different unnesting methods, which eliminate (partial) functions by replacing them with their graph predicates, are equivalence-preserving in the proposed language. Furthermore, we present an extension of the logic with definitions of partial functions and give their semantics in terms of the existing semantics for inductive definitions of sets. Finally, we explore the connection to functional programming.
In this paper, we examine decision problems and optimization problems associated with linear programming. The problems we examine deal with different forms of linear refutations. Our focus is on three different forms of refutations, namely read-once refutations, tree-like refutations, and dag-like refutations. These forms of refutations differ in how they handle the reuse of constraints. Read-once refutations do not allow for the reuse of constraints. The only exception to this condition is if the constraint can be rederived using only unused constraints. Tree-like refutations do allow for the reuse of constraints. However, each time a constraint is reused, it needs to be rederived. This rederivation affects the length of the refutation. Dag-like refutations allow for the reuse of constraints without rederivation. Linear programming is in the complexity class P and hence, it must have short affirmative and disqualifying certificates. One of the more celebrated lemmata in linear programming is Farkas’ lemma, which establishes that both “yes" and “no" certificates can be thought of as solutions to complementary linear programs. Since then, it has been established that if a linear program is feasible, then it must have a solution which is bounded by a polynomial function of the input size. Our goal is to study the computational complexities of determining various constrained refutations for a given infeasible linear programming instance. We establish that checking if a linear program has a read-once refutation is NP-complete, even when it is defined by Binary Two Variable Per Inequality (BTVPI) constraints. Furthermore, the problems of finding the shortest read-once, tree-like, and dag-like refutations are NPO PB-complete, NPO-complete and NPO PB-complete respectively. We also show that the problems of finding bounded-length tree-like and dag-like refutations are NP-hard, even when each constraint has at most three non-zero coefficients.
In Bernoulli discriminative models, log-likelihood is a natural — and, in a well-defined sense, universal — choice of risk score. In this general setting, we propose a non-parametric variant of binary regression, where the model is regularized to be a Lipschitz function taking a metric space to [0, 1]. Our choice of logarithmic loss corresponds to the log-likelihood risk score. This setting presents novel computational and statistical challenges. On the computational front, we derive an efficient optimization algorithm based on interior point methods (IPM); an attractive feature is that it is parameter-free (that is, does not require tuning an update step size). On the statistical front, the unbounded loss function presents a problem for classic generalization bounds, based on covering-number and Rademacher techniques. Additionally, an impossibility result we prove shows that the unboundedness presents an inherent obstruction to learnability. We get around this challenge via an adaptive truncation approach, and also derive a lower bound indicating that the truncation is, in some sense, necessary. To our knowledge, our approach provides the first rigorous computational and theoretical results in this area. Finally, we present encouraging empirical results.
Ubiquitous reactive systems compute by reacting to stimuli from their environment. Their concurrence, nondeterminism and communication behaviours can usually be captured in the well-known Calculus of Communicating Systems (CCS), among other methods. Reactive systems usually suffer from changes related to fixing bugs or new requirements. This paper concerns the problem of automated revision of reactive systems for new requirements in some principle and observable way: A component should remain unchanged unless modification is necessary from the perspective of external observers. For this purpose, this paper generalizes the weak bisimulation of the CCS to given actions and presents a weak forgetting to logically discard given actions for the observable Hennessy-Milner Logic ℋ^O , which can capture the behaviour equivalence of the CCS under weak bisimulation. Finally, the weakest sufficient condition for ℋ^O theories is established via weak forgetting. This sufficient condition provides a theoretical foundation for automated revision of reactive systems (CCS) under the desired principle when the new requirements are expressed as ℋ^O formulas.
Support vector machine with Universum data (USVM) is an effective algorithm which utilizes the prior information embedded in Universum data to improve its generalization ability. However, the l_1 -loss adopted by USVM has an irrationality in geometric definition, which makes it unable to accurately reflect the location information of violated samples, thus degrading the model’s performance to some extent. To address the above limitation, we propose a novel elastic net support vector machine with Universum data (ENUSVM). It adopts the elastic net loss instead of l_1 -loss to achieve a one-to-one mapping between the training samples and the slack variables. This improvement makes it more reasonable in geometric definition and thus improves the performance. Further, we derive the violation tolerance upper bound for labeled samples and Universum samples to better interpret the numerical relationship between the distance of violated samples and the slack variables. Experiments on three artificial datasets and twenty benchmark datasets prove that our proposed ENUSVM performs better. Finally, to enhance the robustness of USVM, we incorporate the RoBoSS loss and propose the least squares RoBoSS USVM ( ℒ_RoBoSS -USVM). The performance is evaluated on five diverse UCI and KEEL datasets (with and without noise).
This paper introduces a novel and more efficient method for constructing oriented hierarchies within the framework of Statistical Implicative Analysis. The primary focus of this study is the computational complexity of the original algorithm proposed by Gras, whose cubic time complexity is established in this work. To address this limitation, a detailed combinatorial analysis of hierarchical structures is performed, leveraging tools from analytic combinatorics. This methodology facilitates the enumeration of the number of possible configurations as a function of input size and enables the investigation of both the depth and width characteristics of the hierarchy’s block structure. This study then proposes a reconstruction algorithm based on a formal correspondence between the statistical implication graph and the oriented hierarchy. The proposed method achieves quadratic worst-case complexity, thereby resulting in a substantial improvement in computational performance. Moreover, the analytic framework also makes it possible to characterise the average-case behaviour of the algorithm. The findings of the comparative computational experiments demonstrate the clear advantage of the proposed method over Gras’s algorithm, both in terms of execution time and overall algorithmic efficiency.
The circumscription is an elegant non-monotonic logic. However, computing circumscription remains challenging due to its computational complexity. This paper presents a weighted partial Maximum Satisfiability (MaxSAT) encoding approach that addresses circumscription, allowing us to leverage state-of-the-art MaxSAT solvers for efficient computation. This approach introduces a linear-time encoding scheme that captures both parallel and prioritized circumscription without requiring fresh predicates. Furthermore, we develop a systematic model enumeration strategy using blocking clauses, which enables the complete and efficient enumeration of circumscription models while avoiding redundancy. Extensive experiments have been conducted on benchmarks such as model-based circuit diagnostics, random and industrial SAT problems, and extended stable marriage problems. The results indicate that our MaxSAT-based implementation, circ-maxsat, achieves comparable performance with state-of-the-art methods such as circ2dlp and aspino. Notably, circ-maxsat outperforms other solvers on the (extended) stable marriage problem in terms of computational efficiency. This study advances the computation of circumscription and introduces new applications of MaxSAT in non-monotonic reasoning.
We study feedforward neural networks with inputs from a topological space (TFNNs). We prove a universal approximation theorem for shallow TFNNs, which demonstrates their capacity to approximate any continuous function defined on this topological space. As an application, we obtain an approximative version of Kolmogorov's superposition theorem for compact metric spaces.
We give an alternative proof of the statement, by using elimination from algebraic geometry, that the only set S⊂ℝ^2 , | S| =6 such that all subsets that form a triangle are isosceles triangles, is the regular pentagon with its center. Our proof can be extended to answer some related questions raised by Erdős.
Texas Graffiti (TxGraffiti) is an automated conjecturing system that operates on a finite, versioned snapshot table of mathematical objects equipped with precomputed numerical invariants and Boolean predicates. For a chosen target invariant and hypothesis predicate, TxGraffiti searches over predicate–predictor combinations and generates table-true conditional inequalities by fitting coefficients within simple, human-readable templates (e.g., univariate affine upper and lower bounds) via a sequence of small linear programs. The resulting candidates are ranked and compressed using heuristics that measure informativeness (e.g., touch/sharp behavior) and remove redundancy or transitive implication, producing a compact set of interpretable conjectures suitable for further testing and proof. We describe the system architecture, data curation workflow, optimization models, and filtering procedures, and we provide an interactive web interface together with an open-source Python implementation. Although our examples focus on graph invariants, the snapshot-table paradigm and optimization-and-filtering pipeline apply broadly whenever objects admit computable features and predicates.
