Research map / Multi-agent systems and games / Human-AI and goal-conditioned
Neural Interactive Proofs
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes a game-theoretic framework (generalised prover-verifier games) for neural interactive proofs, introduces new protocols (NIP, MNIP, ZK-NIP) with theoretical equilibrium correspondences, and tests them on graph isomorphism and LLM code validation.
Problem
How a computationally bounded verifier can learn, with neural networks, to interact with powerful untrusted provers so that it reliably solves a task (e.g., validating code), including worst-case guarantees and zero-knowledge.
Approach
Unify prover-verifier games as messaging games and introduce NIP, a verifier-leading Stackelberg game with worst-case completeness/soundness losses whose equilibria correspond to valid interactive proofs; extend to multi-prover (MNIP) and zero-knowledge (ZK-NIP) variants.
Key results
- On code validation, all protocols modestly improve final test accuracy over a solo verifier; NIP and MNIP see around 11% gains.
- MNIP performs best on the worst-case metric (fraction of data points where the verifier always fails across 10 rollouts).
- On graph isomorphism, NIP verifiers learn to near-perfectly classify valid instances when interacting with the prover, while ADP, Debate and MNIP do not improve.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use NIP instead of a verifier trained in isolation | GPT-4o-mini verifier with GPT-4o prover · APPS code validation | test accuracy | Helped |
| Use NIP instead of a verifier trained in isolation | GPT-4o-mini verifier with GPT-4o prover · APPS code validation | test accuracy: around 11% | Helped |
| Use MNIP instead of a verifier trained in isolation | GPT-4o-mini verifier with GPT-4o prover · APPS code validation | test accuracy: around 11% | Helped |
| Use interaction protocols rather than a solo verifier | Code-validation protocols · APPS code validation | percentage of data points where the verifier always fails | Helped |
| Use MNIP rather than the other protocols | Code-validation protocols · APPS code validation | percentage of data points where the verifier always fails | Helped |
| Use NIP or MNIP rather than other protocols | Code-validation protocols · APPS code validation | false negative rate | Helped |
| Interact with a trained prover rather than a random prover | NIP verifier · Graph isomorphism | test accuracy | Helped |
| Increase verifier model size | NIP verifier · Graph isomorphism | test accuracy | Helped |
| Use NIP rather than ADP, Debate, or MNIP | Graph-isomorphism verifier · Graph isomorphism | test accuracy | Helped |
| Increase the coefficient of the simulator-loss term in the prover's loss (ablation) | ZKNIP prover · Graph isomorphism | message-sequence distribution difference | Helped |
| Replace some verifier guesses with the true label during training (ablation) | Stabilised expert iteration · APPS code validation | percentage of data points where the verifier always fails | Helped |
| Replace some verifier guesses with the true label during training (ablation) | Stabilised expert iteration · APPS code validation | mean test accuracy | Mixed |
Surprising findings
- Standard ADP prover-verifier game equilibria are neither necessary nor sufficient for validity when soundness error is nonzero (proved by counterexample).
- Vanilla expert iteration causes mode collapse toward low acceptance rates; replacing verifier guesses with true labels in an annealed proportion fixes this.
Limitations
- Experiments use simple PPO and expert iteration rather than advanced RL methods, so empirical results lie far from theory.
- Only two domains evaluated (graph isomorphism and code validation).
- Not all protocol variants (e.g., simultaneous vs sequential debate, open protocols) are evaluated.
Experimental setup
Datasets: APPS Erdős-Rényi synthetic graphs
Benchmarks: graph isomorphism synthetic test set APPS code validation test set
Metrics: test accuracy precision recall percentage of data points where verifier always fails
Baselines: ADP Debate solo verifier random prover baseline MNIP
Builds on: prover-verifier games debate Merlin-Arthur classifier LOLA expert iteration
Closest papers by meaning
- Generalizing Verifiable Instruction Following (NeurIPS 2025 · similarity 0.86)
- DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search (ICLR 2025 · similarity 0.86)
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.85)
- Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models (NeurIPS 2025 · similarity 0.85)
- LEGO-Prover: Neural Theorem Proving with Growing Libraries (ICLR 2024 · similarity 0.85)
- PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition (NeurIPS 2024 · similarity 0.85)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.