Online bipartite matching, where agents are known in advance but items arrive sequentially and must be irrevocably assigned, is fundamental to problems ranging from ride-sharing to online advertising. When agents belong to classes such as demographic groups or geographic regions, fairness demands equitable treatment across these groups. Recent work introduced class envy-freeness (CEF), a natural extension of the classical fair division notion: an algorithm is α-CEF if each class receives value at least an α fraction of what it could extract from any other class's bundle. However, all known algorithms achieving constant-factor CEF guarantees attain utilitarian social welfare (total matching value) of at most 1/2 times the optimum, far below the 1-1/e≈ 0.632 achievable without fairness constraints. We resolve the open question of whether fairness necessitates this efficiency loss, by introducing threshold-based algorithms parameterized by γ∈ [0,1] that equalize allocations across classes until threshold γ, then maximize efficiency. For divisible matching, this yields simultaneous (1-e^-γ)-CEF and (1 - e^γ-1/γ+1)-USW guarantees; for indivisible matching, 2-CEF with the same USW. Setting γ> 0 produces the first algorithms beating 1/2-USW while maintaining constant CEF. We complement this with a novel upper bound construction, proving no non-wasteful α-CEF algorithm can exceed 1 +α- e^α-1/1+α-USW and correcting prior bounds that were vacuous for α< 0.58. Our upper bound nearly matches our algorithms' performance, giving the first substantive characterization of the price of fairness in online class matching.

While Large Language Models (LLMs) have demonstrated exceptional capabilities in mathematical reasoning, they frequently produce subtle errors that evade human detection. Formal mathematical languages like Lean 4 offer mechanical proof checking, strongly motivating the need for autoformalization: the automatic translation of natural language mathematics into verifiable code. Recent trends indicate that general-purpose LLMs, heavily optimized for standard programming, now outperform smaller models explicitly fine-tuned for Lean. Leveraging this shift, we introduce an agentic autoformalization framework powered by general coding LLMs. At the core of our system is an orchestrator that manages a multi-agent pipeline tailored for research-level mathematics. Because cutting-edge research frequently relies on concepts outside the scope of existing libraries like Mathlib, our system dynamically extends necessary type definitions and validates them via a novel Auxiliary Lemma technique before formalizing the primary theorems. We applied our approach to PutnamBench, producing machine-checked Lean proofs for a random sample of 32 problems. Furthermore, we evaluate our system on five papers from the ACM Symposium on Theory of Computing (STOC) spanning combinatorics, communication complexity, mechanism design, and learning theory, successfully formalizing their main theorems and validating the generated formalizations with human experts; for all five we also formalize the proofs alongside the statements, and notably two of them are proved with no axioms beyond Lean's kernel. All of our formalizations are available at https://beyondthelibrary.github.io/formal_arxiv .

Selecting representatives based on voters' preferences is a fundamental problem in social choice theory. While cardinal utility functions offer a detailed representation of preferences, ordinal rankings are often the only available information due to their simplicity and practical constraints. The metric distortion framework addresses this issue by modeling voters and candidates as points in a metric space, with distortion quantifying the efficiency loss from relying solely on ordinal rankings. Existing works define the cost of a voter with respect to a candidate as their distance and set the overall cost as either the sum (utilitarian) or maximum (egalitarian) of these costs across all voters. They show that deterministic algorithms achieve a best-possible distortion of 3 for any metric when considering a single candidate. This paper explores whether one can obtain a better approximation compared to an optimal candidate by relying on a committee of $k$ candidates ($k \ge 1$), where the cost of a voter is defined as its distance to the closest candidate in the committee. We answer this affirmatively in the case of line metrics, demonstrating that with $O(1)$ candidates, it is possible to achieve optimal cost. Our results extend to both utilitarian and egalitarian objectives, providing new upper bounds for the problem. We complement our results with lower bounds for both the line and 2-D Euclidean metrics.

CONTEXT:The gold-standard clamp measurements for insulin sensitivity (cSI), β-cell function (cBCF), and disposition index (cDI = cSI × cBCF) are not practical in large-scale studies. OBJECTIVE:We sought to 1) validate a mathematical model-derived DI from oral glucose tolerance tests (OGTT) with insulin (mDI) and without (mDI-woI) against cDI and oral disposition index (oDI) and 2) evaluate the ability of the novel indices to detect prediabetes and type 2 diabetes (T2D). METHODS:We carried out a secondary analysis of previously reported cross-sectional observational studies. The Insulin Sensitivity and Secretion mathematical model for glucose-insulin dynamics was applied to 5-point and 3-point OGTTs synchronized with hyperinsulinemic-euglycemic and hyperglycemic clamps from 130 youth with obesity (68 normal glucose tolerance [NGT], 33 impaired glucose tolerance [IGT], 29 T2D). RESULTS:Model-derived DI correlated well with clamp DI (R = 0.76 [logged]). Between NGT and IGT, mDI and mDI-woI decreased more than oDI and cDI, (60% and 59% vs 29% and 27%), and by receiver operating characteristic analysis were superior at detecting IGT compared with oDI and cDI (area under the curve [AUC] 0.88-0.87 vs 0.68-0.65), as was mean glucose (AUC 0.87). CONCLUSION:mDI-woI is better than oDI or the labor-intensive cDI for detecting dysglycemia in obese youth. Bypassing insulin measurements with mDI-woI from the OGTT provides a cost-effective approach for large-scale epidemiological studies of dysglycemia in youth.

Synthetic training data generation with Large Language Models (LLMs) like Google's Gemma and OpenAI's GPT offer a promising solution to the challenge of obtaining large, labeled datasets for training classifiers. When rapid model deployment is critical, such as in classifying emerging social media trends or combating new forms of online abuse tied to current events, the ability to generate training data is invaluable. While prior research has examined the comparability of synthetic data to human-labeled data, this study introduces a novel sampling algorithm, based on the maximum coverage problem, to select a representative subset from a synthetically generated dataset. Our results demonstrate that training a classifier on this contextually sampled subset achieves superior performance compared to training on the entire dataset. This "less is more" approach not only improves model accuracy but also reduces the volume of data required, leading to potentially more efficient model fine-tuning.

The online bipartite matching problem, extensively studied in the literature, deals with the allocation of online arriving vertices (items) to a predetermined set of offline vertices (agents). However, little attention has been given to the concept of class fairness, where agents are categorized into different classes, and the matching algorithm must ensure equitable distribution across these classes. We here focus on randomized algorithms for the fair matching of indivisible items, subject to various definitions of fairness. Our main contribution is the first (randomized) non-wasteful algorithm that simultaneously achieves a $1/2$ approximation to class envy-freeness (CEF) while simultaneously ensuring an equivalent approximation to the class proportionality (CPROP) and utilitarian social welfare (USW) objectives. We supplement this result by demonstrating that no non-wasteful algorithm can achieve an $\alpha$-CEF guarantee for $\alpha > 0.761$. In a similar vein, we provide a novel input instance for deterministic divisible matching that demonstrates a nearly tight CEF approximation. Lastly, we define the ``price of fairness," which represents the trade-off between optimal and fair matching. We demonstrate that increasing the level of fairness in the approximation of the solution leads to a decrease in the objective of maximizing USW, following an inverse proportionality relationship.

We here address the problem of fairly allocating indivisible goods or chores to $n$ agents with weights that define their entitlement to the set of indivisible resources. Stemming from well-studied fairness concepts such as envy-freeness up to one good (EF1) and envy-freeness up to any good (EFX) for agents with equal entitlements, we present, in this study, the first set of impossibility results alongside algorithmic guarantees for fairness among agents with unequal entitlements. Within this paper, we expand the concept of envy-freeness up to any good or chore to the weighted context (WEFX and XWEF respectively), demonstrating that these allocations are not guaranteed to exist for two or three agents. Despite these negative results, we develop a WEFX procedure for two agents with integer weights, and furthermore, we devise an approximate WEFX procedure for two agents with normalized weights. We further present a polynomial-time algorithm that guarantees a weighted envy-free allocation up to one chore (1WEF) for any number of agents with additive cost functions. Our work underscores the heightened complexity of the weighted fair division problem when compared to its unweighted counterpart.

We give the first non-trivial decremental dynamic embedding of a weighted, undirected graph $G$ into $\ell_p$ space. Given a weighted graph $G$ undergoing a sequence of edge weight increases, the goal of this problem is to maintain a (randomized) mapping $\phi: (G,d) \to (X,\ell_p)$ from the set of vertices of the graph to the $\ell_p$ space such that for every pair of vertices $u$ and $v$, the expected distance between $\phi(u)$ and $\phi(v)$ in the $\ell_p$ metric is within a small multiplicative factor, referred to as the distortion, of their distance in $G$. Our main result is a dynamic algorithm with expected distortion $O(\log^2 n)$ and total update time $O\left((m^{1+o(1)} \log^2 W + Q)\log(nW) \right)$, where $W$ is the maximum weight of the edges, $Q$ is the total number of updates and $n, m$ denote the number of vertices and edges in $G$ respectively. This is the first result of its kind, extending the seminal result of Bourgain '85 to the expanding field of dynamic algorithms. Moreover, we demonstrate that in the fully dynamic regime, where we tolerate edge insertions as well as deletions, no algorithm can explicitly maintain an embedding into $\ell_p$ space that has a low distortion with high probability.

Clustering is a fundamental building block of modern statistical analysis pipelines. Fair clustering has seen much attention from the machine learning community in recent years. We are some of the first to study fairness in the context of hierarchical clustering, after the results of Ahmadian et al. from NeurIPS in 2020. We evaluate our results using Dasgupta's cost function, perhaps one of the most prevalent theoretical metrics for hierarchical clustering evaluation. Our work vastly improves the previous $O(n^{5/6}poly\log(n))$ fair approximation for cost to a near polylogarithmic $O(n^\delta poly\log(n))$ fair approximation for any constant $\delta\in(0,1)$. This result establishes a cost fairness tradeoff and extends to broader fairness constraints than the previous work. We also show how to alter existing hierarchical clusterings to guarantee fairness and cluster balance across any level in the hierarchy.

Efficient and accurate methods to estimate insulin sensitivity (SI) and beta-cell function (BCF) are of great importance for studying the pathogenesis and treatment effectiveness of type 2 diabetes. Many methods exist, ranging in input data and technical requirements. Oral glucose tolerance tests (OGTTs) are preferred because they are simpler and more physiological. However, current analytical methods for OGTT-derived SI and BCF also range in complexity; the oral minimal models require mathematical expertise for deconvolution and fitting differential equations, and simple algebraic models (e.g., Matsuda index, insulinogenic index) may produce unphysiological values. We developed a new ISS (Insulin Secretion and Sensitivity) model for clinical research that provides precise and accurate estimates of SI and BCF from a standard OGTT, focusing on effectiveness, ease of implementation, and pragmatism. The model was developed by fitting a pair of differential equations to glucose and insulin without need of deconvolution or C-peptide data. The model is derived from a published model for longitudinal simulation of T2D progression that represents glucose-insulin homeostasis, including post-challenge suppression of hepatic glucose production and first- and second-phase insulin secretion. The ISS model was evaluated in three diverse cohorts including individuals at high risk of prediabetes (adult women with a wide range of BMI and adolescents with obesity). The new model had strong correlation with gold-standard estimates from intravenous glucose tolerance tests and hyperinsulinemic-euglycemic clamp. The ISS model has broad clinical applicability among diverse populations because it balances performance, fidelity, and complexity to provide a reliable phenotype of T2D risk.

We present an oracle-efficient relaxation for the adversarial contextual bandits problem, where the contexts are sequentially drawn i.i.d from a known distribution and the cost sequence is chosen by an online adversary. Our algorithm has a regret bound of $O(T^{\frac{2}{3}}(K\log(|\Pi|))^{\frac{1}{3}})$ and makes at most $O(K)$ calls per round to an offline optimization oracle, where $K$ denotes the number of actions, $T$ denotes the number of rounds and $\Pi$ denotes the set of policies. This is the first result to improve the prior best bound of $O((TK)^{\frac{2}{3}}(\log(|\Pi|))^{\frac{1}{3}})$ as obtained by Syrgkanis et al. at NeurIPS 2016, and the first to match the original bound of Langford and Zhang at NeurIPS 2007 which was obtained for the stochastic case.

Research in fair machine learning, and particularly clustering, has been crucial in recent years given the many ethical controversies that modern intelligent systems have posed. Ahmadian et al. [2020] established the study of fairness in hierarchical clustering, a stronger, more structured variant of its well-known flat counterpart, though their proposed algorithm that optimizes for Dasgupta's [2016] famous cost function was highly theoretical. Knittel et al. [2023] then proposed the first practical fair approximation for cost, however they were unable to break the polynomial-approximate barrier they posed as a hurdle of interest. We break this barrier, proposing the first truly polylogarithmic-approximate low-cost fair hierarchical clustering, thus greatly bridging the gap between the best fair and vanilla hierarchical clustering approximations.

Decision trees are widely used for their low computational cost, good predictive performance, and ability to assess the importance of features. Though often used in practice for feature selection, the theoretical guarantees of these methods are not well understood. We here obtain a tight finite sample bound for the feature selection problem in linear regression using single-depth decision trees. We examine the statistical properties of these "decision stumps" for the recovery of the s active features from p total features, where s

In this paper, we analyze a natural learning algorithm for uniform pacing of advertising budgets, equipped to adapt to varying ad sale platform conditions. On the demand side, advertisers face a fundamental technical challenge in automating bidding in a way that spreads their allotted budget across a given campaign subject to hidden, and potentially dynamic, cost functions. This automation and calculation must be done in runtime, implying a necessarily low computational cost for the high frequency auction rate. Advertisers are additionally expected to exhaust nearly all of their sub-interval (by the hour or minute) budgets to maintain budgeting quotas in the long run. To resolve this challenge, our study analyzes a simple learning algorithm that adapts to the latent cost function of the market and learns the optimal average bidding value for a period of auctions in a small fraction of the total campaign time, allowing for smooth budget pacing in real-time. We prove our algorithm is robust to changes in the auction mechanism, and exhibits a fast convergence to a stable average bidding strategy. The algorithm not only guarantees that budgets are nearly spent in their entirety, but also smoothly paces bidding to prevent early exit from the campaign and a loss of the opportunity to bid on potentially lucrative impressions later in the period. In addition to the theoretical guarantees, we validate our algorithm with experimental results from open source data on real advertising campaigns to further demonstrate the effectiveness of our proposed approach.

The Santa Claus problem is a fundamental problem in fair division: the goal is to partition a set of heterogeneous items among heterogeneous agents so as to maximize the minimum value of items received by any agent. In this paper, we study the online version of this problem where the items are not known in advance and have to be assigned to agents as they arrive over time. If the arrival order of items is arbitrary, then no good assignment rule exists in the worst case. However, we show that, if the arrival order is random, then for $n$ agents and any $\varepsilon > 0$, we can obtain a competitive ratio of $1-\varepsilon$ when the optimal assignment gives value at least $\Omega(\log n / \varepsilon^2)$ to every agent (assuming each item has at most unit value). We also show that this result is almost tight: namely, if the optimal solution has value at most $C \ln n / \varepsilon$ for some constant $C$, then there is no $(1-\varepsilon)$-competitive algorithm even for random arrival order.

Behavior during 3-4 Hz spike-wave discharges (SWDs) in absence epilepsy can vary from obvious behavioral arrest to no detectible deficits. Knowing if behavior is impaired is crucial for clinical care but may be difficult to determine without specialized behavioral testing, often inaccessible in practice. We aimed to develop a pure electroencephalography (EEG)-based machine-learning method to predict SWD-related behavioral impairment. Our classification goals were 100% predictive value, with no behaviorally impaired SWDs misclassified as spared; and maximal sensitivity. First, using labeled data with known behavior (130 SWDs in 34 patients), we extracted EEG time, frequency domain, and common spatial pattern features and applied support vector machines and linear discriminant analysis to classify SWDs as spared or impaired. We evaluated 32 classification models, optimized with 10-fold cross-validation. We then generalized these models to unlabeled data (220 SWDs in 41 patients), where behavior during individual SWDs was not known, but observers reported the presence of clinical seizures. For labeled data, the best classifier achieved 100% spared predictive value and 93% sensitivity. The best classifier on the unlabeled data achieved 100% spared predictive value, but with a lower sensitivity of 35%, corresponding to a conservative classification of 8 patients out of 23 as free of clinical seizures. Our findings demonstrate the feasibility of machine learning to predict impaired behavior during SWDs based on EEG features. With additional validation and optimization in a larger data sample, applications may include EEG-based prediction of driving safety, treatment adjustment, and insight into mechanisms of impaired consciousness in absence seizures.

Studies of attention emphasize cortical circuits for salience monitoring and top-down control. However, subcortical arousal systems have a major influence on dynamic cortical state. We hypothesize that task-related increases in attention begin with a "pulse" in subcortical arousal and cortical attention networks, which are reflected indirectly through transient fMRI signals. We conducted general linear model and model-free analyses of fMRI data from two cohorts and tasks with mixed block and event-related design. 46 adolescent subjects at our center and 362 normal adults from the Human Connectome Project participated. We identified a core shared network of transient fMRI increases in subcortical arousal and cortical salience/attention networks across cohorts and tasks. Specifically, we observed a transient pulse of fMRI increases both at task block onset and with individual task events in subcortical arousal areas including midbrain tegmentum, thalamus, nucleus basalis and striatum; cortical-subcortical salience network regions including the anterior insula/claustrum and anterior cingulate cortex/supplementary motor area; in dorsal attention network regions including dorsolateral frontal cortex and inferior parietal lobule; as well as in motor regions including cerebellum, and left hemisphere hand primary motor cortex. The transient pulse of fMRI increases in subcortical and cortical arousal and attention networks was consistent across tasks and study populations, whereas sustained activity in these same networks was more variable. The function of the transient pulse in these networks is unknown. However, given its anatomical distribution, it could participate in a neuromodulatory surge of activity in multiple parallel neurotransmitter systems facilitating dynamic changes in conscious attention.