Science & Mathematics

Reasoning about higher identity types uses two equalities, strict equality and equivalence of cells witnessed by a path. Strict equality is a congruence for every operation on cells, but associativity and the identity laws fail for it. Equivalence of cells satisfies those two laws, but it is not a congruence. Representations of higher identity types often conflate equational properties that hold strictly with those that hold only up to a path. We separate the two and axiomatize the former, introducing SEq, an equational theory generated by eleven axioms for strict equality between cells. We prove soundness and completeness for homotopy models, and completeness already over finite CW-complexes. Nine of these axioms form a strongly normalizing rewrite system whose normal forms are unique up to picture equivalence, and the resulting word problem is decidable in exponential time. We also give presheaf models over a cubical base category in which composition arises from a pushout in the base category itself, without requiring Kan filling structure. The same pushout structure provides explicit higher-dimensional witnesses for associativity and the identity laws.

Multi-agent reinforcement learning (MARL) offers a principled way of populating simulated economies with many heterogeneous decision makers. Its adoption, pioneered in finance, has nonetheless been slow in macroeconomics because of two main limitations: the lack of a shared frame of reference connecting MARL systems to dynamic stochastic general equilibrium (DSGE) models the profession already trusts, and the very long training times. The first limitation was recently addressed by the Multi-Agent Reinforcement Learning Business Cycle (MARL-BC), which places deep RL households in a real business cycle economy and reduces to classic DSGE models in specific limits. Here we address the second limitation. We present JaxMARL-BC, a JAX-accelerated simulator that trains MARL-BC economies in seconds (between 75x and 724x faster than the reference implementation), and scales to 200,000 independent learning households. We verify its correctness against the known DSGE limits, characterise its scaling through a simple cost law, and demonstrate its value by a proof-of-concept calibration of an extended model with heterogeneous returns on capital, in a two-hour experiment that would previously have taken over a month. We release JaxMARL-BC as open source.

Deep research systems iteratively plan, gather evidence, synthesize, and revise, making end-to-end latency a key bottleneck for interactive use. Almost all production systems are built on autoregressive (AR) language models and inherit left-to-right decoding in planning and long-form writing. We present DiffResearch, an open multi-agent deep research framework that places a diffusion language model (dLLM) at the core of every stage, and measure how a diffusion backbone changes latency and report quality. Holding the agentic scaffold, retrieval code, prompts, and evaluation fixed, we swap the backbone between an open diffusion model and a comparable AR model. Across 100 Deep Research Bench tasks, the diffusion backbone is roughly 6 times faster end-to-end, driven by order-of-magnitude reductions in planning and writing. We further introduce dFast, a decomposition mode that reads intermediate denoising states and extracts subqueries before generation finishes, providing a 1.99 times median speedup for decomposition in isolation with no loss of report quality. On the benchmark's RACE rubric, dFast obtains the best overall score among the three configurations. Finally, in a public system-level leaderboard snapshot, an instance built on a stronger diffusion model ranks above several commercial systems. We release DiffResearch under an Apache-2.0 license.

Natural direct and indirect effects are defined through cross-world interventional counterfactuals. We propose an alternative construction based on backtracking counterfactuals. Rather than intervening on the treatment or mediator, we use a backtracking conditional distribution to construct an alternative exogenous state satisfying a desired treatment-mediator constraint. This yields the backtracking direct and indirect effects, and also the backtracking total effect. Likewise, we adapt the population intervention effects.

This paper charts the evolution of the Prolog textbook Simply Logical -- Intelligent Reasoning by Example from print with runnable programmes on a 3.5-inch diskette published in 1994, via various intermediate online versions, to the fully interactive online edition available today. Our aim is to investigate -- from both the writer's and the reader's perspectives -- the potential impact of technology on educational materials. The three authors of this paper present three distinct and complementary points of view, which come together to shape an interactive online book that offers an immersive learning experience. Peter describes the philosophy behind the original book and experiences teaching from it. Jan demonstrates how contemporary web programming has enabled a fully interactive realisation of the book's philosophy. Kacper reports how different technologies can be adopted to build a versatile authoring toolkit that underpins the interactive online edition of the book. Collating these distinct yet coherent perspectives allows us to reflect on future opportunities for interactive Prolog teaching materials arising from the continuous development of web technologies. The insights we offer should be of interest to teachers of Prolog as well as those wanting to find out about the latest educational technologies.

In this paper, we study continuous-time reinforcement learning, where the state follows an unknown stochastic differential equation but only a fixed off-policy batch of discrete-time transitions is available. Standard discrete-time Q-learning becomes problematic as the sampling interval shrinks, because differences between action values vanish. Continuous-time alternatives, such as Deep Advantage Updating and martingale q-learning, preserve the action signal but jointly learn a value function and an action-dependent critic. Building on the PhiBE-Q formulation (arXiv:2606.21925), we develop a model-free PhiBE policy iteration (PhiBE-PI) framework that uses a single state-action critic while preserving the continuous-time action-ranking scale. At each iteration, the framework learns the critic directly from sampled increments and uses it to improve the policy. The same batch is reused throughout, without explicitly estimating the drift or diffusion. We further develop an implementation under linear function approximation and establish a local end-to-end suboptimality guarantee for the learned policy. Our analysis quantifies how errors from time discretization, function approximation, and finite-sample policy evaluation propagate through policy iteration. It accounts for the dependence of successive policies on the reused data, so the guarantee does not require a fresh batch at each iteration. Moreover, we identify a bias-variance trade-off: smaller sampling intervals improve the approximation to the continuous-time problem but can increase statistical error at a fixed sample size. Thus, finer time discretization does not necessarily lead to better policy performance.

Language generation in the limit studies whether a learner observing an enumeration of an unknown target language can eventually generate only valid, previously unseen elements. We study stability, introduced by Kalavasis, Mehrotra, and Velegkas (2025), which requires the generator's infinite output set to eventually remain unchanged, and introduce the stronger notion of certifiability, which requires the generator to determine from its observations that its current output is valid. Drawing on teaching sets in learning theory, we introduce a hierarchy of teaching dimensions for generation under three increasingly strict success criteria: correctness, stability, and certifiability. These dimensions measure the minimum number of selected examples whose appearance guarantees the corresponding success condition. We also study stability and certifiability in the membership-query model of Charikar and Pabbaraju (2025). We characterize stable and certifiable generation, both with and without query feedback, and establish their relationships with uniform generation and identification in the limit. In particular, we give a finite-witness characterization of stable generation, analogous to Angluin's tell-tale characterization of identification, resolving a gap left open by Kalavasis, Mehrotra, and Velegkas (2025). We further compare these generation notions with identification in the limit and contrast their teaching requirements on well-studied language families, including regular and erasing pattern languages.

Blind and visually impaired individuals face uncertainty when navigating unfamiliar areas. Whether a cane or a guide dog is used for navigation, this may prove to be challenging. To mitigate this challenge, we present the Context-Aware Navigation Explanation framework that explains guide dog movements for obstacle avoidance and navigation using a large language model. This system integrates perceptual context with planned future trajectories to generate natural-language explanations of robot movement. We deploy the system on a Unitree Go2 platform in indoor navigation scenarios and evaluate how different explanation context configurations affect user trust and explanation satisfaction. Results show a strong positive relationship between explanation satisfaction and trust, and suggest that combining obstacle information with future trajectory leads to the most effective explanations. These findings highlight the potential of context-aware language explanations to improve transparency and trust in assistive robot navigation.

Generative LLMs can label spans without task-specific training, but their output is not tied to positions in the input: a returned span may be absent from the input or occur several times. We present constrained tagging, a training-free method in which the model reproduces the input and wraps each span in labeled inline markup. A logits processor using a byte-level token trie and a finite-state machine admits only tokens that continue the input verbatim or form a valid tag, so the output reproduces the input exactly with labels from the given set, and spans may begin or end at any character boundary, even inside a token. Two-phase decoding lets reasoning models reason before the constraint engages. On six datasets and six open-weight models, the guarantee holds in all but 0.022% of 255,312 constrained generations, each failure a reasoning model exhausting its token budget or never closing its reasoning, and the constraint adds no measurable cost. Unlike context-based prompting, which loses 8.5% of its spans, constrained tagging locates every span it proposes on every dataset; it is as accurate on two datasets, and on the other four its errors lie in which spans the model chooses, not where they are.

With the increasing complexity and scalability demands of cryogenic electronic systems, such as quantum computing platforms, conversion of power within the cryogenic environment has become a primary concern. Magnetic inductors are among the key components affecting converter performance, as their electrical and magnetic properties can change significantly at low temperatures. In this paper, five commercially available Vishay SMD power inductors are experimentally characterized down to 4 K: DC resistance is measured continuously during cooldown, while frequency-dependent AC inductance and resistance are measured up to 2 MHz at both room temperature and 4 K. The results show substantial DC resistance reductions of 25x-58x at 4 K, while the inductance degrades by only about 5-5.5%. Although cryogenic operation slightly increases the AC resistance (due to the intensified skin effect) and raises core losses, converter-level analysis shows an inductor-only efficiency improvement of approximately 5.3-6.9 percentage points at 1 A, and up to 22.8 points at 3 A. The measured frequency-dependent impedance of each inductor is imported into Cadence and a complete single-phase 24 V-to-1 V buck converter with GaN power devices is simulated at 1, 2, and 3 A at 4 K. The full-converter efficiency at 4 K is shown to improve by 3.0-5.2 percentage points at 1 A and by up to 22.5 points at 3 A for the AC-characterized devices. These findings indicate that commercially available off-the-shelf power inductors remain operationally viable under cryogenic conditions and can simultaneously increase inductor efficiency and reduce the overall power loss in cryogenic power conversion systems.

Modern robotic agents are increasingly expected to support steerable control, where a single policy can adjust its behavioral style at runtime under changing user preferences. Preference-conditioned reinforcement learning provides this interface, but conditioning alone does not ensure that a requested behavior change is strong, does not leak into unrelated behaviors, and does not compromise task performance. Our evaluation combines Preference Reward Responsiveness (PRR) with coverage and utility metrics. We use these measures to compare reward-level, advantage-level, loss-level, and PCGrad-based aggregation across two humanoid-control frameworks. No aggregation level performs best across all environments and criteria. Experiments show that aggregating objectives early produces a wider range of behavioral responses but greater unintended changes in other objectives, while aggregating them later improves control precision at some cost to responsiveness.

Solvers for graph isomorphism and related problems are widely used in both theoretical and applied domains, but their complexity often requires users to trust their correctness without verification. We present a certifying algorithm for computing a generating set of the automorphism group of a given graph, meaning that it produces an independently verifiable certificate that the output list of automorphisms generates the entirety of the automorphism group. The problem of constructing a certificate is reduced to certifying that a system of multivariate polynomial equations is infeasible. An individualization-refinement algorithm produces a derivation within an algebraic proof system, representing a Nullstellensatz certificate of infeasibility. We provide an implementation of both the certifying algorithm and a certificate verifier, and demonstrate their viability on graphs with hundreds of vertices.

This technical report documents the design and implementation of Scriptorium, a digital library search interface designed to support multi-human, multi-AI collaboration: full cross-user transparency of search activity combined with a Manager--Worker architecture of seven role-specialized generative AI agents. A companion short demonstration paper describes Scriptorium's interaction design; because a demonstration format is constrained to a few pages, it necessarily omits most implementation detail. This report documents Scriptorium's complete system architecture, data model, collaborative-interaction design rationale, and AI orchestration mechanism, including verbatim agent prompts, the deterministic guardrails that constrain them, the language model and retrieval configuration, and the steps needed to run the system, so that the design can be inspected, critiqued, reproduced, and reused by other researchers. We also discuss the system's current limitations and the user study we are planning to evaluate its central hypothesis: that combining collaborative transparency with scoped multi-agent AI assistance increases serendipitous cross-pollination between collaborators' research threads.

We study deterministic gossiping in unknown strongly connected directed radio networks with $n$ vertices, $m$ arcs, and distinct identifiers in $[N]$, where $N=n^{\mathcal O(1)}$. Messages are unrestricted and collision detection is unavailable. Our neighborhood-clearing procedure reuses an elected receiver to secure its entire closed in-neighborhood in $\mathcal O(n\log^2n\log\log n)$ rounds. Charging each distinct closed neighborhood once yields $\mathcal O(m\log^2n\log\log n)$ rounds under an explicit degree-concentration condition, for every polynomial identifier range. A complementary adaptive-pruning procedure combines quadratic contraction with completion sensitive to the number of unsecured sources. If $a\ge1$ sources remain at completion entry, permutation selectors reduce the balanced completion budget by a factor of $\log^{2/3}(a+1)$ relative to interleaved path selectors. A geometric execution attains $\widetilde{\mathcal O}(k^2+nτ+\min\{u^2,(nu)^{2/3}\})$ for a path cover of scale $k$, weight $τ$, and $u$ exceptions. For directed graphs with common in- and out-degree $Δ$, the portfolio achieves $\widetilde{\mathcal O}(\min\{n\sqrtΔ,n^2/Δ\})$. Every graph also admits $\widetilde{\mathcal O}(\min\{n^{4/3},N+(mn)^{3/5}\})$ rounds. Only $n,N$ are inputs; degrees, covers, and structural constants are used solely in the analysis. The unrestricted polynomial-identifier density extension remains open.

In interval graphs and many generalizations thereof, problems such as Matching, Independent Set, and Dominating Set can be solved with simple greedy algorithms in linear (i.e., $O(m+n)$) time. However, it is sometimes possible to improve on this runtime if a suitable representation as intersection graph is given; for example it is possible to find a minimum dominating set in an interval graph in $O(n)$ time. We study RDV graphs, a generalization of interval graphs, namely, the intersection graphs of directed paths in a rooted tree. It was known that the above three problems can be solved in $O(n\log n)$ time if a suitably small representation is given. In this paper, we reduce the runtime to $O(n)$. Furthermore, while the previous results used non-trivial operations such as range-minimum queries and ray-shooting queries, we need nothing more complicated than lists and (for Matching) a Union-Find data structure.