arXiv subjects

Haonan Li

Publications and source records attributed to Haonan Li.

At least 19 recordsLinked to original sources

arXiv2026

MCPHunt: An Evaluation Framework for Cross-Boundary Data Propagation in Multi-Server MCP Agents

Multi-server MCP agents create an information-flow control (IFC) problem: faithful tool composition can turn individually benign read/write permissions into cross-boundary credential propagation -- a structural side effect of workflow topology, not necessarily malicious model behavior. We present MCPHunt, to our knowledge the first controlled benchmark that isolates non-adversarial, exact-match credential propagation across multi-server MCP trust boundaries, with three methodological contributions: (1) canary-based taint tracking that reduces propagation detection to objective string matching; (2) an environment-controlled coverage design with risky, benign, and hard-negative conditions that validates pipeline soundness and adds a matched alternative-value control (same tasks, distinct synthetic credentials); (3) completion-requires-secret (CRS) stratification that disentangles task-mandated propagation (faithful execution of verbatim-transfer instructions) from policy-violating propagation (credentials included despite the option to redact). Across 3,615 main-benchmark traces from 5 models spanning 147 tasks and 9 mechanism families, policy-violating propagation rates of 11.5-41.3% persist across all models. This propagation is pathway-specific (rates from 0.0% to 74.4% across mechanisms for GPT-5.4) and concentrated in browser-mediated data flows; under the matched alternative-value control, propagation persists (25.9% vs. 20.4%; the matched-pair CI spans zero, so the comparison neither distinguishes nor equates the two rates). A prompt-mitigation study across 3 models shows policy-violating propagation rates as low as 0.3% (98% relative reduction from baseline) while preserving 80.5% utility, but effectiveness varies across models, motivating data-flow-aware defenses beyond prompting. Code, traces, and the labeling pipeline are publicly available under MIT and CC BY 4.0.

cs.AI↗

arXiv2026

The Hitchhiker's Guide to Program Analysis, Part III: Mostly Harmless LLMs

Filtering out a static-analysis warning asserts that no feasible execution can trigger the reported error, whereas confirming a bug requires only one that does. Recent work uses LLMs to filter out warnings. However, LLM-generated explanations alone cannot establish that the reported error is impossible, and mistakenly filtering out a warning conceals a real bug. Sound static analysis can provide this guarantee, but scalable analyses leave behind the very warnings we seek to filter, whereas sufficiently precise whole-program analysis is impractical. Fortunately, analyzing a small part of the program is often enough to show that a warning is a false alarm. We therefore assign LLMs a different role: rather than judging the validity of warnings, they identify relevant code and construct a harness that supplies the context needed for precise, targeted static analysis. We present Evident, which combines LLMs with the static analyzer Frama-C/Eva. Because a generated harness may exclude inputs or paths that trigger real bugs, Evident restricts how the harness initializes inputs and validates it using the value flow reported by the original detector. A warning is filtered out only when validation passes and Eva rules out the reported error in the harness; otherwise, the warning is kept. On 200 real Android kernel-driver warnings, including 40 confirmed bugs, Evident filters out 48.8-63.8% of the 160 false alarms across four LLMs without missing any confirmed bug, whereas baselines that let LLMs make the final decision miss confirmed bugs with every evaluated model. With GPT-5.5, although these baselines achieve 2.0-5.5 percentage points higher overall accuracy by filtering out more false alarms, they miss 27.5-45.0% of the confirmed bugs. Evident also rediscovers a confirmed vulnerability that had previously been overlooked by both LLM-based filtering and manual review.

cs.SE↗

arXiv2026

CXLResume: Retained-State Checkpoint and Restore for In-Memory Services

Checkpointing and restoring an in-memory service typically require writing its memory pages to checkpoint images and refilling them at the destination. When application state already resides in shared memory that remains accessible after failover, copying those pages into and out of checkpoint images is unnecessary. We present CXLResume, a prototype that retains the service's main heap objects in shared memory while checkpointing the remaining execution state and mapping metadata. Checkpointing preserves the shared heap at the same freeze point as the serialized process state. During recovery, CXLResume remaps the same shared memory at its original virtual addresses before restoring execution, preserving direct pointers within and across shared and private memory. We evaluate CXLResume with Redis and Memcached using QEMU CXL functional emulation. At 6 GiB, CXLResume reduces combined checkpoint and restore time from 15.015 s to 0.242 s for Redis and from 19.770 s to 0.276 s for Memcached in the evaluated deployments. These results show that retaining shared application state removes large application heaps from the checkpoint data path and substantially reduces checkpoint and restore latency.

cs.OS↗

arXiv2026

AgentFly: Scaling Agentic Reinforcement Learning with Unified Resource System

Methods to build LLM agents have evolved from prompt engineering and supervised finetuning to agentic reinforcement learning (agentic RL). However, agentic RL remains bottlenecked by its surrounding systems: agents must interact with heterogeneous environments, such as sandboxes, model services, and external APIs. Their allocation, reuse, and lifecycle dominate rollout cost and cap the scale at which training becomes practical. In this work, we present AgentFly, an agentic RL framework built with a unified resource layer that treats each of these environments as a distinct, typed resource scheduled through one engine, with per-tool acquisition for multi-turn reuse, asynchronous backpressure, and rollout versus global-scoped lifecycles. AgentFly adopts a four-layer design: (I) agent layer that abstracts the agent, tool, and reward concepts, decomposing agentic RL into defining agents, tools, and reward functions; (II) rollout layer that composes these into agent loops and computes rewards; (III) context layer that organizes rollouts, injects contextual information, and arranges resources; and (IV) a low-level resource layer that performs resource management. We provide a suite of prebuilt tools and environments, demonstrate successful agent training across multiple tasks and models, and report the first controlled cross-framework throughput comparison against agentic RL frameworks.

cs.AI↗

arXiv2026

Do Neural PDE Solvers Learn the Right Dynamics?

Neural PDE solvers can achieve low prediction errors, but do they reproduce the dynamics of the systems they model? Prediction scores alone offer an incomplete answer: they measure agreement with reference solutions but provide limited insight into how errors accumulate, nearby states diverge, or extreme events arise. We propose an evaluation framework that directly examines these behaviors in deterministic and stochastic neural solvers. By evolving ensembles of nearby initial states and comparing them with direct numerical simulation, we assess three complementary aspects of learned dynamics: error formation, ensemble geometry, and extreme events. Experiments on two-dimensional Kolmogorov flow reveal limitations that conventional scores can obscure. Smaller trajectory errors can reflect weaker error amplification despite less accurate local updates. Models can match an ensemble's overall spread and effective dimension while failing to capture the spatial directions where nearby states diverge. Similarly, matching overall event frequencies can conceal failures to predict persistent extreme events. These findings show that improved prediction accuracy does not necessarily imply greater dynamical fidelity. Our framework makes this distinction measurable, providing concrete criteria for evaluating whether advances in neural PDE solvers better capture the underlying dynamics.

cs.LG↗

arXiv2026

SyzHarness: Patch-Based Kernel Bug Reproduction with LLM-Synthesized Fuzzing Harnesses

Automated kernel vulnerability reproduction is essential for bug triage, patch validation, and regression testing, but still lacks an effective and efficient solution. The core challenge is twofold: a reproducer must first recover the trigger scaffold needed to reach the vulnerable state and determine the precise concrete values that actually trigger the bug. Existing directed fuzzing approaches are ineffective at recovering the necessary trigger scaffold, while LLM-only generation is brittle because it struggles with concrete-value discovery and runtime nondeterminism. We design SyzHarness, a framework that combines LLM reasoning with coverage-guided fuzzing for patch-based Linux kernel vulnerability reproduction. Given a patch, SyzHarness uses an LLM agent grounded by code navigation tools to synthesize a parameterized fuzzing harness that fixes the prerequisite setup logic while exposing only uncertain, bug-critical input parameters to be mutated by Syzkaller. SyzHarness then translates this harness into a Syzkaller compatible interface and iteratively refines it using hierarchical reachability feedback. We evaluate SyzHarness on multiple datasets of triggerable real-world Linux kernel vulnerabilities. On 100 KernelCTF cases, SyzHarness achieves a 78% bug reproduction success rate. On the SyzDirect benchmark, SyzHarness achieves a 73% bug reproduction success rate, substantially outperforming prior directed greybox fuzzing. On 50 recent, known-triggerable syzbot bugs fixed after March 2026, SyzHarness reproduces 40/50 (80%) using only the fix commits as input.

cs.CR↗

arXiv2026

Quotient Morita Theory with Applications

We study equivalences between quotient categories of module categories associated with Gabriel topologies. We establish necessary and sufficient conditions for a Morita context to induce an equivalence between quotient categories and characterize such equivalences in terms of Morita contexts after passing to rings of quotients. Motivated by Artin--Zhang's noncommutative Serre theorem, we introduce a notion of ampleness relative to a Gabriel topology and use it to characterize quotient categories of finitely generated modules under suitable noetherian hypotheses. As an application, we establish a sufficient condition under which the noncommutative Auslander theorem holds for actions of finite-dimensional Hopf algebras on AS-regular algebras without assuming that the Hopf algebras are semisimple.

math.RA↗

arXiv2026

SkillGym: Training Skill-Use Agents with Automatic Verifiable Environment Generation

Skills equip LLM agents with professional knowledge and guidance to complete long-horizon and complex tasks. Although skills have been widely adopted in recent agent paradigms and harnesses, how to synthesize reliable training data and how to train agents for skill use remain underexplored. In this work, we propose SkillGym, an automatic pipeline to build verifiable environments, collect trajectories, and train skill-use agents. SkillGym first crawls a large volume of skills from the internet, then keeps those whose workflows can run reproducibly offline. A builder-reviewer pipeline is used to construct difficulty-controlled tasks, spanning four task types, each with a reference solution and an executable verifier. With this pipeline, we build 6.8k environments and collect 19k verified successful trajectories for supervised finetuning. Finetuning on these trajectories improves LLMs of different families and sizes, from 2B to 122B parameters across four skill-use benchmarks; Our Qwen3.5-9B SFT model outperforms the 397B untrained model on two of them. Further analysis shows that training teaches agents to invoke skills, raising the rate of reading the relevant skill from 28% to 96%, and that the gains hold across reasoning structures, extending to task types that form a minority of the training data and to skills held out from training

cs.AI↗

arXiv2026

Noncommutative resolutions of noncommutative isolated singularities

Noncommutative resolutions of AS-Gorenstein isolated singularities are investigated by Li--Shen--Wu. However, establishing their existence and constructing such resolutions are generally difficult, even when they exist. In this paper, we study conditions under which a commonly graded AS-regular algebra serves as a noncommutative resolution of an AS-Gorenstein isolated singularity. We investigate projective modules over a noetherian commonly graded AS-regular algebra whose endomorphism rings admit resolutions by the underlying regular algebra. This leads to a more general definition of noncommutative resolutions of balanced Cohen--Macaulay isolated singularities. We show that the existence of such resolutions is equivalent to the existence of cluster tilting modules over balanced CM isolated singularities. The corresponding noncommutative analogue of the Bondal-Orlov conjecture is established in dimensions $2$ and $3$. As an application, we study Hopf actions on commonly graded AS-Gorenstein algebras and investigate noncommutative resolutions of invariant rings. We present three examples of noncommutative resolutions, including one in which the noncommutative isolated singularity is not connected graded.

math.RA↗

arXiv2026

Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification

Most of mathematical knowledge has been communicated through so-called informal use of mathematics and natural language. With large language models (LLMs) being highly adept in using natural language, they achieve strong performance, yet not perfect, in informal mathematical reasoning. Restraining LLMs to informal reasoning misses out on the opportunity to use the discrete verification abilities that machines offer through machine-checkable proofs. In this paper, we bridge the gap between informal and formal reasoning by integrating Lean signals into the informal reasoning process. We introduce Magenta, a training-free agentic pipeline that, given only a natural-language problem, produces an answer, expresses it as a Lean 4 statement, and constructs a machine-checked proof. A statement judge verifies whether the formalisation preserves the original problem, while an error-attribution judge routes failed attempts either to mathematical re-derivation or local Lean repair. Magenta achieves 100% accuracy across all evaluated olympiad benchmarks, including AIME 2025, AIME 2026, and HMMT February 2026. When paired with the open-weight K2-Horizon-7B reasoner, it solves all six IMO 2026 problems. Our analysis shows that statement adjudication is essential for preventing false certificates and that feedback-guided correction outperforms independent resampling on difficult problems.

cs.AI↗

arXiv2026

K2-V2: A 360-Open, Reasoning-Enhanced LLM

We introduce K2-V2, a 360-open LLM built from scratch as a superior base for reasoning adaptation, in addition to functions such as conversation and knowledge retrieval from general LLMs. It stands as the strongest fully open model, rivals open-weight leaders in its size class, outperforms Qwen2.5-72B and approaches the performance of Qwen3-235B. We actively infuse domain knowledge, reasoning, long-context, and tool use throughout the training process. This explicitly prepares the model for complex reasoning tasks. We demonstrate this potential using simple supervised fine-tuning, establishing a strong baseline that indicates significant headroom for advanced alignment. By releasing the full training history and data composition, we maximize the effectiveness of continuous training, a key open source production scenario. We release the model weights and signature LLM360 artifacts, such as complete training data, to empower the community with a capable, reasoning-centric foundation.

cs.LG↗

arXiv2026

From Leaky Thoughts to Private Reasoning: Controlling What LRMs Say to Themselves

Large reasoning models (LRMs) produce reasoning traces (RTs) that often contain sensitive information. These leaky thoughts are difficult to control and frequently violate explicit privacy directives. Because RTs can be exposed through prompt injection attacks, this becomes a direct privacy risk to the user. We approach this as a controllability problem: since privacy directives are themselves instructions, improving instruction-following (IF) within the RT provides a direct path to reducing privacy leaks. To this end, we introduce an SFT dataset that teaches models to follow general instructions throughout their reasoning process, and propose Staged Decoding, a simple decoding strategy that decouples RT and answer generation using separate LoRA adapters to maximize IF of each component. We evaluate our approach on six models from two families (1.7B-14B parameters), across two IF benchmarks and two privacy benchmarks. Our method yields substantial improvements, with gains of up to 20.9 points in IF and 51.9 percentage points on privacy benchmarks, though these can come at the cost of task utility due to the trade-off between reasoning performance and IF. Our results show that improving IF in LRMs can significantly enhance privacy, suggesting a promising direction for future privacy-aware LRMs. Our code is available at https://github.com/UKPLab/arxiv2026-controllable-reasoning-models.

cs.CL↗

arXiv2026

Training and Benchmarking Code Generation for Physics-Inspired Animations

Large language models (LLMs) have been widely studied in areas such as mathematical reasoning, complex coding, and scientific problem solving. However, their ability to generate executable code that visually depicts physical scenarios and their qualitative dynamics remains underexplored. We propose SimuScene, the first systematic study that trains and evaluates LLMs on code generation for physics-inspired animations across 52 concepts spanning five physics domains. We build an automated data collection pipeline with human verification to ensure data quality. The resulting dataset contains 7,659 scenarios, including a 334-example human-verified test set. We evaluate 10 contemporary LLMs and find that even the strongest model achieves only a 21.5\% Avg@8 accuracy, demonstrating the difficulty of generating animations that are both executable and visually aligned with physical scenario descriptions. Finally, we introduce a reinforcement learning pipeline that uses visual rewards from code-generated videos to train text-only LLMs, with a vision-language model evaluating videos through verification questions. Experiments show that training with our data and video-based rewards improves LLM performance on physics-inspired animation generation.

cs.LG↗

arXiv2026

Beyond Solution-Centric Search: Adaptive Inquiry and Knowledge Revision for Autonomous ML Engineering

Long-horizon autonomous research tasks such as machine learning engineering require systems to make interdependent decisions under a limited budget. Existing LLM-based agents typically organize candidate-solution improvement through tree, graph, or chain structures, meaning that the search process determines how information is acquired and managed. We call this design solution-centric search and propose instead the information paradigm, in which an evolving information state represents the system's understanding of the task and guides solution improvement. We instantiate this paradigm in Iris, an inquiry-revision loop. For information acquisition, Iris generates local action plans from the current information state and uses epistemic actions to probe decision-critical unknowns without modifying the retained solution. For information management, Iris synthesizes observations across experiments into task knowledge composed of revisable claims with explicit scope and status. It updates this knowledge as new evidence arrives and constructs each decision context from raw evidence, structured summaries, or task knowledge at the required level of detail. On MLE-Bench, Iris attains a 64.9% any-medal rate under a 12-hour budget, the highest among compared systems. Across four tasks spanning harness engineering and model post-training, Iris also demonstrates cross-domain generalization.

cs.AI↗

arXiv2026

Numbers Beat Words: A Rigorous On-Premise Benchmark for Coupled MIMO Controller Tuning

Tuning controllers for strongly coupled multi-input multi-output (MIMO) processes is difficult because decentralized auto-tuning ignores loop interaction and local optimization is start-sensitive. We benchmark whether on-premise open-weight large language models (LLMs) provide useful structural priors, while testing classical alternatives that may make them unnecessary. On a single-loop CSTR, relay-feedback tuning outperforms the LLM. On a pathological quadruple-tank, naive relay, naive LLM, and balanced-start local optimization fail, whereas a scaffolded LLM finds a reliable asymmetric basin and, after local refinement, reaches J = 12.0 +/- 0.16 in 10/10 runs. However, an ablation shows that this reliability depends more on an answer-shaped prompt example than on reasoning over coupling data. A direct data-driven alternative, Virtual Reference Feedback Tuning (VRFT), uses one open-loop experiment and no LLM; with the same refinement it succeeds in 10/10 runs and improves the result to J = 11.12 +/- 0.05. Although VRFT requires a reference-model time constant tau, a deterministic median-tau rule matches or exceeds LLM-guided selection at no extra cost. Across four structurally different plants, the relative gain array computed from step tests predicts when a structural prior is worth using; optimizer start-sensitivity provides a confirming second signal. The resulting boundary is clear: use classical tuning on benign plants, prefer VRFT when informative open-loop data are available, and reserve LLMs for structural initialization when direct routes are unavailable. The benchmark shows that the LLM's value is structural rather than numerical, and that on the central case, numbers beat words.

cs.AI↗

arXiv2026

Scalable LLM Agent Tool Access in the Cloud

LLM agents increasingly rely on tool calling to act on external systems, and the Model Context Protocol (MCP) has quickly become its de facto interface. Operating MCP at cloud scale, however, becomes difficult. On the tool provider side, legacy services are not directly callable through MCP; the rapid protocol development also creates ongoing compatibility cost. On the agent side, the number of accessible tool is limited by the LLM context window and inference overhead; mounting a large tool set increases token usage and inference latency and can reduce task success rate. Moreover, for stateful MCP backends with multiple replicas, preserving session affinity increases client-side complexity. We present a cloud-scale gateway system for MCP service. It breaks the direct-connect model on the data plane and offloads legacy service integration, consolidating incompatible MCP variants, access control, tool recommendation, and session-aware routing to the gateway. Hybrid retrieval sustains 98% Top-15 recall; it scales agent tool access to 3,000+ with high tool selection accuracy, and reduces tool selection time by $8.9\times$ and token usage by $23.8\times$, with low per-call overhead, stable under scale-out. Finally, we share the lessons learned from deploying the gateway system in production.

cs.DC↗

arXiv2026

AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language

Interactive theorem proving (ITP) underpins program verification and formalized mathematics, but its manual effort limits scalability. LLM-based proof agents promise to ease this effort, but their heavy token consumption and API cost remain a major obstacle. We trace this cost to a shared root: current agents operate on serialized concrete syntax, emitting proofs as source text and recovering proof states through separate, line-number-based queries, so every edit shifts later lines and forces repeated relocation of errors and states. This same dependence on concrete syntax also blocks adoption of Minilang, a recent proof language that reaches SOTA on LLM-based proving but is too new for LLMs' training corpora. We address both problems by lifting the agent off source text and onto the abstract syntax tree (AST): the model supplies proofs as JSON representations of Minilang's AST -- native to tool-calling LLMs -- and drives the prover through a tree-edit model that fuses proof operations and states into one proof tree, so each operation carries its own subgoal's state, readable directly off the tree. We realize this design in \emph{Agent over AST} (AoA). Against Amazon's Isabelle Agent on miniF2F and NTP4VC-Pearl common success sets, AoA cuts API cost by 2.3--4.7x (normalized input-cache accounting), uses 2.9--6.9x fewer tokens and 3.9--8.9x fewer tool calls, and finishes 1.4--2.0x faster -- while also solving far more problems on the harder verification benchmark.

cs.SE↗

arXiv2026

Jais 2: A Family of Arabic-Centric Open Large Language Models

Jais 2 is a family of Arabic-centric large language models developed jointly by MBZUAI, Cerebras, and Inception, designed to advance Arabic-centric language modeling, with strong performance across the Arabic and culturally grounded benchmarks evaluated in this report. The family includes, to our knowledge, the largest open Arabic-centric LLM trained from scratch at 70B parameters, and a competitive 8B-parameter variant among the evaluated open models. A custom Arabic-centric vocabulary enables efficient training and inference. In addition, an optimized architecture and training recipe yield highly compute-efficient training. With a substantially smaller token budget than comparable models, Jais 2 achieves strong Arabic performance on the benchmarks considered in this report and competitive English results. The models obtain leading results among the evaluated open models on OALL2 and AraGen. They also perform strongly on several culturally grounded Arabic benchmarks, including poetry, religion, cuisine, and dream interpretation, as well as in general tasks such as translation and summarization. We release the models in HuggingFace under a commercially permissive license. Jais 2 70B is also released as a chat app on the Web, iOS, and Android; it runs on Cerebras hardware, delivering up to 2,000 tokens per second, and enabling high-throughput Arabic-centric chat serving in our deployment setting. By uniting scale, linguistic diversity, cultural fidelity, openness, and speed, Jais 2 provides an open-weight foundation intended to support further research and development in Arabic-centric LLMs.

cs.CL↗