Neural Concept Verifiers: Proving with Concepts, not Pixels
TL;DR: This is a short summary of our paper Neural Concept Verifier: Scaling Prover-Verifier Games via Concept Encodings by Berkant Turan, Suhrab Asadulla, David Steinmann, Kristian Kersting, Wolfgang Stammer, and Sebastian Pokutta. The paper was accepted as a spotlight at ICML 2026 (top ~2.2% of submissions). In a nutshell, we move Prover-Verifier Games from pixel space to concept space: a prover selects a sparse set of human-readable concepts, a verifier must classify using only those concepts, and an adversarial prover tests whether the verifier can be fooled. The result is a scalable route to verifiable, nonlinear concept-based classification on datasets such as CLEVR-Hans, CIFAR-100, ImageNet-1k, and COCOLogic.
Why another interpretability model?
Interpretability in machine learning has a slightly uncomfortable failure mode: the explanation is often easier to look at than to trust. A heatmap may highlight part of an image, but it is not obvious whether the highlighted pixels are actually needed for the decision, whether the model would behave differently under a competing explanation, or whether the visual saliency is mostly a correlation artifact. This is particularly problematic in settings where we care about being right for the right reasons, not merely about having a plausible-looking explanation.
Prover-Verifier Games (PVGs) give a clean abstraction for this. A prover provides evidence; a verifier is forced to decide from that evidence; and an adversarial prover tries to construct misleading evidence. The idea has a long lineage: it descends from interactive proof systems in complexity theory [GMR85], entered machine learning as a game between learning agents [AZWG21], is closely related to debate-style oversight [ICA18], and has recently been used to make LLM outputs easier to check [KCELMB24]. In earlier work on Merlin-Arthur classifiers, we instantiated this structure for classification and obtained formal interpretability guarantees by selecting sparse input features and measuring completeness and soundness [WSTZP24]. However, doing this directly on pixels creates a very practical bottleneck: high-dimensional images are hard to optimize over, and pixel masks are often not the units humans actually reason with.
Concept Bottleneck Models (CBMs) go in the opposite direction [KNTMPKL20]. They map an input into an intermediate layer of concepts and then classify from those concepts. This is attractive because the interface is no longer raw pixels; it is something like “red object”, “metal sphere”, “handle”, or “striped texture”. The usual catch is that many CBMs use a linear classifier on top of the concept layer, which is interpretable but also brittle when the task requires nonlinear interactions among concepts. Counting, XOR-like rules, and permutation-invariant object relations are the standard examples.
Neural Concept Verifier (NCV) combines these two ideas. We keep the concept layer, but replace the simple classifier by a prover-verifier game over sparse concept subsets. Put differently: the proof is not a pixel mask, but a small set of concepts.
The setup
NCV has four moving parts:
- A concept extractor maps the input image to a concept encoding.
- Merlin, the cooperative prover, selects a sparse subset of concepts that should support the correct class.
- Morgana, the adversarial prover, selects a sparse subset of concepts that tries to mislead the verifier.
- Arthur, the verifier, predicts using only the selected concepts, and may reject when the evidence is not good enough.
The important shift is that Merlin and Morgana no longer play in pixel space. They play in concept space. This reduces dimensionality and makes the evidence more meaningful; it also lets Arthur be nonlinear without giving up the prover-verifier structure. In our experiments, the concept extractor is instantiated either through Neural Concept Binder (NCB) for CLEVR-Hans [SWSK24], or through CLIP/SpLiCE-style concept scores for CIFAR-100, ImageNet-1k, and COCOLogic [BOSCL24]. Sparsity is enforced at selection time: per input, the provers select 12 of the NCB slot encodings on CLEVR-Hans, and 32 concepts out of a 10,000-term CLIP vocabulary (derived from LAION captions) on the natural-image datasets.
What changes empirically?
The short version is that pixel-level PVGs scale poorly on real images, while NCV remains competitive and often improves over both linear CBMs and black-box baselines. The table in the paper is dense, so the widget below lets you inspect one dataset at a time. Completeness is the cooperative side of the game, essentially accuracy under Merlin’s selected concepts. Soundness is the adversarial side, i.e., whether Arthur avoids a wrong answer under Morgana’s misleading concepts, possibly by rejecting.
There are three observations that are worth keeping separate.
First, the pixel-level PVG baseline works on the synthetic CLEVR-Hans setting, but it does not scale gracefully to natural images. On CIFAR-100, for example, Pixel-MAC has high soundness but very poor completeness, which means that it is hard to recover the correct class from the selected pixel evidence. This is precisely the failure mode one expects when the game is played on the wrong representation.
Second, NCV narrows the interpretability-accuracy gap of concept bottleneck models. On CLEVR-Hans3 it reaches about 99% completeness, compared with about 95% for the linear CBM. On COCOLogic, where the target rules require more compositional reasoning, NCV reaches about 75% completeness versus about 59% for the linear CBM and about 66% for ResNet-50. The paper’s table also contains a nonlinear (but opaque) classifier head on the same concepts as a control; on COCOLogic, NCV beats even that baseline by about five points, so the gain is not merely about adding nonlinearity. Note that ImageNet is more nuanced: the linear CBM is slightly better in raw completeness there, while NCV still provides the adversarial soundness side of the game.
Third, NCV appears to help with shortcut learning. On the confounded CLEVR-Hans versions, adding even a small amount of clean data reduces the validation-test gap more sharply for NCV than for the CBM baselines. This is not because NCV was designed as a shortcut-mitigation method; rather, Morgana makes shortcuts visible to Arthur during training by trying to exploit misleading concept subsets.
What the game actually guarantees
Completeness and soundness are not only performance numbers. In the Merlin-Arthur framework they carry an information-theoretic reading, and NCV inherits it. The original guarantee [WSTZP24] was formulated for binary classification tasks; we extend it to the multi-class setting by reading it one class at a time, one-vs-rest, so that high completeness and soundness for a class become a lower bound on the mutual information between that class and Merlin’s selected concepts. The bound is conditional and cleanest for discrete, moderate-size concept vocabularies, so we treat the bound as the justification for our faithfulness criterion rather than a quantity we compute directly. But it is what makes the evidence provably informative rather than merely suggestive, and it is why the verification step is more than a metric.
Why this fits the broader story
There is a simple rule-of-thumb behind the paper: if the proof object is meant to be inspected by humans, then it should live in a representation that humans can understand. Pixels are not that representation. Concepts are not perfect either, and we are very explicit about this limitation, but they are a much better interface for classification evidence.
This also illustrates a broader Math-to-AI pattern that we keep returning to in our group. The underlying prover-verifier structure is mathematical and game-theoretic; it gives us language for completeness, soundness, rejection, sparse evidence, and adversarial testing. The concept extractor is modern AI infrastructure; it gives us a compressed and semantically meaningful representation of high-dimensional data. NCV is the hybrid: use the representation power of learned systems, but wrap the decision in a structured verification game.
For me this also closes a personal loop. Back in 2011, together with Santanu Dey, I proposed a scheme for generating cutting planes in integer programming by means of verification, called design and verify [DP14]: instead of restricting cut generation to procedures that are simple enough to be analyzed in closed form, one allows an essentially arbitrary generation process and pairs it with a separate, efficient verification step that certifies validity of whatever is produced. NCV follows the same division of labor, one abstraction level up: the prover may be an arbitrary learned system, as long as the verifier can check its output. Good proof systems decouple the cost of finding a proof from the cost of checking it; that asymmetry is what makes verification practical.
NB. Concept quality remains the bottleneck. If the concept extractor produces noisy, entangled, or culturally biased concepts, NCV inherits this. The framework improves where the concept space is good enough to support classification and inspection. It does not magically turn bad concepts into good ones.
Closing
The main point is not that NCV solves interpretability. It does something more modest and, in my view, more useful: it moves verifiable classification from pixel masks, which only hold up on small synthetic images, to concepts, which scale to real-world vision tasks. This makes the proof object smaller, more semantic, and easier to test adversarially.
Put differently, NCV asks the classifier to show its work, but in concepts rather than pixels. For interpretable AI, that is a much better place to start.
References
[TASKSP26] Turan, B., Asadulla, S., Steinmann, D., Kersting, K., Stammer, W., & Pokutta, S. (2026). Neural Concept Verifier: Scaling Prover-Verifier Games via Concept Encodings. ICML 2026 (spotlight). arxiv
[AZWG21] Anil, C., Zhang, G., Wu, Y., & Grosse, R. (2021). Learning to Give Checkable Answers with Prover-Verifier Games. arXiv preprint. arxiv
[BOSCL24] Bhalla, U., Oesterling, A., Srinivas, S., Calmon, F., & Lakkaraju, H. (2024). Interpreting CLIP with Sparse Linear Concept Embeddings (SpLiCE). NeurIPS 2024. paper
[DP14] Dey, S.S. & Pokutta, S. (2014). Design and Verify: A New Scheme for Generating Cutting-Planes. Mathematical Programming, 145, 199–222 (conference version in IPCO 2011). paper
[GMR85] Goldwasser, S., Micali, S., & Rackoff, C. (1985). The Knowledge Complexity of Interactive Proof-Systems. STOC 1985. paper
[ICA18] Irving, G., Christiano, P., & Amodei, D. (2018). AI Safety via Debate. arXiv preprint. arxiv
[KCELMB24] Kirchner, J.H., Chen, Y., Edwards, H., Leike, J., McAleese, N., & Burda, Y. (2024). Prover-Verifier Games Improve Legibility of LLM Outputs. arXiv preprint. arxiv
[KNTMPKL20] Koh, P.W., Nguyen, T., Tang, Y.S., Mussmann, S., Pierson, E., Kim, B., & Liang, P. (2020). Concept Bottleneck Models. ICML 2020. paper
[SWSK24] Stammer, W., Wuest, A., Steinmann, D., & Kersting, K. (2024). Neural Concept Binder. NeurIPS 2024. paper
[WSTZP24] Waeldchen, S., Sharma, K., Turan, B., Zimmer, M., & Pokutta, S. (2024). Interpretability Guarantees with Merlin-Arthur Classifiers. AISTATS 2024. paper
Comments