概率式证明状态压缩：优化 LLM 引导的形式化验证

基于摘要分析。研究针对 LLM 引导的形式化证明搜索中搜索空间过大、可扩展性受限的问题，将现成 LLM 与基于 conformal prediction 的证明状态压缩结合，以降低搜索计算开销。 其核心机制是利用 conformal prediction 区间指导自适应的概率分箱，压缩证明状态空间。作者称该方法在降低计算需求的同时保留统计层面的证明保证；但摘要未说明区间的构造与校准方式、分箱如何影响搜索过程，以及统计保证所针对的事件和成立条件。这些信息尚需全文核对，不能将其直接等同于对搜索完备性的保证。 作者报告，在 Lean miniF2F 测试集上的初步实验中，成功率相近，passes 减少 75%，平均实际运行时间减少 23%。摘要未明确 passes 的操作定义，也未提供所用 LLM、具体对照基线、成功率数值、计算预算和计时环境，因此这些结果只能在其所述测试集背景下理解，不能据此推断跨模型或跨任务的效率优势。实验协议、消融及统计信息尚未验证。 该论文的主要研究对象是形式化证明搜索，而非 EEG 信号建模或 BCI。现有材料未提供证明状态压缩与 EEG 瓶颈之间的具体机制对应，不据此生成 BCI 迁移效果或复现实验建议。