世界语作为概念基语——迈向可审计数学推理的中间表示设计

Phaenarete ASI Lab 2026 年 8 月 3 日

摘要

机器迈向可靠数学推理的关键瓶颈，往往不在推理层，而在理解层。2025年至2026年间，自动定理证明取得了爆发式进展：Seed-Prover在IMO 2025上以六题中五题正式验证的成绩达到金牌水平，在MiniF2F基准上达到99.6%的正确率，该基准已趋于饱和；DeepSeekMath-V2在Putnam 2024上得分118/120。推理层的天花板正在快速逼近。然而，自动形式化——将自然语言数学问题映射为形式化陈述——仍然面临根本困难。Zhang等（2025）在EMNLP 2025发表的研究表明，数学定义的形式化远比基准测试更具挑战性，模型在自我纠错和与数学库对齐方面仍然困难。Shi等（ICLR 2026）明确指出，现有方法"缺乏可靠的语义一致性检查来确保形式化代码准确保留原始语句的含义"。

正是在这一背景下，本文提出一个工程假说：在自然语言与形式语言之间，引入一种以世界语为基语的受控中间表示EFS，可能有助于把"问题被理解成了什么"这一原本隐藏在模型内部的过程，转化为人类可审计、错误可定位、歧义可记录的语言对象。这一方案并非孤例——MALINCA项目（2025）同样明确提出"使用受控自然语言作为中间表示，辅以自动定理证明器验证人类规模的证明步骤"。

本文不主张世界语已经经验验证为最优中间语言，也不主张世界语本身无歧义；相反，我们明确指出世界语在宾格、词缀、句法辖域等方面仍存在不可消除的歧义，并据此将主张收紧为：世界语是一种低歧义负荷的基语，其形态规则性使在其上定义受控子语言的成本较低，且结果在有限学习时间内仍可保持人类可读。PNAS（2025）发表的功能性磁共振成像研究为此提供了独立的神经科学支持：世界语理解激活与自然语言相同的大脑区域，而非数学或编程语言区域——这意味着审计者的认知转换成本可能低于从形式证明迹进行审计的成本。

文章首先给出可靠推理的最小工作单元——概念三元组，其中表面形式是接口，推理规则定义操作语义，验证条件是连接二者的闸门。随后，我们以一道可完全核验的诊断题说明：模型可能在推理规则正确的情况下，错误绑定验证条件，并产生形式上无懈可击、实质上完全错误的解答。APOLLO（NeurIPS 2025）的实证数据为这一诊断提供了量化锚点：通用模型在直接形式化上的准确率仅3–7%，经编译器引导修复后跃升至40%以上——这说明即使Layer 2的修复能力极强，Layer 1的初始质量仍然严重制约端到端性能。

进一步，本文给出EFS的受控语法设计、词表策略、编译管道、审计日志格式，以及候选枚举与往返一致性检验两项防御机制。LoC-Decomp（ICLR 2026）提出的"语义一致性检查器"可视为后一机制的外部验证——该工作通过分治-合并策略检测形式化与原始语句之间的细微不一致，在PutnamBench上达到93%的成功率。最后，我们预注册六条可证伪预测，明确证伪阈值与实验协议，并列出本文可能出错的方式、伦理风险与部署边界。

本文的核心结论不是"世界语已经解决了数学推理问题"，而是：当推理层的能力已接近甚至超越人类金牌选手时，理解层错误的不可审计性正变得更加紧迫。机器可以在推理上赢过人类，却仍然可能在"理解题意"这个最基础的环节上犯错——而目前没有任何机制能告诉我们它错在哪里。以世界语为基语的受控中间表示，是填补这一机制缺口的一个值得严格检验的工程方案。

1 引言：当推理层逼近天花板，理解层成为瓶颈

1.1 2026年的数学推理图景

2025年至2026年间，AI在数学推理上的进展改变了我们对"机器能否做数学"这一问题的理解。Seed-Prover在IMO 2025上以六题中五题正式验证的成绩达到金牌水平，在MiniF2F基准上达到99.6%的正确率——该基准已趋于饱和——并于九小时内解决了Putnam 2025竞赛十二题中的十一题。DeepSeekMath-V2在Putnam 2024上得分118/120。这些数字意味着：在已形式化的数学推理任务上，机器的能力正快速逼近甚至超越人类顶尖选手。

然而，这些成就并不能回答一个更基础的问题：机器是否真正"理解"了它要解决的数学问题？或者换一种更精确的提问方式：当机器把一道自然语言表述的数学题转化为形式证明时，它是否可能在转化的第一步就犯了错，而后续所有严密的推理都在为这个错误服务？

1.2 两类数学推理失败

答案取决于我们如何区分两种不同类型的失败。

第一类，系统在推理层犯错。它误用规则——除以可能为零的量，或在前提不满足时调用引理。这种失败发生在推理链内部，现代证明助手已能相当可靠地捕获它。2025–2026年的进展主要攻克的是这一类问题。

第二类，系统在理解层犯错。它将"过点A作曲线的切线"读作"在点A处作曲线的切线"，随后无懈可击地执行所有代数操作。每一步均有效。验证器通过。答案错误。

第二类失败不是边缘案例。它是形式验证尽其所能之后仍然存在的残余类——因为验证器无法验证自己的输入。这不是实现缺陷，而是定义边界：证明可靠性是"前提到结论"映射的性质；关于"世界到前提"的映射，它本身不置一词。

2025–2026年的研究进展从多个角度佐证了这一判断。Zhang等（2025）在EMNLP 2025发表的获奖研究表明，数学定义的形式化远比基准测试更具挑战性，模型在自我纠错和与数学库对齐方面仍然困难——即使推理能力大幅提升，从自然语言到形式语言的映射仍然是核心瓶颈。Shi等（ICLR 2026）明确指出，现有方法"缺乏可靠的语义一致性检查来确保形式化代码准确保留原始语句的含义"。PROOFFLOW（2025）的报告更为直接：其系统在本科数学问题上仅达到37.5%的句法准确率，而此前在中学数学上仅为6.10%——即使形式化技术提升六倍，语义错误仍占主导。

本文的工程主张建立在这一诊断之上：当错误发生在问题被理解这一层时，任何下游的严格性都无法补救它。验证器只能验证它被给定的东西。

1.3 本文的核心命题

我们提出以下命题，并将其理解为设计假说，而非已经验证的结论：

在自然语言与形式语言之间，以世界语为基语的受控中间表示EFS，可能是一种成本较低、歧义负荷较低、审计透明度较高的中间表示。它有助于把"概念如何被实例化"这一隐藏过程，转化为可编译、可验证、可被非形式逻辑专家审阅的语言对象。

这一假说可进一步拆分为三个可检验子命题：

第一，理解层瓶颈假说。在当前大语言模型数学推理中，理解层错误是一类重要且常被忽视的残余错误源。APOLLO（NeurIPS 2025）的数据为此提供了量化锚点：通用模型在直接形式化上的准确率仅3–7%，经编译器引导修复后跃升至40%以上——说明即使Layer 2的修复能力极强，Layer 1的初始质量仍然严重制约端到端性能。

第二，受控世界语假说。在高中数学等受限领域内，以世界语为基语的受控语言能够以较低成本显式化部分关键语义承诺。MALINCA项目（2025）同样明确提出"使用受控自然语言作为中间表示，辅以自动定理证明器验证人类规模的证明步骤"，表明这一方向并非孤例。

第三，可审计性假说。相对于形式证明迹，EFS审计日志可能更容易被学科教师理解、定位和纠错；相对于受控英语，它可能减少一种特定的认知陷阱——我们称之为"透明性幻觉"。PNAS（2025）发表的fMRI研究为这一假说提供了独立的神经科学支持：世界语理解激活与自然语言相同的大脑区域，而非数学或编程语言区域，这意味着审计者的认知转换成本可能低于从形式证明迹进行审计的成本。

本文不主张世界语是"天然最优"的语言，也不主张世界语本身无歧义。世界语之所以进入我们的工程视野，是因为它的形态规则性使某些语义承诺更容易被强制写入表层形式。它不是推理的终点，而是一种可能的"概念座架"：使概念的推理结构从隐匿转为可见。

1.4 本文在专栏中的位置

赫尔墨斯计算语言学专栏始于一个追问：当机器开始言说，信任与意义何处安放？随后，专栏给出了理论地基：Token的限度、概念三元组、语义信息论框架，以及对自回归生成方法论的批判。

本文是这一序列的第三篇。它试图把抽象定义的"概念"，操作化为一种具体的、可编译的、人类可读的语言实体。世界语在这里不是被崇拜的对象，而是被检验的工具。它是否胜任，最终不取决于语言美学，而取决于实验、审计与部署反馈。

2 地基：为什么推理单元必须从Token上升到概念

2.1 Token的角色与限度

Token是分词器词表中的最小索引单元。它的身份由训练语料中的共现分布决定，而非由指称或真值条件决定。自回归生成中，每个Token是模型对下一个符号的条件概率分布的一次采样。序列的"连贯性"仅意味着该序列在该分布下具有较高典型性，而不必然意味着逻辑一致性。

最关键的是：Token本身不承载证明义务。一个Token序列可以同时是语法合法、语义连贯、在训练分布中高概率的，而且是逻辑错误的。

由此得到一个工程结论：Token可以作为输入输出接口，但不能单独作为可靠推理的最小责任单元。

这不是对大语言模型的全盘否定。大语言模型可以生成候选概念、提出证明草稿、补全形式化片段、解释错误、辅助审计。问题在于：如果最终推理责任仍停留在Token概率层面，而没有进入可执行、可验证、可审计的符号结构，那么系统就无法区分"听起来正确"与"被证明正确"。

因此，攻击点不是优化Token的生成质量，而是替换推理的基本责任单元。

2.2 概念三元组

可靠推理的最小工作单元应当是概念。为工程起见，我们将概念定义为三元组：

\mathcal{C} = (\mathcal{S}, \mathcal{R}, \mathcal{V})

其中， $\mathcal{S}$ 是表面形式——概念的自然语言表达或符号表达，它是接口，不单独锚定概念同一性。 $\mathcal{R}$ 是推理规则——概念的操作语义：它可以参与哪些推理步，在什么条件下可引入或消去。 $\mathcal{V}$ 是验证条件——将概念实例化到具体对象上时必须满足的条件。 $\mathcal{V}$ 是 $\mathcal{S}$ 与 $\mathcal{R}$ 之间的闸门：唯有 $\mathcal{V}$ 被满足， $\mathcal{R}$ 才对该对象生效。

在工程实践中，我们采用如下同一性判据：两个表面形式是否表达同一概念，主要看它们是否绑定到同一组推理规则与同一组验证条件。这一判据并不试图解决全部哲学意义上的概念同一性问题。它只服务于一个工程目标：让机器和人类能够判断，某个表达式是否被正确地纳入了证明义务体系。

世界语之所以进入这一框架，是因为它有可能降低从表面形式到验证条件的映射成本。若一门语言能够使其表面形式与验证条件之间的映射趋于清晰，则概念实例化错误就更可能被看见、被定位、被纠正。

2.3 诊断题：当概念实例化错误不可见

我们用一个可完全核验的诊断题说明本文所针对的失败类型。

D-1. 已知曲线 $C: y = x^3 - 3x$ ，点 $A(1, -2)$ 。过点 $A$ 作曲线 $C$ 的切线，求所有切线的方程。

注意 $f(1) = 1 - 3 = -2$ ，因此 $A$ 在曲线 $C$ 上。这正是陷阱所在。

读法甲：切线经过 $A$ ，切点待定。解得两个切点 $s \in \{-1/2, 1\}$ ，对应两条切线： $y = -2$ 和 $y = -\frac{9}{4}x + \frac{1}{4}$ 。

读法乙：切点就是 $A$ 。由于 $f'(1) = 0$ ，唯一切线为 $y = -2$ 。

在非正式模型探测中，多个前沿推理模型在中文提示下倾向于采用读法乙：它们验证 $A$ 在曲线上，计算 $f'(1)=0$ ，给出 $y=-2$ ，然后停止。每一步代数操作都正确。失败发生在第一句话被读入的时刻；此后轨迹中没有任何一步能够侦测到它。

这正是概念实例化错误的典型样本。模型取到了正确的表面形式（"切线"），也取到了正确的推理规则（切点在曲线上、斜率等于导数值），却错误绑定了验证条件：哪个点是切点，哪个点只是经过点。

这类错误具有三个特征。第一，不可由下游发现——读法乙的解答内部自洽，任何只检查前提到结论有效性的验证器都会通过它。第二，不因模型规模提升而自动消失——"过点A作曲线的切线"的误读风险来自表达与情境的交互，而非单纯模型能力不足。第三，在自然语言中难以局部定位——若最终答案错误，回溯机制很难机械指出是哪一个词元承担了错误承诺。

PROOFFLOW（2025）的研究为这一诊断提供了外部佐证：即使形式化技术从6.10%提升至37.5%，语义保持不良仍然是形式化的主要瓶颈。问题不只是"模型理解错了"，而是：错误没有留下可供审计的表面痕迹。

2.4 神经模型提议，符号系统裁决

"预测下一个概念"与"预测下一个Token"不是同一类计算问题。Token序列的概率分布是所有Token上的分布，统计学习可以逼近其中的规律。概念序列则不同：在给定推理上下文和目标结论的条件下，从一个概念到下一个概念的迁移合法性由推理规则决定。许多概念组合在逻辑上不是低概率，而是不可能。

因此，本文并不主张神经模型不能生成概念候选。相反，神经模型非常适合生成候选。关键在于：候选必须由可执行的推理规则引擎裁决，必须由验证器检查，必须由审计日志记录。

APOLLO（NeurIPS 2025）的工作为这一架构提供了独立验证：通过Lean编译器引导的LLM输出修复，通用模型的准确率从3–7%提升至40%以上，在miniF2F上达到84.9%。这恰好说明了"神经模型提议、符号系统裁决"范式的有效性——神经模型提出形式化草稿，编译器捕获并修复错误，二者协作而非替代。

换言之：神经模型可以提议，符号系统必须裁决，人类审计者必须能够看见裁决依据。混淆"提议"与"裁决"，是当前方法论中的一类范畴错误。

2.5 歧义负荷的度量

设 $U$ 为待表达的语义状态， $\tilde U$ 为其语言表面形式。歧义负荷的合理度量不是表面形式自身的熵，而是条件熵：

\mathcal{L}_{\text{ambig}} = H(U \mid \tilde U)

由信息论恒等式 $H(U) = I(U; \tilde U) + H(U \mid \tilde U)$ 可知，降低歧义负荷等价于提高表面形式对语义状态的互信息。

这一框架给出三点后果。第一， $\mathcal{L}_{\text{ambig}}$ 可以有经验估计量：令多个独立形式化器对同一表面形式产出形式化结果，并按语义等价类聚类，其经验分布的熵即为估计值。对D-1的某些中文表述，该分布在两个读法上分裂，熵接近1 bit；中间表示的设计目标，是在受控语言层面使该熵趋近0。第二，正确优化框架不是无限展开，而是率失真优化：在描述长度预算约束下最小化条件熵。第三，任何表面语言都有其射程——世界语或EFS能够减少的，主要是来自句法、形态和论元角色的那部分歧义负荷；来自省略的领域约定、缺失的背景知识的那部分歧义，不在任何中间语言的单独射程之内。

LoC-Decomp（ICLR 2026）的工作可视为这一理论框架的操作化实现：它通过分治-合并策略检测形式化与原始语句之间的细微不一致，在PutnamBench上达到93%的成功率。该工作与本文EFS的"往返一致性检验"防御机制在目标上高度一致。

3 世界语的逻辑解剖：真实性质与不可回避的反例

本章是全文最需要克制的地方。我们不再主张"世界语无歧义"——该主张不成立，且任何具备世界语知识的读者都可以迅速指出反例。本文的技术主张必须被收紧为：世界语是一种低歧义负荷的基语，它的形态规则性使在其上定义受控子语言的成本较低，并使结果在有限学习时间内仍对人类可读。确定性来自我们施加的受控语法，不来自世界语自身。

3.1 三项真实成立的形态学性质

宾格标记有助于锚定核心论元角色。 世界语名词以-o结尾，直接宾语强制添加-n。因此，在简单句中，施事与受事角色可由形态标记而非词序单独决定。两句"狗咬人"与"人咬狗"的语义差异主要由形态承担。对受控语言设计而言，这意味着论元角色可以被较早、较稳定地识别。在概念三元组视角下，这有助于把验证条件中的角色绑定从推断问题转化为识别问题。

相关词表使部分否定辖域词汇化。 世界语的相关词系统使某些否定辖域在词形上分离。"都不是"与"不都是"在中文中只差一个字，却对应不同辖域，在学生作答和模型输出中容易被混淆。世界语中，这两个辖域由不同词项承担，因此表面承诺更显式。

词缀派生具有较强的组合性。 世界语词缀可在一定程度上视为作用于词根的函数。从"健康"出发，通过词缀叠加可以得到"不健康""不健康的人""病人所在场所""康复"等一系列概念。在最小描述长度意义上，这种派生系统允许用较少基本部件表达较多概念。对受控词表设计而言，这意味着高频组合概念可以保留透明性，而不必为每个新概念单独枚举词条。

Oya（2025）发布的通用依存树库和Bick（2025）发布的标注错误语料库表明，世界语的自然语言处理基础设施正在迅速扩展。这些资源为EFS的数据驱动开发提供了底层支持。

3.2 四处反例：世界语不是无歧义语言

以下反例必须明确交出。

反例一：宾格不是纯粹的受事标记。 宾格标记-n不仅标记直接宾语，也标记方向（进入房间）、度量（停留了三天）等。因此，"见到-n即推断为受事"不是安全规则。

反例二：-um-是明文规定的无固定意义词缀。 《世界语基础》本身承认-um-没有固定语义。衣领、履行、感冒——这些意义不能由词根和词缀机械推导。

反例三：词缀组合透明，指称仍依赖约定。 "切割工具"的组合语义既可以指刀，也可以指锯或剪刀。"病人所在场所"既可以指医院，也可以指检疫营。最终意义由语言共同体约定，而非由规则单独决定。此外，复合词的括号化本身也可能产生结构歧义。

反例四：句法歧义仍然保留。 世界语仍然具有自然语言常见的句法歧义，包括介词短语附着、量词辖域、并列结构辖域、动词及物性约定等。因此，世界语并不因为形态规则性而自动成为无歧义语言。

3.3 把主张改窄，论证反而变强

上述反例并不摧毁本文。它们摧毁的是过度宣传，而不是工程假说。

本文的正确主张应是：世界语是一门低歧义负荷的基语。它的形态规则性使得在其上定义一个确定性受控子集的成本较低，同时使结果在有限学习时间内对人类保持可读。

世界语提供的是三项工程优势：形态标记有助于显式化论元角色；词缀系统有助于降低受控词表构造成本；规则性有助于减少受控语法设计中的例外处理。但这些优势必须通过实验比较来检验。它并不自动意味着世界语优于受控英语、受控汉语、逻辑语或自定义数学DSL。

4 EFS：以世界语为基语的受控语言

4.1 EFS的三条设计律

EFS不是自然世界语，而是世界语的一个受控子集。它由三条设计律定义。

设计律一：词表封闭。 EFS只使用预先审定的封闭词表。在高中数学域，目标词表规模约为500–800词条。每个词条绑定唯一的形式语义。开放派生被禁止——这直接针对世界语自身的反例：禁止自由使用-um-，禁止未经审定的词缀派生，禁止约定性指称进入核心推理词表，禁止复合词括号化自由扩展。

设计律二：句型封闭。 EFS只允许有限条句型模板。每条模板对应一条确定性编译规则。介词短语附着位置由模板固定，而非由解析器自由猜测。这消除了大量PP附着歧义。

设计律三：量化与角色显式。 所有量词必须显式表达。所有几何关系由指定介词标记，并建立介词到角色的单射——trapasi表示经过，tanĝi ĉe表示在某点处相切，kuŝi sur表示位于其上。

在这些设计律下，EFS的受控片段可被设计为确定性可解析。需要强调的是：这是受控片段的性质，不是自然世界语的性质。

4.2 EFS对诊断题D-1的处理

D-1的两种读法可表示为：

EFS-甲
Trovu ĉiujn rektojn, kiuj trapasas la punkton A(1, −2)
kaj tanĝas la kurbon y = x³ − 3x.

求所有经过点A(1, −2)且与曲线y = x³ − 3x相切的直线。

EFS-乙
Trovu la rekton, kiu tanĝas la kurbon y = x³ − 3x
ĉe la punkto A(1, −2).

求在点A(1, −2)处与曲线y = x³ − 3x相切的直线。

这带来三项收益。

第一，验证条件被强制显式。trapasas表示直线经过某点，ĉe表示相切发生于某点。模型不能在不留下表面痕迹的情况下，把"经过"偷换为"在……处"。

第二，基数承诺被强制显式。甲式使用复数宾格ĉiujn rektojn（所有直线），乙式使用单数la rekton（那条直线）。中文原题"求切线方程"对解的个数常常保持沉默——而D-1的陷阱恰恰在于满足条件的切线有两条。EFS通过数和格的一致关系，把隐含承诺转化为显式承诺。只有显式承诺可被审计。

第三，错误可定位到词元。如果验证失败，回溯机制可以指出失败源于某个具体词元。在中文原句中，往往没有一个形态单元能够稳定承担这一定位功能。

4.3 词表策略与透明度边界

词表封闭有代价。在高中数学域内，多数概念可由少量词根规则组合，最小描述长度优势成立。但进入高等数学后，若坚持全派生，会产生过长的复合词，违反描述长度预算。

因此，词表采用混合策略：高频组合概念使用词缀派生，保留透明性；高度专门化概念引入标准化词根，牺牲局部透明度，保全长度与句法刚性；所有词条绑定唯一形式语义，禁止开放扩展。这意味着EFS不追求"每个词都可从词根推出"，而追求"每个词都有唯一可编译语义"。

4.4 管道全景

我们设想的管道如下：

自然语言题目
   │
   ▼
Layer 1: 神经语义解析（NL → EFS）
   │        输出：带置信度的多个EFS候选
   ▼
EFS ───────────────────────────────► 人类审计接口
   │                                         ▲
   ▼ 确定性编译                              │
形式语言                                     │
   │                                         │
   ▼                                         │
Layer 2: 符号证明搜索                         │
   │                                         │
   ▼                                         │
Layer 3: 纯句法验证 ────► 审计日志（EFS）────┘
   │
   ├─ 通过 → 输出
   └─ 失败 → 回溯到EFS具体词元 → 要求Layer 1重译该子句

在这一管道中，EFS不是最终证明语言。证明搜索与验证仍在形式语言中完成。EFS的任务是：把理解层的承诺固定下来，并交给人和机器共同检查。

4.5 歧义转移问题与两项防御机制

最尖锐的反对意见是：将歧义自然语言翻译为无歧义EFS，本身需要数学理解力。如果Layer 1理解不足，它会自信地将歧义中文错译为精确EFS。自然语言是模糊地犯错，EFS是精确地犯错。这一问题无法被彻底消除，只能通过设计使其变得可检测。

防御一：候选枚举与置信度标定。 Layer 1不应只输出单点翻译，而应输出多个候选及其置信度。消歧决策从不可见的内部选择，转移为可见的外部分支。Layer 2可并行探索，Layer 3可裁决，审计者可看到候选及其置信度。需要注意的是，置信度本身必须经过校准——未校准的置信度会成为新的权威幻觉。

防御二：往返一致性定点检验。 由于EFS与形式语言之间的编译被设计为确定性双向映射，可执行定点检验：将EFS编译为形式语言，再反编译回EFS'，若二者在规范化意义下不一致，则触发告警。

该检验的价值在于：它只在受控语言中可执行。自然语言往返翻译不具有稳定定点性质，因此难以作为严格检验。但它也有明确边界：往返一致性不能检测"错误但自洽"的翻译。如果EFS忠实编译了一个错误理解，再反编译回同一EFS，往返检验仍会通过。因此，它只能检测编译不一致，不能替代语义正确性审查。

LoC-Decomp（ICLR 2026）提出的语义一致性检查器可视为这一机制的外部验证：该工作通过分治-合并策略检测形式化与原始语句之间的细微不一致。本文的往返检验与LoC-Decomp在目标上一致——都是在形式化之后设置一道语义审计关——但实现路径不同：LoC-Decomp依赖LLM自检，EFS依赖受控语言的确定性编译。

4.6 审计日志：歧义在案

一个修正后的审计日志示例如下：

[Paŝo 2] KONTROLO: aserto "A kuŝas sur la kurbo"
  DONITA:   f(x) = x³ − 3x ;  A = (1, −2)
  KALKULO:  f(1) = 1 − 3 = −2
  STATO:    VALIDA

[Paŝo 3] AVERTO: ambigueco en la originala fonta teksto
  KANDIDATO 1: la rekto TRAPASAS la punkton A       (fido 0.72)
  KANDIDATO 2: la rekto TANĜAS la kurbon ĈE A       (fido 0.24)
  AGO:      ambaŭ branĉoj estas serĉataj paralele

[Paŝo 7] KONTROLO: aserto "ekzistas ĝuste du tanĝaj rektoj tra A"
  BEZONATA: solvi 3s² − 3 = s² + s − 2
  RIMEDO:   faktorigo (2s + 1)(s − 1) = 0
  REZULTO:  s ∈ {−1/2, 1}
  STATO:    VALIDA

关键不在系统没有歧义，而在歧义被写入日志。这就是"歧义在案"：以词元粒度，以目标审计者可读的语域呈现。与之相对，失败的审计日志往往不是不可读，而是太可读：它流畅地认证了一个错误前提，却没有把错误承诺暴露为可质疑的对象。

4.7 可读性的诚实边界

EFS的可读性主张是相对主张，不是绝对主张。相对于形式证明迹，EFS可能更容易被学科教师理解。但深度嵌套量词在任何线性化自然语言中都会造成工作记忆负担。因此，本文将可读性主张限定于：推理深度不超过4、量词嵌套不超过2的高中数学常见命题与证明。超出该范围，审计日志应配合交互式展开、折叠、图示和证明树导航使用。

PNAS（2025）发表的fMRI研究为这一主张提供了独立的神经科学支持：世界语理解激活与自然语言相同的大脑区域（n=19），而非数学或编程语言区域。这意味着审计者在阅读EFS日志时，调用的仍然是日常语言处理能力，而不是专门的符号推理能力——这降低了从形式证明迹（如Lean）转向EFS审计的认知转换成本。至于教师需要多少世界语学习时间才能达到可用审计水平，目前无可信估计。该参数属于待测量项，不作为论据使用。

5 端到端可靠性：世界语只作用于理解层

5.1 贡献边界

端到端可靠性可分为两个阶段。Layer 1是理解层——将自然语言题目翻译为正确的形式化陈述。Layer 2是搜索层——从正确陈述出发找到证明。EFS的贡献主要在Layer 1。它不直接降低数学证明搜索的内在难度。推理的困难由数学结构决定，不因表示语言的语法特性而自动改变。

2025–2026年的进展使这一边界更加清晰。Seed-Prover在MiniF2F上达到99.6%，意味着在已形式化的推理任务上，Layer 2的正确率已接近天花板。然而，APOLLO的数据显示通用模型在直接形式化上的准确率仅3–7%——Layer 1与Layer 2之间存在一个巨大的能力落差。填补这一落差，正是EFS的定位所在。

因此：EFS优化的是"问题被正确理解"的概率，而不是"问题被正确解决"的概率。任何暗示世界语能提高数学推理能力的说法，都是范畴错误。

5.2 端到端可靠性分解

端到端正确率可写为全概率公式：解析正确时推理成功的概率乘以解析正确率，加上解析错误时仍碰对的概率乘以解析错误率。这是恒成立的恒等式，不需要任何独立性假设。

真正需要经验估计的，是解析正确率、解析错误但最终答案仍正确的概率，以及解析正确后证明成功率。在证明题中，解析错误后碰对的概率通常较低；在选择题或填空题中，它可能因猜测而升高。因此，该参数必须按任务类型分别测量。

APOLLO（2025）的数据可作为一个量化锚点：通用模型在直接形式化上的准确率从3–7%跃升至40%以上，经过编译器引导的修复。这一定量数据说明：即使Layer 2的修复能力极强，Layer 1的初始质量仍然严重制约端到端性能。

EFS的价值在于：它把解析正确率从一个隐藏在模型内部的不可控量，转化为可测量、可审计、可回溯的工程参数。

5.3 本文不作未经测量的数值外推

早期版本曾给出具体的数值估计。这些数字目前缺乏实验基础，属于理论外推，不应作为论文主张。本文撤回这些未经测量的数值承诺。

我们只承诺测量以下参数：歧义熵、解析正确率、审计者纠错率、审计者误报率、往返检验召回率、达到可用审计水平所需训练时间。在原型系统完成之前，任何具体数值都应被视为假说，而非结果。

6 预注册：可证伪的预测

6.1 待估量

本文定义以下待测量参数：歧义熵——多个独立形式化器对同一表面形式产出结果的语义等价类经验熵；解析正确率——产出形式化与专家标注在语义等价意义下一致的比率；审计者纠错率——目标审计者正确标记错误中间表示的概率；审计者误报率——目标审计者错误标记正确中间表示的概率；置信度—准确率差距——平均自报置信度减去纠错率；往返检验召回率——按错误类别分别报告。

6.2 预测与证伪阈值

P1：歧义熵。 EFS条件的歧义熵显著低于自然语言条件。证伪条件：差异不显著，或相对缩减小于30%。

P2：解析正确率。 NL→EFS→FL的解析正确率显著高于直接NL→FL。证伪条件：提升不显著，或绝对增益小于5个百分点。Zhang等（2025）的研究表明，数学定义的形式化比基准测试更具挑战性——因此检验需要区分"题目级形式化"与"定义级形式化"，EFS可能在后者上优势更明显，因为受控语言的词表封闭性直接针对"定义理解"这一难点。

P3：审计者纠错率。 EFS审计日志的教师纠错率显著高于Lean证明迹。证伪条件：差异不显著。

P4：透明性幻觉。 相对EFS，ACE受控英语表现出更低的纠错率和更高的置信度—准确率差距。证伪条件：两个分量均不显著，或符号反转。

P5：解析错误后的碰对率。 在证明题子集中，解析错误但最终答案正确的概率小于5%。证伪条件：实测值大于等于5%。

P6：往返检验召回率。 往返一致性检验对语义不匹配类错误的召回率不低于30%。证伪条件：召回率低于30%。

若P2与P3同时被证伪，则本文核心工程主张被推翻：EFS既未改善理解，也未改善审计。此时不应继续辩护。若P4被证伪，则世界语基语相对于受控英语的论证失效；更合理的推荐将变为使用受控英语，同时保留本文关于可审计中间表示的一般框架。

6.3 实验协议

实验一：歧义对抗集。 构建不少于100道高度依赖句法或语义歧义消解的题目，以D-1为种子题。所有题目标注金标准形式化，并报告标注一致性。比较五条路径：直接NL→FL、NL→EFS→FL、NL→Lojban→FL、NL→ACE→FL、交互式澄清基线。测量解析正确率、歧义熵、候选覆盖率和置信度校准误差。测试P1、P2。

实验二：审计者认知负荷。 高中数学教师随机分为三组，分别阅读Lean 4证明迹、中文伪代码证明和EFS审计日志。所有材料注入前提层错误。测量纠错率、误报率、阅读时间、错误定位准确率、NASA-TLX认知负荷，以及达到可用阅读水平所需世界语学时。测试P3与可读性边界。

实验三：透明性幻觉。 匹配内容分别以EFS与ACE受控英语呈现，注入语义错误。测量纠错率、误报率、自位置信度、置信度—准确率差距，以及受试对语言自然度与受控性的主观感知。参与者按英语母语状态分层，并预训练至统一标准。测试P4。

实验四：歧义转移量化。 在实验一的失败样本上分类NL→EFS错误，并测量解析错误但最终答案正确的概率，区分证明题与客观题。测试P5。

实验五：往返一致性。 注入形式化错误，按类型分类为句法错误、类型错误、非法项错误、语义不匹配错误和歧义转移错误。测量各类别的召回率和误报率。语义不匹配类是P6的主要对象；歧义转移类预期召回率接近零。测试P6。

所有人类参与者实验将使用经功效分析预先确定的样本量，目标功效为80%。代码、词表、对抗集与分析脚本将在实验前公开。

7 局限性与本文可能出错的方式

本文报告的所有量化主张均为预注册预测，而非已测量结果。EFS是原型规格，不是完整部署系统。非正式模型探测仅用于说明诊断题的价值，不构成模型普遍失败率的证据。

本文可能出错的方式至少有以下六种。

第一，EFS可能是有损环节。NL→EFS→FL的总错误率未必低于直接NL→FL。引入中间表示只有在NL→EFS比NL→FL更容易学习、EFS→FL几乎无损、且审计收益足以抵消额外工程成本时才划算。实验一的直接对比检验这一假设。

第二，端到端模型可能使中间表示多余。若未来模型在直接形式化上达到近天花板准确率，则中间表示的主要价值将只剩人类监督。我们判断，在教育、考试、辅导等场景中，监督不会是可选项。但这是关于制度与监管的预测，而不是关于模型能力的预测。

第三，可读性可能不转移。如果实验二发现教师达到可用审计水平需要数百小时，则EFS在基础教育系统中不可部署。此时更合理的方向可能是证明可视化、交互式解释或受控母语界面，而非世界语。

第四，中立性论据是道德性的，不是技术性的。世界语不属于任何民族国家，这一性质在技术效用函数中占零权重。我们不做道德折算，但也不放弃该考量：默认选择英语同样是一种语言政治选择，只是它常常不被体验为选择。

第五，世界语对非印欧语使用者可能更难学。世界语词汇以罗曼语和日耳曼语为主，并带有斯拉夫语形态句法影响。本文的公平性主张只是比较性的：世界语没有民族语言制度优势，并不等于它对所有人同等容易。

第六，交互式澄清可能更优。对部分歧义案例，系统直接询问用户"你是想求经过A的切线，还是在A处的切线"，可能比引入受控语言更经济。我们在实验一中纳入交互式澄清基线。

伦理与部署边界

一个可读但无效的审计界面，比没有审计界面更危险，因为它制造监督的幻觉。因此，本文坚持以下部署原则：在实验二完成之前，不应宣称EFS日志"可被教师可靠审计"；置信度必须经过校准，否则不得向审计者展示为权威数值；审计日志必须记录候选、分支、人类修改与最终执行路径；教育场景中的学生是受影响方，系统不应仅以"可解释"为名获得过度信任；语言选择必须承认世界语的印欧语偏见，不得包装为全球中立。

8 结语：桥的长度，要走过去才知道

2025年至2026年间，AI在数学推理上的进展令人瞩目。Seed-Prover在IMO 2025上以六题中五题正式验证的成绩达到金牌水平。DeepSeekMath-V2在Putnam 2024上得分118/120。MiniF2F基准已趋于饱和。推理层的能力正快速逼近甚至超越人类顶尖选手。

然而，这些成就不应让我们忽视一个更基础的问题。机器可以在推理上赢过人类，却仍然可能在"理解题意"这个最基础的环节上犯错——而目前没有任何机制能告诉我们它错在哪里。APOLLO的数据显示，即使是最先进的通用模型，在直接形式化上的准确率也仅3–7%。理解层与推理层之间，横亘着一个巨大的能力落差。

这正是本文全部工程主张的来源。赫尔墨斯第一次追问语言的归属。第二次搭建理论与架构的桥。第三次，他携来一座用语言砌成的桥。但这座桥不应被崇拜。世界语不是数学推理的终点，甚至不是推理语言本身——推理仍在形式语言中执行。世界语在这里只承担一个中间角色：使推理得以从自然语言的歧义地带，安全抵达形式语言的确定港口。

它是概念座架：使概念的推理结构从隐匿变为可见的方法论眼镜。

它只做一件事：把"问题被理解成了什么"这件本来发生在模型内部、不留痕迹、不可回溯的事，变成一行必须写下来、可以被一位高中教师读到、并且能被指着说"这个词错了"的文字。

如果机器要在教育场景中获得有限信任，它不能只展示答案，也不能只展示流畅解释。它必须交出理解过程。它必须允许人类指着某一行说：这里，你读错了。

这正是可信智能的技术含义之一。至于世界语是否真的能承担这一角色，不由修辞决定，而由词表、语法、实验、审计和失败案例决定。

桥已在此。它有多长、能否承重，要走过去才知道。

参考文献

2025–2026年关键进展

Chen, L., Gu, J., Huang, L., et al. (2025). Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving. arXiv:2507.23726.
Ospanov, A., Farnia, F., & Mohit, R. (2025). APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning. NeurIPS 2025.
Kung, P.-N., Song, L., Hwang, D., et al. (2026). LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks. arXiv:2606.03303.
Shao, Z., et al. (2025). DeepSeekMath-V2: Towards Expert-Level Mathematical Reasoning. Technical Report.
Zhang, L., Valentino, M., & Freitas, A. (2025). Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions. EMNLP 2025, pp. 1720–1738.
Shi, J., Zhang, Z., Ma, B., et al. (2026). LoC-Decomp: LLM Autoformalization via Logical Concept Decomposition and Iterative Feedback Correction. ICLR 2026.
Moakhar, A. S., Gholami, I., Springer, M., et al. (2026). Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics. arXiv:2607.
MALINCA Project (2025). Towards Autoformalization of Textbook Mathematics with Natural Proof Checking. MALINCA Kick-off Meeting, IHP Paris, Oct 2025.
ITP 2025. A Natural Language Formalization of Perfectoid Rings in Naproche. 16th International Conference on Interactive Theorem Proving (ITP 2025).

世界语计算语言学

Oya, M. (2025). UD Treebanks for Esperanto as a Natural Language. Association for Computational Linguistics.
Bick, E. (2025). An Annotated Error Corpus for Esperanto. Proceedings of the 9th Workshop on Constraint Grammar and Finite State NLP, pp. 1–8.
PNAS (2025). Constructed Languages Are Processed by the Same Brain Mechanisms as Natural Languages. PNAS.

数学推理基准

ArXivMath Benchmark (2026). MathArena.ai.
IMProofBench (2025). NeurIPS Datasets and Benchmarks 2025.

基础文献

Amodei, D., Olah, C., Steinhardt, J., Christiano, P., Schulman, J., & Mané, D. (2016). Concrete Problems in AI Safety. arXiv:1606.06565.
Bender, E. M., & Koller, A. (2020). Climbing towards NLU: On Meaning, Form, and Understanding in the Age of Data. ACL.
Bowman, S. R., et al. (2022). Measuring Progress on Scalable Oversight for Large Language Models. arXiv:2211.03540.
Cappelen, H. (2018). Fixing Language: An Essay on Conceptual Engineering. Oxford University Press.
Cover, T. M., & Thomas, J. A. (2006). Elements of Information Theory (2nd ed.). Wiley.
Cowan, J. W. (1997). The Complete Lojban Language. Logical Language Group.
de Moura, L., & Ullrich, S. (2021). The Lean 4 Theorem Prover and Programming Language. CADE.
Fuchs, N. E., Kaljurand, K., & Kuhn, T. (2008). Attempto Controlled English for Knowledge Representation. Reasoning Web.
Jacovi, A., & Goldberg, Y. (2020). Towards Faithfully Interpretable NLP Systems. ACL.
Jiang, A. Q., et al. (2023). Draft, Sketch, and Prove. ICLR.
Kuhn, T. (2014). A Survey and Classification of Controlled Natural Languages. Computational Linguistics.
Lightman, H., et al. (2024). Let's Verify Step by Step. ICLR.
Margolis, E., & Laurence, S. Concepts. The Stanford Encyclopedia of Philosophy.
Nosek, B. A., et al. (2018). The Preregistration Revolution. PNAS.
Piantadosi, S. T., Tily, H., & Gibson, E. (2012). The Communicative Function of Ambiguity in Language. Cognition.
Rudin, C. (2019). Stop Explaining Black Box Models for High Stakes Decisions. Nature Machine Intelligence.
Tarski, A. (1956). The Concept of Truth in Formalized Languages. In Logic, Semantics, Metamathematics. Oxford University Press.
Turpin, M., et al. (2023). Language Models Don't Always Say What They Think. NeurIPS.
Wu, Y., et al. (2022). Autoformalization with Large Language Models. NeurIPS.
Zamenhof, L. L. (1905). Fundamento de Esperanto. Hachette.
Zheng, K., et al. (2022). miniF2F: A Cross-System Benchmark for Formal Olympiad-Level Mathematics. ICLR.