The CCR framework unifies refinement and separation logic to provide ownership-based modular reasoning and transitive incremental reasoning in open settings that involve unverified code. However, when reasoning about function invocations, the reasoning principles available to clients remain confined to pre- and postconditions, which struggle to capture effectful behaviors such as I/O actions or interactions with arbitrary unverified code. This limitation becomes particularly acute in hybrid verification , where a mixture of different verification techniques is applied and some code is never formally verified but instead tested or model-checked. To overcome this limitation, we introduce imaginary specifications —a novel notion that freely mixes executable code with ownership assertions—and reasoning principles for their use. Through key technical developments, we present CRIS (Contextual Refinement with Imaginary Specifications), a framework that generalizes CCR with support for imaginary specifications. We demonstrate CRIS’s expressiveness and reasoning power through examples involving hybrid verification with unverified code exhibiting arbitrary side effects such as I/O or divergence, with complete mechanization in Rocq.

Deep learning kernels exhibit a high level of predictable memory accesses and compute patterns, making GPU's architecture well-suited for their execution. Moreover, software and runtime system for GPUs further enable optimizations that aim to better utilize the stream multiprocessors, on-chip bandwidth, multiple levels of cache hierarchy, and off-chip high-bandwidth memory. In the context of deep learning, the entire space of models and GPUs is constantly evolving, as newer models emerge with simultaneous upgrades to the device. However, access to newer GPUs is often limited, raising important questions about the performance of new model architectures on existing GPUs, existing models on new GPUs, and new model architectures on new GPUs. To address these questions, we introduce NeuSight, a forecasting framework to predict the performance of a diverse range of deep learning models, for both training and inference, on unseen GPUs, without requiring actual execution of the target model on the target GPU. The framework leverages both GPU hardware behavior and software library optimizations to estimate the end-to-end performance of these models. We observe that prior work in this area suffers from high absolute error percentages when forecasting performance on unseen models and new GPUs, as they attempt to model the complex task of predicting the latency of a deep learning kernel on a GPU directly using a machine learning approach. Instead, with NeuSight, we decompose the prediction into smaller problems, while bounding the prediction through fundamental performance laws. NeuSight decomposes a single deep learning kernel prediction into smaller working sets called tiles, which are executed independently on the GPU. Tile-granularity predictions are determined using a machine learning approach and aggregated to estimate the end-to-end latency. As such, NeuSight outperforms prior work across a variety of deep learning workloads and the most up-to-date GPUs. It reduces the percentage error from 121.4% and 30.8% to 2.3% in predicting the latency of GPT3 model for training and inference on H100, in comparison to state-of-the-art prior work, respectively, where GPT3 and H100 were not used to train any framework.

Open-Vocabulary Part Segmentation (OVPS) is an emerging field for recognizing fine-grained parts in unseen categories. We identify two primary challenges in OVPS: (1) the difficulty in aligning part-level image-text correspondence, and (2) the lack of structural understanding in segmenting object parts. To address these issues, we propose Part-CATSeg, a novel framework that integrates object-aware part-level cost aggregation, compositional loss, and structural guidance from DINO. Our approach employs a disentangled cost aggregation strategy that handles object and part-level costs separately, enhancing the precision of part-level segmentation. We also introduce a compositional loss to better capture part-object relationships, compensating for the limited part annotations. Additionally, structural guidance from DINO features improves boundary delineation and inter-part understanding. Extensive experiments on Pascal-Part-116, ADE20K-Part-234, and PartImageNet datasets demonstrate that our method significantly outperforms state-of-the-art approaches, setting a new baseline for robust generalization to unseen part categories.

Recent advancements in text-to-image diffusion models have shown impressive results but often fail to fully capture user’s intent. Existing methods combining textual inputs with bounding boxes or region masks lack precise spatial guidance, leading to misaligned or unintended object orientations. To address these issues, we propose Scribble-Guided Diffusion (ScribbleDiff), a training-free approach that employs user-provided scribbles as visual prompts for image generation. However, incorporating scribbles poses challenges due to their sparse and thin nature, which complicates accurate alignment. To resolve this, we introduce moment alignment and scribble propagation, enabling effective and flexible alignment between generated images and scribble inputs. Experiments on the PASCAL-Scribble dataset demonstrate notable improvements in spatial control and consistency, validating the effectiveness of our method in scribble-guidance.

Score distillation sampling (SDS) has emerged as an effective framework in text-driven 3D editing tasks, leveraging diffusion models for 3D-consistent editing. However, existing SDS-based 3D editing methods suffer from long training times and produce low-quality results. We identify that the root cause of this performance degradation is their conflict with the sampling dynamics of diffusion models. Addressing this conflict allows us to treat SDS as a diffusion reverse process for 3D editing via sampling from data space. In contrast, existing methods naively distill the score function using diffusion models. From these insights, we propose DreamCatalyst, a novel framework that considers these sampling dynamics in the SDS framework. Specifically, we devise the optimization process of our DreamCatalyst to approximate the diffusion reverse process in editing tasks, thereby aligning with diffusion sampling dynamics. As a result, DreamCatalyst successfully reduces training time and improves editing quality. Our method offers two modes: (1) a fast mode that edits Neural Radiance Fields (NeRF) scenes approximately 23 times faster than current state-of-the-art NeRF editing methods, and (2) a high-quality mode that produces superior results about 8 times faster than these methods. Notably, our high-quality mode outperforms current state-of-the-art NeRF editing methods in terms of both speed and quality. DreamCatalyst also surpasses the state-of-the-art 3D Gaussian Splatting (3DGS) editing methods, establishing itself as an effective and model-agnostic 3D editing solution.

This paper characterizes the interplay between overlapping compute and communication in GPU-accelerated distributed training, a critical but often overlooked aspect impacting performance and power. We systematically evaluate state-of-the-art NVIDIA (H100/A100) and AMD (MI250/MI210) GPUs, investigating the effects of hardware features including numeric precision, specialized cores, and power capping. Experiments across GPT and LLaMA models show that overlap causes significant compute slowdown (an average of 18.9 % and upto 40.0 %) compared to an ideal scenario where compute executes without communication interference. However, overlapping execution is still faster than sequential execution by an average 10.2 % and maximum of 26.6 %. We find overlap increases peak power, specialized datapaths have mixed effects, and power capping severely exacerbates slowdowns. These results emphasize the need for balanced strategies in optimizing distributed training throughput and power efficiency.

Skeleton-based hand gesture recognition plays a crucial role in enabling intuitive human–computer interaction. Traditional methods have primarily relied on hand-crafted features—such as distances between joints or positional changes across frames—to alleviate issues from viewpoint variation or body proportion differences. However, these hand-crafted features often fail to capture the full spatio-temporal information in raw skeleton data, exhibit poor interpretability, and depend heavily on dataset-specific preprocessing, limiting generalization. In addition, normalization strategies in traditional methods, which rely on training data, can introduce domain gaps between training and testing environments, further hindering robustness in diverse real-world settings. To overcome these challenges, we exclude traditional hand-crafted features and propose Skeleton Kinematics Extraction Through Coordinated grapH (SKETCH), a novel framework that directly utilizes raw four-dimensional (time, x, y, and z) skeleton sequences and transforms them into intuitive visual graph representations. The proposed framework incorporates a novel learnable Dynamic Range Embedding (DRE) to preserve axis-wise motion magnitudes lost during normalization and visual graph representations, enabling richer and more discriminative feature learning. This approach produces a graph image that richly captures the raw data’s inherent information and provides interpretable visual attention cues. Furthermore, SKETCH applies independent min–max normalization on fixed-length temporal windows in real time, mitigating degradation from absolute coordinate fluctuations caused by varying sensor viewpoints or differences in individual body proportions. Through these designs, our approach becomes inherently topology-agnostic, avoiding fragile dependencies on dataset- or sensor-specific skeleton definitions. By leveraging pre-trained vision backbones, SKETCH achieves efficient convergence and superior recognition accuracy. Experimental results on SHREC’19 and SHREC’22 benchmarks show that it outperforms state-of-the-art methods in both robustness and generalization, establishing a new paradigm for skeleton-based hand gesture recognition. The code is available at https://github.com/capableofanything/SKETCH.

Open-vocabulary part segmentation (OVPS) is an emerging research area focused on segmenting fine-grained entities using diverse and previously unseen vocabularies. Our study highlights the inherent complexities of part segmentation due to intricate boundaries and diverse granularity, reflecting the knowledge-based nature of part identification. To address these challenges, we propose PartCLIPSeg, a novel framework utilizing generalized parts and object-level contexts to mitigate the lack of generalization in fine-grained parts. PartCLIPSeg integrates competitive part relationships and attention control, alleviating ambiguous boundaries and underrepresented parts. Experimental results demonstrate that PartCLIPSeg outperforms existing state-of-the-art OVPS methods, offering refined segmentation and an advanced understanding of part relationships within images. Through extensive experiments, our model demonstrated a significant improvement over the state-of-the-art models on the Pascal-Part-116, ADE20K-Part-234, and PartImageNet datasets.

Frequent subgraph mining is an important and well-studied problem with numerous applications such as the prediction of protein functionalities and graph indexing. Many studies use the minimum-image-based support (MNI) to measure the frequency of subgraphs in single graph mining. Given a graph G and an integer k , top- k frequent subgraph mining is to find top- k frequent subgraphs in the graph G based on MNI. However, there are two main challenges in top- k frequent subgraph mining. (1) Computing MNI is time-consuming. (2) The number of subgraphs for which MNI should be computed is large. In this paper, we propose a novel algorithm Minting to address these challenges. We propose a method to significantly reduce the number of subgraphs for which MNI computation is required by using a tight upper bound of the MNI value. We also improve the computation of MNI itself by utilizing both a lower bound and an upper bound of the MNI value. Experiments shows that our algorithm outperforms the state-of-the-art algorithms by up to three orders of magnitude in terms of the elapsed time. Our algorithm is also a feasible solution for this challenging problem, even for large k.

We present template-guided concolic testing, a new technique for effectively reducing the search space in concolic testing. Addressing the path-explosion problem has been a significant challenge in concolic testing. Diverse search heuristics have been proposed to mitigate this problem but using search heuristics alone is not sufficient to substantially improve code coverage for real-world programs. The goal of this paper is to complement existing techniques and achieve higher coverage by exploiting templates in concolic testing. In our approach, a template is a partially symbolized input vector whose job is to reduce the search space. However, choosing a right set of templates is nontrivial and significantly affects the final performance of our approach. We present an algorithm that automatically learns useful templates online, based on data collected from previous runs of concolic testing. The experimental results with open-source programs show that our technique achieves greater branch coverage and finds bugs more effectively than conventional concolic testing.