arXiv subjects

Ji Wang

Publications and source records attributed to Ji Wang.

At least 19 recordsLinked to original sources

arXiv2026

Data-Driven Safe Output Regulation of Strict-Feedback Linear Systems with Input Delay

This paper develops a data-driven safe control framework for linear systems possessing a known strict-feedback structure, but with most plant parameters, external disturbances, and input delay being unknown. By leveraging Koopman operator theory, we utilize Krylov dynamic mode decomposition (DMD) to extract the system dynamics from measured data, enabling the reconstruction of the system and disturbance matrices. Concurrently, the batch least-squares identification (BaLSI) method is employed to identify other unknown parameters in the input channel. Using control barrier functions (CBFs) and backstepping, we first develop a full-state safe controller. Based on this, we build an output-feedback controller by performing system identification using only the output data and actuation signals as well as constructing an observer to estimate the unmeasured plant states. The proposed approach achieves: 1) finite-time identification of a substantial set of unknown system quantities, and 2) exponential convergence of the output state (the state furthest from the control input) to a reference trajectory while rigorously ensuring safety constraints. The effectiveness of the proposed method is demonstrated through a safe vehicle platooning application.

eess.SY↗

arXiv2026

Worst-Case Optimal $\sqrtε$-Rate Stability of KL Divergence under Perturbations of Gaussian Distributions

We establish a stability bound for the Kullback-Leibler (KL) divergence when its Gaussian reference distribution is perturbed. Existing relaxed triangle inequalities of KL divergence between Gaussian distributions require all three distributions to be Gaussian, which limits their use in applications such as out-of-distribution detection with flow-based generative models. Let $\mathcal{N}_1$ and $\mathcal{N}_2$ be $d$-dimensional Gaussian distributions, and let $P$ be any $d$-dimensional distribution satisfying $\mathbb{E}_P[\|X\|^2]<\infty$ and $\mathrm{KL}(P\Vert \mathcal{N}_1)<\infty$. If $\mathrm{KL}(\mathcal{N}_1\Vert\mathcal{N}_2)\leqε$ for $0<ε<1/12$, we give an upper bound of $\left|\mathrm{KL}(P\Vert\mathcal{N}_1)-\mathrm{KL}(P\Vert\mathcal{N}_2)\right|$. Under suitable uniform boundedness conditions, the bound is $ \frac{\sqrt{6dε}}{2}+K\sqrtε+o(\sqrtε)$ as $ε\rightarrow 0$ for fixed $d$, where $K$ depends on the parameters of $\mathcal{N}_1$ and $\mathcal{N}_2$, and on $\mathbb{E}_P[\|X\|]$ and $\mathbb{E}_P[\|X\|^2]$. Furthermore, we prove that the $\sqrtε$ dependence is worst-case optimal. The result extends stability guarantees restricted to Gaussian triples to comparisons involving an arbitrary distribution and two nearby Gaussian references. Experiments on synthetic distributions and latent representations from flow-based models support the predicted stability behavior.

cs.LG↗

arXiv2026

Autoregressive Decoding as a Martingale: Characterizing the Stochastic Dynamics of LLM Generation

Large language models (LLMs) have achieved remarkable success across a wide range of language tasks. At their core, autoregressive LLMs are conditional probability models that learn to approximate the next-token distribution given the preceding context. Despite this probabilistic nature, the stochastic dynamics of autoregressive decoding have rarely been investigated from a rigorous probabilistic perspective. In this work, we define the per-step prediction error as the difference between the sampled token indicator and the model's conditional predictive distribution, and prove that the cumulative error process is a martingale with respect to the decoding filtration, implying that its conditional first-order moment is identically zero. Beyond this first-order property, we derive a closed-form expression for the second-order behavior of the martingale sequence: its predictable quadratic variation reduces to $\sum_t\left(1-p(y_t\mid y_{<t})\right)$, computable from realized token probabilities alone. This identity establishes a direct theoretical connection between sequence fluctuations and predictive uncertainty during autoregressive decoding. White-box experiments on Llama-3.x and Qwen2.5 families (1B to 72B parameters) verify that the empirically measured second-order moments closely match the theoretical predictions derived from our martingale analysis. These results provide a probabilistic framework for analyzing autoregressive LLM decoding, reveal intrinsic probabilistic fingerprints of different language models, and establish a rigorous mathematical foundation for LLM-generated text detection and uncertainty quantification.

cs.LG↗

arXiv2026

Taylor-Approximation-Based Repair of High Floating-Point Errors

Numerical libraries can still lose many bits of accuracy on localized ill-conditioned inputs, such as roots, poles, cancellation points, and branch boundaries. This paper presents NPTaylor, a Taylor-approximation-based framework for repairing localized high floating-point errors in numerical C routines. Given a high-error input, a localized repair domain, a high-precision oracle, and an error threshold, NPTaylor searches over Taylor degree, expansion center, segmentation, and floating-point evaluation strategy. It emits guarded C patches that use a generated Taylor evaluator inside the repair domain and fall back to the original routine outside it. Candidate patches are accepted only after validating the emitted C code on recorded local samples, guard endpoints, and the pre-repair peak input. The generated evaluator uses coefficient splitting and compensated Horner evaluation to reduce rounding error introduced by the patch itself. We evaluate NPTaylor on GSL benchmark workloads. On 38 one-input functions, both NPTaylor and AutoRNP repair all 114 configurations across three accuracy thresholds. NPTaylor is 3.33x faster by geometric-mean offline repair time and emits 0.162x as many C bytes. In the strictest setting, its median repair time is 3.74s versus 81.97s for AutoRNP. NPTaylor also repairs localized multi-input benchmark cases beyond AutoRNP's implemented one-input workflow. These results show that Taylor-based guarded patches can provide compact, efficient local repairs, while the claims remain validation-relative rather than full-domain proofs.

cs.SE↗

arXiv2026

Rydberg Atomic Quantum Receivers for Wireless Communications: Two-Color vs. Three-Color Excitation

An efficient three-color (3C) laser excitation-based Rydberg atomic quantum receiver (RAQR) architecture is investigated for wireless communications, utilizing a five-level (5L) electronic transition mechanism. Specifically, the conventional two-color (2C) RAQR with the four-level (4L) excitation faces three fundamental obstacles: 1) high cost and engineering challenges due to the reliance on unstable short-wavelength lasers; 2) a fundamental sensitivity limit in thermal atoms caused by residual Doppler broadening; and 3) the inability to detect low-frequency bands due to the energy-level constraint of two-photon resonance. To address these challenges, this paper analyzes a 3C5L-RAQR architecture with all-red/infrared lasers, which not only solves the engineering cost issues but also enables effective Doppler cancellation and low-frequency detection by exploiting the three-photon resonance. Bridging atomic physics and communication theory, an end-to-end equivalent baseband signal model is derived. Furthermore, the performance of different RAQR architectures is evaluated in terms of sensitivity, achievable rate and spectrum access range. Moreover, we provide an exact numerical solution for practical RAQRs by employing the Liouvillian superoperator formalism. Numerical results demonstrate that the exhibited 3C5L-RAQR achieves superior sensitivity compared to the conventional 2C4L-RAQR and a classical antenna-based radio frequency receiver for weak-signal detection. Finally, the inherent sensitivity-rate trade-off is revealed, showing that the 3C5L-RAQR is more suitable for deployment in power-limited communication scenarios demanding broad spectrum access.

cs.IT↗

arXiv2026

UniEvo-VL: An On-policy Self-Distillation Training Recipe for Multimodal Model Self-improvement

Modern multimodal models bring generation and understanding into a single unified system, which enables them to provide and learn from their own feedback. Motivated by this unified capacity, we introduce UniEvo-VL, a self-evolving framework for multimodal models to learn from this constructive self-correction feedback during test-time compute. Instead of relying on a separate, often larger, teacher, we leverage their self-critiques as privileged information and ask a single multimodal model to act as both teacher and student with different contexts. The student only sees the vanilla question, while the teacher conditions on the privileged critique. Then training minimizes the per-state divergence between their denoising diffusion distributions over the student's own sampling trajectories. Experiments demonstrate that UniEvo-VL improves the image generation capabilities of multimodal models, while maintaining their sensitivity to additional reflection information. Specifically, we build on top of the open-source Qwen-image-2512 and observe a significant performance gain from 0.747 to 0.808 on GenEval and from 32.97 to 35.53 on GenEval2 Soft-TIFA. Moreover, attempts with more powerful external critics (e.g., GPT5.6-Luna) show that multimodal models with strong judge capabilities can anticipate a higher self-evolving ceiling. Last but not least, mixed text-rendering outcomes show that our self-improvements may not be uniform across different tasks. Our study aims to shed light on the current hot recursive self-improvement research line to enhance the user experience when using multimodal models without external supervision or guidance.

cs.AI↗

arXiv2026

Output-Positive Adaptive Control of Parabolic PDE-ODE Cascades

In this paper, we propose a safe adaptive boundary control strategy for a class of parabolic partial differential equation-ordinary differential equation (PDE-ODE) cascaded systems with parametric uncertainties in both the PDE and ODE subsystems. The proposed design is built upon an adaptive Control Barrier Function (aCBF) framework that incorporates high-relative-degree CBFs together with a batch least-squares identification (BaLSI)-based adaptive control that guarantees exact parameter identification in finite time. The proposed controller ensures the positivity, i.e., the safety, of the plant output state that is the furthest state from the control input, as well as the exponential regulation of the overall plant state to zero. Numerical simulations are provided to demonstrate the effectiveness of the proposed approach.

eess.SY↗

arXiv2026

PARSEE-VAD: Efficient Training-Free Online Video Anomaly Detection via Proposition-Aware Reasoning and Streaming Evidence Escalation

Training-free online video anomaly detection (VAD) with frozen multimodal language models faces two coupled challenges: extracting reliable current-window semantics under causal and computational constraints, and maintaining temporal continuity without repeatedly transmitting high-dimensional history. Encoding history through text can compress visual evidence and introduce semantic bias, whereas retaining visual history expands multimodal context. We introduce PARSEE-VAD, a two-module framework that separates semantic evidence acquisition from score-state evolution. Proposition-Aware Reasoning (PAR) extracts structured propositional evidence from the current causal window and conditionally activates more specific queries when coarse evidence warrants further refinement. By sharing a reusable causal visual prefix across queries, PAR reduces redundant computation through selective execution. Streaming Evidence Escalation (SEE) maps the acquired proposition evidence into a compact score-domain event state through current evidence escalation, then propagates only the resulting bounded state across decisions to support temporal continuity. Experiments on four benchmarks demonstrate strong training-free online performance while selective routing reduces specialist computation and score-state propagation remains sparse. These results support a current-first principle for streaming multimodal inference: resolve present semantics first, then use compact historical state only to repair residual continuity gaps.

cs.CV↗

arXiv2026

AnthroDial: Benchmarking LLM Anthropomorphism in Autonomous Social Interaction

Large language models (LLMs) are increasingly deployed as social agents, yet credible human-like interaction requires more than fluent responses or persona consistency. Agents must autonomously decide whether, when, and how to communicate while adapting to evolving contexts, goals, and relationships. Existing research, however, lacks a unified approach to enabling, evaluating, and improving such capabilities in continuous, open-ended interaction. We introduce AnthroDial, a unified framework for developing anthropomorphic social agents from three complementary aspects: MindFlow, a lightweight interaction harness that enables autonomous, asynchronous, and adaptive communication through a dynamic Mind Buffer; CAPS-Eval, a theory-grounded framework for evaluating cognitive, affective, and behavioral dimensions of anthropomorphic interaction; and a scalable training paradigm that combines SEEDS for environment expansion with DiAPO for adaptive capability optimization. We further construct evaluation datasets covering everyday communication, game interaction, and long-horizon character interaction. Extensive experiments across diverse models and scenarios demonstrate improved interaction autonomy and naturalness, validate the reliability, discriminativeness, and agreement with human rankings of CAPS-Eval, and confirm the effectiveness of our training paradigm. Together, these components provide a unified framework for developing credible human-like social agents in open-ended interaction.

cs.CL↗

arXiv2026

MetaPermit: Scalable and Auditable Access Control for AI Agents via LLM-Inferred Meta-Attributes

The rise of autonomous AI agents equipped with tools has introduced significant security risks, ranging from unintended tool misuse to adversarial manipulation through Indirect Prompt Injection (IPI) attacks. In practice, deployed agent systems such as OpenAI Codex and Claude Code protect tool invocations through a combination of coarse-grained permission rules and LLM-based judgments about individual proposed actions. Both components, however, have important limitations: static policies must anticipate possible user intents and therefore do not scale to open-ended tasks, while LLM-driven authorization supports dynamic decisions but produces inconsistent outcomes and remains vulnerable to targeted IPI attacks. To provide scalable and more consistent authorization, we propose MetaPermit, a policy-based tool access-control framework that decouples semantic inference from security enforcement. By analyzing agent-user interactions, we derive a compact, task-independent set of meta-attributes that capture the relationships among the user's intent, the execution context, and the proposed tool call. These meta-attributes allow MetaPermit to authorize tool use without enumerating user intents. At runtime, an LLM infers the meta-attribute values for each proposed tool call, while a fixed policy evaluates these values to allow or deny the call, making each decision auditable through the inferred values and the applied policy rule. We evaluate MetaPermit on the AgentDojo and AgentDyn benchmarks, across seven task suites and five attack methods, using two widely deployed open-weight LLMs. The results show that MetaPermit produces 31% more consistent authorization decisions than LLM-driven authorization and outperforms the state-of-the-art defenses CaMeL and IPIGuard in both task completion, with improvements of up to 109%, and robustness to IPI attacks, with no malicious tool calls executed.

cs.CR↗

arXiv2026

The Science Potential of Characterizing Gas Giant Exoplanets with HWO

With the ability to directly image Earth-like exoplanets and search their atmospheres for biosignatures, the upcoming Habitable Worlds Observatory (HWO) will also collect high signal-to-noise ratio (S/N) reflected-light photometry and spectra of nearby gas giant exoplanets. Such high-quality data would allow novel investigations into gas giant atmospheric composition, formation, and kinematic properties, and could enable the detection of exomoons around these planets. We use the EXOSIMS direct imaging mission simulator to model HWO observations of Jupiter-radius gas giants at Earth-like and Jupiter-like instellations around the 164 stars in the ExEP target list. We find that HWO should be able to achieve S/N $\geq$ 5 broadband visible-light detections of gas giants in this instellation range within 5 minutes of integration. 10 hours of R=1000 near-IR spectroscopy with HWO should reveal water, methane, and ammonia absorption features in the atmospheres of Jupiter-like gas giants. HWO time-series photometry should exceed 1% flux precision in one hour for any Earth-instellation gas giants around ExEP stars, and for Jupiter-like gas giants at $d\leq$ 7 parsecs. Time-series light curves at this cadence and precision could, over tens of hours, reveal rotation-induced variability comparable to Jupiter's. Eclipses of Mars-sized exomoons may be detectable in high-cadence light curves of Jupiter sized planets in the habitable zones of ExEP stars at $d\leq$ 10 parsecs. For any hypothetical Earth-like exomoons with oxygen-rich atmospheres at $d\leq$ 7 parsecs from the Solar System, HWO might be able to detect the spectral signature of molecular oxygen amid the parent planet's photon noise in deep ($\sim$400 hour integration) spectroscopic HWO observations at R=1000. Such moons, if they exist, represent additional habitable worlds that HWO could investigate for biosignatures.

astro-ph.EP↗

arXiv2026

A Stellar-Type Dependence in the Rocky and Volatile Composition of Small Exoplanets

We investigate the rocky and volatile composition of small exoplanets by modeling the population-level distribution of densities using a mixture framework that links interior structure models to observable quantities. We analyze three complementary samples spanning different stellar environments: the Luque \& Pallé M-dwarf sample, the DACE M-dwarf sample, and the DACE FGK sample. We consider a log-normal parameterization, which captures a characteristic core mass fraction (CMF) and the intrinsic dispersion to describe a single rocky population. The single rocky population inference suggests a higher CMF for small planets around FGK stars than those around M stars by $\sim$16\% (7-11 $σ$ depending on sample selection). We also consider a power-law parameterization, which probes clustering near compositional boundaries at CMF=0.32. The power-law parameterization provides an alternative interpretation: 89.9\% to 97.0\% of the planets around FGK stars are rocky whereas up to 61.6\% (ranging from 4.1\% to 61.6\%) of planets around M stars are rocky. In addition, we find that volatile mass fractions are highly concentrated. For example, to describe the DACE M-dwarf sample using a mixture of rocky, water-rich, and gas-rich planets, we find that more than 99.5\% gaseous planets have an atmospheric mass fraction (AMF) $\lesssim 0.01\%$, and more than 55.4\% (82.7\%) gaseous planets have a water mass fraction (WMF) $\lesssim 0.1\%$ ($\lesssim 1\%$). These results suggest that while volatile-bearing planets are common, their composition and prevalence depend strongly on stellar environment, and their volatile inventories are tightly constrained by formation and evolutionary processes.

astro-ph.EP↗

arXiv2026

Measuring Harmfulness of Computer-Using Agents

Computer-using agents (CUAs), which can autonomously control computers to perform multi-step actions, might pose significant safety risks if misused. However, existing benchmarks mainly evaluate LMs in chatbots or simple tool use. To more comprehensively evaluate CUAs' misuse risks, we introduce a new benchmark: CUAHarm. CUAHarm consists of 104 expert-written realistic misuse risks, such as disabling firewalls, leaking data, or installing backdoors. We provide a sandbox with rule-based verifiable rewards to measure CUAs' success rates in executing these tasks (e.g., whether the firewall is indeed disabled), beyond refusal rates. We evaluate frontier LMs including GPT-5, Claude 4 Sonnet, Gemini 2.5 Pro, Llama-3.3-70B, and Mistral Large 2. Even without jailbreaking prompts, these frontier LMs comply with executing these malicious tasks at a high success rate (e.g., 90% for Gemini 2.5 Pro). Furthermore, while newer models are safer in previous safety benchmarks, their misuse risks as CUAs become even higher, e.g., Gemini 2.5 Pro is riskier than Gemini 1.5 Pro. Additionally, while these LMs are robust to common malicious prompts (e.g., creating a bomb) when acting as chatbots, they could still act unsafely as CUAs. We further evaluate a leading agentic framework (UI-TARS-1.5) and find that while it improves performance, it also amplifies misuse risks. To mitigate the misuse risks of CUAs, we explore using LMs to monitor CUAs' actions. We find monitoring unsafe computer-using actions is significantly harder than monitoring conventional unsafe chatbot responses. While monitoring chain-of-thoughts leads to modest gains, the average monitoring accuracy is only 77%. A hierarchical summarization strategy improves performance by up to 13%, a promising direction though monitoring remains unreliable. CUAHarm is released at https://github.com/db-ol/CUAHarm to facilitate further research.

cs.CR↗

arXiv2026

On the Impact of Correlated Noise and Spectral Resolution on the Retrieval Analysis of the Habitable World Observatory

Finding signs of life elsewhere in the universe is the holy grail of the field of exoplanets. Future space missions such as the Habitable World Observatory (HWO) are under development to search for biosignatures in exoplanets. We investigate the impact of correlated noise and spectral resolution on the retrieved biosignature chemical abundances. At the nominal spectral resolving power R=140 for HWO, we show that in 40\% of the simulated runs the retrieved biosignature (H$_2$O and O$_2$) abundances are at least 1-$σ$ off the input ground truth. At R=1000, the 1-$σ$ inaccuracy rate drops to 10\%. We provide an empirical relationship between the retrieved biosignature abundance uncertainty and the amplitude of the correlated noise. As part of the mitigation plan to reduce the impact of correlated noise on retrieval accuracy at low spectral resolution, we investigate the synergy between the HWO and LIFE space missions that cover ultraviolet, optical, and thermal-infrared wavelengths. After considering clouds and their effect on planet albedo, we find that the two missions are complementary in that (1) more biosignatures (H$_2$O, CO$_2$, O$_2$, and O$_3$) are detectable with a broader wavelength coverage; (2) retrieval uncertainty improves with the joint HWO+LIFE data set; and (3) LIFE is more sensitive to the atmospheric temperature profile, surface pressure, and planet radius. This work provides evidence to support the choice of a medium resolution at R=1000 instead of R=140 for HWO and a quantitative relationship between the retrieved abundance uncertainty and the level of correlated noise at different spectral resolutions.

astro-ph.EP↗

arXiv2026

IncSFS: Incremental Full-Sparse Flow-Sensitive Pointer Analysis for C/C++

Pointer analysis is a fundamental technique for compiler optimization and program analysis. Flow-sensitive pointer analysis provides high precision but is difficult to scale to large projects. Tailored for rapid iteration scenarios where software evolves continuously, we introduce IncSFS, the first incremental full-sparse flow-sensitive pointer analysis algorithm for C/C++ programs. IncSFS first transforms the value-flow graph into a constraint graph and performs strongly connected component detection to ensure precision. It then propagates increases and decreases in points-to sets in an interleaved manner, supporting code deletion and insertion within a single analysis pass. IncSFS is guaranteed to terminate and compute the least fixed point when the points-to relation remains object-acyclic during analysis. Experiments on six large-scale real-world projects show that IncSFS is precise and efficient, achieving average speedups of 9.60x over full flow-sensitive pointer analysis and 5.84x over the traditional reset-recompute approach. It also improves efficiency by 15.8% over state-of-the-art incremental pointer analysis algorithms that propagate points-to-set changes.

cs.PL↗

arXiv2026

Safe Output Regulation of Coupled Hyperbolic PDE-ODE Systems

This paper presents a safe output regulation control strategy for a class of systems modeled by a coupled $2\times 2$ hyperbolic PDE-ODE structure, subject to fully distributed disturbances throughout the system. A state-feedback controller is developed by the nonovershooting backstepping method to simultaneously achieve output regulation and enforce safety constraints on the regulated output that is the state furthest from the control input. To handle unmeasurable states and external disturbances, an extended observer is designed. Explicit bounds on the estimation errors are derived and used to construct a robust safe regulator that accounts for the uncertainties. The proposed control scheme guarantees that: 1) If the regulated output is initially within the safe region, it remains there; otherwise, it will be rescued to the safety region within a prescribed time; 2) The output tracking error converges to zero; 3) The observer accurately estimates both the distributed states and external disturbances, with estimation errors converging to zero exponentially; 4) All signals in the closed-loop system remain bounded. The effectiveness of the proposed method is demonstrated through a UAV delivery scenario with a cable-suspended payload, where the payload is regulated to track a desired reference while avoiding collisions with barriers.

eess.SY↗

arXiv2026

Modeling the Dynamics and Thermochemistry for the Outer Atmospheres of the Ultra-hot Jupiter WASP-121b

We present three-dimensional simulations of the ultra-hot Jupiter (UHJ) WASP-121b from the planetary surface to extended outflows, coupling hydrodynamics with consistent non-equilibrium thermochemistry, ray-tracing radiative transfer, and hydrodynamics using the GPU-accelerated Kratos framework. The fiducial model exhibits several atmospheric layers, including the lower atmospheres controlled by day-night circulation, and transonic photoevaporative outflows at higher altitudes shaped into two spiral arms by the stellar gravity and orbital motion effects. Different species could trace different regions: Fe probes rotation-dominated inner layers, Na maps dense spiral arms where recombination balances photoionization, and H$α$ and He 10830 A features trace progressively more extended, ionized gas. With spiral arm velocities reaching ~ 40 km/s projected along the line of sight, this morphology naturally reproduces the velocity pattern of observed high-velocity Na and H$α$ absorption features without requiring significant super-rotation jet streams, although the absolute absorption amplitudes could carry uncertainties from stellar UV luminosity and trace elemental abundances. Parametric studies reveal complex dependencies on stellar irradiation: enhanced FUV intensifies outflows and extends spiral arms spatially and kinematically, while EUV and X-ray expands spiral structures into attenuated, ionized regions. Stellar wind confinement compresses the dayside outflow and enhances metastable helium absorption. This work demonstrates that current and future transmission spectral observations that probe multiple species can provide important constraints on astrophysical environments of UHJs by comparing state-of-the-art simulations.

astro-ph.EP↗

arXiv2026

LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference

Loop invariant synthesis is a fundamental problem in program verification, yet the inherent undecidability makes it highly challenging. Recent studies have increasingly employed various machine learning techniques to generate loop invariants. However, most of these methods adopt a monolithic approach. Due to the inability to strictly constrain the learning process, learning-based methods struggle to simultaneously consider all necessary conditions and generate complete invariants when tackling complex problems. In fact, a loop invariant is often an ordered sequence of lemmas, rather than a single invariant formula. This motivates us to propose Incremental ICE, a novel learning framework for incremental synthesis. Our framework integrates the incremental philosophy of IC3 into the general invariant learning framework ICE. By defining a lemma-specific learning objective and introducing a counterexample filtering mechanism, we can achieve sound incremental learning. Under this framework, we instantiate a loop invariant synthesis tool, LimICE, which leverages LLMs to generate the ordered sequence of lemmas and incorporates ICE-DT as a fallback mechanism to complement the lemma sequence. Experiments on 367 linear benchmarks and 50 nonlinear benchmarks demonstrate the effectiveness of the proposed approach. LimICE solves 349 (out of 367) linear problems on an average of 15.2 seconds and 47 (out of 50) nonlinear problems on an average of 8.8 seconds. Compared to the state-of-the-art LLM-based baseline, our approach solves 12-24% more instances while running 36-63% faster across linear and nonlinear benchmarks. LimICE also consistently outperforms strong non-LLM baselines and solves at least 86 and 27 additional instances on the linear and nonlinear benchmarks, respectively.

cs.SE↗