arXiv subjects

Hanyun Jiang

Publications and source records attributed to Hanyun Jiang.

4 recordsLinked to original sources

arXiv2026

DatalogBench: Evaluating Large Language Models on Text-to-Datalog Synthesis

Datalog underpins reasoning tasks such as program analysis, but its programs are hard to write. Existing synthesizers automate this task but require users to state their intent as input-output examples. Large language models (LLMs) suggest a more natural route, text-to-Datalog synthesis from a natural-language question, yet how well they do so has not been systematically evaluated. We present DatalogBench, a benchmark of 136 text-to-Datalog synthesis tasks curated from existing Datalog-based artifacts. Synthesized programs are graded by execution on held-out inputs against an oracle validated by mutation analysis. Across six LLMs and four prompting configurations, exact match peaks at 68.4%, and relation descriptions or an input-output example have only modest, model-dependent effects. Under direct prompting, most failures occur at compile time, typically because a model invents auxiliary predicates that it never declares or types consistently. Two coding agents reach up to 83.8% and eliminate nearly all such failures, leaving mostly semantic errors concentrated in recursive tasks. DatalogBench thus identifies recursive reasoning and decomposition as open challenges for current LLMs and agents, and offers a reliable, execution-grounded measure of both.

cs.PL↗

arXiv2026

Shared-Context Batched Satisfiability

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.

cs.PL↗

arXiv2026

HintPilot: LLM-based Compiler Hint Synthesis for Code Optimization

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.

cs.SE↗

arXiv2025

Versatile and Risk-Sensitive Cardiac Diagnosis via Graph-Based ECG Signal Representation

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.

cs.AI↗