Showing cs.AIShow all
3 papers · 1 filter
cs.AI2026
Neuro-Symbolic Proof Generation for Scaling Systems Software Verification
Baoding He, Zenan Li, Wei Sun +4
Formal verification via interactive theorem proving is increasingly used to ensure the correctness of critical systems, yet constructing large proof scripts remains highly manual a…
cs.AI2025
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…
cs.AI2024
Neuro-Symbolic Data Generation for Math Reasoning
Zenan Li, Zhi Zhou, Yuan Yao +5
A critical question about Large Language Models (LLMs) is whether their apparent deficiency in mathematical reasoning is inherent, or merely a result of insufficient exposure to hi…