少即是多：LLM 数学推理中的认知负荷和单提示天花板

我们在 SAIR 方程理论第一阶段竞赛的背景下，对形式数学推理的即时工程进行了系统的实证研究。这项任务需要确定一个方程定律是否暗示着所有岩浆中的另一个方程定律——这个问题一般来说是不可判定的，但通过有限模型搜索可以判定为 FALSE。在五周的时间里，我们设计、测试和分析了 40 多个提示变体，范围从 0 到 4,878 字节，涉及四个评估分区和三个语言模型（gpt-oss-120b、Llama 3.3 70B、Gemma 4 31B）。我们的中心发现是单提示上限：尽管进行了大量的工程工作，但 gpt-oss-120b 的经验饱和区域的硬精度稳定在大约 60--79% 之间，而无备忘单基线的硬精度为 59.75%。我们确定了这个上限背后的三种机制：（1）真实情况的数学不确定性限制了任何有限提示可以编码的内容； (2) 复杂的规则系统会降低较弱模型的性能（Llama 3.3 70B 崩溃至 0% TRUE 召回率，提示超过 2KB）； （3）即时排序效应与模型注意力以脆弱的、非单调的方式相互作用。我们的最佳提交（AN45c，2,252 字节）在 Hard3 上实现了 79.25% 的准确率（n=400；95% CI：[75.0%, 82.9%]），真实召回率为 95.9%，错误召回率为 63.4%，比无备忘单基线（59.75%）提高了 19.5 个百分点。我们在 https://github.com/israelcazares/sair-prompt-engineering 发布了所有提示变体、评估脚本和结果