Or: what happens when a 1.5B model must show its work as an executable query — 93.3% vs 34.2%, and 81.4% vs 5.8% on names it never saw.
The Problem
Large language models answer questions from memory. When they don't know, they confabulate — confidently, fluently, wrongly. For high-stakes domains (law, medicine, compliance), "trust me" is not an answer format.
The neuro-symbolic alternative: make the model write a query in a formal language, execute it against a knowledge graph, and return the executed path as a proof. If the query doesn't parse, there's no answer. If the graph lacks the fact, the answer is empty — visibly, not silently.
GraphProof-QA implements this loop end-to-end on a single RTX 3060: a Qwen2.5-1.5B model fine-tuned to translate movie questions into a tiny path-query DSL, with grammar-constrained decoding, execution over a 135k-triple knowledge graph, and proof traces on every answer.
The Three Systems (Same Base, Same Data)
Everything below compares identical budgets — same 1.5B base model, same 30k training pairs, same LoRA config (r=16, 3 epochs). Only the task differs:
- System A (direct): fine-tuned to answer questions directly with entity names.
- System B (DSL): fine-tuned to write path queries, decoded unconstrained, then parsed and executed.
- System C (constrained): system B's adapter with xgrammar schema-constrained decoding.
Evaluation: 2,000 held-out test questions per hop level (6,000 total), Hits@1.
Results: Compile-Then-Execute Wins Everywhere
| Hop | A (direct) | B (DSL) | C (constrained) | B−A gap |
|---|---|---|---|---|
| 1-hop | 14.2% | 97.2% | 98.3% | +83.0 |
| 2-hop | 22.2% | 89.7% | 97.2% | +67.5 |
| 3-hop | 66.3% | 93.0% | 94.9% | +26.7 |
| Overall | 34.2% | 93.3% | 96.8% | +59.1 |
System B produced zero parse failures across 6,000 generations — the LoRA learned the grammar cold. System C adds +3.5 overall (largest on hop-2, +7.5), proving structural enforcement helps where ambiguity is highest. The A-vs-B difference is overwhelmingly significant (McNemar exact p≈0 on 6,000 paired items: 3,645 improvements vs 101 regressions).
Why does A fail so badly? It memorizes. On unseen entities it confabulates plausible-sounding wrong answers ("Michael Almereyda directed..." — a real director, wrong film). B can't confabulate entities the same way: its queries execute or return nothing.
The Renamed-Entity Test: 81.4% vs 5.8%
The headline experiment. We renamed 200 entities to novel strings the models never saw in training (e.g. ENTITY_00119), rewrote 531 test questions with the new names, and measured both systems:
| System | Hits@1 on renamed entities |
|---|---|
| B (compile-then-execute) | 81.4% |
| A (direct answer) | 5.8% |
A 75.6-point gap, significant at McNemar p < 1e−80 (411 vs 10 discordant pairs on 531 items; exact binomial p ≈ 1.6e−107, χ² approximation 1.2e−84). System B copies the unseen name into a query and lets the graph do the work. System A, trained on the old names, collapses. This is grounding vs memorisation, measured — not asserted.
Two more conditions, reported honestly:
- Swapped triples (500 edits): B follows edits to new answers 95.6%. True by construction (the executor reads the edited graph) — a demonstration, not a discovery.
- Deleted triples (99 fully-disconnected questions): B abstains 8.1%, A 0.0%. Neither system abstains well; B's wrong queries fail silently with wrong answers instead of empty results. An important negative result: executability ≠ calibration.
Where B Fails (100 Hand-Labelled Misses)
| Failure type | Count |
|---|---|
| Wrong relation choice | 83 |
| No exact gold path exists | 17 |
| Parse error | 0 |
| Wrong entity / direction / hop count | 0 |
The model always writes valid queries about the right entity with the right shape — it picks the wrong relation 83% of the time it fails. That locates the entire problem in one place: relation disambiguation, not syntax, grounding, or planning.
The DSL (Designed, Not Borrowed)
START "Jawbreaker" -> starred_actors <- starred_actors -> directed_by
RETURN ?x EXCEPT "Jawbreaker"
Path queries with directed hops, WHERE filters, and an EXCEPT clause — invented during development when we discovered MetaQA excludes the query entity from answers by construction (making exclusion explicit and checkable beat baking it into the engine). Lark grammar, dict-adjacency executor, proof traces rendered per answer.
Gold queries for all 329k training questions were generated by exact-match relation-sequence search (324,124 found, 100% execution-verified). The remainder: ambiguous film titles the KB merges ("Darling" 1965 + 2007 as one entity) — listed, not hidden.
What Didn't Work
- Full entity-trie enforcement distorts greedy entity selection (a Qwen tokenization-vs-trie-path misalignment in xgrammar's compiled matcher). The 43k-name trie compiles in ~15s but isn't enforced at decode time; system C constrains shape + relations instead. Documented open issue, not a claimed result.
- vLLM was unusable (flashinfer/CUDA incompatibility); all inference is HF Transformers.
- MetaQA is template-generated. 100 paraphrased test questions (gpt-4o-mini, entities preserved) are in the repo; the robustness evaluation on them is still pending.
Reproduce It
git clone https://github.com/raihan-js/graphproof-qa
# adapters: huggingface.co/raihan-js/graphproof-dsl-1.5b
# dataset: huggingface.co/datasets/raihan-js/MetaQA-CF
Limitations
- Template-generated questions flatter all scores; paraphrase check pending.
- Abstention doesn't work (8.1%) — executability is not calibration.
- Single model scale (1.5B); 7B scaling point not run.
- Entity-trie enforcement open (see above).
Every number above comes from per-item JSONL logs. The gate is the product; the headline is the bonus.
Top comments (0)