Jialiang Sun

Toronto, Canada

I am a Ph.D. student in Computer Science at the University of Toronto, supervised by Prof. Kuldeep Meel. I previously completed my Honours Bachelor of Science at the University of Toronto, majoring in Computer Science with minors in Mathematics and Statistics.

My research focuses on automated reasoning at the intersection of AI and formal methods. I combine symbolic methods with large language models to develop neurosymbolic frameworks for automated theorem proving, autoformalization, and constrained generation.

My long-term goal is to automate research-level discovery in mathematics and theoretical computer science without human intervention.

Publications · Curriculum vitae · Email

publications

* Equal contribution. † Equal advising. Click a figure to enlarge.

DreamProver wake-sleep cycle: theorem discovery, lemma abstraction, and library updates.

DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent

Youyuan Zhang^*, Jialiang Sun^*, Hangrui Bi, Chuqin Geng, Wenjie Ma, Zhaoyu Li^†, and Xujie Si^†

In Conference on Language Modeling, 2026

Paper BibTeX

@inproceedings{zhang2026dreamprover,
  title = {{DreamProver}: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent},
  author = {Zhang, Youyuan and Sun, Jialiang and Bi, Hangrui and Geng, Chuqin and Ma, Wenjie and Li, Zhaoyu and Si, Xujie},
  booktitle = {Conference on Language Modeling},
  year = {2026},
}

Two Lean proofs for the same answer-construction problem, contrasting an admissible numeral with an inadmissible circular answer.

Formally Solving Answer-Construction Problems in Lean

Jialiang Sun, Yuzhi Tang, Ao Li, Chris J. Maddison, and Kuldeep S. Meel

In International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2026

Paper BibTeX Code

@inproceedings{sun2026answerconstruction,
  title = {Formally Solving Answer-Construction Problems in {Lean}},
  author = {Sun, Jialiang and Tang, Yuzhi and Li, Ao and Maddison, Chris J. and Meel, Kuldeep S.},
  booktitle = {International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
  year = {2026},
}

PyEuclid architecture connecting geometric inputs, deductive and algebraic reasoning, and generated proofs.

PyEuclid: A Versatile Formal Plane Geometry System in Python

Zhaoyu Li^*, Hangrui Bi^*, Jialiang Sun^*, Zenan Li, Kaiyu Yang, and Xujie Si

In International Conference on Computer Aided Verification, 2025

Paper BibTeX Code

@inproceedings{li2025pyeuclid,
  title = {{PyEuclid}: A Versatile Formal Plane Geometry System in {Python}},
  author = {Li, Zhaoyu and Bi, Hangrui and Sun, Jialiang and Li, Zenan and Yang, Kaiyu and Si, Xujie},
  booktitle = {International Conference on Computer Aided Verification},
  year = {2025},
  doi = {10.1007/978-3-031-98685-7_20},
}

A Lean proof tree branching into subgoals, with successful branches marked by green checks.

A Survey on Deep Learning for Theorem Proving

Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si

In Conference on Language Modeling, 2024

Paper BibTeX Code

@inproceedings{li2024survey,
  title = {A Survey on Deep Learning for Theorem Proving},
  author = {Li, Zhaoyu and Sun, Jialiang and Murphy, Logan and Su, Qidong and Li, Zenan and Zhang, Xian and Yang, Kaiyu and Si, Xujie},
  booktitle = {Conference on Language Modeling},
  year = {2024},
}

Euclidean geometry translated into Lean theorems and proofs, with SMT solvers checking equivalence and filling reasoning gaps.

Autoformalizing Euclidean Geometry

Logan Murphy^*, Kaiyu Yang^*, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si

In International Conference on Machine Learning, 2024

Paper BibTeX Code

@inproceedings{murphy2024autoformalizing,
  title = {Autoformalizing Euclidean Geometry},
  author = {Murphy, Logan and Yang, Kaiyu and Sun, Jialiang and Li, Zhaoyu and Anandkumar, Anima and Si, Xujie},
  booktitle = {International Conference on Machine Learning},
  year = {2024},
}

SAT-RL training workflow: synthetic data and supervised fine-tuning followed by reinforcement learning with symbolic-solver rewards.

SAT-RL: Training Language Models for Logic Reasoning with Symbolic Solvers

Jialiang Sun and Kuldeep Meel

2026

Under review, ACL ARR August 2026

Paper BibTeX

@unpublished{sun2026satrl,
  title = {{SAT-RL}: Training Language Models for Logic Reasoning with Symbolic Solvers},
  author = {Sun, Jialiang and Meel, Kuldeep},
  year = {2026},
  note = {Under review, ACL ARR August 2026},
}

Unrolled NFA for length four, showing layered states and colored paths converging on the accepting state.

Provably Tractable NFA Constrained Language Generation

Jialiang Sun and Kuldeep Meel

2026

Under review, ACL ARR August 2026

Paper BibTeX

@unpublished{sun2026nfa,
  title = {Provably Tractable {NFA} Constrained Language Generation},
  author = {Sun, Jialiang and Meel, Kuldeep},
  year = {2026},
  note = {Under review, ACL ARR August 2026},
}