Author name cluster

Hanpin Wang

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

29 papers

2 author rows

AAAI Conference 2026 Conference Paper

Beyond Conservation: Flexible Molecular Assembly with Unbalanced Diffusion Bridge

Rongchao Zhang
Yiwei Lou
Yu Huang
Yi Xin
Yongzhi Cao
Hanpin Wang

Molecular assembly (MA) has long been a fundamental task in chemistry and biology, with the potential to create new materials and enable novel functions beyond the molecular scale. However, its vast conformational search space poses substantial challenges, and current generative models remain limited in capturing molecular flexibility and preventing non-physical poses. In this paper, we propose AssemUDB, a diffusion bridge–based framework that learns transport mappings between two distinct flexible domains for molecular assembly generation. We reformulate the marginal matching constraint of diffusion bridges as a coupling distribution governed by unbalanced transport rather than imposing strict conservation. Subsequently, we employ a progressive process from structural relaxation in Euclidean space to assembly on the SE(3) manifold. This relaxation of marginal conservation grants the generative model greater flexibility and leads to more physically plausible atom placements. Comprehensive experiments demonstrate the superior performance of AssemUDB. Notably, we find that the method demonstrates performance comparable to, or even better than, mature tools such as PackMol for packing tasks.

PDF Details DOI

AAAI Conference 2026 Conference Paper

MedMKEB: A Comprehensive Knowledge Editing Benchmark for Medical Multimodal Large Language Models

Dexuan Xu
Jieyi Wang
Zhongyan Chai
Yongzhi Cao
Hanpin Wang
Huamin Zhang
Yu Huang

Recent advances in multimodal large language models (MLLMs) have significantly improved medical AI, enabling it to unify the understanding of visual and textual information. However, as medical knowledge continues to evolve, it is critical to allow these models to efficiently update outdated or incorrect information without retraining from scratch. Although textual knowledge editing has been widely studied, there is still a lack of systematic benchmarks for multimodal medical knowledge editing involving image and text modalities. To fill this gap, we present MedMKEB, the first comprehensive benchmark designed to evaluate the reliability, generality, locality, portability, and robustness of knowledge editing in medical multimodal large language models. MedMKEB is built on a high-quality medical visual question-answering dataset and enriched with carefully constructed editing tasks, including counterfactual correction, semantic generalization, knowledge transfer, and adversarial robustness. We incorporate human expert validation to ensure the accuracy and reliability of the benchmark. Extensive experiments on state-of-the-art general and medical MLLMs demonstrate the limitations of existing knowledge editing methods in the medical domain, highlighting the need to develop specialized editing strategies.

PDF Details DOI

AAAI Conference 2026 Conference Paper

Multitasks-based Deep Evidential Fusion Network for Blind Image Quality Assessment

Yiwei Lou
Yuanpeng He
Rongchao Zhang
Yongzhi Cao
Hanpin Wang
Yu Huang

Blind image quality assessment (BIQA) methods often incorporate auxiliary tasks to improve performance. However, existing approaches face limitations due to insufficient integration and a lack of flexible uncertainty estimation, leading to suboptimal performance. To address these challenges, we propose a multitasks-based Deep Evidential Fusion Network (DEFNet) for BIQA, which performs multitask optimization with the assistance of scene and distortion type classification tasks. To achieve a more robust and reliable representation, we design a novel trustworthy information fusion strategy. It first combines diverse features and patterns across sub-regions to enhance information richness, and then performs local-global information fusion by balancing fine-grained details with coarse-grained context. Moreover, DEFNet exploits advanced uncertainty estimation technique inspired by evidential learning with the help of normal-inverse gamma distribution mixture. Extensive experiments on both synthetic and authentic distortion datasets demonstrate the effectiveness and robustness of the proposed framework. Additional evaluation and analysis are carried out to highlight its strong generalization capability and adaptability to previously unseen scenarios.

PDF Details DOI

ICLR Conference 2025 Conference Paper

Differentiable Rule Induction from Raw Sequence Inputs

Kun Gao 0003
Katsumi Inoue
Yongzhi Cao
Hanpin Wang
Yang Feng

Rule learning-based models are widely used in highly interpretable scenarios due to their transparent structures. Inductive logic programming (ILP), a form of machine learning, induces rules from facts while maintaining interpretability. Differentiable ILP models enhance this process by leveraging neural networks to improve robustness and scalability. However, most differentiable ILP methods rely on symbolic datasets, facing challenges when learning directly from raw data. Specifically, they struggle with explicit label leakage: The inability to map continuous inputs to symbolic variables without explicit supervision of input feature labels. In this work, we address this issue by integrating a self-supervised differentiable clustering model with a novel differentiable ILP model, enabling rule learning from raw data without explicit label leakage. The learned rules effectively describe raw data through its features. We demonstrate that our method intuitively and precisely learns generalized rules from time series and image data.

Details

AAAI Conference 2025 Conference Paper

Exploit Your Latents: Coarse-Grained Protein Backmapping with Latent Diffusion Models

Rongchao Zhang
Yu Huang
Yiwei Lou
Yi Xin
Haixu Chen
Yongzhi Cao
Hanpin Wang

Coarse-grained (CG) molecular dynamics of proteins is a preferred approach to studying large molecules on extended time scales by condensing the entire atomic model into a limited number of pseudo-atoms and preserving the thermodynamic properties of the system. However, the significantly increased efficiency impedes the analysis of substantial physicochemical information, since high-resolution atomic details are sacrificed to accelerate simulation. In this paper, we propose LatCPB, a generative approach based on diffusion that enables high-resolution backmapping of CG proteins. Specifically, our model encodes an all-atom into discrete latent embeddings, aligned with learnable multimodal discrete priors for circumventing posterior collapse and maintaining the discrete properties of the protein sequence. During the generation, we further design a latent diffusion process within the continuous latent space due to the potential stochastics in the data. Moreover, LatCPB performs a contrastive learning strategy in latent space to separate feature representations of various molecules and conformations of the same molecule, thus enhancing the comprehension of molecular representational diversity. Experimental results demonstrate that LatCPB is able to backmap CG proteins effectively and achieve outstanding performance.

PDF Details DOI

TCS Journal 2025 Journal Article

Expressive completeness of separation logic in block-based cloud storage systems

Tianyue Cao
Zhao Jin
Bowen Zhang
Yongzhi Cao
Hanpin Wang

Block-based cloud storage systems are widely used to store big data. Although they are highly fault-tolerant, the occurrence of bugs is still inevitable. Separation logic was proposed for mutable data structures, and can be used to verify block-based cloud storage systems. Hoare-style proof system has been constructed to verify these systems, and has been implemented in Coq. However, expressiveness of the assertion language in this formal system has not been fully studied. To fill this gap, we show the expressive completeness of separation logic in block-based cloud storage system, and prove the following three main consequences: (1) this logic is strictly more expressive than first-order logic, (2) this logic is as expressive as separation logic, and (3) this logic is as expressive as weak second-order logic with sequences.

Details DOI

NeurIPS Conference 2025 Conference Paper

MoleBridge: Synthetic Space Projecting with Discrete Markov Bridges

Rongchao Zhang
Yu Huang
Yongzhi Cao
Hanpin Wang

Molecular synthetic space projecting is a critical technique in de novo molecular design, which aims to rectify molecules without synthesizability guarantee by converting them into synthetic postfix notations. However, the vast synthesizable chemical space and the discrete data modalities involved pose significant challenges to postfix notation conversion benchmarking. In this paper, we exploit conditional probability transitions in discrete state space and introduce MoleBridge, a deep generative model built on the Markov bridge approach for designing postfix notations of molecular synthesis pathways. MoleBridge consists of two iterative optimizations: i) Autoregressive extending of notation tokens from molecular graphs, and ii) generation of discrete reaction postfix notations through Markov bridge, where noisy token blocks are progressively denoised over multi-step iterations. For the challenging second iteration, which demands sensitivity to incorrect generative probability paths within intricate chemical spaces, we employ a thinking and denoising separation approach to denoise. Empirically, we find that MoleBridge is capable of accurately predicting synthesis pathways while exhibiting excellent performance in a variety of application scenarios.

PDF Details

TCS Journal 2025 Journal Article

The complexity of ferromagnetic 2-spin systems on bounded degree graphs

Zonglei Bai
Yongzhi Cao
Hanpin Wang

Spin systems model the interactions between neighbors on graphs. An important special case is when there are only 2-spins. For 2-spin systems, the problem of approximating the partition function is well understood for anti-ferromagnetic case, while the ferromagnetic case is still not clear. We study the approximability of ferromagnetic 2-spin systems on bounded degree graphs, and make a new step towards the open problem of classifying the ferromagnetic 2-spin systems. On the algorithmic side, we show that the partition function is zero-free for any external field in the whole complex plane except a ring surrounded by two circles with respect to the degree bounds. Especially, for regular graphs, the two circles coincide, and the partition function vanishes only when the external field lies on the circle. Then using Barvinok's method, we obtain a new efficient and deterministic fully polynomial time approximation scheme (FPTAS) for the partition function in the zero-free regions. On the hardness side, we prove the #BIS-hardness of ferromagnetic 2-spin systems on bounded degree graphs. There exists an interval on the real axis so that this problem is #BIS-hard for any external field in the interval. Especially, the upper bound of the interval coincides with the boundary of the zero-free regions, which implies a complexity transition at the point.

Details DOI

UAI Conference 2025 Conference Paper

Trading Off Voting Axioms for Privacy

Zhechen Li
Ao Liu 0001
Lirong Xia
Yongzhi Cao
Hanpin Wang

In this paper, we investigate tradeoffs among differential privacy (DP) and several important voting axioms: Pareto efficiency, SD-efficiency, PC-efficiency, Condorcet criterion, and Condorcet loser criterion. We provide upper and lower bounds on the two-way tradeoffs between DP and each axiom. We also provide upper and lower bounds on three-way tradeoffs among DP and every pairwise combination of all the axioms, showing that, while the axioms are compatible without DP, their upper bounds cannot be achieved simultaneously under DP. Our results illustrate the effect of DP on the satisfaction and compatibility of voting axioms.

Details

AIJ Journal 2024 Journal Article

A differentiable first-order rule learner for inductive logic programming

Kun Gao
Katsumi Inoue
Yongzhi Cao
Hanpin Wang

Learning first-order logic programs from relational facts yields intuitive insights into the data. Inductive logic programming (ILP) models are effective in learning first-order logic programs from observed relational data. Symbolic ILP models support rule learning in a data-efficient manner. However, symbolic ILP models are not robust to learn from noisy data. Neuro-symbolic ILP models utilize neural networks to learn logic programs in a differentiable manner which improves the robustness of ILP models. However, most neuro-symbolic methods need a strong language bias to learn logic programs, which reduces the usability and flexibility of ILP models and limits the logic program formats. In addition, most neuro-symbolic ILP methods cannot learn logic programs effectively from both small-size datasets and large-size datasets such as knowledge graphs. In the paper, we introduce a novel differentiable ILP model called differentiable first-order rule learner (DFORL), which is scalable to learn rules from both smaller and larger datasets. Besides, DFORL only needs the number of variables in the learned logic programs as input. Hence, DFORL is easy to use and does not need a strong language bias. We demonstrate that DFORL can perform well on several standard ILP datasets, knowledge graphs, and probabilistic relation facts and outperform several well-known differentiable ILP models. Experimental results indicate that DFORL is a precise, robust, scalable, and computationally cheap differentiable ILP model.

Details DOI

IJCAI Conference 2024 Conference Paper

A differentiable first-order rule learner for inductive logic programming (Abstract Reprint)

Kun Gao
Katsumi Inoue
Yongzhi Cao
Hanpin Wang

Learning first-order logic programs from relational facts yields intuitive insights into the data. Inductive logic programming (ILP) models are effective in learning first-order logic programs from observed relational data. Symbolic ILP models support rule learning in a data-ecient manner. However, symbolic ILP models are not robust to learn from noisy data. Neuro-symbolic ILP models utilize neural networks to learn logic programs in a differentiable manner which improves the robustness of ILP models. However, most neuro-symbolic methods need a strong language bias to learn logic programs, which reduces the usability and flexibility of ILP models and limits the logic program formats. In addition, most neuro-symbolic ILP methods cannot learn logic programs effectively from both small-size datasets and large-size datasets such as knowledge graphs. In the paper, we introduce a novel differentiable ILP model called differentiable first-order rule learner (DFORL), which is scalable to learn rules from both smaller and larger datasets. Besides, DFORL only needs the number of variables in the learned logic programs as input. Hence, DFORL is easy to use and does not need a strong language bias. We demonstrate that DFORL can perform well on several standard ILP datasets, knowledge graphs, and probabilistic relation facts and outperform several well-known differentiable ILP models. Experimental results indicate that DFORL is a precise, robust, scalable, and computationally cheap differentiable ILP model.

PDF Details DOI

AAAI Conference 2024 Conference Paper

A Learnable Discrete-Prior Fusion Autoencoder with Contrastive Learning for Tabular Data Synthesis

Rongchao Zhang
Yiwei Lou
Dexuan Xu
Yongzhi Cao
Hanpin Wang
Yu Huang

The actual collection of tabular data for sharing involves confidentiality and privacy constraints, leaving the potential risks of machine learning for interventional data analysis unsafely averted. Synthetic data has emerged recently as a privacy-protecting solution to address this challenge. However, existing approaches regard discrete and continuous modal features as separate entities, thus falling short in properly capturing their inherent correlations. In this paper, we propose a novel contrastive learning guided Gaussian Transformer autoencoder, termed GTCoder, to synthesize photo-realistic multimodal tabular data for scientific research. Our approach introduces a transformer-based fusion module that seamlessly integrates multimodal features, permitting for mining more informative latent representations. The attention within the fusion module directs the integrated output features to focus on critical components that facilitate the task of generating latent embeddings. Moreover, we formulate a contrastive learning strategy to implicitly constrain the embeddings from discrete features in the latent feature space by encouraging the similar discrete feature distributions closer while pushing the dissimilar further away, in order to better enhance the representation of the latent embedding. Experimental results indicate that GTCoder is effective to generate photo-realistic synthetic data, with interactive interpretation of latent embedding, and performs favorably against some baselines on most real-world and simulated datasets.

PDF Details DOI

IJCAI Conference 2024 Conference Paper

Label Leakage in Vertical Federated Learning: A Survey

Yige Liu
Yiwei Lou
Yang Liu
Yongzhi Cao
Hanpin Wang

Vertical federated learning (VFL) is a distributed machine learning paradigm that collaboratively trains models using passive parties with features and an active party with additional labels. While VFL offers privacy preservation through data localization, the threat of label leakage remains a significant challenge. Label leakage occurs due to label inference attacks, where passive parties attempt to infer labels for their privacy and commercial value. Extensive research has been conducted on this specific VFL attack, but a comprehensive summary is still lacking. To bridge this gap, our paper aims to survey the existing label inference attacks and defenses. We propose two new taxonomies for both label inference attacks and defenses, respectively. Beyond summarizing the current state of research, we highlight techniques that we believe hold potential and could significantly influence future studies. Moreover, experimental benchmark datasets and evaluation metrics are summarized to provide a guideline for subsequent work.

PDF Details DOI

JBHI Journal 2024 Journal Article

Self-Supervised Medical Image Denoising Based on WISTA-Net for Human Healthcare in Metaverse

Huakun Huang
Chaoran Zhang
Lingjun Zhao
Shuxue Ding
Hanpin Wang
Huijun Wu

Medical image processing plays an important role in the interaction of real world and metaverse for healthcare. Self-supervised denoising based on sparse coding methods, without any prerequisite on large-scale training samples, has been attracting extensive attention for medical image processing. Whereas, existing self-supervised methods suffer from poor performance and low efficiency. In this paper, to achieve state-of-the-art denoising performance on the one hand, we present a self-supervised sparse coding method, named the weighted iterative shrinkage thresholding algorithm (WISTA). It does not rely on noisy-clean ground-truth image pairs to learn from only a single noisy image. On the other hand, to further improve denoising efficiency, we unfold the WISTA to construct a deep neural network (DNN) structured WISTA, named WISTA-Net. Specifically, in WISTA, motivated by the merit of the $l_{p}$ -norm, WISTA-Net has better denoising performance than the classical orthogonal matching pursuit (OMP) algorithm and the ISTA. Moreover, leveraging the high-efficiency of DNN structure in parameter updating, WISTA-Net outperforms the compared methods in denoising efficiency. In detail, for a 256 by 256 noisy image, the running time of WISTA-Net is 4. 72 s on the CPU, which is much faster than WISTA, OMP, and ISTA by 32. 88 s, 13. 06 s, and 6. 17 s, respectively.

Details DOI

AAAI Conference 2023 Conference Paper

Differentially Private Condorcet Voting

Zhechen Li
Ao Liu
Lirong Xia
Yongzhi Cao
Hanpin Wang

Designing private voting rules is an important and pressing problem for trustworthy democracy. In this paper, under the framework of differential privacy, we propose a novel famliy of randomized voting rules based on the well-known Condorcet method, and focus on three classes of voting rules in this family: Laplacian Condorcet method (CMLAP), exponential Condorcet method (CMEXP), and randomized response Condorcet method (CMRR), where λ represents the level of noise. We prove that all of our rules satisfy absolute monotonicity, lexi-participation, probabilistic Pareto efficiency, approximate probabilistic Condorcet criterion, and approximate SD-strategyproofness. In addition, CMRR satisfies (non-approximate) probabilistic Condorcet criterion, while CMLAP and CMEXP satisfy strong lexi-participation. Finally, we regard differential privacy as a voting axiom, and discuss its relations to other axioms.

PDF Details DOI

JAIR Journal 2023 Journal Article

Favoring Eagerness for Remaining Items: Designing Efficient, Fair, and Strategyproof Mechanisms

Xiaoxi Guo
Sujoy Sikdar
Lirong Xia
Yongzhi Cao
Hanpin Wang

In the assignment problem, the goal is to assign indivisible items to agents who have ordinal preferences, efficiently and fairly, in a strategyproof manner. In practice, first-choice maximality, i.e., assigning a maximal number of agents their top items, is often identified as an important efficiency criterion and measure of agents' satisfaction. In this paper, we propose a natural and intuitive efficiency property, favoring-eagerness-for-remaining-items (FERI), which requires that each item is allocated to an agent who ranks it highest among remaining items, thereby implying first-choice maximality. Using FERI as a heuristic, we design mechanisms that satisfy ex-post or ex-ante variants of FERI together with combinations of other desirable properties of efficiency (Pareto-efficiency), fairness (strong equal treatment of equals and sd-weak-envy-freeness), and strategyproofness (sd-weak-strategyproofness). We also explore the limits of FERI mechanisms in providing stronger efficiency, fairness, or strategyproofness guarantees through impossibility results.

PDF Details DOI

IJCAI Conference 2023 Conference Paper

First-Choice Maximality Meets Ex-ante and Ex-post Fairness

Xiaoxi Guo
Sujoy Sikdar
Lirong Xia
Yongzhi Cao
Hanpin Wang

For the assignment problem where multiple indivisible items are allocated to a group of agents given their ordinal preferences, we design randomized mechanisms that satisfy first-choice maximality (FCM), i. e. , maximizing the number of agents assigned their first choices, together with Pareto efficiency (PE). Our mechanisms also provide guarantees of ex-ante and ex-post fairness. The generalized eager Boston mechanism is ex-ante envy-free, and ex-post envy-free up to one item (EF1). The generalized probabilistic Boston mechanism is also ex-post EF1, and satisfies ex-ante efficiency instead of fairness. We also show that no strategyproof mechanism satisfies ex-post PE, EF1, and FCM simultaneously. In doing so, we expand the frontiers of simultaneously providing efficiency and both ex-ante and ex-post fairness guarantees for the assignment problem.

PDF Details DOI

AIJ Journal 2023 Journal Article

Multi resource allocation with partial preferences

Haibin Wang
Sujoy Sikdar
Xiaoxi Guo
Lirong Xia
Yongzhi Cao
Hanpin Wang

We provide efficient, fair, and non-manipulable mechanisms for the multi-type resource allocation problems (MTRAs) and multiple assignment problems where agents have partial preferences over bundles consisting of multiple divisible items. We uncover a natural reduction from multiple assignment problems to MTRAs, which preserves the properties of MTRA mechanisms. We extend the well-known random priority (RP) and probabilistic serial (PS) mechanisms to MTRAs with partial preferences as multi-type PS (MPS) and multi-type RP (MRP) and propose a new mechanism, multi-type general dictatorship (MGD), which combines the ideas of MPS and MRP. We show that for the unrestricted domain of partial order preferences, unfortunately, no mechanism satisfies both sd-efficiency and sd-envy-freeness, even as they each satisfy different weaker notions of the desirable properties of efficiency, fairness, and non-manipulability we consider. Notwithstanding this impossibility result, our main message is positive: When agents' preferences are represented by acyclic CP-nets, MRP satisfies ex-post-efficiency, sd-strategyproofness, and upper invariance, while MPS satisfies sd-efficiency, sd-envy-freeness, ordinal fairness, and upper invariance, recovering the properties of RP and PS; the MGD satisfies sd-efficiency, equal treatment of equals, and decomposability under the unrestricted domain of partial preferences. We introduce a natural domain of bundle net preferences, which generalizes previously studied domain restrictions of partial preferences for multiple assignment problems and is incomparable to the domain of acyclic CP-nets. We show that MRP and MPS satisfy all properties of the RP and PS under bundle net preferences as well.

Details DOI

TCS Journal 2022 Journal Article

An adaptation-complete proof system for local reasoning about cloud storage systems

Zhao Jin
Bowen Zhang
Lei Zhang
Yongzhi Cao
Hanpin Wang

The rapid growth of data presents a significant challenge to the capability of traditional storage technologies to collect and manage data. Cloud storage systems (CSSs) have been proposed as a method to improve storage capacity. To safely and effectively manage cloud storage data and improve data service quality, it is necessary to verify the correctness of CSS management programs. However, the complexity of these systems renders program verification difficult. In this paper, we propose a Hoare-style proof system, in conjunction with two languages, to analyze and verify CSS management programs. The first is a modeling language that describes the program execution. The second is an assertion language based on Separation Logic (SL), used to describe the properties of the CSS file-block-location storage structure. The proof system supports modular local reasoning for CSS programs by a set of adaptation rules, which enable the condition of specifications to be applied to broader contexts. A key question that arises is whether the proof system can meet adaptation completeness. If so, arbitrary satisfiable specifications can be adjusted using the adaptation rules. To this end, we developed local predicate transformers and used their domain to interpret all types of commands. By finding the smallest local predicate transformer, we established adaptation completeness. In summary, this work provides a formalization of automatic modular reasoning patterns and lays a theoretical foundation for the compositional program verification of CSSs.

Details DOI

AAMAS Conference 2022 Conference Paper

Designing Efficient and Fair Mechanisms for Multi-Type Resource Allocation

Xiaoxi Guo
Sujoy Sikdar
Haibin Wang
Lirong Xia
Yongzhi Cao
Hanpin Wang

In the multi-type resource allocation problem (MTRA), there are 𝑑 ≥ 2 types of items, and 𝑛 agents who each demand one unit of items of each type and have strict linear preferences over bundles consisting of one item of each type. For MTRAs with indivisible items, we first present an impossibility result that no mechanism can satisfy both sd-efficiency and sd-envy-freeness. We show that this impossibility result is circumvented under the natural assumption of lexicographic preferences by providing lexicographic probabilistic serial (LexiPS) as an extension of the probabilistic serial (PS) mechanism. We also prove that LexiPS satisfies sd-efficiency and sd-envy-freeness. Moreover, LexiPS satisfies sd-weak-strategy proofness when agents are not allowed to misreport their importance orders. The multi-type probabilistic serial cannot deal with indivisible items, but provides a stronger efficiency guarantee under the unrestricted domain of strict linear preferences for divisible items, while also retaining desirable fairness guarantees.

PDF

IJCAI Conference 2022 Conference Paper

Learning First-Order Rules with Differentiable Logic Program Semantics

Kun Gao
Katsumi Inoue
Yongzhi Cao
Hanpin Wang

Learning first-order logic programs (LPs) from relational facts which yields intuitive insights into the data is a challenging topic in neuro-symbolic research. We introduce a novel differentiable inductive logic programming (ILP) model, called differentiable first-order rule learner (DFOL), which finds the correct LPs from relational facts by searching for the interpretable matrix representations of LPs. These interpretable matrices are deemed as trainable tensors in neural networks (NNs). The NNs are devised according to the differentiable semantics of LPs. Specifically, we first adopt a novel propositionalization method that transfers facts to NN-readable vector pairs representing interpretation pairs. We replace the immediate consequence operator with NN constraint functions consisting of algebraic operations and a sigmoid-like activation function. We map the symbolic forward-chained format of LPs into NN constraint functions consisting of operations between subsymbolic vector representations of atoms. By applying gradient descent, the trained well parameters of NNs can be decoded into precise symbolic LPs in forward-chained logic format. We demonstrate that DFOL can perform on several standard ILP datasets, knowledge bases, and probabilistic relation facts and outperform several well-known differentiable ILP models. Experimental results indicate that DFOL is a precise, robust, scalable, and computationally cheap differentiable ILP model.

PDF Details DOI

TCS Journal 2022 Journal Article

Reasoning about block-based cloud storage systems via separation logic

Zhao Jin
Bowen Zhang
Tianyue Cao
Yongzhi Cao
Hanpin Wang

Owing to the massive growth in the storage demands of big data, cloud storage systems emerge at a historic moment, among which block-based cloud storage systems (BCSSs) are typical. Compared with traditional storage systems, BCSSs have many advantages, such as higher capacity, lower cost, and better scalability. BCSSs are also much more complex and error prone than traditional systems, and therefore, their reliability is a significant concern. Correctness is the most basic requirement for reliability. Therefore, it is of great significance to study BCSS program correctness verification to establish the theoretical basis for cloud storage systems. In this paper, we propose a novel framework based on separation logic (SL) to verify the correctness of BCSS management programs. We first construct a two-tier heap structure as the formal model of the storage architecture for BCSSs and present a modelling language based on this structure to describe the program execution. We then define assertion pairs to describe the properties of the two-tier structure. The two components of an assertion pair affect each other, producing several interesting properties. Finally, we propose a Hoare-style proof system to reason about BCSS programs and establish its soundness. We also demonstrate our proof system's uniqueness, usability, and scalability by verifying several real-world BCSS sample programs. In summary, this work presents a systematic approach that can be used to effectively solve BCSS program verification problems, and provides an SL-based logical modelling strategy, specifically to build its consistency with the actual behaviour of BCSSs.

Details DOI

TCS Journal 2022 Journal Article

Zero-freeness and approximation of real Boolean Holant problems

Zonglei Bai
Yongzhi Cao
Hanpin Wang

Holant problems provide a novel framework to study the complexity of counting problems. It is a refinement to counting constraint satisfaction problems (#CSP) with a more explicit role for the constraint functions. Both graph homomorphisms and #CSP can be viewed as special cases of Holant problems. For approximation algorithms on Holant problems, the attention is focused on proving zero-freeness of the partition functions and establishing fully polynomial-time approximation schemes (FPTAS) using the Taylor expansion method. In this paper, we study the Holant problems defined by a real constraint function satisfying a generalized second-order recurrence. We present fully polynomial-time (deterministic or randomized) approximation schemes for the Holant problems except for a couple of cases. Our algorithms are established in two ways: 1) we construct holographic transformations from the Holant problems to the Ising model, and obtain the algorithms using the approaches with respect to the Ising model; 2) we prove the zero-freeness of the Holant problems, and present an algorithm based on the Taylor expansion method. In addition, for most of the other cases, there exist approximation-preserving reductions between the Holant problems and the problem of counting perfect matchings, which is a central open problem in approximate counting.

Details DOI

JAAMAS Journal 2021 Journal Article

Probabilistic serial mechanism for multi-type resource allocation

Xiaoxi Guo
Sujoy Sikdar
Hanpin Wang

Abstract In multi-type resource allocation (MTRA) problems, there are $d\ge 2$ types of items, and n agents who each demand one unit of items of each type and have strict linear preferences over bundles consisting of one item of each type. For MTRAs with indivisible items, our first result is an impossibility theorem that is in direct contrast to the single type ( $d=1$ ) setting: no mechanism, the output of which is always decomposable into a probability distribution over discrete assignments (where no item is split between agents), can satisfy both sd-efficiency and sd-envy-freeness. We show that this impossibility result is circumvented under the natural assumption of lexicographic preferences. We provide lexicographic probabilistic serial (LexiPS) as an extension of the probabilistic serial (PS) mechanism for MTRAs with lexicographic preferences, and prove that LexiPS satisfies sd-efficiency and sd-envy-freeness, retaining the desirable properties of PS. Moreover, LexiPS satisfies sd-weak-strategyproofness when agents are not allowed to misreport their importance orders. For MTRAs with divisible items, we show that the existing multi-type probabilistic serial (MPS) mechanism satisfies the stronger efficiency notion of lexi-efficiency, and is sd-envy-free under strict linear preferences and sd-weak-strategyproof under lexicographic preferences. We also prove that MPS can be characterized both by leximin-optimality and by item-wise ordinal fairness, and the family of eating algorithms which MPS belongs to can be characterized by lexi-efficiency.

Details DOI

AAAI Conference 2020 Conference Paper

Multi-Type Resource Allocation with Partial Preferences

Haibin Wang
Sujoy Sikdar
Xiaoxi Guo
Lirong Xia
Yongzhi Cao
Hanpin Wang

We propose multi-type probabilistic serial (MPS) and multitype random priority (MRP) as extensions of the well-known PS and RP mechanisms to the multi-type resource allocation problems (MTRAs) with partial preferences. In our setting, there are multiple types of divisible items, and a group of agents who have partial order preferences over bundles consisting of one item of each type. We show that for the unrestricted domain of partial order preferences, no mechanism satisﬁes both sd-efﬁciency and sd-envy-freeness. Notwithstanding this impossibility result, our main message is positive: When agents’ preferences are represented by acyclic CPnets, MPS satisﬁes sd-efﬁciency, sd-envy-freeness, ordinal fairness, and upper invariance, while MRP satisﬁes ex-postefﬁciency, sd-strategyproofness, and upper invariance, recovering the properties of PS and RP. Besides, we propose a hybrid mechanism, multi-type general dictatorship (MGD), combining the ideas of MPS and MRP, which satisﬁes sd-efﬁciency, equal treatment of equals and decomposability under the unrestricted domain of partial order preferences.

PDF Details

I&C Journal 2017 Journal Article

Differential privacy in probabilistic systems

Jiannan Yang
Yongzhi Cao
Hanpin Wang

Ever since proposed by Dwork, differential privacy has been a hot topic in academia. However, few attempts have been made on reasoning about differential privacy at a system level. In this paper, we propose a formal framework to verify differential privacy in probabilistic systems. With a metric on the states of a system, we formalize differential privacy by the ratio of the probabilities in the distributions after the same labeled transitions of relevant states. We explain how traditional differential privacy can be embedded in our framework and raise an infimum metric, the least distance between two states, while not violating differential privacy. It is proven that the infimum metric is also a metric instance of differential privacy itself. Furthermore, we propose a two-level logic, a privacy variant of the familiar Hennessy–Milner logic, to characterize differential privacy in our framework. Our results have close relations to probabilistic bisimilarity as well.

Details DOI

TCS Journal 2012 Journal Article

Value-passing CCS with noisy channels

Shuqin Huang
Yongzhi Cao
Hanpin Wang
Wanling Qu

Value-passing CCS, a full version of Milner’s CCS, is a process algebra in which actions consist of sending and receiving values through noiseless communication channels. The full calculus is a succinct yet expressive language for the specification and verification of reactive systems. Taking into account the reality of channel noise in reactive systems, in this paper we introduce an extension of value-passing CCS, called value-passing CCS with noisy channels (VCCS N ), in which noise is described by a probability distribution over the values. After presenting the reduction operational semantics and labelled operational semantics of VCCS N, we develop the theory of behavioural equivalence by introducing barbed equivalence, barbed congruence, bisimilarity, and full bisimilarity. In particular, we show that barbed equivalence and barbed congruence coincide with bisimilarity and full bisimilarity, respectively. Based upon the labelled operational semantics of VCCS N, we establish a probabilistic modal logic for expressing system properties and show its connection with the notion of bisimilarity. Finally, we use VCCS N to model a communication protocol for ensuring the reliable transmission of data across an error-prone channel.

Details DOI

TCS Journal 2009 Journal Article

Approximation algorithm for maximum edge coloring

Wangsen Feng
Li’ang Zhang
Hanpin Wang

We propose a polynomial time approximation algorithm for a novel maximum edge coloring problem which arises from wireless mesh networks [Ashish Raniwala, Tzi-cker Chiueh, Architecture and algorithms for an IEEE 802. 11-based multi-channel wireless mesh network, in: INFOCOM 2005, pp. 2223–2234; Ashish Raniwala, Kartik Gopalan, Tzi-cker Chiueh, Centralized channel assignment and routing algorithms for multi-channel wireless mesh networks, Mobile Comput. Commun. Rev. 8 (2) (2004) 50–65]. The problem is to color all the edges in a graph with maximum number of colors under the following q -Constraint: for every vertex in the graph, all the edges incident to it are colored with no more than q ( q ∈ Z, q ≥ 2 ) colors. We show that the algorithm is a 2-approximation for the case q = 2 and a ( 1 + 4 q − 2 3 q 2 − 5 q + 2 ) -approximation for the case q > 2 respectively. The case q = 2 is of great importance in practice. For complete graphs and trees, polynomial time accurate algorithms are found for them when q = 2. The approximation algorithm gives a feasible solution to channel assignment in multi-channel wireless mesh networks.

Details DOI

CSL Conference 2009 Conference Paper

On Model Checking Boolean BI

Heng Guo 0001
Hanpin Wang
Zhongyuan Xu
Yongzhi Cao

Abstract The logic of bunched implications (BI), introduced by O’Hearn and Pym, is a substructural logic which freely combines additive and multiplicative implications. Boolean BI (BBI) denotes BI with classical interpretation of additives and its model is the commutative monoid. We show that when the monoid is finitely generated and propositions are recursively defined, or the monoid is infinitely generated and propositions are restricted to generator propositions, the model checking problem is undecidable. In the case of finitely related monoid and generator propositions, the model checking problem is EXPSPACE-complete.

Details