arXiv Science⌕ Search

SEARCH · arXiv Science

Results for “math.LO”

Search indexed arXiv papers on artificial intelligence, large language models, computer vision and robotics. Read source abstracts and follow links to arXiv.

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

996 records · Page 5Linked to original sources
arXiv2026

Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free

In May 2026 an OpenAI model produced a counterexample to the Erdős unit distance conjecture. Five mathematicians published a human-verified version the same day, and the result entered the literature within weeks. In August 2026 the same laboratory published ten mathematical and theoretical computer science results, each accompanied by a machine-checkable Lean 4 certificate with no unproved steps. Four weeks later, one remained the subject of an unresolved dispute over whether its formalization meant what it claimed. We argue that this difference is structural. We distinguish three layers of verification: derivational validity, which a kernel checks; representational fidelity, whether the formal statement means the intended question; and epistemic significance. Only the first is mechanizable. Making it effectively free therefore does not eliminate verification work but shifts the burden to layers dependent on scarce expert attention. Measurements of the August corpus illustrate the shift. The kernel-checked proofs total 20.6 MB, while the statements requiring human audit total 55.6 KB, a ratio of 379 to 1. Yet those statements contain 218 bespoke definitions rather than relying on community-vetted ones. The audit surface is therefore small in volume but irreducibly expert. We argue that machine checking produces verification abundance while leaving adjudication scarce. We propose a six-category taxonomy of representational mismatch, a disclosure schema for machine-generated mathematical claims, and implications for software, cryptography, and regulated decision systems.

cs.AI↗
arXiv2026

Intelligent Reflecting Surface Deployment for Low-Altitude Coverage: Illumination Geometry, Directional Characteristics, and Optimization

Terrestrial base stations (BSs) are typically configured with fixed downtilt to serve ground users, resulting in weak illumination of low-altitude airspace even under line-of-sight (LoS) propagation. In this paper, we establish a channel model that incorporates BS and intelligent reflecting surface (IRS) radiation patterns for three-dimensional (3D) low-altitude coverage while preserving the existing BS configuration. We formulate a budget-constrained IRS deployment problem that jointly determines candidate-site selection, IRS orientations, and phase shifts to maximize the worst-case signal-to-noise ratio (SNR) over the 3D low-altitude airspace. The selected sites and optimized IRS parameters remain fixed after deployment, yielding a quasi-static IRS configuration. We characterize the illumination geometry between the fixed-downtilt BS and rooftop candidates by deriving the nonnegative installation-height range satisfying the BS main-lobe condition. The separation between the mapped main-lobe height boundaries grows linearly with horizontal BS-to-site distance and decreases inversely with the number of BS antennas. We further derive an analytical lower bound on the regional worst-case normalized array gain achievable through IRS phase design over served directions with different direction spans. The resulting sufficient direction span decreases inversely with the square root of the number of IRS elements when the same worst-case normalized gain guarantee is maintained. We develop a mixed-integer alternating optimization (AO) algorithm to solve the resulting problem. Simulation results validate the analytical characterizations and show that the proposed scheme achieves higher worst-case SNR than benchmarks across different deployment budgets.

cs.IT↗
arXiv2026

On Good-for-MDPs Automata

Nondeterministic good-for-MDPs (GFM) automata are for MDP model checking and reinforcement learning what good-for-games (GFG) automata are for reactive synthesis: a more compact alternative to deterministic automata that displays nondeterminism, but only so much that it can be resolved locally, such that a syntactic product can be analysed. GFM has recently been introduced as a property for reinforcement learning, where the simpler Büchi acceptance conditions it allows to use is key. However, while there are classic and novel techniques to obtain automata that are GFM, there has not been a decision procedure for checking whether or not an automaton is GFM. We show that GFM-ness is decidable and provide an EXPTIME decision procedure as well as a PSPACE-hardness proof. We also compare the succinctness of GFM automata with other types of automata with restricted nondeterminism. The first natural comparison point are GFG automata. Deterministic automata are GFG, and GFG automata are GFM, but not vice versa. This raises the question of how these classes relate in terms of succinctness. GFG automata are known to be exponentially more succinct than deterministic automata, but the gap between GFM and GFG automata as well as the gap between ordinary nondeterministic automata and those that are GFM have been open. We establish that these gaps are exponential, and sharpen this result by showing that the latter gap remains exponential when restricting the nondeterministic automata to separating safety or unambiguous reachability automata.

cs.FL↗
arXiv2026

Property Testing for Recursive Query Languages

In the context of database querying, property testing provides a framework for testing query answers with high confidence while inspecting only a sublinear part of the database, through completion queries and size queries. A fundamental result of Chen and Yoshida (2019) states that non-satisfaction of a Boolean conjunctive query $q$ is testable with a constant number of such queries and one-sided error if and only if $q$ is equivalent to an $α$-acyclic query. In this article, we initiate the study of property testing for recursive query languages, focusing on two-way regular path queries (2RPQs) and monadic Datalog. One of our main results is positive: non-answers to any 2RPQ are constant query testable with one-sided error. We extend this slightly to a certain class of monadic Datalog programs in which recursion is restricted to be linear and rule bodies must be $α$-acyclic. Turning towards unrestricted monadic Datalog, we next show that if a monadic Datalog program $Π$ is not equivalent to an $α$-acyclic program, then falsity of $Π$ is not constant query testable with one-sided error. This is under the assumption that all rule-bodies are self-join free. We leave open the case of monadic Datalog programs with $α$-acyclic rule bodies that are not restricted to linear recursion, but observe as a first step that there exist $α$-acyclic programs that are mildly non-linear and constant query testable with one-sided error.

cs.DB↗
arXiv2026

A characterization of efficiently compilable constraint languages

A central task in knowledge compilation is to compile a CNF-SAT instance into a succinct representation format that allows efficient operations such as testing satisfiability, counting, or enumerating all solutions. Useful representation formats studied in this area range from ordered binary decision diagrams (OBDDs) to circuits in decomposable negation normal form (DNNFs). While it is known that there exist CNF formulas that require exponential size representations, the situation is less well studied for other types of constraints than Boolean disjunctive clauses. The constraint satisfaction problem (CSP) is a powerful framework that generalizes CNF-SAT by allowing arbitrary sets of constraints over any finite domain. The main goal of our work is to understand for which type of constraints (also called the constraint language) it is possible to efficiently compute representations of polynomial size. We answer this question completely and prove two tight characterizations of efficiently compilable constraint languages, depending on whether target format is structured. We first identify the combinatorial property of ``strong blockwise decomposability'' and show that if a constraint language has this property, we can compute DNNF representations of linear size. For all other constraint languages we construct families of CSP-instances that provably require DNNFs of exponential size. For a subclass of ``strong uniformly blockwise decomposable'' constraint languages we obtain a similar dichotomy for structured DNNFs. In fact, strong (uniform) blockwise decomposability even allows efficient compilation into multi-valued analogs of OBDDs and FBDDs, respectively. Thus, we get complete characterizations for all knowledge compilation classes between O(B)DDs and DNNFs.

cs.LO↗
arXiv2026

On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number

This paper investigates $\exists\mathbb{R}(r^{\mathbb{Z}})$, that is the extension of the existential theory of the reals by an additional unary predicate $r^{\mathbb{Z}}$ for the integer powers of a fixed computable real number $r > 0$. If all we have access to is a Turing machine computing $r$, it is not possible to decide whether an input formula from this theory satisfiable. However, we show an algorithm to decide this problem when: 1. $r$ is known to be transcendental, or 2. $r$ is a root of some given integer polynomial (that is, $r$ is algebraic). In other words, knowing the algebraicity of $r$ suffices to circumvent undecidability. Furthermore, we establish complexity results under the proviso that $r$ enjoys what we call a polynomial root barrier. Using this notion, we show that the satisfiability problem of $\exists\mathbb{R}(r^{\mathbb{Z}})$ is 1. in NEXPTIME if $r$ is a natural number, 2. in EXPSPACE if $r$ is an algebraic number, and 3. in 3EXP if $r$ belongs to a family of transcendental numbers including $π$ and Euler's $e$. As a by-product of our results, we are able to remove the appeal to Schanuel's conjecture from the proof of decidability of the entropic risk threshold problem for stochastic games with rational probabilities, rewards and threshold [Baier et al., MFCS'23]: when the base of the entropic risk is Euler's $e$ and the aversion factor is a fixed algebraic number, the problem is in EXP.

cs.LO↗
arXiv2026

The Price of Remembering: A Calibrated Energy Law for Computation

Where does a computer's energy go? Mostly into keeping, not into computing. A bit held in fast storage draws power for every second it stays there, and it costs energy again each time it moves between storage levels. We call the first cost \emph{rent} and the second \emph{fare}, and we state one law: the energy of a computation is at least its operations, plus rent on every live bit for as long as it lives, plus fare on every bit moved. The model under the law prices control as well as data. There is no free clock, and any unpriced register would make the theorems false. One lemma does most of the work: every use of a value is paid for by rent, by fare, or by computing the value again. Three things follow. Exact attention brings every past token back for every new one, so its energy grows with the square of the context length, while a recurrent model with a fixed state grows linearly. The square is a theorem for machines that never re-read past tokens. Under a stated serving hypothesis it is the fare on every past token, which passes the model's own arithmetic near ten thousand tokens, the point where long-context serving becomes bandwidth-bound today. Known bounds on memory over time become joule floors: on any sequential machine with volatile working storage, sorting $n$ items pays rent proportional to $n^2/\log n$ bit-steps on most inputs, and the bound for scrypt makes every password guess cost joules that no amount of parallel hardware reduces.

cs.PF↗
arXiv2026

Identification of Bivariate Causal Directionality Based on Anticipated Asymmetric Geometries

Identification of causal directionality in bivariate numerical data is a fundamental research problem with important practical implications. This paper presents two alternative methods to identify direction of causation by considering conditional distributions: (1) Anticipated Asymmetric Geometries (AAG) and (2) Monotonicity Index (MI). The AAG method compares the actual conditional distributions to anticipated ones along two variables. Different comparison metrics, such as Pearson correlation, cosine distance, Jaccard index, K-L divergence, K-S distance, MAE, MSE, and mutual information have been evaluated. Anticipated distributions have been projected as normal based on dual response statistics: mean and standard deviation. The MI method compares the calculated monotonicity indexes of the gradients of conditional distributions along two axes and exhibits counts of gradient sign changes. Both methods assume stochastic properties of the bivariate data and exploit anticipated unimodality of conditional distributions of the effect. The proposed methods are straightforward and include only a limited number of hyperparameters that affect the accuracy of the identification. For a given set of hyperparameters, both the AAG and MI methods provide a unique, deterministic solution. To address sensitivity to hyperparameters, tuning has been done by utilizing a full factorial Design of Experiment. It turns out that the AAG method outperforms MI, achieving top weighted accuracies of 81.4% with simple tuning and 84.3% with size-adaptive tuning, compared with 81.6% for GRCI or 82.0% for CAREFL-H on the 99 pairs of the Tubingen real-world cause-effect examples. A decision tree has been fitted to distinguish misclassified cases using the input data's symmetrical bivariate statistics to address the question of: How decisive is the identification method of causal directionality?

cs.LG↗
arXiv2026

Why Better Models Can Create Riskier Systems: Evidence from LLM Agents in Financial Markets

Large language models (LLMs) are being deployed at scale in consequential real-world systems, from financial markets to content moderation to hiring. We show that improving individual model capability can degrade rather than improve system-level outcomes. We hypothesize that shared training and architectures can lead more capable LLMs to behave more similarly, creating correlated actions that do not diversify away. We develop a general framework showing how this correlation creates a non-diversifiable risk floor and test its predictions in financial markets using an agent-based simulation with LLM traders of varying general-purpose capability. We find that: (1) frontier LLMs exhibit significantly correlated behavior that increases with capability; (2) when their shared reasoning is accurate, increasing agent participation reduces market-level risk; and (3) when agents share a common misinformation environment, the same correlated behavior becomes a liability. Together, these results identify a capability paradox: improving individual models does not necessarily produce better system-level outcomes. Whether the same dynamics arise in other domains is an open empirical question.

cs.AI↗
arXiv2026

Unary Functions, Automorphisms, and Unlabeled First-Order Model Counting

Every fixed first-order sentence $φ$ determines an enumerative sequence $n\mapsto\mathrm{FOMC}(φ,n)$, counting its models on the labeled domain $[n]$. We study the complexity of these sequences when logical specifications may use genuine unary function symbols and hence nested terms $x,f(x),f^2(x),\ldots$. We first prove that, for every fixed sentence $φ\in\mathrm{C}^1_{=}[f]$, with one unary function and an arbitrary finite relational vocabulary, $\mathrm{FOMC}(φ,n)$ is computable in time polynomial in $n$. By contrast, permitting either a second variable or a second unary function already yields hardness. Without counting quantifiers, there is a fixed sentence in $\mathrm{FO}^2_{=}[f]$ whose model-counting function is $\#\mathrm{P}_1$-complete. With one variable and two unary functions, there is a fixed constant-free universal sentence in $\mathrm{FO}^1_{=}[f,g]$, using only unary predicates besides $f$ and $g$, whose model-counting function is again $\#\mathrm{P}_1$-complete. We also relate labeled and unlabeled enumeration exactly. For every relational sentence $φ$, we construct an extension $φ_{\mathrm{aut}}$ in which a unary function records an automorphism and $\mathrm{FOMC}(φ_{\mathrm{aut}},n)=n!\cdot\mathrm{UFOMC}(φ,n)$, where $\mathrm{UFOMC}(φ,n)$ denotes the number of $n$-element models of $φ$ up to isomorphism. Thus automorphism marking gives a one-query exact reduction from unlabeled to labeled model counting at the same domain size. Over relational vocabularies of maximum arity at most $k$, where $k\geq2$, eliminating the auxiliary function yields single-query reductions from unlabeled $\mathrm{FO}^k_{=}$ and $\mathrm{C}^k$ model counting to labeled $\mathrm{FO}^{k+1}_{=}$ and $\mathrm{C}^{k+1}$ model counting, respectively.

cs.LO↗
arXiv2026

Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing

Formal theorem proving with large language models remains challenging due to the difficulty of navigating large proof search spaces efficiently. Existing tree search approaches either feed verbose compiler error messages directly into the generation context, increasing context usage during search, or employ non-standard evaluation protocols that prevent direct comparison with established baselines. We propose a three-role Monte Carlo Tree Search (MCTS) framework that treats the Lean 4 compiler purely as a reward oracle using compiler output as a scalar signal for UCB-guided tree updates without feeding error content into the generation context. Our framework decomposes proof search into three roles: a generator for proof attempts, a decomposer for subgoal decomposition, and a critic for subgoal quality evaluation. We evaluate across 4 benchmarks spanning competition mathematics and physics (MiniF2F, PutnamBench, LeanPhysBench, PhysLeandata) with three prover models at standard proof attempt budgets (PAB@16 to PAB@256). Our method achieves 87.1\% on MiniF2F with Goedel-Prover-V2-8B at PAB@256 and solves 26/659 PutnamBench problems at PAB@32 surpassing base sampling 18/659 at same proof attempt budget. Through an exhaustive axiom-level audit of every compiled proof, we further identify reward hacking in search-based theorem proving: DeepSeek-Prover-V2-7B produces proofs on PutnamBench that pass compilation and the standard sorry-token scan while depending on sorryAx. The audit removes 4 and 8 such proofs from whole-proof sampling at PAB@32 and PAB@128, and 11 and 19 from MCTS. We do not attribute these counts to the search procedure; we report them to establish that kernel-level auditing is necessary for compiler-verified evaluation.

cs.AI↗
arXiv2026

A quantum let within the lambda calculus

Since the seminal work of Selinger and Valiron, the standard design for quantum lambda calculi has kept the quantum state outside the program: terms manipulate pointers to an external register. This is largely due to the difficulty of eliminating tensor products. For example, the calculus $λ_ρ^\circ$ embeds density matrices directly within terms, where terms carry the entire computation state, a feature particularly appealing for program verification. However, lacking a tensor elimination construct, it can neither access the individual qubits of a compound state nor discard them. Borgna showed that this inability to discard qubits makes the calculus strictly less expressive than the quantum lambda calculus of Selinger and Valiron. In this paper we show that tensor elimination is possible in this setting. The key observation is that the Pauli decomposition, combined with the spectral decomposition of the Pauli matrices, allows any $n$-qubit density matrix to be expressed as a real linear combination of tensor products of single-qubit density matrices. Exploiting this fact, we extend $λ_ρ^\circ$ with a construct $\mathrm{let}\ x^{\otimes n} = ρ \mathrm{in}\ t$, which binds each $x_i$ to a single-qubit density matrix arising from the decomposition of $ρ$. We equip the extended calculus with a rewrite system, a type system, and a denotational semantics, and prove Subject Reduction, Progress, Strong Normalisation, Soundness, and Adequacy. The new construct also recovers the missing ability to discard qubits, thereby restoring expressiveness. Moreover, we show that this is achieved in a physically principled way: a variable unused in $t$ is interpreted exactly as being partial-traced out, as dictated by the no-deleting theorem. We illustrate the resulting compositionality through quantum teleportation and the three-qubit bit-flip code.

cs.LO↗
arXiv2026

Diversifying Long Prompt Image Generation through Structured Prompt Embedding Space Sampling

Modern text-to-image models produce impressive visual results from richly specified prompts, yet their behavior under long prompts remains insufficiently understood. In this paper, we study a practical failure mode in which accumulated semantic constraints progressively suppress output variation, causing diversity to collapse even when many visual factors remain unspecified. We show that this phenomenon appears consistently across recent generation models as prompt length increases, and provide a theoretical motivation that connects long-prompt conditioning with reduced sampling entropy in the prompt embedding space. Based on this observation, we introduce PromptMoG, a training-free approach that samples prompt embeddings from a Mixture-of-Gaussians distribution to restore generative flexibility while maintaining semantic fidelity. To support systematic evaluation, we further present LPD-Bench, a structured benchmark of long and semantically dense prompts for measuring both fidelity and diversity under compositional text conditioning. Extensive experiments on four large-scale diffusion models, including SD3.5-Large, Flux.1-Krea-Dev, CogView4, and Qwen-Image, show that PromptMoG consistently improves diversity for long-prompt image generation. The code is publicly available at https://github.com/basiclab/PromptMoG.

cs.CV↗
arXiv2026

A Rubric-Guided Large Language Model Solution for Opioid Use Disorder Computable Phenotyping

Opioid use disorder (OUD) remains a public health crisis in the United States, yet it is difficult to identify from electronic health records (EHRs) because missing diagnosis codes and supporting evidence are buried in clinical narratives. Accurate OUD identification is critical to support interventions and improve health outcomes. This study developed a rubric-guided large language model (LLM) that incorporated Optimization by PROmpting (OPRO) for OUD computable phenotyping (CP). The framework used an 18-item, expert-identified rubric to instruct LLMs to automatically extract critical text with supporting evidence to determine OUD flags. Two UF Health physicians (GMR and WMG) chart-reviewed 253 patients, including 68 OUD-positive cases. Our LLM-based computable phenotype (CP) achieved the best F1 score of 0.774 and an AUROC of 0.934, outperforming the machine learning-based CP using EHR and natural language processing-extracted variables, and zero-shot LLMs by relative F1 improvements of 12.8% and 44.4%, respectively. The proposed LLM-based CP could link LLM-extracted evidence to OUD phenotyping for better explainability.

cs.CL↗
arXiv2026

EarlyEval: Cheaper Agent Evaluation via Early Outcome Prediction

Evaluating LLM agents is essential for guiding their development, yet it has grown prohibitively expensive: a single pass of a frontier model over an agentic benchmark can cost hundreds to thousands of dollars, a price paid repeatedly across iterative development cycles. Prior efforts, centered on benchmark distillation, reduce the number of evaluation tasks but leave the cost of executing each retained task untouched. In this work, we introduce early outcome prediction, a complementary axis of efficiency that instead cuts cost within each task. Our key insight is that an agent's final outcome is often evident from its intermediate behavior well before execution completes. We instantiate this idea in EarlyEval, a lightweight framework that trains a pair of LightGBM success and failure classifiers over behavioral, textual, and reference-solution features, and halts an agent run the moment either classifier crosses a calibrated confidence threshold, adding negligible per-step overhead. Across three benchmarks, SWE-bench Verified, TerminalBench, and Toolathlon, EarlyEval can eliminate 13%-26% of agent steps and up to 44.1% input tokens and 29.4% output tokens at 89%-97% prediction accuracy, while perturbing per-agent resolve rates by only one to two percentage points on average.

cs.CL↗
arXiv2026

Are Non-English Papers Reviewed Fairly? Language-of-Study Bias in NLP Peer Reviews

Peer review plays a central role in the NLP publication process, but is susceptible to various biases. Here, we study language-of-study (LoS) bias: the tendency for reviewers to evaluate a paper differently based on the language(s) it studies, rather than its scientific merit. Despite being explicitly flagged in reviewing guidelines, such biases are poorly understood. Prior work treats such comments as part of broader categories of weak or unconstructive reviews without defining them as a distinct form of bias. We present the first systematic characterization of LoS bias, distinguishing negative and positive forms, and introduce the human-annotated dataset LOBSTER (Language-Of-study Bias in ScienTific pEer Review) and an LLM-based detection pipeline achieving 87.37 macro F1. We analyze 15,645 reviews to estimate how negative and positive biases differ with respect to the LoS, and find that non-English papers face substantially higher bias rates than English-only ones, with negative bias consistently outweighing positive bias. Finally, we identify four subcategories of negative bias, and find that demanding unjustified cross-lingual generalization is the most dominant form. We publicly release all resources to support work on fairer reviewing practices in NLP and beyond.

cs.CL↗
arXiv2026

The $\mathsf{AC}^0$-Complexity Of Visibly Pushdown Languages

We study the question of which visibly pushdown languages (VPLs) are in the complexity class $\mathsf{AC}^0$ and how to effectively decide this question. Our contribution is to introduce a particular subclass of one-turn VPLs, called intermediate VPLs, for which the raised question is entirely unclear: to the best of our knowledge our research community is unaware of containment or non-containment in $\mathsf{AC}^0$ for any language in our newly introduced class. Our main result states that there is an algorithm that, given a visibly pushdown automaton, correctly outputs exactly one of the following: that its language $L$ is in $\mathsf{AC}^0$, some $m\geq 2$ such that $L$ is $\mathsf{ACC}^0(m)$-hard (implying that $L$ is not in $\mathsf{AC}^0$), or a finite disjoint union of intermediate VPLs that $L$ is constant-depth equivalent to. In the latter of the three cases one can moreover effectively compute $k,l\in\mathbb{N}_{>0}$ with $k\not=l$ such that the concrete intermediate VPL $L(S\rightarrow \varepsilon\mid a c^{k-1} S b_1\mid ac^{l-1}Sb_2)$ is constant-depth reducible to the language $L$. Due to their particular nature we conjecture that either all intermediate VPLs are in $\mathsf{AC}^0$ or all are not. As a corollary of our main result we obtain that in case the input language is a visibly counter language our algorithm can effectively determine if it is in $\mathsf{AC}^0$ - hence our main result generalizes a result by Krebs et al. stating that it is decidable if a given visibly counter language is in $\mathsf{AC}^0$ (when restricted to well-matched words). For our proofs we revisit so-called Ext-algebras (introduced by Czarnetzki et al.), which are closely related to forest algebras (introduced by Bojańczyk and Walukiewicz), and use Green's relations.

cs.FL↗
arXiv2026

Extending Fill-In-the-Middle with Instructions for Steerable Code Completion

Code completion models often fail when the developer's intent is under-specified in the code context. To mitigate this, developers frequently use natural language comments to clarify objectives. However, current code completion models fail to prioritize these directives effectively since they are merely pre-trained using the Fill-In-the-Middle (FIM) objective. On the one hand, the natural language instructions, mixed with the noisy code comments, are just treated as part of the background context within the prefix. On the other hand, the pre-training datasets for the FIM objective are mostly sourced from open-source repositories, which results in a scarcity of high-intent instruction-to-code pairings that reflect the developers' workflow in code completion. To bridge this gap, we propose Instruction-aware Fill-In-the-Middle (IFIM), a fine-tuning method that extends the FIM structure with a dedicated, structurally separated instruction section. Our evaluation shows that IFIM substantially improves adherence to developer intent, while leaving infilling performance unchanged when no instruction is given. The gains hold on an in-the-wild benchmark of 100 instructions written by real developers and across model scales from 1.5B to 7B. IFIM thus offers a backward-compatible upgrade path for existing FIM-based code completion systems at a modest training cost.

cs.SE↗