预测下一状态还不够：用于精益定理证明的JEPA表示
Predicting the Next State Is Not Enough: JEPA Representations for Lean Theorem Proving
浏览论文内容
中文总结 AI 辅助
本研究探讨神经定理证明中单步转换排序作为分支信号的有效性，发现JEPA表示虽在排序诊断上优于InfoNCE，但在完整证明求解上不如提议器排序，表明一步排序不足以指导长视界搜索。
中文摘要 AI 辅助
神经定理证明器必须同时提出策略并决定探索哪些有效的后继状态。我们研究单步Lean转换是否为分支排序提供自监督信号。一种JEPA风格的模型预测潜在后继表示，并仅对由固定预训练ByT5提议器生成的、经内核验证的非终止后继进行评分。在相同定理排序诊断中，JEPA的Top-1准确率高于匹配的InfoNCE（50.18%对比31.55%），但在三个随机种子上平均解决了987个定理中的282.3个，而提议器排序为308个，同时需要更多的策略检查。在此设置中，准确的一步转换排序因此不足以作为长视界搜索价值。受控评估将表示与提议质量分离，并将内核检查的证明完成作为主要终点。
英文摘要
Neural theorem provers must both propose tactics and decide which valid successor states to explore. We study whether one-step Lean transitions provide a self-supervised signal for branch ordering. A JEPA-style model predicts latent successor representations and scores only kernel-validated, nonterminal successors generated by a fixed pretrained ByT5 proposer. JEPA achieves higher Top-1 than matched InfoNCE on a same-theorem ranking diagnostic(50.18% versus 31.55%), but averages 282.3 of 987 solved theorems across three seeds versus 308 for proposer ordering, while requiring more tactic checks. In this setting, accurate one-step transition ranking is therefore insufficient as a long-horizon search value. The controlled evaluation separates representation from proposal quality and treats kernel-checked proof completion as the primary endpoint.
