Ankyra: Sound Neuro-Symbolic Reasoning with Verifiable Proofs

Abstract

We present Ankyra, a domain-general neuro-symbolic reasoning system built on a strict separation of roles: the language model \emph{proposes} a formalization, and a deterministic symbolic engine \emph{decides} it. The system spans a family of decidable formalisms - from definite Horn clauses and stratified negation to positive first-order logic with disjunction and quantifiers, finite-domain constraints, exact arithmetic, and defeasible defaults with specificity. Each formalism comes with a sound decision procedure and a declared fragment. Every answer carries a machine-checkable proof trace, and no statement enters the theory without either a verbatim quotation or an explicit hypothesis tag. We report a demonstration-scale evaluation on standard collections: on covered slices the system achieves high accuracy while producing no confidently wrong conclusions, and it abstains honestly (out_of_fragment) where the implemented logic cannot express the problem. We also compare against two open-source neuro-symbolic systems - Logic-LM and NC --- on identical inputs and the same model, and show that under a small, inexpensive model the binding constraint is the translation interface rather than the reasoning. We make no claim to state-of-the-art performance: the evaluation uses fixed subsamples rather than full test sets, and we state the statistical and methodological limitations explicitly.