Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs

📄 arXiv: 2610.02444v1 📥 PDF

作者: Omar Farouk Zouak, Houssam Eddine Boukhalfa, Soumaya Lakehal, Shiv Katiyar, Samia Nefti-Meziani

分类: cs.CL, cs.AI

发布日期: 2026-10-01

备注: Accepted at EMNLP 2026 Findings

🔗 代码/项目: GITHUB

💡 一句话要点

通过定理符号验证器生成反例以解决伪命题问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 反例生成 符号验证 强化学习 定理证明 数学模型

📋 核心要点

  1. 现有大型语言模型在证明定理时存在伪命题缺口，无法有效驳斥相关虚假定理。
  2. 本文提出通过符号验证器生成反例，构建SymCE语料库，并利用其作为训练环境进行模型优化。
  3. 实验结果显示，使用稀疏奖励的强化学习方法显著提升了模型在真实定理识别上的表现。

📝 摘要（中文）

大型语言模型通常能够证明一个定理，但却无法驳斥一个相关的虚假定理，这种现象称为伪命题缺口，现有的监督微调方法无法弥补这一缺口，甚至可能加剧这一问题。本文将反例生成框架化为针对确定性定理的Python验证器的约束见证发射，并发布了SymCE，一个包含4707个虚假的本科代数和实分析猜想的语料库，每个猜想都配有可执行的验证器。通过在该环境下训练Qwen3-4B，发现仅依赖反例的监督微调会导致真实定理识别率从0.27降至0.00，而使用稀疏结果奖励的强化学习方法则修复了这一问题，识别率提升至0.66。我们的4B模型在所有评估的7B数学专用模型中表现最佳，并在多个基准测试中保持竞争力。

🔬 方法详解

问题定义：本文旨在解决大型语言模型在定理证明中存在的伪命题缺口问题，现有的监督微调方法无法有效驳斥虚假定理，甚至可能导致性能下降。

核心思路：通过将反例生成视为针对确定性定理的约束见证发射，利用符号验证器生成反例，并将其作为训练环境，优化模型的学习过程。

技术框架：整体架构包括SymCE语料库的构建、Python验证器的设计，以及基于该验证器的强化学习训练流程，主要模块包括反例生成、模型训练和验证器评估。

关键创新：最重要的创新在于将验证器作为奖励函数，形成了新的训练环境，并通过稀疏奖励机制修复了模型在真实定理识别上的崩溃现象。

关键设计：在训练过程中，采用了稀疏和密集奖励的对比实验，发现稀疏奖励在持出校准探针上的表现优于密集奖励，关键参数设置和损失函数设计均围绕这一目标进行优化。

🖼️ 关键图片

img_0
img_1
img_2

📊 实验亮点

实验结果显示，使用稀疏奖励的强化学习方法使得模型在真实定理识别率上从0.00提升至0.66，显著优于仅依赖反例的监督微调方法。此外，4B模型在多个基准测试中表现优于所有评估的7B数学专用模型，展现出强大的竞争力。

🎯 应用场景

该研究的潜在应用领域包括教育、自动定理证明和数学问题求解等。通过生成反例，能够帮助学生更好地理解数学概念，同时也为自动化工具提供了更强的验证能力，未来可能在智能教育和科研中发挥重要作用。

📄 摘要（原文）

Large language models often solve a theorem forward yet fail to disprove a closely related false one: a falsification gap that supervised fine-tuning does not close and can actively worsen. We frame counterexample generation as constrained witness emission against a deterministic per-theorem Python verifier, and release SymCE, a corpus of 4,707 false undergraduate-algebra and real-analysis conjectures, each paired with executable verifiers. The verifier also serves as the reward function, making SymCE a training environment. Training Qwen3-4B with SFT followed by GRPO under this oracle reveals an imitation trap: counterexample-only SFT collapses true-theorem recognition from 0.27 to 0.00, while RLVR with a sparse outcome-only reward repairs this and exceeds the base, to 0.66. The collapse replicates across four seeds and on Gemma-3-4B. Sparse and dense rewards yield statistically indistinguishable in-domain success yet diverge by 33 points on a held-out calibration probe, a dissociation we trace to the partial-credit term. Our 4B model outperforms every evaluated 7B open-weights math specialist, remains competitive with six frontier commercial APIs, and transfers under unchanged prompting to GSM8K, MATH-500 and MMLU-college-math. A human audit of 177 verifier decisions finds 97.7% accuracy. Code, data, verifier modules and annotations: https://github.com/ce-rlvr/SymCE.