arXiv Science⌕ Search

arXiv subjects

Junyi Liu

Publications and source records attributed to Junyi Liu.

At least 19 recordsLinked to original sources

Quantification of Tail-trimming Effects for Interval CVaR Based Nonlinear Regression

The tail trimming strategy is widely adopted for robustness against outlier contamination in statistical learning and operations research. However, it generally lacks the thorough understanding that to what extent the tail-trimming technique is effective for nonlinear regression. In this paper, we address the robust nonlinear regression based on the so-called interval conditional value-at-risk (In-CVaR), which is introduced to guard against outliers by trimming extreme losses. We first analyze the trimming effect of the In-CVaR based estimator under distributional perturbation. Our first finding is that the In-CVaR based estimator is qualitatively robust under distributional perturbation in terms of the Prokhorov metric if and only if the largest portion of losses is trimmed. Furthermore, under sample contamination, we derive a probably approximately correct (PAC) bound for the In-CVaR based estimator, showing that the preliminary covariate filtering that is customary in the literature is not needed for In-CVaR based regression. The nonconvexity of the In-CVaR objective, together with unboundedness of covariates, responses and parameter space create the technical challenges for our developed theory, and thus necessitate the new treatment of the qualitative robustness and PAC analysis. Overall, this study rigorously analyzes robustness properties of In-CVaR based nonlinear regression models, which illustrates to what extent the right tail-trimming of the loss by In-CVaR risk measure is essential and effective for robust nonlinear regression. These theoretical findings are further supported by numerical experiments.

math.OC↗

OasisKV: Scaling In-Decode KV Cache Beyond HBM with Lookahead Sparse Prefetching

Large language model (LLM) inference serving is increasingly constrained by memory rather than compute. As long-context and long-form reasoning workloads become more prevalent, the key-value (KV) cache dominates both memory footprint and memory traffic at the token generation (i.e., decode) stage. HBM capacity has therefore become a critical bottleneck, constraining inference batch size and throughput. This paper introduces OasisKV, a memory-centric LLM inference system that alleviates HBM limitations by offloading the KV-cache to alternative memory tiers. Exploiting the sparsity of decode-time attention and leveraging speculative decoding to predict important tokens, OasisKV selectively prefetches and stages only the most relevant KV entries in HBM for efficient LLM inference computation. To support growing LLM context and the larger batches enabled by sparse HBM residency, OasisKV employs tiered KV management across decode, prefill, and remote-memory nodes, relaxing decode-host memory capacity limits under disaggregated serving. An asynchronous prefetch pipeline hides off-GPU transfer latency while bounding per-step traffic to fit the available bandwidth. We implement OasisKV on vLLM. With only 2,048 KV tokens resident in HBM, OasisKV maintains average accuracy within a negligible 0.61 points of full attention on LongBench v2 for long-context understanding and across AIME24-25 and GPQA-Diamond for long-form reasoning. This sparsity translates into a 1.86x throughput gain over vLLM on AIME24. Synthetic long-context workloads further show up to 2.2x higher throughput in multi-GPU serving. Under prefill-decode disaggregation, OasisKV achieves 2.29x vLLM's throughput while supporting 2.42x as many concurrent requests under the same host-memory budget.

cs.DC↗

QEDIA: Quantum Program Verification in Lean

Practical quantum programs interleave quantum and classical computation: classical data shape the quantum operations that are performed, and measurement outcomes shape the classical computation that follows. Formal verification of such programs in a proof assistant requires mechanizing a program logic that handles this interplay consistently at every level, from the mathematics of quantum mechanics, through program syntax and semantics, to specifications and proof rules. Such mechanizations, along with the program proofs built on them, typically require substantial manual effort. We present QEDIA, a framework for verifying quantum programs with classical variables in Lean 4. At its foundation is an open library that formalizes the quantum Hoare logic QHL+ across all these levels and proves the logic sound for both partial and total correctness. We construct the library and the program proofs, under human supervision, using an LLM-based prover agent, whose general-purpose core we extend for quantum program verification. We illustrate QEDIA with verified programs including the quantum Fourier transform, phase estimation, repeat-until-success circuits, and Hamiltonian simulation.

quant-ph↗

RISC-Q: A Generator for Real-Time Quantum Control System-on-Chips Compatible with RISC-V

Quantum computing imposes stringent requirements for the precise control of large-scale qubit systems, including, for example, microsecond-latency feedback and nanosecond-precision timing of gigahertz signals-demands that far exceed the capabilities of conventional real-time systems. The rapidly evolving and highly diverse nature of quantum control necessitates the development of specialized hardware accelerators. While a few custom real-time systems have been developed to meet the tight timing constraints of specific quantum platforms, they face major challenges in scaling and adapting to increasingly complex control demands-largely due to fragmented toolchains and limited support for design automation. To address these limitations, we present RISC-Q---an open-source flexible generator for Quantum Control System-on-Chip (QCSoC) designs, featuring a programming interface compatible with the RISC-V ecosystem. Developed using SpinalHDL, RISC-Q enables efficient automation of highly parameterized and modular QCSoC architectures, supporting agile and iterative development to meet the evolving demands of quantum control. We demonstrate that RISC-Q can replicate the performance of existing QCSoCs with significantly reduced development effort, facilitating efficient exploration of the hardware-software co-design space for rapid prototyping and customization.

cs.AR↗

ProsaBuddy: Assisting Mechanized Real-Time Schedulability Analysis with LLM-based Agents

Rigorous schedulability analysis is essential for the design of hard real-time systems, yet errors in pen-and-paper proofs threaten the safety of critical applications. The Prosa initiative addresses this by offering a foundation for building machine-checkable schedulability analysis proofs in the Rocq proof assistant. However, the substantial time and expertise required to construct such proofs remain a major barrier for wider adoption of Prosa. This work presents ProsaBuddy, an LLM?based agent system designed to lower the effort needed to develop mechanized real-time schedulability proofs. ProsaBuddy employs a ReAct loop with retrieval over the Prosa codebase, access to Rocq tools and optional human-written hints. It uses a subgoal?delegation architecture, decomposing a lemma into subgoals and dispatches them to subagents for proof. We evaluate ProsaBuddy on a mini benchmark drawn from real-time scheduling literature. Experiment results show that ProsaBuddy significantly outper?forms state-of-the-art LLM-based Rocq automated proving agent systems and a general coding agent OpenCode

cs.LO↗

MemExplorer: Navigating the Heterogeneous Memory Design Space for Agentic Inference NPUs

Emerging agentic large language model (LLM) workloads are driving rapidly growing demand for memory capacity and bandwidth. Different phases of inference, such as prefill and decode, have distinct requirements. Industry is responding by combining heterogeneous accelerators into interconnected systems, as exemplified by NVIDIA's Vera Rubin platform, where each device has its own memory architecture. The range of available memory technologies is also expanding. High-density on-chip SRAM, HBM, LPDDR, GDDR, and emerging options such as high-bandwidth flash (HBF) each offer different trade-offs in capacity, bandwidth, and power. Identifying efficient memory architectures for next-generation inference accelerators remains challenging because the design space spans workload characteristics, NPU design choices, and memory system designs. To address this challenge, we present MemExplorer, a new memory system synthesizer for heterogeneous NPU systems. MemExplorer provides a unified way to model memory technologies at different levels of the hierarchy, including on-chip and off-chip memory. It automatically selects an efficient heterogeneous memory system alongside NPU design choices, such as matrix engine size, to balance throughput and power across prefill and decode devices in a multi-device system. For agentic workloads under the same power budget, MemExplorer achieves up to 2.3 times the energy efficiency of the baseline NPU and 3.23 times that of an H100 in the prefill-only setting. At equivalent performance targets in the decode setting, it delivers up to 1.93 times and 2.72 times the power efficiency of the baseline NPU and H100, respectively.

cs.AR↗

Learning-Based Surrogate Method for Stochastic Optimization under Decision-Dependent Uncertainty with Adaptive Random Designs

We study stochastic programs in which the latent decision-dependent uncertainty is described via a nonparametric regression model. The major challenge is that, without convexity assumptions on either the cost function or the regression model, the resulting objective is both nonconvex and nonsmooth, and its first-order information is unavailable due to the unknown decision-dependent distribution. To address this issue, we construct a learning-based surrogate model that integrates simulation and statistical learning by embedding Jacobian estimates of the regression function, which are updated iteratively and interactively during the optimization procedure. We develop an adaptive random design that concentrates design points around the current iterate for Jacobian estimation and we show that the mean squared error of Jacobian estimates achieves a dimension-independent convergence rate. Building on this, we propose the learning-based stochastic prox-linear (L-SPL) algorithm with adaptive random design and establish its nonasymptotic convergence rates under various parameter settings. Numerical results demonstrate that L-SPL algorithm significantly improves sample efficiency and achieves substantially lower objective values compared to the state-of-the-art methods. More broadly, our method implies that the statistical design in an iterative learning-based optimization algorithm can be novelly tailored to the local information of the optimization procedure to sharpen estimates and enhance the convergence performance and sample efficiency of the resulting algorithm.

math.OC↗

A New Perspective on Clustering: A Mixed-norm Model and its Solution by Progressive Integer Programming

Extending the classical $K$-means and $K$-medians models, this paper introduces an $\ell_{p,q}$ mixed-norm clustering model where the centroid updates and cluster assignments are under the $\ell_p$ and $\ell_q$ norms, respectively. The model is formulated as a mixed-integer program (MIP) with Heaviside composite constraints that describe the nearest-center assignments. The framework recovers $K$-means and $K$-medians when $p=q=2$ and $p=q=1$, respectively, and yields new models when $p\ne q$. To address the computational challenges, we develop a progressive integer programming (PIP) method that adaptively fixes confident assignments and solves restricted mixed-integer subproblems. For $q=1$, we develop a convex inner approximation of the difference-of-convex constraints in the restricted subproblems, for which a global solution can be computed. Importantly, we establish the connection between the local minimizer and the strong center-local minimizer of the mixed-norm clustering problem and the global optimal solution of the restricted subproblems under certain assumptions. This connection provides a practical certificate of a local minimizer of the nonconvex mixed-norm clustering model. We further develop techniques for constructing adaptive fixing sets and working sets for $q=1$. Extensive numerical experiments demonstrate the superior performance of the mixed-norm clustering model and the efficiency of PIP for solving the MIP model, which may be intractable otherwise. In particular, the $\ell_{2,1}$ mixed-norm clustering model is effective under coordinate-sparse, mean-balanced contamination, whereas the $\ell_{1,2}$ model is preferred under dense coordinatewise Cauchy contamination. The numerical results also show that PIP can escape poor alternating solutions and obtain substantially better feasible clustering, while preserving strong warm starts when no improvement is found.

math.OC↗

Verified Pythagorean Composition for Adaptive Cryptographic Games: Noise Flooding in Homomorphic Encryption

Noise flooding is a standard defense against decryption attacks on approximate homomorphic encryption, but its security proof is unusually sensitive to composition. Replacing each of $q$ adaptive decryption answers with a statistically close simulation and applying an ordinary hybrid argument loses linearly in $q$. The cryptographic proof instead accumulates conditional Kullback-Leibler (KL) costs and converts to statistical distance once, giving the parameter-critical square-root loss. We machine-check this argument using Rocq and SSProve. Given any fully homomorphic encryption scheme that is approximately correct and IND-CPA secure, we formalize a reduction for every $q$-query IND-CPAD adversary and prove \[ \Pr[\mathsf{IND\text{-}CPAD}_{\mathsf{NF}}^{\mathcal A}=1] \leq β_{\mathsf{CPA}}(\mathcal B_{\mathcal A,q}) + \frac{\sqrt{qn}}{2γ}. \] where $n$ is the plaintext dimension and $γ$ is the flooding-width multiplier. Our proof constructs a new relational program logic over SSProve semantics. Its Pythagorean judgment composes conditional KL budgets without converting them to statistical distance, and a verified trace compiler lifts a local oracle rule to arbitrary adaptive programs with a single final conversion.

cs.CR↗

DTMC-Based Analysis and Scheduling for Periodic Flows with Proactive HARQ

Ultra-Reliable Low-Latency Communication (URLLC) requires strict reliability and latency guarantees for heterogeneous periodic traffic. Proactive HARQ improves resource efficiency through early termination, but slot-level timing effects, particularly delayed feedback, complicate schedulability analysis. This paper presents a discrete-time Markov chain (DTMC)-based framework for periodic flows with proactive HARQ. By expanding the state space, the model captures HARQ round-trip time and other cross-slot timing effects. The framework determines the transmission opportunities required to satisfy heterogeneous reliability and latency constraints and supports offset-based scheduling through a two-stage genetic algorithm. Simulations with industrial URLLC traffic show that the proposed method achieves higher schedulability than reactive HARQ, K-Repetition, and non-guaranteed proactive HARQ, with acceptable computational overhead.

cs.NI↗

S1-Omni: A Unified Multimodal Reasoning Model for Scientific Understanding, Prediction, and Generation

We present S1-Omni, a unified multimodal reasoning model for scientific understanding, prediction, and generation. AI for Science (AI4S) has advanced significantly through domain-specific models, tool-augmented LLMs, and scientific language models. However, model capabilities remain highly fragmented, limiting the joint modeling of heterogeneous data, scientific laws, and expert knowledge. S1-Omni addresses this gap by consolidating these capabilities into a single, coherent scientific reasoning model. The architecture of S1-Omni is built upon three core components: unified representation of scientific data, natural-world knowledge alignment, and decoding for domain-specific tasks. First, S1-Omni maps natural-language instructions and scientific objects, including CIF, SMILES, protein sequences, spectra, and scientific images, into a shared representation space. Second, it incorporates scientific laws and expert knowledge into data construction and training, enabling the model to reason from scientific evidence. Third, it performs task-specific decoding to support a broad range of applications, including property prediction, spectrum-to-molecular generation, protein site and structure prediction, and scientific image generation and editing. S1-Omni is trained on S1-Omni-Corpus, which covers 200 scientific tasks and contains millions of reasoning samples, and is evaluated on over 60 scientific benchmarks. It outperforms GPT-5.5 and Gemini-3.1-Pro on most benchmarks and matches or surpasses domain-specific models on several benchmarks. Overall, S1-Omni provides a practical path toward unified scientific modeling.

cs.AI↗

GIGA-Lens 2.0: Strong-Lens Modeling on Multiple GPU Nodes

We present GIGA-Lens 2.0: a major upgrade to the GPU-accelerated Bayesian framework for modeling strong lensing systems that allows it to be run across multiple GPU nodes. We have succeeded in running GIGA-Lens 2.0 on 128 nodes or 512 A100 GPUs. We demonstrate the speed benefits of this new version, and apply them to modeling 100 simulated systems and a real system, DESI J238.5690+04.7276. We also present other changes to the framework that have yielded further improvement on performance.

astro-ph.CO↗

Solving Constrained Affine Heaviside Composite Optimization Problems by a Progressive IP Approach

This paper discusses the computational resolution and presents numerical results for solving affine combinations of Heaviside composite optimization problems (abbreviated as A-HSCOPs) by a progressive integer programming (abbreviated as PIP) method. The characteristics of these problems are that the Heaviside functions, which appear in the objective and define the constraints, are discontinuous, and their mixed-signed combinations result in the overall objective lacking the matching semicontinuity needed for the optimization and in the feasible set being not necessarily closed. Added to these challenging properties is the nondifferentiability of the inner functions in the composition. In this paper, we propose resolutions to all these challenges by first an approximation to remedy the lack of semicontinuity in the objective and closedness in the constraints, followed by a progressive integer programming approach with successive decomposition to handle the intrinsically discrete nature of the Heaviside function. Convergence to the local optimizers of the given Heaviside optimization problem is established. The effectiveness of the overall solution strategy is supported by extensive computational experiments on the score-based and tree-based multiclass classification problems with precision constraints.

math.OC↗

Light 'em Up: Enabling Few-Shot Low-Light 3D Gaussian Splatting with Multi-Scale Explicit Retinex Illumination Decoupling

Full 360$^\circ$ novel view synthesis under low-light conditions remains challenging. Insufficient illumination, noise amplification, and view-dependent photometric inconsistencies prevent existing methods from jointly preserving geometric consistency and photorealism. Unsupervised approaches often exhibit color drift under large viewpoint variations, while supervised low-light enhancement models, though effective for 2D tasks, struggle to generalize to new scenes and typically require retraining. To address this issue, we propose MERID-GS, a Multi-Scale Explicit Retinex Illumination-Decoupled Gaussian framework for low-light 360$^\circ$ synthesis. Based on Retinex theory, the method explicitly separates illumination and reflectance, and suppresses noise propagation while enhancing dark-region structures via a learnable gain and Illumination-State-Guided Frequency Gating. Combined with lightweight Reflection Head and 3D Gaussian Splatting, MERID-GS adapts to new scenes with only a few shots and enables stable low-light novel view synthesis from sparse-view observations. In addition, we construct a low-light multi-view dataset covering full 360$^\circ$ scenes for joint evaluation. Thorough experiments across multiple datasets in this area demonstrate that MERID-GS achieves SOTA performance, exhibiting superior cross-scene generalization and view consistency. The source code and pre-trained models are available at https://github.com/YhuoyuH/MERID-GS..

cs.CV↗

POCA: Pareto-Optimal Curriculum Alignment for Visual Text Generation

Current visual text generation models struggle with the trade-off between text accuracy and overall image coherence. We find that achieving high text accuracy can reduce aesthetic quality and instruction-following capability. Although reinforcement learning approaches can alleviate the problem through aligning with multiple rewards, they are often unstable for text generation, as existing approaches normally optimize multiple rewards in a weighted-sum way. In addition, it is difficult to balance the weight of each reward. Moreover, reinforcement learning requires a set of training instructions. A large number of prompts require more training time and computing resources, while a small set leads to poor performance. Hence, how to select the prompts for efficient training is an unsolved problem. In this study, we propose Pareto-Optimal Curriculum Alignment (POCA), a framework that addresses this issue as a multi-objective problem by: 1) identifying the Pareto-optimal set to avoid simple scalarization and 2) designing an adaptive curriculum alignment strategy to manage a learning sequence of a multi-reward dataset using automatic difficulty assessment, which is crucial for optimal convergence as RL methods explore in a limited data environment. In synergy, POCA finds the Pareto-optimal set in a unified reward space, which eliminates inconsistent signals to find the best trade-off solution from different rewards under an easy-to-hard optimization landscape. The experimental results show that POCA significantly improves all metrics such as CLIP, HPS scores and sentence accuracy.

cs.CV↗

Hackers or Hallucinators? A Comprehensive Analysis of LLM-Based Automated Penetration Testing

The rapid advancement of Large Language Models (LLMs) has created new opportunities for Automated Penetration Testing (AutoPT), spawning numerous frameworks aimed at achieving end-to-end autonomous attacks. However, despite the proliferation of related studies, existing research generally lacks systematic architectural analysis and large-scale empirical comparisons under a unified benchmark. Therefore, this paper presents the first Systematization of Knowledge (SoK) focusing on the architectural design and comprehensive empirical evaluation of current LLM-based AutoPT frameworks. At systematization level, we comprehensively review existing framework designs across six dimensions: agent architecture, agent plan, agent memory, agent execution, external knowledge, and benchmarks. At empirical level, we conduct large-scale experiments on 13 representative open-source AutoPT frameworks and 2 baseline frameworks utilizing a unified benchmark. The experiments consumed over 10 billion tokens in total and generated more than 1,500 execution logs, which were manually reviewed and analyzed over four months by a panel of more than 15 researchers with expertise in cybersecurity. By investigating the latest progress in this rapidly developing field, we provide researchers with a structured taxonomy to understand existing LLM-based AutoPT frameworks and a large-scale empirical benchmark, along with promising directions for future research.

cs.CR↗

Team of Thoughts: Efficient Test-time Scaling of Agentic Systems through Orchestrated Tool Calling

Existing Multi-Agent Systems (MAS) typically rely on homogeneous model configurations, failing to exploit the diverse expertise inherent in different post-trained architectures. We propose Team-of-Thoughts, a heterogeneous MAS framework that treats diverse models as specialized tools within an orchestrator-driven paradigm. Team-of-Thoughts introduces two novel components: (1) Orchestrator Calibration, which identifies models with superior coordination and synthesis capabilities, and (2) Agent Self-Assessment, a protocol where tool agents profile their own domain-specific strengths to guide selection. At inference, the orchestrator dynamically activates the most compatible agents based on these profiles to maximize capability coverage. Across five mathematical reasoning and code generation benchmarks, Team-of-Thoughts consistently outperforms individual models and existing MAS baselines. Notably, on AIME24 and LiveCodeBench, Team-of-Thoughts achieves 96.00% and 77.91% accuracy, respectively, significantly improving over homogeneous role-play baselines (80.00% and 65.93%).

cs.CL↗

A Scalable Open-Source QEC System with Sub-Microsecond Decoding-Feedback Latency

Quantum error correction (QEC) is essential for realizing large-scale, fault-tolerant quantum computation, yet its practical implementation remains a major engineering challenge. In particular, QEC demands precise real-time control of a large number of qubits and low-latency, high-throughput and accurate decoding of error syndromes. While most prior work has focused primarily on decoder design, the overall performance of any QEC system depends critically on all its subsystems including control, communication, and decoding, as well as their integration. To address this challenge, we present an open-source, fully integrated QEC system built on RISC-Q, a generator for RISC-V-based quantum control architectures. Implemented on RFSoC FPGAs, our system prototype integrates real-time qubit control, a scalable distributed multi-board architecture, and the state-of-the-art hardware QEC decoder within a low-latency, high-throughput decoding pipeline, forming a complete hardware platform ready for deployment with superconducting qubits. Experimental evaluation on a three-board prototype based on AMD ZCU216 RFSoCs demonstrates an end-to-end QEC decoding-feedback latency of 446 ns for a distance-3 surface code, including syndrome aggregation, network communication, syndrome decoding, and error distribution. Extrapolating from measured subsystem performance and state-of-the-art decoder benchmarks, the architecture can achieve sub-microsecond decoding-feedback latency up to a distance-21 surface code ($\sim$881 physical qubits) when scaled to larger hardware configurations.

quant-ph↗