Publications

  • PyEuclid: A Versatile Formal Plane Geometry System in Python
    Zhaoyu Li*, Hangrui Bi*, Jianliang Sun*, Zenan Li, Kaiyu Yang, Xujie Si
    CAV 2025

  • TypyBench: Evaluating LLM Type Inference for Untyped Python Repositories
    Honghua Dong, Jiacheng Yang, Xun Deng, Yuhe Jiang, Gennady Pekhimenko, Fan Long, Xujie Si
    ICML 2025

  • APPL: A Prompt Programming Language for Harmonious Integration of Programs and Large Language Model Prompts
    Honghua Dong*, Qidong Su*, Yubo Gao, Zhaoyu Li, Yangjun Ruan, Gennady Pekhimenko, Chris J. Maddison, Xujie Si
    ACL 2025

  • Understanding Behavioral Metric Learning in Deep RL: A Large-Scale Study on Distracting Environments
    Ziyan (Ray) Luo, Tianwei Ni, Pierre-Luc Bacon, Doina Precup, Xujie Si
    RLC 2025

  • Decoupling Training-Free Guided Diffusion by ADMM
    Youyuan Zhang, Zehua Liu, Zenan Li, Zhaoyu Li, James J. Clark, Xujie Si
    CVPR 2025

  • Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning
    Zenan Li*, Zhaoyu Li*, Wen Tang, Xian Zhang, Yuan Yao, Xujie Si, Fan Yang, Kaiyu Yang, Xiaoxing Ma
    ICLR 2025

  • LogiCity: Advancing Neuro-Symbolic AI with Abstract Urban Simulation
    Bowen Li, Zhaoyu Li, Qiwei Du, Jinqi Luo, Wenshan Wang, Yaqi Xie, Simon Stepputtis, Chen Wang, Katia P. Sycara, Pradeep Kumar Ravikumar, Alexander G. Gray, Xujie Si, Sebastian Scherer
    NeurIPS 2024

  • Code Repair with LLMs gives an Exploration-Exploitation Tradeoff
    Hao Tang, Keya Hu, Jin Peng Zhou, Sicheng Zhong, Wei-Long Zheng, Xujie Si, Kevin Ellis
    NeurIPS 2024

  • Modernizing SMT-Based Type Error Localization
    Max Kopinsky, Brigitte Pientka and Xujie Si
    FMCAD 2024

  • Chronosymbolic: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning
    Ziyan Luo and Xujie Si
    The 7th International Symposium on AI Verification (SAIV), 2024

  • A Survey on Deep Learning for Theorem Proving
    Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, Xujie Si
    COLM 2024

  • Autoformalizing Euclidean Geometry
    Logan Murphy*, Kaiyu Yang*, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, Xujie Si
    ICML 2024

  • G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks
    Zhaoyu Li, Jinpei Guo, Xujie Si
    Transactions on Machine Learning Research (TMLR) 2024

  • Learning Reliable Logical Rules with SATNet
    Zhaoyu Li, Jinpei Guo, Yuhe Jiang, Xujie Si
    NeurIPS 2023

  • Towards Reliable Neural Specifications
    Chuqin Geng, Nham Le, Xiaojie Xu, Zhaoyue Wang, Arie Gurfinkel, Xujie Si
    ICML 2023 (Oral) [slides, talk recording]

  • TorchProbe: Fuzzing Dynamic Deep Learning Compilers
    Qidong Su, Chuqin Geng, Gennady Pekhimenko, Xujie Si
    APLAS 2023

  • Identifying different student clusters in functional programming assignments: From quick learners to struggling students.
    Chuqin Geng, Wenwen Xu, Yingjie Xu, Brigitte Pientka, Xujie Si
    SIGCSE'23: The 54th ACM Technical Symposium on Computer Science Education

  • NSNet: A General Neural Probabilistic Framework for Satisfiability Problems.
    Zhaoyu Li, Xujie Si
    NeurIPS 2022

  • Novice Type Error Diagnosis with Natural Language Models.
    Chuqin Geng, Haolin Ye, Yixuan Li, Tianyu Han, Brigitte Pientka, Xujie Si
    APLAS 2022

  • Techniques for Symbol Grounding with SATNet.
    Sever Topan, David Rolnick, Xujie Si
    NeurIPS 2021 [paper, slides, artifact]
    Spotlight

  • Scallop: From Probabilistic Deductive Databases to Scalable Differentiable Reasoning.
    Jiani Huang, Ziyang Li, Binghong Chen, Karan Samel, Mayur Naik, Le Song, Xujie Si
    NeurIPS 2021 [paper, code]

  • Data-driven Optimization of Inductive Generalization.
    Nham Le, Xujie Si, Arie Gurfinkel
    FMCAD 2021 [paper, slides, artifact]

  • Code2Inv: A Deep Learning Framework for Program Verification.
    Xujie Si, Aaditya Naik, Hanjun Dai, Mayur Naik, Le Song
    CAV 2020 [paper, slides, artifact, demo]

  • Synthesizing Datalog Programs using Numerical Relaxation.
    Xujie Si, Mukund Raghothaman, Kihong Heo, Mayur Naik
    IJCAI 2019 [paper, slides, poster, artifact]

  • Learning a Meta-Solver for Syntax-Guided Program Synthesis.
    Xujie Si, Yuan Yang, Hanjun Dai, Mayur Naik, Le Song
    ICLR 2019 [paper, poster, artifact]

  • Continuously Reasoning about Programs via Differential Bayesian Inference.
    Kihong Heo, Mukund Raghothaman, Xujie Si, Mayur Naik
    PLDI 2019 [paper, slides, artifact, video abstract]
    ACM SIGPLAN Distinguished Paper Award

  • Syntax-Guided Synthesis of Datalog Programs.
    Xujie Si, Woosuk Lee, Richard Zhang, Aws Albarghouthi, Paris Koutris, Mayur Naik
    FSE 2018 [paper, slides, artifact]

  • Learning Loop Invariants for Program Verification.
    Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, Le Song
    NeurIPS 2018 [paper, slides, poster, artifact, video abstract]
    Spotlight

  • Maximum Satisfiability in Software Analysis: Applications and Techniques
    Mayur Naik, Xujie Si, Xin Zhang, Radu Grigore
    VMCAI Invited Tutorial 2018 [abstract, slides]

  • Effective Interactive Resolution of Static Analysis Alarms
    Xin Zhang, Radu Grigore, Xujie Si, Mayur Naik
    OOPSLA 2017 [paper]

  • Maximum Satisfiability in Software Analysis: Applications and Techniques
    Xujie Si, Xin Zhang, Radu Grigore, Mayur Naik
    CAV 2017 [paper, slides]
    Invited Tutorial

  • APISan: Sanitizing API Usages through Semantic Cross-checking
    Insu Yun, Changwoo Min, Xujie Si, Yeongjin Jang, Taesoo Kim, Mayur Naik
    USENIX Security 2016 [paper, slides, code]
    CSAW Best Applied Research Paper Finalist

  • On Incremental Core-Guided MaxSAT Solving
    Xujie Si, Xin Zhang, Vasco Manquinho, Mikolas Janota, Alexey Ignatiev, Mayur Naik
    CP 2016 [paper, slides, code]

Workshop