| --- |
| title: QVerify |
| emoji: 🔬 |
| colorFrom: blue |
| colorTo: yellow |
| sdk: docker |
| app_port: 7860 |
| pinned: false |
| license: apache-2.0 |
| hardware: cpu-basic |
| tags: |
| - quantum-computing |
| - qiskit |
| - pennylane |
| - llm-verification |
| - logic |
| - grover |
| --- |
| |
| # QVerify — verifier-only Space |
|
|
| ## What this demonstrates |
|
|
| This Space runs the QVerify verifier component: a propositional CNF is |
| grounded over a declared universe of constants, encoded into a Grover |
| circuit, and executed on either a CPU-side PennyLane statevector simulator |
| or IBM Quantum's Heron r2 processor (156 qubits, `ibm_fez` backend). |
|
|
| Three pre-built CNF examples are provided via a dropdown — a two-atom |
| propositional formula, a single ground first-order atom, and a universally |
| quantified rule grounded over two constants. Selecting an example shows the |
| formula in clause-normal form, the universe, and a plain-language description |
| of what the verifier should return. Two verification modes are available: |
|
|
| - **consistency**: checks that `premises ∧ step` is satisfiable. A satisfying |
| assignment means the formula is consistent; UNSAT means the clauses |
| contradict each other. |
| - **entailment**: checks that `premises ∧ ¬step` is satisfiable. A satisfying |
| assignment is a counter-model showing the step is not entailed. |
|
|
| The classical post-check walks the most-frequent measured bitstrings until |
| one satisfies the CNF. This mirrors the post-check used in the full local |
| pipeline. |
|
|
| IBM hardware runs take 2-20 minutes wall-clock on the free tier (queue + |
| transpile + execution + result fetch). The Space submits the job and polls |
| every 8 seconds, yielding the job ID immediately so you can copy it before |
| the browser session ends. A fallback "recover by job ID" panel lets you |
| retrieve the result from any previous submission even if the live stream |
| dropped mid-run. |
|
|
| IBM hardware credit is shared across all users on the Open Plan |
| (approximately 10 minutes of quantum time per month total). The simulator |
| path runs locally in the Space container and has no external cost. |
|
|
| ## What is not in this Space |
|
|
| The translator — Gemma 4 E4B with grammar-constrained generation — converts |
| natural-language premises and conclusions into first-order CNF. It requires |
| a GPU and is not loaded here; CPU Basic Spaces cannot host a 4-billion- |
| parameter model. The full pipeline (translator + grounding + verifier) runs |
| locally from the GitHub repository and requires a CUDA-capable GPU and a |
| Hugging Face account with access to `google/gemma-4-E4B-it`. |
|
|
| The grounding step (Cartesian-product expansion of first-order CNF over a |
| finite universe) is included here and runs automatically before the Grover |
| circuit is constructed. |
|
|
| ## Resources |
|
|
| - [GitHub repository](https://github.com/Quantum-Labor/qverify) — source, |
| local install instructions, test suite, architecture documentation |
| - [Hardware run](https://github.com/Quantum-Labor/qverify#hardware-run) — |
| reproducibility record from the 2026-04-28 run on IBM Heron r2 (job ID |
| `d7o7dsqk4prs73dt4s6g`, 1024 shots, 2 Grover iterations, ~6 s quantum |
| runtime) |
| - [docs/architecture.md](https://github.com/Quantum-Labor/qverify/tree/main/docs/architecture.md) — |
| detailed walk-through of all four pipeline components |
|
|
| ## Citation |
|
|
| ```bibtex |
| @misc{brinza2026qverify, |
| author = {Serghei Brinza}, |
| title = {QVerify: quantum-assisted verification of LLM reasoning}, |
| year = {2026}, |
| publisher = {GitHub}, |
| howpublished = {\url{https://github.com/Quantum-Labor/qverify}}, |
| } |
| ``` |
|
|
| ## Author |
|
|
| [@SergheiBrinza](https://github.com/SergheiBrinza) |
|
|
