arXiv subjects

Jingyang Li

Publications and source records attributed to Jingyang Li.

At least 19 recordsLinked to original sources

arXiv2026

TIPCODER: Reinforcement Learning Boosted Test-time Instruction Proposer for Code Generation

Test-time scaling for code generation typically explores the solution space by sampling multiple programs from a fixed instruction. We study a complementary direction: instance-level instruction-space exploration. Our observation is that many coding failures stem from missing constraints, overlooked edge cases, or misleading reasoning paths induced by the original prompt. To address this, we propose TipCoder, a test-time instruction proposer that generates problem-specific auxiliary tips before code synthesis. TipCoder distills multi-turn debugging trajectories into proactive guidance and further optimizes the Proposer with reinforcement learning using a marginal-utility reward. At inference time, it generates both a base solution and a tip-guided solution, and applies a Reward Model for post-hoc selection. This exploration-selection design allows tips to expose additional candidate potential while reducing regressions from unnecessary guidance. Across the evaluated code-generation benchmarks and target Code LLMs, TipCoder provides a consistent instruction-level test-time scaling strategy, comparing favorably with stochastic sampling and generic prompt optimization baselines under a shared reward-model-based selection protocol.

cs.SE↗

arXiv2026

Logos: Certified Order-Sensitive SQL Rewrites with Mechanized Semantics and LLM Guidance

SQL rewrite verification must account for duplicate rows, observable row order, and typed value semantics. Existing verifiers have yet to combine proofs over database instances of arbitrary finite cardinality with an ordered-list semantics for nested, tie-sensitive top-k. Unbounded systems reason primarily over bags or handle ordering through syntax-directed restrictions, whereas bounded systems either support only restricted top-k forms or impose a deterministic ordering rather than retain all legal tie-induced outcomes. Support for typed expression and aggregate semantics, observable runtime errors, and integrity constraints also remains partial. In Rocq, we mechanize a compositional logical semantics for a typed SQL core with order-sensitive operators, capturing all possible ordered lists and observable SQL failures in the supported fragment. To our knowledge, this is the first mechanized SQL semantics to combine nested, tie-sensitive top-k with a closure-based lifting from bag equivalence to ordered-list equivalence, enabling sound reuse of bag-theoretic reasoning while preserving compositionality across order-sensitive and correlated contexts. The formalization further provides executable semantics for PostgreSQL-oriented scalar and aggregate evaluation and an explicit account of integrity constraints. Building on this semantics, we present Logos, an LLM-guided Rocq verifier for unbounded SQL rewrite equivalence. Its agent uses a verified SQL-specific lemma library to construct query-specific Rocq proofs. Our evaluation covers 389 query pairs from Apache Calcite optimizer tests, TPC-H and TPC-DS rewrites, and WeTune's real-application workloads. Logos solves 86.9% of them, compared with 64.0% for SQLSolver, the strongest baseline.

cs.DB↗

arXiv2026

Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis

Zero-Knowledge Ethereum Virtual Machines (zkEVMs) secure Ethereum rollups by generating zero-knowledge proofs that guarantee off-chain execution correctness. However, subtle implementation bugs (e.g., incorrect gas accounting) can lead to valid proofs certifying semantically faulty states, thereby silently defeating cryptographic guarantees. Formal verification via SMT solvers can prevent this, but is bottlenecked by specification: current zkEVM development practice lacks automated methods to translate Rust opcode handlers into verification models. Current practices rely on unsustainable manual specifications, while LLM-based approaches suffer from hallucination and lack formal guarantees. To address this, we propose VeriSynth, a framework that synthesizes executable Python/Z3 verification models from Rust zkEVM code. VeriSynth enforces a hybrid paradigm: an LLM acts strictly as a formalization frontend to translate code into symbolic constraints, while an SMT solver serves as the correctness arbiter. To handle complex multi-component state transitions, VeriSynth integrates semantic decomposition, retrieval-grounded prompting, and verification-guided auto-repair into a closed-loop pipeline. We evaluate VeriSynth on the first source-level zkEVM verification benchmark, encompassing both correct and faulty opcode implementations. VeriSynth achieves a bug detection rate of over 90%, substantially outperforming direct and conversational LLM baselines, as well as a production-grade handwritten mutation-testing suite. Ablation studies confirm that each pipeline component is critical to the framework's overall effectiveness.

cs.SE↗

arXiv2026

MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling

We present MaxProof, a population-level test-time scaling framework for competition-level mathematical proof in the MiniMax-M3 series. M3 first trains three proof-oriented capabilities -- proof generation, proof verification, and critique-conditioned proof repair -- using a defense-in-depth generative verifier engineered for low false-positive rate. These capabilities are merged into a single released M3 model. At test time, MaxProof treats the model as a generator, verifier, refiner, and ranker, searches over a population of candidate proofs, and returns one final proof through tournament selection. With MaxProof test-time scaling, the M3 model reaches 35/42 on IMO 2025 and 36/42 on USAMO 2026, exceeding the human gold-medal threshold on both.

cs.LG↗

arXiv2026

The MiniMax-M2 Series: Mini Activations Unleashing Max Real-World Intelligence

We introduce the MiniMax-M2 series, a family of Mixture-of-Experts language models built around the principle that mini activations can unleash maximum real-world intelligence. The flagship M2 contains 229.9B total parameters with only 9.8B activated per token. Designed end-to-end for agentic deployment, the M2 series rests on three components: (i) agent-driven data pipelines producing large-scale, verifiable trajectories across agentic coding and agentic cowork, each grounded in an executable workspace and an artifact-aligned reward; (ii) Forge, a scalable agent-native RL system that adapts to long-horizon agent trajectories, paired with windowed-FIFO scheduling, prefix-tree merging, inference optimization, and a clean training-inference-agent decoupling that supports both white-box and black-box agents; (iii) the latest M2.7 checkpoint takes an early step toward self-evolution -- autonomously debugging training runs and modifying its own scaffold. Across M2 through M2.7, this combination translates a mini-activation footprint into frontier-tier performance on agentic coding, deep search, office-task, and reasoning benchmarks.

cs.AI↗

arXiv2026

Online Riemannian Gradient Descent for Quantum State Tomography with Matrix Product Operators

Matrix product operators (MPOs) provide a scalable approach for quantum state tomography (QST) by offering a compact representation of many-body mixed states with limited entanglement, using only a number of parameters that scales polynomially with the system size. In this paper, we study QST for quantum density matrices that can be represented by MPOs. We first derive an equivalent characterization of Hermiticity in terms of the MPO core tensors and show that the coefficient tensor of an MPO under the Pauli or generalized Gell-Mann basis admits a real-valued low tensor-train (TT) rank structure. This establishes an explicit connection between MPO-based QST and noisy low-rank tensor completion. Motivated by this formulation, we develop an online Riemannian gradient descent (oRGD) algorithm that sequentially incorporates measurement data during the reconstruction process. With a proper initialization, we prove that oRGD converges linearly to the target MPO and succeeds with a number of distinct measurement settings that scales quadratically with the system size. As a byproduct, our analysis also yields a significantly improved sample complexity bound for the low TT rank tensor completion task. Furthermore, we propose a tailored spectral initialization method and establish its theoretical guarantee. Numerical experiments on several classes of quantum states validate the effectiveness and scalability of the proposed method.

quant-ph↗

arXiv2026

Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation

The problem of probabilistic verification of a neural network investigates the probability of satisfying the safe constraints in the output space when the input is given by a probability distribution. It is significant to answer this problem when the input is affected by disturbances often modeled by probabilistic variables. In the paper, we propose a novel neural network probabilistic verification framework which computes a guaranteed range for the safe probability by efficiently finding safe and unsafe probabilistic hulls. Our approach consists of three main innovations: (1) a state space subdivision strategy using regression trees to produce probabilistic hulls, (2) a boundary-aware sampling method which identifies the safety boundary in the input space using samples that are later used for building regression trees, and (3) iterative refinement with probabilistic prioritization for computing a guaranteed range for the safe probability. The accuracy and efficiency of our approach are evaluated on various benchmarks including ACAS Xu and a rocket lander controller. The result shows an obvious advantage over the state of the art.

cs.AI↗

arXiv2026

Uncertainty Quantification for Noisy Low-tubal-rank Tensor Completion

High-dimensional tensor data often exhibit strong temporal correlations that appear as low-dimensional structures in the frequency domain. While the low-tubal-rank tensor model effectively captures these spectral features, making it potentially suitable for geophysical data, existing methods primarily focus on point estimation. Uncertainty quantification (UQ) of imputed values and rigorous statistical inference for these models remain largely unexplored. In this work, we propose a flexible inference framework for linear forms of high-dimensional tensors. Employing a double-sample debiasing technique followed by a low-rank projection, we construct asymptotically Gaussian estimators that yield valid statistical inference under mild assumptions. More precisely, we can perform hypothesis testing and construct confidence intervals with this result. We validate the theoretical results through extensive simulations and demonstrate the practical effectiveness of our method in completing the global total electron content data. We demonstrate, using those numerical results, that our entrywise confidence intervals are robust and reliable, yielding informative uncertainty quantification that captures underlying variability.

stat.ME↗

arXiv2026

The survival of the weakest in a biased donation game

Cooperating first then mimicking the partner's act has been proven to be effective in utilizing reciprocity in social dilemmas. However, the extent to which this, called Tit-for-Tat strategy, should be regarded as equivalent to unconditional cooperators remains controversial. Here, we introduce a biased Tit-for-Tat (T) strategy that cooperates differently toward unconditional cooperators (C) and fellow T players through independent bias parameters. The results show that, even under strong dilemmas in the donation game framework, this three-strategy system can exhibit diverse phase diagrams on the parameter plane. In particular, when T-bias is small and C-bias is large, a ``hidden T phase'' emerges, in which the weakest T strategy dominates. The dominance of the weakened T strategy originates from a counterintuitive mechanism characterizing non-transitive ecological systems: T suppresses its relative fitness to C, rapidly eliminates the cyclic dominance clusters, and subsequently expands slowly to take over the entire population. Analysis in well-mixed populations confirms that this phenomenon arises from structured populations. Our study thus reveals the subtle role of bias regulation in cooperative modes by emphasizing the ``survival of the weakest'' effect in a broader context.

cs.GT↗

arXiv2026

SimCert: Probabilistic Certification for Behavioral Similarity in Deep Neural Network Compression

Deploying Deep Neural Networks (DNNs) on resource-constrained embedded systems requires aggressive model compression techniques like quantization and pruning. However, ensuring that the compressed model preserves the behavioral fidelity of the original design is a critical challenge in the safety-critical system design flow. Existing verification methods often lack scalability or fail to handle the architectural heterogeneity introduced by pruning. In this work, we propose SimCert, a probabilistic certification framework for verifying the behavioral similarity of compressed neural networks. Unlike worst-case analysis, SimCert provides quantitative safety guarantees with adjustable confidence levels. Our framework features: (1) A dual-network symbolic propagation method supporting both quantization and pruning; (2) A variance-aware bounding technique using Bernstein's inequality to tighten safety certificates; and (3) An automated verification toolchain. Experimental results on ACAS Xu and computer vision benchmarks demonstrate that SimCert outperforms state-of-the-art baselines.

cs.SE↗

arXiv2026

Counterexample Guided Branching via Directional Relaxation Analysis in Complete Neural Network Verification

Deep Neural Networks demonstrate exceptional performance but remain vulnerable to adversarial perturbations, necessitating formal verification for safety-critical deployment. To address the computational complexity of this task, researchers often employ abstraction-refinement techniques that iteratively tighten an over-approximated model. While structural methods utilize Counterexample-Guided Abstraction Refine- ment, state-of-the-art dataflow verifiers typically rely on Branch-and-Bound to refine numerical convex relaxations. However, current dataflow approaches operate with blind refinement processes that rely on static heuristics and fail to leverage specific diagnostic information from verification failures. In this work, we argue that Branch-and-Bound should be reformulated as a Dataflow CEGAR loop where the spurious counterexample serves as a precise witness to local abstraction errors. We propose DRG-BaB, a framework that introduces the Directional Relaxation Gap heuristic to prioritize branching on neurons actively contributing to falsification in the abstract domain. By deriving a closed-form spurious counterexample directly from linear bounds, our method transforms generic search into targeted refinement. Experiments on high-dimensional benchmarks demonstrate that this approach significantly reduces search tree size and verification time compared to established baselines.

cs.SE↗

arXiv2025

Spectral Joint Subspace Estimation for Heterogeneous Multi-View Data: Geometry and Reweighting

Many modern datasets consist of multiple related matrices measured on a common set of units, with the goal of recovering a shared low-dimensional subspace. The Angle-based Joint and Individual Variation Explained (AJIVE) framework addresses this problem through equal-weight aggregation, which can be suboptimal when views exhibit statistical heterogeneity in signal-to-noise ratios and dimensions, as well as structural heterogeneity from individual components. For equal-weight AJIVE, we show that the previously identified ``non-diminishing'' error barrier is geometry dependent: under near-orthogonal deterministic loading orientations, the second-order term is reduced, whereas under sign-symmetric random loadings, it is centered and averages out, yielding a $K^{-1/2}$-type rate without iterative refinement. Under a majority sign-alignment condition in rank-one setting, a bias at the squared single-view perturbation scale can persist. For general weights, we establish error bounds that disentangle the two layers of heterogeneity, and propose HeteroJIVE, the weighted AJIVE estimator using an explicit weight that is optimal whenever its identifiability gap is constant. We also provide a data-driven plug-in implementation of HeteroJIVE, together with an optional geometry-adaptive extension of this data-driven procedure. Simulations and analyses of multi-omics and image data illustrate the practical benefits of HeteroJIVE.

math.ST↗

arXiv2025

Local Interaction Autoregressive Model for High Dimension Time Series Data

High-dimensional matrix and tensor time series often exhibit local dependency, where each entry interacts mainly with a small neighborhood. Accounting for local interactions in a prediction model can greatly reduce the dimensionality of the parameter space, leading to more efficient inference and more accurate predictions. We propose a Local Interaction Autoregressive (LIAR) framework and study Separable LIAR, a variant with shared row and column components, for high-dimensional matrix/tensor time series forecasting problems. We derive a scalable parameter estimation algorithm via parallel least squares with a BIC-type neighborhood selector. Theoretically, we show consistency of neighborhood selection and derive error bounds for kernel and auto-covariance estimation. Numerical simulations show that the BIC selector recovers the true neighborhood with high success rates, the LIAR achieves small estimation errors, and the forecasts outperform matrix time-series baselines. In real data applications, a Total Electron Content (TEC) case study shows the model can identify localized spatio-temporal propagation and improved prediction as compared with non-local time series prediction models.

stat.ME↗

arXiv2025

Bridging Draft Policy Misalignment: Group Tree Optimization for Speculative Decoding

Speculative decoding accelerates large language model (LLM) inference by letting a lightweight draft model propose multiple tokens that the target model verifies in parallel. Yet existing training objectives optimize only a single greedy draft path, while decoding follows a tree policy that re-ranks and verifies multiple branches. This draft policy misalignment limits achievable speedups. We introduce Group Tree Optimization (GTO), which aligns training with the decoding-time tree policy through two components: (i) Draft Tree Reward, a sampling-free objective equal to the expected acceptance length of the draft tree under the target model, directly measuring decoding performance; (ii) Group-based Draft Policy Training, a stable optimization scheme that contrasts trees from the current and a frozen reference draft model, forming debiased group-standardized advantages and applying a PPO-style surrogate along the longest accepted sequence for robust updates. We further prove that increasing our Draft Tree Reward provably improves acceptance length and speedup. Across dialogue (MT-Bench), code (HumanEval), and math (GSM8K), and multiple LLMs (e.g., LLaMA-3.1-8B, LLaMA-3.3-70B, Vicuna-1.3-13B, DeepSeek-R1-Distill-LLaMA-8B, Qwen3-8B), GTO increases acceptance length by (7.4%) and yields an additional (7.7%) speedup over prior state-of-the-art EAGLE-3. By bridging draft policy misalignment, GTO offers a practical, general solution for efficient LLM inference. Code and draft models are available at https://github.com/hsj576/GTO.

cs.CL↗

arXiv2025

WebExplorer: Explore and Evolve for Training Long-Horizon Web Agents

The paradigm of Large Language Models (LLMs) has increasingly shifted toward agentic applications, where web browsing capabilities are fundamental for retrieving information from diverse online sources. However, existing open-source web agents either demonstrate limited information-seeking abilities on complex tasks or lack transparent implementations. In this work, we identify that the key challenge lies in the scarcity of challenging data for information seeking. To address this limitation, we introduce WebExplorer: a systematic data generation approach using model-based exploration and iterative, long-to-short query evolution. This method creates challenging query-answer pairs that require multi-step reasoning and complex web navigation. By leveraging our curated high-quality dataset, we successfully develop advanced web agent WebExplorer-8B through supervised fine-tuning followed by reinforcement learning. Our model supports 128K context length and up to 100 tool calling turns, enabling long-horizon problem solving. Across diverse information-seeking benchmarks, WebExplorer-8B achieves the state-of-the-art performance at its scale. Notably, as an 8B-sized model, WebExplorer-8B is able to effectively search over an average of 16 turns after RL training, achieving higher accuracy than WebSailor-72B on BrowseComp-en/zh and attaining the best performance among models up to 100B parameters on WebWalkerQA and FRAMES. Beyond these information-seeking tasks, our model also achieves strong generalization on the HLE benchmark even though it is only trained on knowledge-intensive QA data. These results highlight our approach as a practical path toward long-horizon web agents.

cs.CL↗

arXiv2025

Phase field simulation of dendrite growth in solid-state lithium batteries based on mechanical-thermo-electrochemical coupling

Solid-state lithium batteries possess numerous advantages, such as high energy density, excellent cycle stability, superior mechanical strength, non-flammability, enhanced safety, and extended service life. These characteristics make them highly suitable for applications in aerospace, new energy vehicles, and portable electronic devices. However, the growth of lithium dendrite at the electrode/electrolyte interface remains a critical challenge, limiting both performance and safety. The growth of lithium dendrites in the electrolyte not only reduces the Coulombic efficiency of the battery but also poses a risk of puncturing the electrolyte, leading to internal short circuits between the anode and cathode. This study is to solve the problem of lithium dendrite growth in solid-state lithium batteries by employing phase-field theory for numerical simulations. A phase-field model is developed by coupling the mechanical stress field, thermal field, and electrochemical field, to investigate the morphology and evolution of lithium dendrites under the condition of different ambient temperatures, external pressures, and their combined effects. The results indicate that higher temperature and greater external pressure significantly suppress lithium dendrite growth, leading to fewer side branches, smoother surfaces, and more uniform electrochemical deposition. Increased external pressure inhibits longitudinal dendrite growth, resulting in a compressed morphology with higher compactness, but at the cost of increased mechanical instability. The combined effect of temperature and pressure exhibits a pronounced inhibitory influence on dendrite growth, with stress concentrating at the dendrite roots. This stress distribution promotes lateral growth, facilitating the formation of flatter and denser lithium deposits.

cond-mat.mtrl-sci↗

arXiv2025

MiniMax-M1: Scaling Test-Time Compute Efficiently with Lightning Attention

We introduce MiniMax-M1, the world's first open-weight, large-scale hybrid-attention reasoning model. MiniMax-M1 is powered by a hybrid Mixture-of-Experts (MoE) architecture combined with a lightning attention mechanism. The model is developed based on our previous MiniMax-Text-01 model, which contains a total of 456 billion parameters with 45.9 billion parameters activated per token. The M1 model natively supports a context length of 1 million tokens, 8x the context size of DeepSeek R1. Furthermore, the lightning attention mechanism in MiniMax-M1 enables efficient scaling of test-time compute. These properties make M1 particularly suitable for complex tasks that require processing long inputs and thinking extensively. MiniMax-M1 is trained using large-scale reinforcement learning (RL) on diverse problems including sandbox-based, real-world software engineering environments. In addition to M1's inherent efficiency advantage for RL training, we propose CISPO, a novel RL algorithm to further enhance RL efficiency. CISPO clips importance sampling weights rather than token updates, outperforming other competitive RL variants. Combining hybrid-attention and CISPO enables MiniMax-M1's full RL training on 512 H800 GPUs to complete in only three weeks, with a rental cost of just $534,700. We release two versions of MiniMax-M1 models with 40K and 80K thinking budgets respectively, where the 40K model represents an intermediate phase of the 80K training. Experiments on standard benchmarks show that our models are comparable or superior to strong open-weight models such as the original DeepSeek-R1 and Qwen3-235B, with particular strengths in complex software engineering, tool utilization, and long-context tasks. We publicly release MiniMax-M1 at https://github.com/MiniMax-AI/MiniMax-M1.

cs.CL↗

arXiv2025

MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression

The rapid development of deep learning has led to challenges in deploying neural networks on edge devices, mainly due to their high memory and runtime complexity. Network compression techniques, such as quantization and pruning, aim to reduce this complexity while maintaining accuracy. However, existing incremental verification methods often focus only on quantization and struggle with structural changes. This paper presents MUC-G4 (Minimal Unsat Core-Guided Incremental Verification), a novel framework for incremental verification of compressed deep neural networks. It encodes both the original and compressed networks into SMT formulas, classifies changes, and use \emph{Minimal Unsat Cores (MUCs)} from the original network to guide efficient verification for the compressed network. Experimental results show its effectiveness in handling quantization and pruning, with high proof reuse rates and significant speedup in verification time compared to traditional methods. MUC-G4 hence offers a promising solution for ensuring the safety and reliability of compressed neural networks in practical applications.

cs.LG↗