93 citations · 212 across the 24 of their papers we have counts for
25 papers
Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning
Ji Feng, Zhouxing Shi
With large language models (LLMs) increasingly applied to mathematical reasoning, formal proof assistants such as Lean can be leveraged to verify reasoning outputs with machine-che…
Evaluating the Robustness of Proof Autoformalization in Lean 4
Zhengtao Gui, Sheng Yang, Zhouxing Shi
Proof autoformalization aims to translate a mathematical informal proof in natural language into a formal proof in a formal language such as Lean 4. Existing LLM-based models for p…
GRLO: Towards Generalizable Reinforcement Learning in Open-Ended Environments from Zero
Shangjian Yin, Yu Fu, Yue Dong +1
Post-training has become a crucial step for unlocking the capabilities of large language models, with reinforcement learning (RL) emerging as a critical paradigm. Recent RL-based p…
Talking with Verifiers: Automatic Specification Generation for Neural Network Verification
Yizhak Y. Elboher, Reuven Peleg, Zhouxing Shi +2
Neural network verification tools currently support only a narrow class of specifications, typically expressed as low-level constraints over raw inputs and outputs. This limitation…
PII-VisBench: Evaluating Personally Identifiable Information Safety in Vision Language Models Along a Continuum of Visibility
G M Shahariar, Zabir Al Nazi, Md Olid Hasan Bhuiyan +1
Vision Language Models (VLMs) are increasingly integrated into privacy-critical domains, yet existing evaluations of personally identifiable information (PII) leakage largely treat…
Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits
Yizhak Yisrael Elboher, Avraham Raviv, Amihay Elboher +4
Ensuring the safety and efficiency of AI systems is a central goal of modern research. Formal verification provides guarantees of neural network robustness, while early exits impro…
PIKA: Expert-Level Synthetic Datasets for Post-Training Alignment from Scratch
Shangjian Yin, Shining Liang, Wenbiao Ding +4
High-quality instruction data is critical for LLM alignment, yet existing open-source datasets often lack efficiency, requiring hundreds of thousands of examples to approach propri…
SoundnessBench: A Soundness Benchmark for Neural Network Verifiers
Xingjian Zhou, Keyi Shen, Andy Xu +4
Neural network (NN) verification aims to formally verify properties of NNs, which is crucial for ensuring the behavior of NN-based models in safety-critical applications. In recent…
Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control
Zhouxing Shi, Haoyu Li, Cho-Jui Hsieh +1
We study the problem of learning verifiably Lyapunov-stable neural controllers that provably satisfy the Lyapunov asymptotic stability condition within a region-of-attraction (ROA)…
Neural Network Verification with Branch-and-Bound for General Nonlinearities
Zhouxing Shi, Qirui Jin, Zico Kolter +3
Branch-and-bound (BaB) is among the most effective techniques for neural network (NN) verification. However, existing works on BaB for NN verification have mostly focused on NNs wi…
Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation
Lujie Yang, Hongkai Dai, Zhouxing Shi +3
Learning-based neural network (NN) control policies have shown impressive empirical performance in a wide range of tasks in robotics and control. However, formal (Lyapunov) stabili…
Defending LLMs against Jailbreaking Attacks via Backtranslation
Yihan Wang, Zhouxing Shi, Andrew Bai +1
Although many large language models (LLMs) have been trained to refuse harmful requests, they are still vulnerable to jailbreaking attacks which rewrite the original prompt to conc…
Improving the Generation Quality of Watermarked Large Language Models via Word Importance Scoring
Yuhang Li, Yihan Wang, Zhouxing Shi +1
The strong general capabilities of Large Language Models (LLMs) bring potential ethical risks if they are unrestrictedly accessible to malicious users. Token-level watermarking ins…
Red Teaming Language Model Detectors with Language Models
Zhouxing Shi, Yihan Wang, Fan Yin +3
The prevalence and strong capability of large language models (LLMs) present significant safety and ethical risks if exploited by malicious users. To prevent the potentially decept…
Effective Robustness against Natural Distribution Shifts for Models with Different Training Data
Zhouxing Shi, Nicholas Carlini, Ananth Balashankar +4
"Effective robustness" measures the extra out-of-distribution (OOD) robustness beyond what can be predicted from the in-distribution (ID) performance. Existing effective robustness…
Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagation
Zhouxing Shi, Yihan Wang, Huan Zhang +2
Lipschitz constants are connected to many properties of neural networks, such as robustness, fairness, and generalization. Existing methods for computing Lipschitz constants either…
On the Convergence of Certified Robust Training with Interval Bound Propagation
Yihan Wang, Zhouxing Shi, Quanquan Gu +1
Interval Bound Propagation (IBP) is so far the base of state-of-the-art methods for training neural networks with certifiable robustness guarantees when potential adversarial pertu…
On the Sensitivity and Stability of Model Interpretations in NLP
Fan Yin, Zhouxing Shi, Cho-Jui Hsieh +1
Recent years have witnessed the emergence of a variety of post-hoc interpretations that aim to uncover how natural language processing (NLP) models make predictions. Despite the su…
Fast Certified Robust Training with Short Warmup
Zhouxing Shi, Yihan Wang, Huan Zhang +2
Recently, bound propagation based certified robust training methods have been proposed for training neural networks with certifiable robustness guarantees. Despite that state-of-th…
On the Adversarial Robustness of Vision Transformers
Rulin Shao, Zhouxing Shi, Jinfeng Yi +2
Following the success in advancing natural language processing and understanding, transformers are expected to bring revolutionary changes to computer vision. This work provides a…
Robust Text CAPTCHAs Using Adversarial Examples
Rulin Shao, Zhouxing Shi, Jinfeng Yi +2
CAPTCHA (Completely Automated Public Truing test to tell Computers and Humans Apart) is a widely used technology to distinguish real users and automated users such as bots. However…
Knowledge-Aided Open-Domain Question Answering
Mantong Zhou, Zhouxing Shi, Minlie Huang +1
Open-domain question answering (QA) aims to find the answer to a question from a large collection of documents.Though many models for single-document machine comprehension have ach…
Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond
Kaidi Xu, Zhouxing Shi, Huan Zhang +6
Linear relaxation based perturbation analysis (LiRPA) for neural networks, which computes provable linear bounds of output neurons given a certain amount of input perturbation, has…
Robustness Verification for Transformers
Zhouxing Shi, Huan Zhang, Kai-Wei Chang +2
Robustness verification that aims to formally certify the prediction behavior of neural networks has become an important tool for understanding model behavior and obtaining safety…