Argunauts:掌握论证分析的开放大型语言模型,运用 Argdown

这是我的 Argunauts 项目的启动公告。我目前正尝试使用 Argdown 教大型语言模型(LLMs)进行逻辑论证分析和论证映射,并将在一系列文章中分享进展和经验教训,今天将从简要介绍总体目标、背景和初步计划开始。
目标:精通 Argdown
Argdown 是一种简单的标记语言,用于构建复杂的论证结构。它对于映射全面的辩论(例如关于地球工程或食用动物)以及记录单个论证的详细逻辑分析特别有用。
Argunauts 是精通这些方法的大型语言模型。
本项目旨在通过教授大型语言模型以下技能来构建 Argunauts:
- 1️⃣ 进行全面深入的论证分析,
- 2️⃣ 以标准化形式记录其重构,
- 3️⃣ 有效利用外部工具(解析器、定理证明器)实现这些目的,
- 4️⃣ 不牺牲基础模型所具备的任何其他技能。
训练将侧重于生成语义良好的 Argdown 片段,但 Argunauts 也应该能够可靠地使用 XML 注释源文本或编写 Z3 代码进行形式化和有效性检查。
Argunauts 有什么用?例如,它们可以:
- 作为宽容的 AI 导师,协助学生学习逻辑论证分析;
- 作为强大的副驾驶,赋能专家论证分析师;
- 在 AI 工作流和代理式 AI 系统中执行自我批判任务;
- 作为专家 AI,驱动基于大型语言模型的批判性思维工具;
- 作为专家模型,为 MoE(专家混合)模型提供专业领域知识。
挑战
1. 大型语言模型在预训练期间几乎没有接触过 Argdown 代码。
Argdown 是一个边缘项目。
在 Github 上几乎找不到 Argdown 代码示例(根据 Github 搜索结果)
语言 | 搜索字符串 | 命中数(文件数) |
---|---|---|
YAML | ```yaml | 180 万 |
Mermaid.js | ```mermaid | 25.7 万 |
Argdown | ```argdown | 266 |
这体现在,例如,与 Llama-3.3-70B 的共享聊天中。(然而,我有点惊讶和高兴地看到 Llama-3.3-70B 似乎知道 Argdown 是什么。)
2. 大型语言模型在预训练期间也未接触过如何分析单个论证或如何映射整个争议。
进行逻辑分析并以标准形式呈现论证,考虑到我们自然语言文本语料库的整体,是绝对罕见的例外。大多数说话者和读者永远不会遇到论证图或看到逻辑推理以标准形式呈现。(以前提-结论结构呈现论证在哲学中确实有些常见,但主要限于其某些分支。)
谷歌图书 Ngrams 证实了这一点:表示显式逻辑论证分析的特征词的频率比非特指的“理由”或“论证”低好几个数量级。
n-gram | 频率(2020 年) |
---|---|
优点和缺点 | ~2e-4 |
政治辩论 | ~6e-5 |
争议问题 | ~2e-5 |
推理规则 | ~4e-6 |
论证模式 | ~7e-7 |
因此,虽然大型语言模型可能在预训练期间迅速学习摘要、翻译、算术或 JavaScript,但对于深入的逻辑论证分析并非如此。
3. 难以找到足够的逻辑论证分析微调训练数据。
此外,尽管有大量关于批判性思维的文献,包括介绍逻辑分析语言和方法的教科书及其他培训材料,但我认为,通过分步演示明确教授逻辑分析的文本相对较少:学生几乎从未被展示如何逐步应用抽象的论证理论或通用的分析方法来重构或映射杂乱的源文本。
因此,明确且有针对性的语料库抓取和文献研究是否能产生足够大且多样化的微调数据集,远不清楚。
4. Argdown 论证分析是一个复杂的问题,需要协调执行多样且困难的子任务。
论证分析并非单一、明确的自然语言处理任务。
如果我们将摘要、NLI 和 RTE、分类、多步问答、改写、形式化等比作地基、屋顶、管道、电气安装、保温或油漆,那么分析论证更像是建造一整栋房子。
一位熟练的论证分析师:
- 将全面的论证分析分解为目标明确、成功标准具体的任务,
- 可靠地执行语言和逻辑子任务(从文本标注到 FOL 形式化),
- 通过适应性规划有效协调分析论证所涉及的子任务,
- 同时在整个分析过程中评估和监控重构的整体质量。
因此,大型语言模型将必须接受大量基本批判性思维任务的训练,并且必须能够批判性地评估给定的分析状态,并进行提前规划。
5. 没有明确的对错之分。
论证分析是理性重构。分析师提取、澄清并将其推理呈现为透明且正确的论证。重构的质量主要由两个问题决定:
- 论证重构是否忠实于源文本(解释学充分性)?
- 论证重构是否逻辑正确且在认知上合理(系统充分性)?
现在我们可以明白为什么在重构论证时没有金标准或真实情况:
- 我们缺乏关于解释的忠实性,或论证的逻辑正确性和认知合理性意味着什么的学术共识。
- 因此,没有关于解释学和系统充分性的约定操作化定义。
- 即使解释学和系统充分性被仔细规定并能明确评估,这两个标准通常也会相互矛盾(更忠实意味着更不合理,反之亦然),在平衡标准时留下了酌情处理的空间。
- 同样,解释学和系统充分性都包含许多不同的子标准(例如,相关性、推理有效性、清晰度),这些子标准在评估重构质量时应用于重构的不同部分(例如,每个前提可能与科学共识相关、一致或矛盾;也可能不相关)。这要求对标准进行权衡,并进一步增加了评估的灵活性和逻辑分析的整体不确定性。
6. 人类在这方面也并非擅长。
认知科学家们对于人类到底有多不理性存在分歧,这正是“理性大辩论”的焦点。
二十多年来教授批判性思维和逻辑论证分析,让我成为一个怀疑论者:学生和学者(包括我自己)都不擅长提出正确的论证,在有争议的辩论中苦苦挣扎,并且通常无法评估、反思、澄清和改进他们的论证。(有趣的是:邓宁-克鲁格效应最初似乎是在批判性思维任务中发现的。)
批判性思维测试的实证数据似乎证实了我的个人经验。如果感兴趣,请参阅 Fabio Paglieri 的讨论以作进一步阅读。
因此,大规模收集人类反馈也不一定能提高大型语言模型的论证能力。
总而言之,构建 Argunauts 的挑战在于教大型语言模型一种方法,
- 这种方法涉及一种它们完全不熟悉的语义丰富的标记语言,
- 它们几乎没有亲眼见过其执行过程,并且
- 需要复杂的协调和规划
——所有这些都不能依赖于
- 现有的大量且多样化的教科书和演示语料库,
- 假设任何给定重构任务都存在真实结果,并且
- 诉诸于(众包)人类反馈。
背景与相关工作
我正在重新审视之前关于使用大型语言模型进行论证分析的研究,特别是 DeepA2 项目,在该项目中,Kyle Richardson 和我描述了一个用于使用多用途序列到序列模型实现复杂论证分析的通用框架。您可以在DeepA2 论文中找到大量与构建 Argunauts 相关的指针和参考文献。
Argunauts 旨在弥合自然语言和符号推理之间的差距。近年来,这已成为一个引人入胜的领域——特别是在数学推理、证明和 Lean 方面。我在这里的重点将是教大型语言模型形式化和逻辑语义分析,将这个问题框定为解释、理解和理性重构论证文本所需的子任务。
当然,还有强大的 AI 和论证社区,他们在过去十年中一直在培养论证挖掘领域。我认为论证挖掘,理解为论证文本标注,是分析和重构复杂论证中一个特定且潜在有用的子任务。
总纲
鉴于目标和挑战,我的初步策略是:
- 以 Tülu 3 等多步骤后期训练流程作为概念起点。
- 遵循 《教科书是你所需要的一切》,生成大量合成数据集,其中包含协调的、多步骤的批判性思维和逻辑分析任务演示。
- 将首次 SFT 后期训练步骤概念化为持续预训练,旨在使大型语言模型熟悉 Argdown 语法和语义。
- 通过(在线)DPO 反复从高质量示例中学习,避免记忆。
- 构建基于 Argdown 解析器的工具和多样化验证器,以进一步迭代 RLVR。
- 保持训练方法简单直接,偏离并简化现有设计。
- 在训练人工智能时,尽量从大学和学校批判性思维教学经验中吸取经验。
- 慷慨地混合通用指令遵循和推理数据,以保留现有技能。
- 建立高级批判性思维/论证分析基准以跟踪性能。
- 开放科学和开源。
- 邀请其他人加入(但如果没有人跟随,也不要沮丧)。
资源
欲了解更多信息,部分内容已在上方链接:
- Argdown.org: 示例、文档、教程、沙盒
- “分析实践论证” (G Brun 和 G Betz),收录于《政策分析中的论证转向。不确定性推理》。施普林格出版社。
- 介绍 DeepaA2 的博客文章
- “生态论证技术的呼吁” (F Paglieri) 《哲学与技术》。