Hanyun Jiang

Hanyun Jiang, Peisen Yao, Kaiyue Li et al.

Code optimization remains a core objective in software development, yet modern compilers struggle to navigate the enormous optimization spaces. While recent research has looked into employing large language models (LLMs) to optimize source code directly, these techniques can introduce semantic errors and miss fine-grained compiler-level optimization opportunities. We present HintPilot, which bridges LLM-based reasoning with traditional compiler infrastructures via synthesizing compiler hints, annotations that steer compiler behavior. HintPilot employs retrieval-augmented synthesis over compiler documentation and applies profiling-guided iterative refinement to synthesize semantics-preserving and effective hints. Upon PolyBench and HumanEval-CPP benchmarks, HintPilot achieves up to 6.88x geometric mean speedup over -Ofast while preserving program correctness.

Yue Wang, Yuyang Xu, Renjun Hu et al.

Despite the rapid advancements of electrocardiogram (ECG) signal diagnosis and analysis methods through deep learning, two major hurdles still limit their clinical adoption: the lack of versatility in processing ECG signals with diverse configurations, and the inadequate detection of risk signals due to sample imbalances. Addressing these challenges, we introduce VersAtile and Risk-Sensitive cardiac diagnosis (VARS), an innovative approach that employs a graph-based representation to uniformly model heterogeneous ECG signals. VARS stands out by transforming ECG signals into versatile graph structures that capture critical diagnostic features, irrespective of signal diversity in the lead count, sampling frequency, and duration. This graph-centric formulation also enhances diagnostic sensitivity, enabling precise localization and identification of abnormal ECG patterns that often elude standard analysis methods. To facilitate representation transformation, our approach integrates denoising reconstruction with contrastive learning to preserve raw ECG information while highlighting pathognomonic patterns. We rigorously evaluate the efficacy of VARS on three distinct ECG datasets, encompassing a range of structural variations. The results demonstrate that VARS not only consistently surpasses existing state-of-the-art models across all these datasets but also exhibits substantial improvement in identifying risk signals. Additionally, VARS offers interpretability by pinpointing the exact waveforms that lead to specific model outputs, thereby assisting clinicians in making informed decisions. These findings suggest that our VARS will likely emerge as an invaluable tool for comprehensive cardiac health assessment.

Jiening Siow, Hanrui Zuo, Hanyun Jiang et al.

Program analyzers often issue batches of SMT queries that share a large symbolic context and differ only in a small predicate. We formalize this recurring pattern as \emph{Shared-Context Batched Satisfiability}: given a formula $φ$ and predicates $P$, determine whether $φ\land p$ is satisfiable for each $p \in P$. We study three theory-agnostic strategies for this problem: predicate-by-predicate checking, disjunctive over-approximation, and Core-Literal Filter (CLF), a new algorithm that learns literals inconsistent with $φ$ and uses them to reject later predicates. Our evaluation on symbolic abstraction and active property checking shows that no strategy dominates universally: over-approximation is fastest on solved symbolic-abstraction queries, while CLF increases the number of solved hard instances and is fastest on active property checking. We advocate treating shared-context batched satisfiability as a first-class primitive in design program analyzers and exploring the algorithmic design space more systematically.