LeanContext

新的 LeanContext 基准测试评估神经定理证明器

研究人员推出了 LeanContext，这是一个旨在评估神经定理证明系统的新基准测试。该基准测试包含超过 129,000 个 Lean 整体证明生成问题，用于解耦数学资源与局部形式化上下文对证明生成的影响。使用包括 LLaDA 和 Llama 在内的基于扩散和自回归的模型进行的实验表明，使用数学上下文进行训练可显著提高性能。优先考虑目标引用的已省略声明可进一步提高成功率。