Xujie Si

2024-03-04

ICLR.cc/2024/Workshop/SeT_LLM (published)

G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks

Zhaoyu Li

Jinpei Guo

Graph neural networks (GNNs) have recently emerged as a promising approach for solving the Boolean Satisfiability Problem (SAT), offering po… (see more)tential alternatives to traditional backtracking or local search SAT solvers. However, despite the growing volume of literature in this field, there remains a notable absence of a unified dataset and a fair benchmark to evaluate and compare existing approaches. To address this crucial gap, we present G4SATBench, the first benchmark study that establishes a comprehensive evaluation framework for GNN-based SAT solvers. In G4SATBench, we meticulously curate a large and diverse set of SAT datasets comprising 7 problems with 3 difficulty levels and benchmark a broad range of GNN models across various prediction tasks, training objectives, and inference algorithms. To explore the learning abilities and comprehend the strengths and limitations of GNN-based SAT solvers, we also compare their solving processes with the heuristics in search-based SAT solvers. Our empirical results provide valuable insights into the performance of GNN-based SAT solvers and further suggest that existing GNN models can effectively learn a solving strategy akin to greedy local search but struggle to learn backtracking search in the latent space.

2024-01-01

ICLR.cc/2024/Conference/Rejected_Submission (rejected)

Scalar Invariant Networks with Zero Bias

Chuqin Geng

Xiaojie Xu

Haolin Ye

Just like weights, bias terms are the learnable parameters of many popular machine learning models, including neural networks. Biases are th… (see more)ought to enhance the representational power of neural networks, enabling them to solve a variety of tasks in computer vision. However, we argue that biases can be disregarded for some image-related tasks such as image classification, by considering the intrinsic distribution of images in the input space and desired model properties from first principles. Our findings suggest that zero-bias neural networks can perform comparably to biased networks for practical image classification tasks. We demonstrate that zero-bias neural networks possess a valuable property called scalar (multiplication) invariance. This means that the prediction of the network remains unchanged when the contrast of the input image is altered. We extend scalar invariance to more general cases, enabling formal verification of certain convex regions of the input space. Additionally, we prove that zero-bias neural networks are fair in predicting the zero image. Unlike state-of-the-art models that may exhibit bias toward certain labels, zero-bias networks have uniform belief in all labels. We believe dropping bias terms can be considered as a geometric prior in designing neural network architecture for image classification, which shares the spirit of adapting convolutions as the transnational invariance prior. The robustness and fairness advantages of zero-bias neural networks may also indicate a promising path towards trustworthy and ethical AI.

2023-11-28

NeurIPS.cc/2023/Workshop/NeurReps (poster)

TorchProbe: Fuzzing Dynamic Deep Learning Compilers

Qidong Su

Chuqin Geng

Gennady G. Pekhimenko

Static and dynamic computational graphs represent two distinct approaches to constructing deep learning frameworks. The former prioritizes c… (see more)ompiler-based optimizations, while the latter focuses on programmability and user-friendliness. The recent release of PyTorch 2.0, which supports compiling arbitrary deep learning programs in Python, signifies a new direction in the evolution of deep learning infrastructure to incorporate compiler techniques in a more dynamic manner and support more dynamic language features like dynamic control flows and closures. Given PyTorch's seamless integration with Python, its compiler aims to support arbitrary deep learning code written in Python. However, the inherent dynamism of Python poses challenges to the completeness and robustness of the compiler. While recent research has introduced fuzzing to test deep learning compilers, there is still a lack of comprehensive analysis on how to test dynamic features. To address this issue, we propose several code transformations to generate test cases involving dynamic features. These transformations preserve the program's semantics, ensuring that any discrepancy between the transformed and original programs indicates the presence of a bug. Through our approach, we have successfully identified twenty previously unknown bugs in the PyTorch compiler and its underlying tensor compiler Triton.

2023-10-30

ArXiv (preprint)

Learning Reliable Logical Rules with SATNet

Zhaoyu Li

Jinpei Guo

Yuhe Jiang

2023-10-03

ArXiv (preprint)

G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks

Zhaoyu Li

Jinpei Guo

2023-09-29

ArXiv (preprint)

Learning Reliable Logical Rules with SATNet

Zhaoyu Li

Jinpei Guo

Yuhe Jiang

Idiolect: A Reconfigurable Voice Coding Assistant

Breandan Considine

Nicholas Albion

This paper presents Idiolect, an open source 1 IDE plugin for voice coding and a novel approach to building bots that allows for users to de… (see more)fine custom commands on-the-fly. Unlike traditional chatbots, Idiolect does not pretend to be an omniscient virtual assistant but rather a reconfigurable voice programming system that empowers users to create their own commands and actions dynamically, without rebuilding or restarting the application. We offer an experience report describing the tool itself, illustrate some example use cases, and reflect on several lessons learned during the tool’s development.

2023-05-20

2023 IEEE/ACM 5th International Workshop on Bots in Software Engineering (BotSE) (published)

Can ChatGPT Pass An Introductory Level Functional Language Programming Course?

Chuqin Geng

Yihan Zhang

Brigitte Pientka

The recent introduction of ChatGPT has drawn significant attention from both industry and academia due to its impressive capabilities in sol… (see more)ving a diverse range of tasks, including language translation, text summarization, and computer programming. Its capability for writing, modifying, and even correcting code together with its ease of use and access is already dramatically impacting computer science education. This paper aims to explore how well ChatGPT can perform in an introductory-level functional language programming course. In our systematic evaluation, we treated ChatGPT as one of our students and demonstrated that it can achieve a grade B- and its rank in the class is 155 out of 314 students overall. Our comprehensive evaluation provides valuable insights into ChatGPT's impact from both student and instructor perspectives. Additionally, we identify several potential benefits that ChatGPT can offer to both groups. Overall, we believe that this study significantly clarifies and advances our understanding of ChatGPT's capabilities and potential impact on computer science education.

2023-04-29

ArXiv (preprint)

Identifying Different Student Clusters in Functional Programming Assignments: From Quick Learners to Struggling Students

Chuqin Geng

Wenwen Xu

Yingjie Xu

Brigitte Pientka

Instructors and students alike are often focused on the grade in programming assignments as a key measure of how well a student is mastering… (see more) the material and whether a student is struggling. This can be, however, misleading. Especially when students have access to auto-graders, their grades may be heavily skewed. In this paper, we analyze student assignment submission data collected from a functional programming course taught at McGill university incorporating a wide range of features. In addition to the grade, we consider activity time data, time spent, and the number of static errors. This allows us to identify four clusters of students: "Quick-learning", "Hardworking", "Satisficing", and "Struggling" through cluster algorithms. We then analyze how work habits, working duration, the range of errors, and the ability to fix errors impact different clusters of students. This structured analysis provides valuable insights for instructors to actively help different types of students and emphasize different aspects of their overall course design. It also provides insights for students themselves to understand which aspects they still struggle with and allows them to seek clarification and adjust their work habits.

2023-03-03

Proceedings of the 54th ACM Technical Symposium on Computer Science Education V. 1 (published)

Towards Reliable Neural Specifications

Chuqin Geng

Nham Le

Xiaojie Xu

Zhaoyue Wang

Arie Gurfinkel

2023-01-01

ICML (published)

proceedings.mlr.press

Towards Reliable Neural Specifications

Chuqin Geng

Nham Le

Xiaojie Xu

Zhaoyue Wang

Arie Gurfinkel

2023-01-01

ICML (published)