精读笔记

Problem Setting

这篇论文真正面对的是 verifiable multimodal geometry reasoning 的接口问题，而不是单纯提高几何题准确率。现有 neuro-symbolic GPS 通常假设前端能把图文输入转换成干净 formal predicates，后端 solver 再做确定性推理；但实际瓶颈恰好在这个接口：formalization 看似语义正确，却可能不可 parse、类型不一致、缺实体、与 solver 规则不匹配，最终无法执行。

第二个困难是 solver 的封闭性。即使 formalization 正确，固定 theorem library 和有限搜索预算也会让 solver 卡在 deductive impasse：缺少某个中间关系、没有优先尝试某个 theorem instance，或需要一个小的 auxiliary construction。关键矛盾是：神经模型可以猜到这些隐含结构，但不能被允许直接写入证明；符号系统可以验证，但自己不擅长在巨大候选空间里发现“该猜什么”。

Motivation

已有路线不够的根源不是模型不够大，而是 objective mismatch。autoformalization 被训练成 annotation imitation，优化的是形式序列相似度或人工标注一致性，但 downstream solver 关心的是 executability 和 solvability。几何题里一个点名、角关系或长度表达式错一点，就不是“噪声”，而是另一个 formal problem。

作者的核心观察是：solver 本身提供了最有价值的监督信号。parse 是否成功、proof state 是否一致、query 是否能闭合、哪个 subgoal 卡住，这些反馈比人工 predicate token 更接近最终目标。关键缺口因此是闭环：过去系统把 solver 放在最后验收，SD-GPS 把 solver 变成训练和推理中的 oracle。

Core Idea

SD-GPS 的本质不是新增一个更强 parser 或更大 MLLM，而是重新组织信息流：从“图文 → formal language → solver”单向 pipeline，变成“图文 formalizer ↔ solver execution feedback ↔ repair/proposal”的闭环系统。这个改变引入的 inductive bias 很明确：任何 neural output 必须落到 solver 可执行状态，不能只在自然语言或形式语言表面上 plausible。

这比 prior 更可扩展的地方在于，它把监督从 expensive gold formalization 部分转移到可自动计算的 execution reward 上；同时把 theorem prediction 从 closed-library classification 改成 verifier-controlled proposal。理论上，这能让系统利用神经模型的模式识别能力探索候选结构，同时把 correctness authority 保留给 symbolic verifier。真正的本质差异是：neural component 不再是独立前端，而是被 solver interface shape 过的 proposal policy。

Method

方法里值得保留的机制只有几层。第一，统一 multimodal formalizer 直接从 raw diagram 和 problem text 生成 typed predicates，解决 cascaded OCR / diagram parser / text parser 之间的信息丢失和 referential mismatch。它的必要性在于几何 formalization 经常需要图文互相 disambiguate，分开解析再 rectification 本质上太脆。

第二，SG-RL 把 formalizer 的优化目标从 imitation 转向 solver-readiness。reward 由 parse validity、non-contradictory execution state 和 answer solvability 组成，实际是在训练模型输出“能被后端证明系统消费的表示”。这不是一般 RL for reasoning，而是 representation alignment：让 latent multimodal understanding 对齐 symbolic API。

第三，bounded repair 是工程上很关键的闭环补丁。它处理的是 invalid / incomplete formalization，而不是证明能力本身。它可能贡献了不少分数，但机制上属于 execution-aware regeneration。

第四，verified theorem proposing 只在 solver 有 consistent state 但无法闭合时触发。agent 提出 schema-constrained lemma / relation / construction，solver 逐项检查 well-typed、applicable、verifiable、goal-reducing。核心变化是把 neural theorem prediction 从“选规则”变成“提出可验证局部搜索跳板”。

Key Insight / Why It Works

最核心的有效性来自 representation alignment，而不是新推理算法。GPS 的大量错误不是 solver 不会推理，而是输入 formal state 已经坏了；一旦 formalization 被 solver feedback 约束，系统会显著减少不可执行或弱 grounded predicates。SFT 负责学语言和格式，SG-RL 负责把输出分布推向 solver-compatible region，repair 负责 test-time recover。这三者加起来大概率是主要增益来源。

theorem proposing 的贡献更微妙。它确实提供了 test-time compute 和 search-space expansion，但从消融看边际增益相对小。它更像 verifier-guided hint generation，而不是真正扩展几何知识边界。由于 proposal 必须被 solver verify，它不能凭空创造新真理；它最多帮助 solver 发现已有规则空间内低优先级、隐式或局部构造相关的中间事实。

这篇论文的重要 insight 是：在可验证任务里，LLM/MLLM 最适合扮演 proposal distribution，而不是 judge。solver feedback 同时承担 reward、filter、diagnostic 和 certificate authority。这个范式比“让大模型直接解题”稳健，也比纯 symbolic search 更有启发式能力。

需要直接指出：部分增益可能主要来自 data 和 engineering。curated real data、synthetic templates、annotation normalization、solver filtering、bounded repair、same-domain formal language adaptation 都会强烈提升 benchmark 表现。文中未充分说明 synthetic data 与 benchmark templates 的距离，也没有把 SG-RL、repair、data cleaning、test-time retries 的贡献完全拆干净。因此不要把结果过度解读为通用几何推理能力突破。

Relation To Prior Work

它最接近 Inter-GPS / Auto-GPS / Pi-GPS 这条 formal language + symbolic solver 的 neuro-symbolic GPS 路线，也吸收了 verifiable RL、LLM autoformalization 和 proof-state-guided proposal 的思想。和 AlphaGeometry 类路线相比，它不是面向 olympiad-level theorem proving 的大规模 synthetic theorem search，而是面向 benchmark GPS 的 multimodal formalization + executable solving。

真正不同点在于 solver 的角色。prior 多数把 solver 当后端，或用 parser/rectifier 修补前端；SD-GPS 把 solver feedback 前移到 formalizer training，并在 theorem impasse 时作为 proposal verifier。看似新的 theorem proposing 其实是已有“LLM generates candidate, symbolic system verifies”范式在 geometry solver state 上的实例化；实质创新更多在于把这个范式系统性嵌入 GPS 的两个关键接口：formalization 和 theorem selection。

它属于 verifiable neural-symbolic alignment 谱系：神经网络负责生成候选表示和局部提示，符号系统负责执行、验证和裁剪。新增的信息不是某个几何定理，而是一个更紧的 solver-coupled training/inference loop。

Dataset / Evaluation

evaluation 覆盖 Geometry3K 和 PGPS9K，基本能验证 plane-geometry benchmark setting 下的 claim，尤其是 raw multimodal input 到 executable formalization 再到 final answer 的闭环效果。completion 和 choice 两种设置也区分了 exact solving 与选项约束下的求解。

更有价值的是 cross-modal point-reference split，它确实触及了本文主张的核心问题：文本点集完整、图中补充点、图文 mismatch 下 formalization 的鲁棒性。这个分析比主表数字更能说明 solver-driven formalizer 为什么有用。

但 evaluation 仍然主要是同类 benchmark 内验证。它没有充分证明跨 formal language、跨 solver、跨几何域的泛化；也没有真实部署场景。benchmark 是否真正支持“verifiable theorem proposing improves reasoning coverage”这个 claim 较弱，因为 theorem agent 的单独增益有限，且缺少 proposal 通过率、certificate 类型、失败原因和搜索预算对照。

Limitation

方法成立依赖几个强前提。第一，必须有一个足够强且可诊断的 symbolic solver；否则 solver feedback 既不能作为 reward，也不能作为 verifier。第二，formal language 必须覆盖目标问题；不在 predicate vocabulary 和 theorem library 内的几何结构无法被表达或验证。

第三，泛化可能 heavily rely on data coverage。curated annotations、PGPS/Geometry3K normalization、synthetic templates 和 curriculum sampling 很可能让模型学到 benchmark-specific formalization patterns。所谓推理提升的一大部分可能是更好的 executable retrieval / template matching，而不是抽象几何推理能力。

第四，theorem proposing 可能只是把搜索问题转移给 neural hint generator。由于 accepted lemma 必须可由 solver verify，它并没有突破 verifier 的理论边界；如果 verifier 缺规则或 construction language 不够，proposal 也无能为力。若 proposal schema、diagnostic summary 或 solver agenda 暴露了过强结构信息，也可能形成 hidden supervision。

第五，增益归因不清。SFT、synthetic data、solver feedback RL、repair loop、test-time proposal、timeout 设置和 baseline reproduction 都交织在一起。文中未充分说明哪些提升来自核心思想，哪些只是 engineering / scaling / data cleaning。

Takeaway

• 最值得记住的不是 SD-GPS 的具体模块，而是“solver as execution oracle”这一组织原则：在可验证多模态推理中，训练目标应尽早绑定 downstream verifier，而不是先学一个看似语义正确的中间表示。
• 第二个可迁移 insight 是，LLM/MLLM 更适合作为 bounded proposal policy。
• 只要 verifier 足够强，模型可以大胆生成候选 lemma、repair、construction 或 formalization，而 soundness 不必交给模型本身。
• 第三，未来 GPS 的关键可能不再是单纯扩大 MLLM，而是设计更好的 formal interface、diagnostic protocol、proof-state serialization 和 verifier-compatible reward。

一句话总结

SD-GPS 是一篇把 geometry problem solving 从“神经前端 + 符号后端”的松耦合 pipeline 推向 solver-coupled verifiable proposal system 的工作，真正贡献在于用 symbolic execution 对齐 formalization 与局部 theorem search，而不是发明新的几何推理机制。