Papers

Safety alignment of large reasoning models (LRMs) via supervised fine-tuning (SFT) and reinforcement learning (RL) often yields near-perfect safety scores, yet this apparent success comes at the cost of severe over-refusal and degraded general capabilities. Through systematic empirical analysis, we find that these failures are closely associated with the learning of spurious shortcuts rather than robust intent-sensitive safety evaluation. Specifically, we identify two dominant shortcuts: formatting shortcuts, where refusal behaviors are overly bound to structural prompt templates that frequently appear in safety alignment corpora; and lexical shortcuts, where sensitive keywords reflexively trigger refusals on benign queries. To mitigate reliance on these shortcuts, we propose DeShortcut-Align, a shortcut-decoupling alignment framework that reduces dependence on superficial cues. DeShortcut-Align operates across three coordinated stages: (1) Refusal Sensitivity Attribution, which masks input tokens to quantify their impact on the final refusal response distribution; (2) Attribution-Guided Contrastive Augmentation, which constructs benign contrastive samples using high-sensitivity tokens to mitigate lexical shortcuts; and (3) Counterfactual Consistency Regularization, which constructs template-ablated states via attention blinding to enforce decision consistency across SFT and RL, mitigating formatting shortcut dependence. Experiments on 7B and 14B models demonstrate that DeShortcut-Align significantly improves robustness against template-stripping bypass attacks (reducing performance drops by up to 72%), substantially reduces over-refusal by over 58%, and better preserves general-purpose reasoning capabilities, thereby mitigating the alignment tax commonly observed in safety training.

Existing online video segmentation methods struggle to track objects in long, complex videos with long-term occlusions. We hypothesize that this limitation is caused by (i) the inability of their temporal propagation mechanism to adaptively select the object information that is propagated across time, and (ii) their inability to be trained on long videos due to memory requirements and vanishing gradients. To address the first limitation, we propose to use a lightweight GRU-based temporal propagation module that can learn to select which information it keeps in memory and propagates across time. Second, to allow training on long videos, we introduce Truncated Query Propagation (TQP), a training strategy in which the model processes a video in chunks of frames, where information about tracked objects is propagated between chunks but backpropagation is only conducted in individual chunks, enabling longer temporal supervision without out-of-memory issues, inference overhead, or vanishing gradients. The resulting model is called the Long-term Video Mask Transformer (LVMT). Extensive experiments on six benchmarks show that LVMT sets a new state of the art across a range of video segmentation tasks, while retaining the speed of the highly efficient model it is based on, making it 10X faster than the prior state of the art. Code: https://github.com/tue-mps/lvmt

We present work in progress towards an intuitionistic version of Applicative Matching Logic. We introduce a semantics based on complete Heyting algebras, and propose a proof system which we prove to be sound relative to this semantics.

Learning-based manipulation policies relying on RGB cameras often suffer from degraded observations under extreme exposure. Event cameras mitigate this degradation by asynchronously detecting pixel-level intensity changes to offer a high dynamic range. However, their observations heavily depend on camera placement, as fixed cameras miss static scene content while wrist-mounted camera motion causes previously visited regions to leave the field of view. To address these spatial-temporal limitations, we present ECHO (Event-augmented Context with Hindsight and Outlook), a wrist-only latent world action model that encodes wrist events into compact motion representations to provide temporal and spatial context for policy reasoning. Specifically, ECHO utilizes a pretrained event encoder to explain visual-feature changes between frames. Its hindsight module preserves the gripper trajectory with past event stream as addressable off-camera context. Concurrently, the outlook module introduces learnable event foresight queries supervised to anticipate the event window for future actions, enabling the policy to predict upcoming scene changes. Evaluated on wrist-only RLBench tasks, ECHO outperforms RGB and RGB+event baselines by 20.6 and 12.0 percentage points under normal lighting, and by 14.6 and 11.3 points under severe exposure drops, respectively, while also surpassing RGB references using a third-person camera. Real-world experiments with a wrist-mounted event camera validate that ECHO outperforms RGB-only and RGB+event baselines across multiple tasks under both nominal and severely dark lighting. Project page is at https://echo-wam.github.io/.

This paper investigates model composition—often referred to as "gluing"—within the framework of matching logic. Specifically, we examine the systematic combination of existing signatures, variable valuations, theories, and their corresponding models. Our primary objective is to ensure that this composition preserves satisfaction proofs; that is, any theory validated by the individual constituent models is also validated by the resulting composite model. Our definitions are based on a polyadic, sorted variant of matching logic, which has also been expressed in the Rocq proof assistant. Therefore, we outline our definitions with dependent types for this work to serve as a direct blueprint for the mechanization in the short-term future.

Structural analysis is central to Petri Net (PN) research, complementing state-space methods while avoiding their combinatorial issues. It is well studied for classical PNs but much less for High-Level Petri Nets (HLPN). Symmetric Nets (SN), a common HLPN formalism, use compact annotations to encode behavioral symmetries, allowing symbolic reachability graphs and associated lumped Markov chains for stochastic SN. In the past two decades, specific structural techniques for SN have emerged, notably the SNexpression tool, which implements a calculus for symbolic structural relations such as conflict and causality. We propose using this calculus to semi-automatically verify symbolic structural invariants, currently possible only for restricted SN subclasses, for an extended SN formalism (ESN) closed under key functional operators. We focus on flows and outline, at least in theory, how to construct a flow-generating family. We also sketch a framework for formally verifying a wider range of invariant properties. Representative examples illustrate the main concepts.

Public policies addressing urgent social and environmental challenges need to explicitly consider the diverse, often conflicting perspectives of the affected stakeholders. Despite computational decision-support approaches increasingly offering recommendations across diverse human value systems, they still tend to deliver a single consensus-driven outcome. We present KITA AI, a modular system in which multiple large language model agents, each grounded in distinct demographic stakeholder personas and conceptual frameworks, deliberate on policy scenarios. The objective of KITA AI is not merely to inform about a preferred policy proposal, but also to automatically surface who is affected by the scenario and provide decision-makers with the rationales and quantitative indicators behind each position. KITA AI treats non-convergence as a first-class explainable output, enabling policymakers to better understand the trade-offs and human impacts of the policies being discussed.

This is a case study on a specific version of the Patience Sort algorithm in which we illustrate the evolution of it from an intuitive but inefficient nested recursion into a more complex but more efficient tail recursion, together with its formal implementation and certification in Theorema and Rocq (formerly Coq). We identify some general principles of algorithm transformation, and we develop the necessary background theory and proof methods. As a significant distinctive aspect, the approach in Theorema uses multisets, which simplifies the whole process and makes it more intuitive. The certification process reveals significant differences between the Theorema and Rocq approaches, about which we provide a comparative analysis with respect to algorithm definition, proof development, and proof effort. This analysis offers insights into how algorithm design influences the complexity and structure of formal proofs and demonstrates how non-trivial algorithms can be effectively verified across different formal frameworks.

We present a domain-theoretical formalization of interaction trees in the Rocq prover. Unlike existing formalizations, ours does not rely on Rocq's built-in coinduction. Hence, we avoid complications occurring in earlier works, such as artificially including silent steps to comply with Rocq's productivity checker, treating monad laws as weak bisimulations, and coinductive bisimulation reasoning. We define an inductive program equivalence relation as the congruence closure of a base relation on primitive effects with respect to action sequencing and least upper bounds. This enables reasoning about possibly non-terminating programs by reducing their equivalences to equivalences of their terminating approximations, which are then proved by induction. This relation is proved correct: provided the base relation is correct, equivalent computations have equal denotations in any monad that faithfully implements the effects. We illustrate the framework by showing the equivalence of two programs encoding the Syracuse sequence, whose termination is an open mathematical conjecture.

Tabular foundation models (TFMs) provide predictive distributions for regression, but their prediction regions can exhibit undercoverage or overcoverage even when point predictions are accurate. We introduce C-USIM (Conditionally-Uniformized Score Integration Method), a lightweight application of highest predictive density split conformal prediction that accommodates multimodal predictions. Given calibration and test outputs, it requires no additional training or model inference. It provides finite-sample marginal validity under our assumptions. We bound conditional-marginal coverage gaps using distribution-estimation error and score discreteness, and examine coverage heterogeneity through percentile rank-score plots. Experiments with TabPFN and TabICL show improved marginal coverage accuracy and lower average conditional and group coverage errors. Under a fixed data budget, allocating more observations to calibration can reduce marginal coverage error despite less accurate point predictions.

LLM-assisted Verus verification is a less tedious method to verify Rust implementations, but paired with self-referential structures, e.g., Doubly Linked Lists (DLLs)—notoriously difficult to formalise for verification—it becomes a substantially more demanding verification task. Moreover, a specification weakness can arise when verification relies on unproven or invalidated assumptions, such as axiomatic lemmas and assume statements. We investigate whether LLM agents can synthesize strong DLL specifications while minimizing these trusted base. The analysis follows three different approaches: manual verification, property-specific verification, and a defined skill for the specific case of DLLs and certain properties of this type of data structure. The skill encodes domain knowledge and a task-decomposition strategy. We show that an LLM agent equipped with a carefully designed verification skill can generate strong, low-trust specifications for DLLs in Verus.

A resonant classical field drives a two-level system coherently and, with ordinary relaxation, produces saturation rather than directional population transfer. Here we show that directionality emerges when the excitation source is retained as a quantum subsystem and subsequently traced out. We model the source as a single-excitation degree of freedom, or equivalently a stream of two-level ancillas, exchange-coupled to a target two-level system. The source first moment generates the usual coherent drive, while its second moments produce upward and downward dissipative channels. For a number-diagonal, fully excited source, the first moment vanishes and only the upward channel remains, yielding monotonic pumping of the target. The same structure follows from both an exact collision map and a fluctuation-regulated second-order quantum master equation. For exponentially decaying source correlations, the pumping rate shows a Lorentzian detuning dependence governed by the correlation time $\tau_c$, accompanied by a dispersive frequency shift. In the presence of thermal relaxation, the steady-state excited-state population can exceed the resonantly driven optical-Bloch limit of one half. Within the fluctuation-regulated master equation, this directional pumping arises as a drive-induced dissipative contribution whose strength and spectral response are controlled by $\tau_c$.

Post-training quantization reduces the deployment cost of vision-language models (VLMs), but preserving multimodal capabilities at low bit widths remains challenging. Existing methods rely on modality- or token-level gradient statistics, which are susceptible to cross-sample variations in visual-to-textual token ratios and the positions of visual information, limiting statistical stability. Moreover, overly coarse aggregation through absolute values and averaging discards gradient signs and channel-wise differences, limiting the separation of modality-specific sensitivities. In contrast, the channel space provides a shared coordinate system across samples, making it a more natural basis for capturing stable task-sensitive structures. We therefore propose SubRot, a signed gradient subspace calibration method for VLM rotation quantization. Through eigendecomposition of the empirical Fisher matrix of activation gradients, SubRot identifies a sensitive channel subspace with three properties: cross-sample stability, clear sensitivity separation, and consistent signed effects on the autoregressive loss along certain directions. Guided by a local Taylor expansion, SubRot combines signed first-order guidance along sign-stable directions with second-order constraints along the remaining sensitive directions, while retaining MSE for overall reconstruction quality. This objective steers quantization errors toward loss-decreasing directions while controlling their magnitude. Experiments on five VLMs across five benchmarks show consistent average-score improvements over FlatQuant under W4A6 and W4A4, reaching 1.4 percentage points on LLaVA-NeXT-7B. Under W4A4, average accuracy degradation from FP16 remains within 1.4 percentage points across all evaluated models, while LLaVA-v1.5-13B exceeds its FP16 average score by 0.4 percentage points.

We describe the formalization in Dafny of two computational models, Turing Machines and the Lambda Calculus. We present several application of the formalizations: machine proofs of termination for Turing machines, Dafny proofs for Church encodings, and a mechanized proof of the Church-Rosser theorem.

We present a formalization in Dafny of the Omega Test, an algorithm used to decide the satisfiability of a system of inequalities. The implementation defines executable representations for rational numbers, linear expressions, inequalities, equalities, divisibility constraints, and systems of constraints, together with their semantic interpretation through valuations. We fully specify and verify the implementation in Dafny. We describe the lessons learned and how the formalization process led to new insights into the algorithm.

In distributed systems, model checking is usually used at design time for specifying an abstract model of the system and then exhaustively checking all possible behaviors. TLA+ is commonly used in this way as a specification language, together with the TLC model checker. In this paper, we present a monitoring tool that, at its core, utilizes TLA+ specifications in a different way. The tool utilizes a TLA+ trace-checking specification to detect violations in behavior inferred from Kubernetes audit logs. Our primary use case focuses on multitenancy violations; however, the pipeline is not limited to that setting. Specifically, it demonstrates how formal reasoning can be incorporated into live Kubernetes environments to improve monitoring and correctness checking.

A resolvable network is a directed-graph representation of SAT: every SAT instance can be translated into an RN, and every RN has an associated CNF formula. Each reach represents one clause. In a mixed reach, the head and tail are disjoint sets of variables containing the variables occurring negatively and positively in the clause, respectively; the distinguished symbols Source and Sink represent a missing negative- or positive-literal side. RN-Solver is a proof-of-concept SAT solver based on this representation. Its all-positive clauses are represented by white reaches, and its token distributions are the inclusion-minimal hitting sets of the current white tails, generated by monotone CNF-DNF dualization. RN-Solver learns new white reaches by private-pivot resolution, a structured resolution sequence that uses old white reaches as pivot witnesses. In the original algorithm, every candidate white reach generated by such a chain was followed by a global subsumption test against the current network. Profiling showed that this subsumption test can dominate the runtime on random 3-SAT instances. We show that this check is unnecessary when the mixed reach used for learning is falsified by the current token distribution, meaning that the distribution makes all variables in the head true and all variables in the tail false. The key invariant is simple: the resulting white tail is disjoint from the triggering token distribution, while the same distribution intersects every old white tail. Hence no old white reach can subsume the generated reach. This structural observation allows us to construct a simpler, snapshot-based, subsumption-free variant of RN-Solver, where each main-loop iteration uses a fixed set of old reaches and installs newly generated white reaches only at the end of the iteration. We prove soundness of the revised algorithm. Empirical evaluation confirms the elimination of the targeted checks: within an 8 second budget, snapshot/full-DNF solves 963 of 1,000 uf20-91 instances, compared with 724 for the original control flow. A separate 100-instance comparison identifies exact incremental DNF as the most effective of the three tested configurations.

Tool agents use large language models to act through external tools, yet successfully executed calls can still leave user requests unfulfilled. Tool-agent repair seeks alternative call sequences that execute successfully and fulfill the original requests. However, repair requires exploring both operation choices and their concrete realizations, making complete-sequence regeneration costly. Moreover, regeneration repeats operation selection even when failure arises from how those operations are realized. The resulting challenge is to reduce this repetition while preserving exploration of alternative operations and realizations. Therefore, we formulate repair as hierarchical search over operation supports, which we introduce as sets of permitted operation types that define reusable search regions for concrete tool-call sequences. We propose ReCommit, a training-free, diffusion-guided framework for improving tool-agent failure recovery while reducing repair computation. ReCommit amortizes operation-level proposal computation across repair trials by reusing operation-type scores from a single parallel readout of a masked diffusion language model. These scores guide search across supports, while realization search explores alternative entity bindings, arguments, and action composition within each support. Experiments on real failures across four enterprise services in the Agent-Diff benchmark show 75.9% and 63.2% relative recovery gains with 61.3% and 51.3% reductions in mean full-budget repair time at repair budgets $B=3$ and $B=13$, respectively, over the strongest evaluated 8B comparison method. ReCommit achieves a favorable recovery–cost trade-off, including in comparisons with the evaluated 32B models.

Ensuring safe software updates in safety-critical systems without interrupting operation and without provisioning and activating cold spare hardware poses a fundamental challenge due to the conflict between system availability and update execution. In this paper, we present a bounded SMT encoding for synthesizing fixed global-time update schedules for timed-games with linear update automata and a fixed number of update transitions. We model the interaction between the system and the update as a two-player timed game. Our key contribution is the synthesis of global time points that define a fixed update schedule which guarantees safe and complete deployment of the update independently of the autonomous system behavior. To this end, we reduce the scheduling problem to a reachability and safety objective and encode it as a quantified SMT problem. We demonstrate it on an example system of a trajectory planner for autonomous driving, showing that the synthesized schedule ensures safe deployment under all admissible executions.

The axiomatization of the theory of hereditarily finite sets in first-order classical logic is systematically explored and formalized in Isabelle/HOL. The formalization uses a hierarchy of locales, each corresponding to a fragment of the theory given by a particular collection of axioms. An inductive definition of first-order definable predicates is introduced and used to formalize axiom schemata. Special attention is paid to several equivalent axioms of finiteness, as well as to several equivalent ways of expressing regularity. The work also formalizes several facts about the independence of an axiom from a system of axioms by defining appropriate models.

In this paper, we study the hypersurfaces in $\mathbb{H}^m\times\mathbb{H}^n$ ($m\geq3, n\geq2$) with constant principal curvatures. Let $g$ be the number of distinct constant principal curvatures. First, we classify all such hypersurfaces with $g\leq2$. Then, we prove that a hypersurface with constant principal curvatures and constant product angle function has $g\le3$, and we obtain a complete classification of these hypersurfaces. As a corollary, we classify the isoparametric hypersurfaces in $\mathbb{H}^m\times \mathbb{H}^n$ ($m\geq3, n\geq2$) with constant principal curvatures.

Reliable positioning, navigation, and timing support intelligent transportation, autonomous systems, and space-air-ground integrated networks. However, global navigation satellite system (GNSS) jamming recognizers that treat each mixture as a separate class are difficult to extend to new combinations. Therefore, this paper proposes SPOC-Net, which decomposes the recognition problem into identifying a set of basic jamming components. Multi-resolution time-frequency features and learned component queries provide evidence for each component type. A high-resolution branch estimates the number of active types, and a structured decoder combines this estimate with component evidence to select a valid set. For training, measured single-component records are the only physical samples used in gradient optimization. Their associated clean in-phase and quadrature (IQ) sequences are combined on demand during training to produce labeled mixtures with different relative powers and jamming-to-noise ratios. Separate measured mixtures from ten training-listed compositions support model selection and decoder calibration; six other compositions are reserved for final testing. Evaluation on 14,220 independently generated, conductively combined, and recorded radio frequency mixtures yields 80.69% exact-set accuracy and a 92.84% micro-averaged F1 score. On combinations excluded from model development, SPOC-Net achieves 80.89% exact-set accuracy, exceeding the strongest comparison method by 18.77 percentage points under the reported protocols.

We present spsurv, an R package for semi-parametric time-to-event regression based on Bernstein-polynomial estimation of unknown baseline functions. The package provides a unified modelling interface for proportional hazards (PH), proportional odds (PO), and accelerated failure time (AFT) models for right-censored data, with either maximum likelihood or Bayesian estimation via Stan. Smooth baseline hazard, odds-function, or log-time structures are estimated without assuming a parametric baseline family, while retaining familiar hazard-ratio, odds-ratio, and time-ratio interpretations. We describe methodology, implementation, and syntax; evaluate finite-sample behaviour in a Monte Carlo study; and illustrate usage with oncology trials.

Modern endpoint malware detection is distributed: a lightweight agent on each endpoint collects features from a scanned file or process, sends them to a remote server for analysis, and then enforces the returned verdict locally by blocking, quarantining, or disinfecting. Because the endpoint acts on the verdict, the distributed machinery surrounding detection must never turn a transient server failure into a wrong action. We present a formal model, in Promela, of the endpoint decision pipeline of such a system, abstracted from a production architecture at Bitdefender. The model captures the system's graceful-degradation fallback chain: when the primary analysis server times out, the endpoint falls back to an older legacy-protocol server, and failing that to a reduced-signature local scan, before enforcing a verdict. Assuming detection signatures are sound, we specify six safety and liveness properties in linear temporal logic (LTL) and verify them exhaustively with the SPIN model checker. We prove that the fallback machinery never causes a false positive (an enforcement action against a benign file), commits to exactly one verdict per scan even when timed-out responses arrive late, weakens detection strength only in an explicit and ordered way, and always terminates in an enforcement decision, so the pipeline is deadlock-free. Each property is checked to hold non-vacuously, and we report how the state space grows with concurrent scans and endpoints. The work shows how model checking can give strong correctness guarantees for the failure-handling logic of a production security system, a layer that has received little direct formal attention.

The O-band telecommunication spectral range combines minimal chromatic dispersion with low transmission loss, making it highly suitable for optical communications. Semiconductor telecom lasers utilizing low-dimensional active regions, such as quantum dots, offer low threshold power and high thermal stability. However, long-wavelength quantum dot emitters often suffer from thermal carrier escape through excited states when the energy separation between the ground and excited states is insufficient. Here we demonstrate the optimization of InAs quantum dot emitters grown on InP by molecular-beam epitaxy for O-band laser active regions. By optimizing the design for better carrier capture efficiency and tuning the emission wavelength to the O-band, we show ways of improving the carrier confinement. Absorption spectroscopy on the finalized structure confirms substantial energy separation between the quantum dot ground and excited states, effectively suppressing thermal carrier escape even at elevated temperatures. These results highlight critical design for improving carrier capture and retention in long-wavelength quantum dot lasers.

The large safety instrumentation & control (I&C) systems in civil nuclear power plants (NPPs) are mainly safe-shutdown systems (reactor protection) or limitation and control systems. Framatome's established TELEPERM XS (TXS Core) product family is a digital I&C system platform to cover all these applications. We illustrate the role of verification in the different stages of the software production toolchain, focus on the formal compilation process, and discuss the contribution of the CompCert certified compiler to the safety case of the product. Scrutinizing the object code produced by this compiler has exhibited suboptimal run-time performance in a certain simple but recurring generated code pattern. We explain how formal methods allow us to address this issue in the compiler while simultaneously reducing its trusted computing base (TCB), thereby strengthening the safety case rather than merely preserving it.

Light scattering in heterogeneous media underpins a broad range of natural phenomena and optical technologies, yet remains difficult to understand in porous nanocomposites. State-of-the-art theories generally treat these materials as two-phase systems consisting of particles and a matrix, overlooking the air pores that are intrinsically present in porous composites. Here we experimentally determine the scattering coefficients of six BaSO4-acrylic and TiO2-acrylic coatings spanning a range of particle volume fractions and develop a three-phase scattering framework that explicitly accounts for pore-induced scattering. By representing the composite as two coupled scattering subsystems, particle-matrix and particle-air, the framework resolves discrepancies between theory and experiment: conventional two phase models substantially underpredict scattering in BaSO4 coatings while overpredicting scattering in TiO2 coatings, whereas the three-phase model accurately captures the observed trends and reduces the mean absolute logarithmic error from 0.667 to 0.379. This framework identifies air pores as a fundamental and independently controllable contributor to optical scattering, providing new physical insights and design principles for engineering highly scattering porous nanocomposites.

Interatomic potentials are central tools in the atomistic modeling of materials. The atomic cluster expansion (ACE) parameterizes such potentials from ab initio data, conventionally encoding the chemical degrees of freedom with a one-hot representation that yields chemically stratified models. The alternative chemical representations used in on-lattice configurational cluster expansions have not been assessed for interatomic potentials. Here we revisit the multicomponent ACE for an arbitrary chemical site basis. We then establish an exact analytical mapping between a fitted linear ACE and the average-atom potential that describes a perfectly random alloy. We benchmark potentials built on the occupational, Chebyshev, and conventional ACE bases against solute binding and vacancy formation energies in Mg-Nd, and against the mixing enthalpies of the Mo-Nb and Cr-W solid solutions. When training data are scarce, the occupational basis converges fastest and offers the best control over targeted material properties, while the conventional and Chebyshev bases face challenges in reproducing these properties. The occupational basis likewise yields the most reliable average-atom description of disordered alloy thermodynamics. In the large-data limit the three bases perform identically. The chemical basis is therefore a design choice that governs data efficiency. Its explicit treatment opens a route to average-atom potentials for the thermodynamic, mechanical, and kinetic properties of concentrated alloys.

This study presents multi-epoch photometry from the Wide-field Infrared Survey Explorer to investigate variability in white dwarf debris disks, utilizing the full 14.5 yr mission datasets pre- and post-cryogen. Unambiguous variations are detected across the bulk of the 52 confirmed dusty white dwarfs and are consistent with universal variability after correcting for the sensitivity of WISE relative to Spitzer. Some disk light curves exhibit trends such as possible oscillations, sudden brightening, and steadily decaying fluxes, but all infrared excesses persist utterly. On baselines longer than 0.5 yr, flux changes are significantly skewed toward decreases, in contrast to the symmetric distribution found at shorter baselines with Spitzer, consistent with gradual dust depletion over time. Disk emission generally becomes redder when dimmer and bluer when brighter, consistent with changes in the grain size distribution following collisions, although five disks exhibit the opposite trend possibly due to dust production near apastron. A moderate positive correlation is observed between disk luminosity and photospheric Ca abundance, consistent with the accretion of disk material in an optically thin configuration. Taken together with the Spitzer legacy of dusty white dwarfs, these results provide a comprehensive view of debris disk variability and provide empirical constraints on models of disk structure and evolution.

Vision language models have achieved strong performance across a wide range of multimodal applications, yet their substantial computational and memory costs hinder efficient deployment. Visual token pruning and post-training quantization reduce inference overhead along two complementary dimensions, namely sequence length and numerical precision. Existing workflows typically optimize these techniques independently or apply them sequentially. Their distinct optimization objectives leave critical interactions unaddressed and constrain the achievable compression performance. We revisit these designs and present P4Q, a practical co-design framework that jointly optimizes visual token pruning and low-bit quantization for efficient VLM inference. First, P4Q introduces a quantization-aware visual token selection strategy before the LLM. It applies fake quantization to copies of the features produced by the projector and selects visual tokens using statistics computed from these fake-quantized features, thereby conditioning the selector's feature-based decisions on simulated low-bit perturbations. Second, P4Q introduces a pruning-aware quantization calibration strategy. It uses the same selection strategy as pruning to calibrate the quantized model on the retained-token distribution, thereby aligning the calibration process with the pruned execution path used during deployment. By coupling these two components, P4Q achieves substantial inference speedups while maintaining comparable task performance, resulting in a better efficiency-accuracy trade-off than independently optimized pipelines. For instance, on LLaVA-NeXT, P4Q achieves an average end-to-end inference speedup of 2.8x across eight distinct test sets, while retaining higher accuracy than prior compression and quantization methods.