8 citations · 12 across the 15 of their papers we have counts for
16 papers
Law And Order: Tax Law Autoformalization
Sophia Simeng Han, Yoshiki Takashima, Anjiang Wei +2
Legal systems are increasingly implemented through software, yet scalable methods for translating legal texts into accurate symbolic representations remain underdeveloped. We study…
P: Joint Program-and-Proof Planning for Verified Code Generation
Zenan Li, Ziran Yang, Peiyang Song +2
Verified code generation asks a large language model (LLM) to generate both an executable program and a machine-checkable proof that the program meets a formal specification, promi…
Euclid-Omni : A Unified Neuro-Symbolic Framework for Plane Geometry
Zhaoyu Li, Hangrui Bi, Youyuan Zhang +5
Euclidean geometry is a compelling testbed for AI reasoning, as it demands the combination of intuitive diagram understanding, axiomatic deduction, and algebraic computation. Yet,…
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…
Learning to Disprove: Formal Counterexample Generation with Large Language Models
Zenan Li, Zhaoyu Li, Kaiyu Yang +2
Mathematical reasoning demands two critical, complementary skills: constructing rigorous proofs for true statements and discovering counterexamples that disprove false ones. Howeve…
Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning
Zenan Li, Zhaoyu Li, Wen Tang +6
Large language models (LLMs) can prove mathematical theorems formally by generating proof steps (\textit{a.k.a.} tactics) within a proof system. However, the space of possible tact…
Decoupling Training-Free Guided Diffusion by ADMM
Youyuan Zhang, Zehua Liu, Zenan Li +3
In this paper, we consider the conditional generation problem by guiding off-the-shelf unconditional diffusion models with differentiable loss functions in a plug-and-play fashion.…
Neuro-symbolic Learning Yielding Logical Constraints
Zenan Li, Yunpeng Huang, Zhaoyu Li +5
Neuro-symbolic systems combine the abilities of neural perception and logical reasoning. However, end-to-end learning of neuro-symbolic systems is still an unsolved challenge. This…
Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency
Zenan Li, Yifan Wu, Zhaoyu Li +4
Autoformalization, the task of automatically translating natural language descriptions into a formal language, poses a significant challenge across various domains, especially in m…
APPL: A Prompt Programming Language for Harmonious Integration of Programs and Large Language Model Prompts
Honghua Dong, Qidong Su, Yubo Gao +5
Large Language Models (LLMs) have become increasingly capable of handling diverse tasks with the aid of well-crafted prompts and integration of external tools, but as task complexi…
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…
Learning Reliable Logical Rules with SATNet
Zhaoyu Li, Jinpei Guo, Yuhe Jiang +1
Bridging logical reasoning and deep learning is crucial for advanced AI systems. In this work, we present a new framework that addresses this goal by generating interpretable and v…
G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks
Zhaoyu Li, Jinpei Guo, Xujie Si
Graph neural networks (GNNs) have recently emerged as a promising approach for solving the Boolean Satisfiability Problem (SAT), offering potential alternatives to traditional back…
NSNet: A General Neural Probabilistic Framework for Satisfiability Problems
Zhaoyu Li, Xujie Si
We present the Neural Satisfiability Network (NSNet), a general neural framework that models satisfiability problems as probabilistic inference and meanwhile exhibits proper explai…
Graph Contrastive Pre-training for Effective Theorem Reasoning
Zhaoyu Li, Binghong Chen, Xujie Si
Interactive theorem proving is a challenging and tedious process, which requires non-trivial expertise and detailed low-level instructions (or tactics) from human experts. Tactic p…