OpenRaiser/Intern-Atlas huggingface dataset:
SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Venue: arXiv cs.AI 2026
Year: 2026

We present SorryDB, a dynamically-updating benchmark of open Lean tasks drawn from 78 real world formalization projects on GitHub. Unlike existing static benchmarks, often composed of competition problems, hillclimbing the SorryDB benchmark will yield tools that are aligned to the community needs, more usable by mathematicians, and more capable of understanding complex dependencies. Moreover, by providing a continuously updated stream of tasks, SorryDB mitigates test-set contamination and offers a robust metric for an agent's ability to contribute to novel formal mathematics projects. We evaluate a collection of approaches, including generalist large language models, agentic approaches, and specialized symbolic provers, over a selected snapshot of 1000 tasks from SorryDB. We show that current approaches are complementary: even though an agentic approach based on Gemini Flash is the most performant, it is not strictly better than other off-the-shelf large-language models, specialized provers, or even a curated list of Lean tactics.
ITLC at SemEval-2026 Task 11: Normalization and Deterministic Parsing for Formal Reasoning in LLMs
Venue: arXiv cs.CL 2026
Year: 2026

Large language models suffer from content effects in reasoning tasks, particularly in multi-lingual contexts. We introduce a novel method that reduces these biases through explicit structural abstraction that transforms syllogisms into canonical logical representations and applies deterministic parsing to determine validity. Evaluated on the SemEval-2026 Task 11 multilingual benchmark, our approach achieves top-5 rankings across all subtasks while substantially reducing content effects and offering a competitive alternative to complex fine-tuning or activation-level interventions.
LLMs for High-Frequency Decision-Making: Normalized Action Reward-Guided Consistency Policy Optimization
Venue: arXiv cs.AI 2026
Year: 2026

While Large Language Models (LLMs) form the cornerstone of sequential decision-making agent development, they have inherent limitations in high-frequency decision tasks. Existing research mainly focuses on discrete embodied decision scenarios with low-frequency and significant semantic differences in state space (e.g., household planning). These methods suffer from limited performance in high-frequency decision-making tasks, since high-precision numerical state information in such tasks undergoes frequent updates with minimal fluctuations, and exhibiting policy misalignment between the learned sub-tasks and composite tasks. To address these issues, this paper proposes Normalized Action Reward guided Consistency Policy Optimization (NAR-CP). 1) Our method first acquires predefined dense rewards from environmental feedback of candidate actions via reward functions, then completes reward shaping through normalization, and theoretically verifies action reward normalization does not impair optimal policy. 2) To reduce policy misalignment in composite tasks, we use LLMs to infer sub-observation candidate actions and generate joint policies, with consistency loss ensuring precise alignment between global semantic policies and sub-semantic policies. Experiments on UAV pursuit, a typical high-frequency task, show our method delivers superior performance on independent and composite tasks with excellent generalization to unseen tasks.
MMH-Planner: Multi-Mode Hybrid Trajectory Planning Method for UAV Efficient Flight Based on Real-Time Spatial Awareness
Venue: arXiv cs.RO 2026
Year: 2026

Motion planning is a critical component of intelligent unmanned systems, enabling their complex autonomous operations. However, current planning algorithms still face limitations in planning efficiency due to inflexible strategies and weak adaptability. To address this, this paper proposes a multi-mode hybrid trajectory planning method for UAVs based on real-time environmental awareness, which dynamically selects the optimal planning model for high-quality trajectory generation in response to environmental changes. First, we introduce a goal-oriented spatial awareness method that rapidly assesses flight safety in the upcoming environments. Second, a multi-mode hybrid trajectory planning mechanism is proposed, which can enhance the planning efficiency by selecting the optimal planning model for trajectory generation based on prior spatial awareness. Finally, we design a lazy replanning strategy that triggers replanning only when necessary to reduce computational resource consumption while maintaining flight quality. To validate the performance of the proposed method, we conducted comprehensive comparative experiments in simulation environments. Results demonstrate that our approach outperforms existing state-of-the-art (SOTA) algorithms across multiple metrics, achieving the best performance particularly in terms of the average number of planning iterations and computational cost per iteration. Furthermore, the effectiveness of our approach is further verified through real-world flight experiments integrated with a self-developed intelligent UAV platform.
Deterministic Edge Coloring with few Colors in CONGEST
Venue: arXiv cs.DS 2026
Year: 2026

As the main contribution of this work we present deterministic edge coloring algorithms in the CONGEST model. In particular, we present an algorithm that edge colors any $n$-node graph with maximum degree $Δ$ with with $(1+\varepsilon)Δ+O(\sqrt{\log n})$ colors in $\tilde{O}(\log^{2.5} n+\log^2 Δ\log n)$ rounds. This brings the upper bound polynomially close to the lower bound of $Ω(\log n/\log\log n)$ rounds that also holds in the more powerful LOCAL model [Chang, He, Li, Pettie, Uitto; SODA'18]. As long as $Δ\geq c\sqrt{\log n}$ our algorithm uses fewer than $2Δ-1$ colors and to the best of our knowledge is the first polylogarithmic-round CONGEST algorithm achieving this for any range of $Δ$. As a corollary we also improve the complexity of edge coloring with $2Δ-1$ colors for all ranges of $Δ$ to $\tilde{O}(\log^{2.5} n+\log^2 Δ\log n)$. This improves upon the previous $O(\log^8 n)$-round algorithm from [Fischer, Ghaffari, Kuhn; FOCS'17]. Our approach builds on a refined analysis and extension of the online edge-coloring algorithm of Blikstad, Svensson, Vintan, and Wajc [FOCS'25], and more broadly on new connections between online and distributed graph algorithms. We show that their algorithm exhibits very low locality and, if it can additionally have limited local access to future edges (as distributed algorithms can), it can be derandomized for smaller degrees. Under this additional power, we are able to bypass classical online lower bounds and translate the results to efficient distributed algorithms. This leads to our CONGEST algorithm for $(1+\varepsilon)Δ+O(\sqrt{\log n})$-edge coloring. Since the modified online algorithm can be implemented more efficiently in the LOCAL model, we also obtain (marginally) improved complexity bounds in that model.
Small Bottle, Big Pipe: Quantifying and Addressing the Impact of Data Centers on Public Water Systems
Venue: arXiv cs.CY 2026
Year: 2026

Water is a critical resource for data centers and an efficient means of cooling. However, meeting the growing water demand of data centers requires substantial peak water withdrawals, which many communities in the United States cannot supply, especially during the hottest days of the year. This largely overlooked water capacity constraint is emerging as a bottleneck for data centers and can force operators to rely on less efficient dry cooling, further stressing the power grid during summer peaks. In this paper, we focus on the direct water withdrawal of U.S. data centers for cooling and examine their impacts on public water systems. Our analysis indicates that, if the 2024 water use intensity persists, U.S. data centers could collectively require 697-1,451 million gallons per day (MGD) of new water capacity through 2030, comparable to New York City's average daily supply of roughly 1,000 MGD. Under an optimistic scenario with a compound annual water use intensity reduction by 10%, the water capacity demand decreases to 227-604 MGD, although high-growth IT loads could still require enough capacity to hypothetically supply about half of New York City for most of the year. The total valuation of the new water capacity is on the order of \$10 billion, reaching up to \$58 billion in the high-growth case. These impacts are highly concentrated on communities hosting data centers. Finally, we provide recommendations to address the growing water capacity demand of U.S. data centers, including reporting peak water use, developing corporate-community partnerships, adopting a Water Capacity Neutral approach (colloquially "Pipe Neutral") to allow host communities to retain limited water capacity resources, and implementing coordinated water-power planning to responsibly leverage water for peak power reduction and opportunistically utilize surplus power to mitigate impacts on public water systems.
MiM-DiT: MoE in MoE with Diffusion Transformers for All-in-One Image Restoration
Venue: arXiv cs.CV 2026
Year: 2026

All-in-one image restoration is challenging because different degradation types, such as haze, blur, noise, and low-light, impose diverse requirements on restoration strategies, making it difficult for a single model to handle them effectively. In this paper, we propose a unified image restoration framework that integrates a dual-level Mixture-of-Experts (MoE) architecture with a pretrained diffusion model. The framework operates at two levels: the Inter-MoE layer adaptively combines expert groups to handle major degradation types, while the Intra-MoE layer further selects specialized sub-experts to address fine-grained variations within each type. This design enables the model to achieve coarse-grained adaptation across diverse degradation categories while performing fine-grained modulation for specific intra-class variations, ensuring both high specialization in handling complex, real-world corruptions. Extensive experiments demonstrate that the proposed method performs favorably against the state-of-the-art approaches on multiple image restoration task.
The power of small initialization in noisy low-tubal-rank tensor recovery
Venue: arXiv cs.LG 2026
Year: 2026

We study the problem of recovering a low-tubal-rank tensor $\mathcal{X}\_\star\in \mathbb{R}^{n \times n \times k}$ from noisy linear measurements under the t-product framework. A widely adopted strategy involves factorizing the optimization variable as $\mathcal{U} * \mathcal{U}^\top$, where $\mathcal{U} \in \mathbb{R}^{n \times R \times k}$, followed by applying factorized gradient descent (FGD) to solve the resulting optimization problem. Since the tubal-rank $r$ of the underlying tensor $\mathcal{X}_\star$ is typically unknown, this method often assumes $r < R \le n$, a regime known as over-parameterization. However, when the measurements are corrupted by some dense noise (e.g., Gaussian noise), FGD with the commonly used spectral initialization yields a recovery error that grows linearly with the over-estimated tubal-rank $R$. To address this issue, we show that using a small initialization enables FGD to achieve a nearly minimax optimal recovery error, even when the tubal-rank $R$ is significantly overestimated. Using a four-stage analytic framework, we analyze this phenomenon and establish the sharpest known error bound to date, which is independent of the overestimated tubal-rank $R$. Furthermore, we provide a theoretical guarantee showing that an easy-to-use early stopping strategy can achieve the best known result in practice. All these theoretical findings are validated through a series of simulations and real-data experiments.
Practical FP4 Training for Large-Scale MoE Models on Hopper GPUs
Venue: arXiv cs.LG 2026
Year: 2026

Training large-scale Mixture-of-Experts (MoE) models is bottlenecked by activation memory and expert-parallel communication, yet FP4 training remains impractical on Hopper-class GPUs without native MXFP4 or NVFP4 support. In this work, we present a training recipe that enables MXFP4 efficiency for MoE models on Hopper architectures without native 4-bit computation support. A central challenge is to integrate FP4 into an existing BF16/FP8 hybrid training pipeline without incurring costly precision round-trips (e.g., FP4 $\leftrightarrow$ BF16 $\leftrightarrow$ FP8). We address this challenge by introducing direct FP8-to-FP4 quantization and de-quantization, together with scaling-aware FP4 row-wise to column-wise conversion, enabling FP4 activations and expert-parallel communication with minimal overhead. Core MoE computations are executed in FP8, while activations and expert-parallel communication are compressed using MXFP4, achieving substantial memory and bandwidth savings without degrading convergence. At the 671B parameter scale, our method achieves end-to-end training performance comparable to strong FP8 baselines, while reducing peak activation memory by 14.8\% (11.8 GB) and improving training throughput by 12.5\%, from 1157 to 1302 tokens per GPU per second. These results show that FP4 efficiency can be practically realized for large-scale MoE training through careful software-hardware co-design, even without native FP4 Tensor Core support.
Shatter Throughput Ceilings: Leveraging Reflection Surfaces to Enhance Transmissions for Vehicular Fast Data Exchange
Venue: arXiv cs.IT 2026
Year: 2026

Rapid emergence of smart mobility necessitates high-volume bursty data transmission over a single link between a target vehicle and its designated edge computing-enabled Base Station (BS) or Roadside Unit (RSU), which must be completed within a short time period when the vehicle traverses the coverage area. However, in bandwidth-limited scenarios, conventional communication systems face a fundamental throughput ceiling at each single vehicle. This limitation persists even when all time-frequency resources are allocated to a single vehicle, as the underlying channel lacks sufficient spatial diversity to support higher data rates. To break this throughput ceiling, in this paper, we propose a novel reflection-enhanced transmission framework by strategically employing dedicated specular reflecting surfaces along roadways to proactively augment the transmission environments. This setup concentrates dispersed signals from multiple directions toward a target vehicle, analogous to the light-focusing effect of a concave magnifying lens, thereby enhancing the spatial diversity and achievable rank of an individual channel. This allows a BS to allocate more transmission layers to one single user, consequently significantly raising the throughput ceiling for individual vehicles. Moreover, we also introduce dynamic virtualization methods for reflecting panel patch groups, compatible with existing communication systems, to flexibly manage interference with other coexisting users. Furthermore, collaborative rotation among multiple reflecting panels is introduced to enhance signal concentration. Finally, the schematic effectiveness is rigorously validated through 3GPP-compliant system-level simulations, demonstrating significant throughput boosts.
From Solver to Tutor: Evaluating the Pedagogical Intelligence of LLMs with KMP-Bench
Venue: arXiv cs.CL 2026
Year: 2026

Large Language Models (LLMs) show significant potential in AI mathematical tutoring, yet current evaluations often rely on simplistic metrics or narrow pedagogical scenarios, failing to assess comprehensive, multi-turn teaching effectiveness. In this paper, we introduce KMP-Bench, a comprehensive K-8 Mathematical Pedagogical Benchmark designed to assess LLMs from two complementary perspectives. The first module, KMP-Dialogue, evaluates holistic pedagogical capabilities against six core principles (e.g., Challenge, Explanation, Feedback), leveraging a novel multi-turn dialogue dataset constructed by weaving together diverse pedagogical components. The second module, KMP-Skills, provides a granular assessment of foundational tutoring abilities, including multi-turn problem-solving, error detection and correction, and problem generation. Our evaluations on KMP-Bench reveal a key disparity: while leading LLMs excel at tasks with verifiable solutions, they struggle with the nuanced application of pedagogical principles. Additionally, we present KMP-Pile, a large-scale (150K) dialogue dataset. Models fine-tuned on KMP-Pile show substantial improvement on KMP-Bench, underscoring the value of pedagogically-rich training data for developing more effective AI math tutors.
VSearcher: Long-Horizon Multimodal Search Agent via Reinforcement Learning
Venue: arXiv cs.CV 2026
Year: 2026

Large models are increasingly becoming autonomous agents that interact with real-world environments and use external tools to augment their static capabilities. However, most recent progress has focused on text-only large language models, which are limited to a single modality and therefore have narrower application scenarios. On the other hand, multimodal large models, while offering stronger perceptual capabilities, remain limited to static knowledge and lack the ability to access and leverage up-to-date web information. In this paper, we propose VSearcher, turning static multimodal model into multimodal search agent capable of long-horizon, multi-turn tool use in real-world web environments, including text search, image search, and web browsing, via reinforcement learning. Specifically, we introduce Iterative Injection Data Synthesis pipeline to generate large-scale, complex multimodal QA questions, which are further filtered with comprehensive metrics to ensure high quality and sufficient difficulty. We then adopt an SFT-then-RL training pipeline to turn base multimodal models to agent capable of multi-turn tool calling in real-world web environments. Besides, we propose a multimodal search benchmark MM-SearchExam dedicated to evaluating search capabilities of multimodal search agents, which proves highly challenging for recent proprietary models. Extensive evaluations across multiple multimodal search benchmarks reveal effectiveness of our method. VSearcher achieves superior performance compared to recent multimodal search agents and even surpasses several proprietary models on multimodal web search tasks.
Grounded String Representations of Series-Parallel Graphs without Transitive Edges
Venue: arXiv cs.CG 2026
Year: 2026

In a {\em grounded string representation} of a graph there is a horizontal line $\ell$ and each vertex is represented as a simple curve below $\ell$ with one end point on $\ell$ such that two curves intersect if and only if the respective vertices are adjacent. A grounded string representation is a {\em grounded L-reverseL-representation} if each vertex is represented by a 1-bend orthogonal polyline. It is a {\em grounded L-representation} if in addition all curves are L-shaped. We show that every biconnected series-parallel graph without edges between the two vertices of a separation pair (i.e., {\em transitive edges}) admits a grounded L-reverseL-representation if and only if it admits a grounded string representation. Moreover, we can test in linear time whether such a representation exists. We also construct a biconnected series-parallel graph without transitive edges that admits a grounded L-reverseL-representation, but no grounded L-representation.
Toward Early Quality Assessment of Text-to-Image Diffusion Models
Venue: arXiv cs.CV 2026
Year: 2026

Recent text-to-image (T2I) diffusion and flow-matching models can produce highly realistic images from natural language prompts. In practical scenarios, T2I systems are often run in a ``generate--then--select'' mode: many seeds are sampled and only a few images are kept for use. However, this pipeline is highly resource-intensive since each candidate requires tens to hundreds of denoising steps, and evaluation metrics such as CLIPScore and ImageReward are post-hoc. In this work, we address this inefficiency by introducing Probe-Select, a plug-in module that enables efficient evaluation of image quality within the generation process. We observe that certain intermediate denoiser activations, even at early timesteps, encode a stable coarse structure, object layout and spatial arrangement--that strongly correlates with final image fidelity. Probe-Select exploits this property by predicting final quality scores directly from early activations, allowing unpromising seeds to be terminated early. Across diffusion and flow-matching backbones, our experiments show that early evaluation at only 20\% of the trajectory accurately ranks candidate seeds and enables selective continuation. This strategy reduces sampling cost by over 60\% while improving the quality of the retained images, demonstrating that early structural signals can effectively guide selective generation without altering the underlying generative model. Code is available at https://github.com/Guhuary/ProbeSelect.
Adapting Time Series Foundation Models through Data Mixtures
Venue: arXiv cs.LG 2026
Year: 2026

Time series foundation models (TSFMs) have become increasingly popular for zero-shot forecasting. However, for a new time series domain not fully covered by the pretraining set, performance can suffer. Therefore, when a practitioner cares about a new domain and has access to a set of related datasets, the question arises: how best to fine-tune a TSFM to improve zero-shot forecasting? A typical approach to this type of problem is to fine-tune a LoRA module on all datasets or separately on each dataset. Tuning a separate module on each dataset allows for the specialisation of the TSFM to different types of data distribution, by selecting differing combinations of per-dataset modules for different time series contexts. However, we find that, using per-dataset modules might not be optimal, since a time series dataset can contain data from several types of distributions, i.e. sub-domains. This can be due to the distribution shifting or having differing distributions for different dimensions of the time series. Hence, we propose MixFT which re-divides the data using Bayesian mixtures into sets that best represent the sub-domains present in the data, and fine-tunes separately on each of these sets. This re-division of the data ensures that each set is more homogeneous, leading to fine-tuned modules focused on specific sub-domains. Our experiments show that MixFT performs better than per-dataset methods and when fine-tuning a single module on all the data. This suggests that by re-partitioning the data to represent sub-domains we can better specialise TSFMs to improve zero-shot forecasting.
LaTeX Compilation: Challenges in the Era of LLMs
Venue: arXiv cs.CL 2026
Year: 2026

As large language models (LLMs) increasingly assist scientific writing, limitations and the significant token cost of TeX become more and more visible. This paper analyzes TeX's fundamental defects in compilation and user experience design to illustrate its limitations on compilation efficiency, generated semantics, error localization, and tool ecosystem in the era of LLMs. As an alternative, Mogan STEM, a WYSIWYG structured editor, is introduced. Mogan outperforms TeX in the above aspects by its efficient data structure, fast rendering, and on-demand plugin loading. Extensive experiments are conducted to verify the benefits on compilation/rendering time and performance in LLM tasks. Furthermore, we show that due to Mogan's lower information entropy, it is more efficient to use .tmu (the document format of Mogan) to fine-tune LLMs than TeX. Therefore, we launch an appeal for larger experiments on LLM training using the .tmu format.