Premise selection is a critical bottleneck in interactive theorem proving, particularly with large libraries. Existing methods, primarily relying on semantic embeddings, often fail to effectively leverage the rich structural information inherent in mathematical expressions. This paper proposes a novel framework for premise selection based on the structure of expression trees. The framework enhances premise selection ability by explicitly utilizing the structural information of Lean expressions and by means of the simplified tree representation obtained via common subexpression elimination. Our method employs a multi-stage filtering pipeline, incorporating structure-aware similarity measures including the Weisfeiler-Lehman kernel, tree edit distance, Constnode Jaccard similarity, and collapse-match similarity. An adaptive fusion strategy combines these metrics for refined ranking. To handle large-scale data efficiently, we incorporate cluster-based search space optimization and structural compatibility constraints. Comprehensive evaluation on a large theorem library extracted from Mathlib4 demonstrates that our method significantly outperforms existing premise retrieval tools across various metrics. Experimental analysis, including ablation studies and parameter sensitivity analysis, validates the contribution of individual components and highlights the efficacy of our structure-aware approach and multi-metric fusion.

We provide more information on AIPS' deductive engine and the training process for the value network. To highlight the reasoning ability and maintain readability of proofs, we avoid using brute-force methods such as augmentation-substitution and Wu's method Wu [1978].

We explore if RL can be useful for symbolic mathematics. Previous work showed contrastive learning can solve linear equations in one variable. We show model-free PPO \cite{schulman2017proximal} augmented with curiosity-based exploration and graph-based actions can solve nonlinear equations such as those involving radicals, exponentials, and trig functions. Our work suggests curiosity-based exploration may be useful for general symbolic reasoning tasks.

We provide more information on AIPS' deductive engine and the training process for the value network. To highlight the reasoning ability and maintain readability of proofs, we avoid using brute-force methods such as augmentation-substitution and Wu's method Wu [1978].

--Appointment scheduling is a great challenge in healthcare operations management. Appointment rules (AR) provide medical practitioners with a simple yet effective tool to determine patient appointment times. Genetic programming (GP) can be used to evolve ARs. However, directly applying GP to design ARs may lead to rules that are difficult for end-users to interpret and trust. A key reason is that GP is unaware of the dimensional consistency, which ensures that the evolved rules align with users' domain knowledge and intuitive understanding. In this paper, we develop a new dimensionally aware GP algorithm with dimension repair to evolve ARs with dimensional consistency and high performance. A key innovation of our method is the dimension repair procedure, which optimizes the dimensional consistency of an expression tree while minimizing structural changes and ensuring that its output dimension meets the problem's requirements. We formulate the task as a mixed-integer linear programming model that can be efficiently solved using common mathematical programming methods. With the support of the dimension repair procedure, our method can explore a wider range of AR structures by temporarily breaking the dimensional consistency of individuals, and then restoring it without altering their overall structure, thereby identifying individuals with greater potential advantages. We evaluated the proposed method in a comprehensive set of simulated clinics. The experimental results demonstrate that our approach managed to evolve high-quality ARs that significantly outperform not only the manually designed ARs but also existing state-of-the-art dimensionally aware GP methods in terms of both objective values and dimensional consistency. In addition, we analyzed the semantics of the evolved ARs, providing insight into the design of more effective and interpretable ARs. PPOINTMENT scheduling plays a crucial role in healthcare systems, impacting clinical, operational, and financial performance. A well-designed appointment system can improve the efficiency of medical providers and patient satisfaction by smoothing demand and mitigating uncertainty in patient arrivals [1]. Patients expect fast and timely service and find long wait times increasingly difficult to tolerate. Medical providers face pressure to efficiently utilize resources, including doctors' availability and expensive diagnostic machines.

Additionally, existing zero-cost proxies fail to generalize across neural architecture design spaces.

In a regression task, a function is learned from labeled data to predict the labels at new data points. The goal is to achieve small prediction errors. In symbolic regression, the goal is more ambitious, namely, to learn an interpretable function that makes small prediction errors. This additional goal largely rules out the standard approach used in regression, that is, reducing the learning problem to learning parameters of an expansion of basis functions by optimization. Instead, symbolic regression methods search for a good solution in a space of symbolic expressions. To cope with the typically vast search space, most symbolic regression methods make implicit, or sometimes even explicit, assumptions about its structure. Here, we argue that the only obvious structure of the search space is that it contains small expressions, that is, expressions that can be decomposed into a few subexpressions. We show that systematically searching spaces of small expressions finds solutions that are more accurate and more robust against noise than those obtained by state-of-the-art symbolic regression methods. In particular, systematic search outperforms state-of-the-art symbolic regressors in terms of its ability to recover the true underlying symbolic expressions on established benchmark data sets.

Solutions of symbolic regression problems are expressions that are composed of input variables and operators from a finite set of function symbols. One measure for evaluating symbolic regression algorithms is their ability to recover formulae, up to symbolic equivalence, from finite samples. Not unexpectedly, the recovery problem becomes harder when the formula gets more complex, that is, when the number of variables and operators gets larger. Variables in naturally occurring symbolic formulas often appear only in fixed combinations. This can be exploited in symbolic regression by substituting one new variable for the combination, effectively reducing the number of variables. However, finding valid substitutions is challenging. Here, we address this challenge by searching over the expression space of small substitutions and testing for validity. The validity test is reduced to a test of functional dependence. The resulting iterative dimension reduction procedure can be used with any symbolic regression approach. We show that it reliably identifies valid substitutions and significantly boosts the performance of different types of state-of-the-art symbolic regression algorithms.

The ultimate goal of verification is to guarantee the safety of deployed neural networks. Here, we claim that all the state-of-the-art verifiers we are aware of fail to reach this goal. Our key insight is that theoretical soundness (bounding the full-precision output while computing with floating point) does not imply practical soundness (bounding the floating point output in a potentially stochastic environment). We prove this observation for the approaches that are currently used to achieve provable theoretical soundness, such as interval analysis and its variants. We also argue that achieving practical soundness is significantly harder computationally. We support our claims empirically as well by evaluating several well-known verification methods. To mislead the verifiers, we create adversarial networks that detect and exploit features of the deployment environment, such as the order and precision of floating point operations. We demonstrate that all the tested verifiers are vulnerable to our new deployment-specific attacks, which proves that they are not practically sound.