Neurosymbolic Transformers (Neural CEGIS)
Training framework that pairs neural networks with symbolic verification — a verifier finds constraint violations and feeds them back as targeted training data until violations reach zero.
Stack
Timeline
2025
Impact
- Augmented Lagrangian with learned dual variables
- Evidence-Conditioned Constraint Gating (ECCG)
- Benchmarks: arithmetic, kinship reasoning, FEVER
Context & Goals
Neural CEGIS (Counterexample-Guided Inductive Synthesis) brings the verification loop from program synthesis into neural-network training. A symbolic verifier finds inputs where a trained model violates domain constraints, feeds them back as targeted training data, and the loop repeats until violations reach zero.
Approach
- Adaptive constraint learning: an augmented Lagrangian with learned dual variables (λ*) automatically balances task accuracy against constraint satisfaction — removing manual penalty tuning.
- Evidence-Conditioned Constraint Gating (ECCG): per-sample gates decide when noisy symbolic extractors are reliable enough to trust.
- GroundedVerifier API: a reusable wrapper that adds symbolic constraints to any NLI model.
- NST-VERI v2: a multi-task variant with focal loss, contradiction detection, and evidence-relevance learning.
Evaluation
Tested across three benchmarks — multi-digit addition, kinship reasoning, and FEVER fact verification — using PyTorch (≥ 2.2), Hugging Face Transformers, DeBERTa NLI models, and LoRA fine-tuning.
Why it matters
The framework drives constraint violations toward zero without sacrificing task accuracy, giving a principled way to make transformers respect hard domain rules.