arXiv subjects

JingJing Zhang

Publications and source records attributed to JingJing Zhang.

4 recordsLinked to original sources

arXiv2026

Enhancing LLM-based Specification Generation via Program Slicing and Logical Deletion

Traditional formal specification generation methods are typically tailored to specific specification types, and therefore suffer from limited generality. In recent years, large language model (LLM)-based specification generation approaches have emerged, offering a new direction for improving the universality of automated specification synthesis. However, when dealing with complex control flow, LLMs often struggle to precisely generate complete specifications that cover substructures. Moreover, the distinctive verification pipelines adopted by existing approaches may incorrectly discard logically correct specifications, while verification tools alone cannot reliably identify correct specifications. To address these issues, we propose SLD-Spec, an LLM-based specification generation method that combines program slicing and logical deletion. Specifically, SLD-Spec augments the conventional specification generation framework with two key stages: (1) a program slicing stage that decomposes the target function into several smaller code slices, enabling LLMs to focus on more localized semantic structures and thereby improving specification relevance and completeness; and (2) a logical deletion stage that leverages LLMs to perform logical reasoning and filtering over candidate specifications so as to retain logically correct ones. Experimental results show that SLD-Spec consistently outperforms existing methods on datasets containing programs of varying complexity, verifying more programs and generating specifications that are more relevant and more complete. Further ablation studies indicate that program slicing mainly improves specification relevance and completeness, whereas logical deletion plays a key role in increasing verification success rates.

cs.SE↗

arXiv2026

Beyond Basic Specifications? A Systematic Study of Logical Constructs in LLM-based Specification Generation

Formal specifications play a pivotal role in accurately characterizing program behaviors and ensuring software correctness. In recent years, leveraging large language models (LLMs) for the automatic generation of program specifications has emerged as a promising avenue for enhancing verification efficiency. However, existing research has been predominantly confined to generating specifications based on basic syntactic constructs, falling short of meeting the demands for high-level abstraction in complex program verification. Consequently, we propose incorporating logical constructs into existing LLM-based specification generation framework. Nevertheless, there remains a lack of systematic investigation into whether LLMs can effectively generate such complex constructs. To this end, we conduct an empirical study aimed at exploring the impact of various types of syntactic constructs on specification generation framework. Specifically, we define four syntactic configurations with varying levels of abstraction and perform extensive evaluations on mainstream program verification datasets, employing a diverse set of representative LLMs. Experimental results first confirm that LLMs are capable of generating valid logical constructs. Further analysis reveals that the synergistic use of logical constructs and basic syntactic constructs leads to improvements in both verification capability and robustness, without significantly increasing verification overhead. Additionally, we uncover the distinct advantages of two refinement paradigms. To the best of our knowledge, this is the first systematic work exploring the feasibility of utilizing LLMs for generating high-level logical constructs, providing an empirical basis and guidance for the future construction of automated program verification framework with enhanced abstraction capabilities.

cs.SE↗

arXiv2024

Unbiased Estimation for Total Treatment Effect Under Interference Using Aggregated Dyadic Data

In social media platforms, user behavior is often influenced by interactions with other users, complicating the accurate estimation of causal effects in traditional A/B experiments. This study investigates situations where an individual's outcome can be broken down into the sum of multiple pairwise outcomes, a reflection of user interactions. These outcomes, referred to as dyadic data, are prevalent in many social network contexts. Utilizing a Bernoulli randomized design, we introduce a novel unbiased estimator for the total treatment effect (TTE), which quantifies the difference in population mean when all individuals are assigned to treatment versus control groups. We further explore the bias of our estimator in scenarios where it is impractical to include all individuals in the experiment, a common constraint in online control experiments. Our numerical results reveal that our proposed estimator consistently outperforms some commonly used estimators, underscoring its potential for more precise causal effect estimation in social media environments.

cs.SI↗

arXiv2024

Ego Group Partition: A Novel Framework for Improving Ego Experiments in Social Networks

Estimating the average treatment effect in social networks is challenging due to individuals influencing each other. One approach to address interference is ego cluster experiments, where each cluster consists of a central individual (ego) and its peers (alters). Clusters are randomized, and only the effects on egos are measured. In this work, we propose an improved framework for ego cluster experiments called ego group partition (EGP), which directly generates two groups and an ego sub-population instead of ego clusters. Under specific model assumptions, we propose two ego group partition algorithms. Compared to the original ego clustering algorithm, our algorithms produce more egos, yield smaller biases, and support parallel computation. The performance of our algorithms is validated through simulation and real-world case studies.

cs.SI↗