Rosetta-PL：用命题逻辑构建大语言模型推理能力的新基准

研究人员通过将Lean定理证明器中的逻辑命题翻译为自定义逻辑语言，创建了Rosetta-PL基准，用于系统评估大语言模型在形式化推理任务中的表现。该基准揭示了模型学习逻辑规则的规律，为低资源语言应用和模型训练优化提供指导。

大语言模型（LLMs）主要在高资源自然语言数据上训练，存在低资源语言表现受限和深度逻辑推理能力不佳的局限。现有评估基准难以区分模型是掌握逻辑规则还是依赖模式匹配完成任务。

Rosetta-PL构建包含四步：1. 选择Lean定理证明器的命题作为数据源（优势：逻辑正确、结构丰富、语法语义明确）；2. 设计自定义逻辑语言（避免预训练见过的符号，消除记忆依赖）；3. 将Lean命题翻译为自定义语言构建数据集；4. 用数据集微调LLM（如GPT-4o）并评估。

实验得出三个关键结论：1. 翻译中保留逻辑关系显著提升推理精度，证明模型能学习抽象规则；2. 训练数据规模在20000样本后趋于饱和，数据质量比数量更重要；3. 模型在陌生符号系统中表现良好，具备真正的逻辑泛化能力。

Rosetta-PL成果对低资源语言的启示：1. 结构化表示（保留底层逻辑关系）有助于模型学习；2. 优先关注数据质量和表示方法而非规模；3. 模型可能具备学习任意结构化符号系统的潜力，为低资源语言适配提供基础。

技术要点包括：翻译策略（保持逻辑等价，映射运算符、保留量词等）；评估指标（真值判断准确率、逻辑等价识别正确率等）；微调策略（学习率调度、正则化、few-shot示例设计等）。

局限：1. 目前仅覆盖命题逻辑；2. 与现实自然语言推理存在差距；3. 主要基于GPT-4o实验。未来方向：多模态逻辑推理、增量学习、可解释性分析、跨领域迁移等。