2 papers
cs.CL2025
SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation
Sina Bagheri Nezhad, Yao Li, Ameeta Agrawal
Large Language Models (LLMs) often struggle with complex mathematical reasoning, where prose-based generation leads to unverified and arithmetically unsound solutions. Current prom…
cs.PL2019
Embracing a mechanized formalization gap
Antal Spector-Zabusky, Joachim Breitner, Yao Li +1
If a code base is so big and complicated that complete mechanical verification is intractable, can we still apply and benefit from verification methods? We show that by allowing a…