Back to Research
Independent research
Counterexample-Guided Verifiable Reasoning — LLM + SMT solver in the loop
An LLM proposes, Z3 disposes: conflict-directed search over SMT counterexamples, evaluated against compute-matched retry baselines.
Target model Qwen3-30B-A3B (MoE, ~3B active parameters) on an A100 80 GB. The interesting comparison is like-for-like compute: generic retry vs. solver-grounded counterexamples.
Results
Every value links to the committed artifact that produces it.
| Metric | Value | Evidence |
|---|---|---|
| Evaluation runs (500 problems × 3 seeds × 5 arms) | 7,500 | data/linear/problems.jsonl + scripts/run_all.sh |
| Ablation arms compared, one-shot → conflict-directed | 5 | scripts/run_all.sh |
Running it
A Z3-only verifier demo (no live LLM generation, so no unbounded per-click cost) is planned; the repo already carries the full evaluation harness.