8 citations · 8 across the 3 of their papers we have counts for
5 papers
SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers
Jialiang Sun, Kuldeep Meel
Large language models (LLMs) have achieved strong performance in mathematical and logical reasoning, yet they still suffer from the curse of complexity and struggle as problem diff…
Provably Tractable NFA-Constrained Language Generation via HMMs
Jialiang Sun, Kuldeep Meel
Constrained generation aims to sample from language models (LMs) conditioned on hard constraints. Existing constrained-generation techniques for nondeterministic finite automaton (…
DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent
Youyuan Zhang, Jialiang Sun, Hangrui Bi +4
We introduce DreamProver, an agentic framework that leverages a "wake-sleep" program induction paradigm to discover reusable lemmas for formal theorem proving. Existing approaches…
Autoformalizing Euclidean Geometry
Logan Murphy, Kaiyu Yang, Jialiang Sun +3
Autoformalization involves automatically translating informal math into formal theorems and proofs that are machine-verifiable. Euclidean geometry provides an interesting and contr…
A Survey on Deep Learning for Theorem Proving
Zhaoyu Li, Jialiang Sun, Logan Murphy +5
Theorem proving is a fundamental aspect of mathematics, spanning from informal reasoning in natural language to rigorous derivations in formal systems. In recent years, the advance…