4 papers
Verifiable Checks for Business Rule Consistency
Joseph Tafese, Milad Hooshyar, Sam Bayless +2
Maintaining consistency between natural language documentation of business rules and their evolving internal implementations is a significant challenge in large-scale systems. We p…
VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning
Vikash Singh, Darion Cassel, Nathaniel Weir +2
Despite the syntactic fluency of Large Language Models (LLMs), ensuring their logical correctness in high-stakes domains remains a fundamental challenge. We present a neurosymbolic…
A Neurosymbolic Approach to Natural Language Formalization and Verification
Chenyang An, Sam Bayless, Stefano Buliani +27
Large Language Models perform well at natural language interpretation and reasoning, but their lack of formal correctness guarantees limits their adoption in regulated industries l…
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
Nick Feng, Alan J. Hu, Sam Bayless +5
Generating proofs of unsatisfiability is a valuable capability of most SAT solvers, and is an active area of research for SMT solvers. This paper introduces the first method to eff…