Each language version is independently generated for its own context, not a direct translation.

这篇论文讲述了一个非常实用的教育技术难题：如何自动给数学课（特别是逻辑证明题）出题，并且保证出的题目难度“差不多”？

想象一下，你是一位数学老师，每天要花大量时间手写出证明题。你想用电脑自动出题，但电脑有个大毛病：它要么出的题太简单（像 $1+1=2$），要么太难（像解天书），而且它不知道“难”和“易”的界限在哪里。

这篇论文就是为了解决这个问题，提出了一套**“自动出题且难度可控”**的魔法。

核心比喻：把证明题变成“乐高积木”

为了理解这个方法，我们可以把数学证明想象成用乐高积木搭城堡。

1. 传统方法的困境：只看积木数量

以前的自动出题系统，就像是一个只看“积木数量”的机器人。

如果题目里有 3 个积木，它觉得很简单。
如果题目里有 10 个积木，它觉得很难。
问题在于：有时候，用 3 个特殊形状的积木（比如带齿轮的）搭出来的结构，比用 10 个普通方块搭出来的还要难！只看数量（语法结构）无法真正反映学生解题时的脑力消耗（证明复杂度）。

2. 这篇论文的解决方案：看“搭法”和“规则”

作者提出了一种新方法，不再只看积木有多少，而是看**“搭这个城堡需要遵循什么规则”以及“需要动多少步”**。

他们发明了一套**“无逻辑符号的专用规则书”**（Theory-specific rules）。

普通逻辑：就像用通用的乐高说明书，里面充满了复杂的术语（“如果 A 且 B 则 C"）。
专用规则：作者把这些复杂的术语“翻译”成了学生熟悉的、没有生僻符号的**“操作指令”**。
- 比如，在集合论里，不再说“对于所有 x，如果 x 属于 A 且 x 属于 B..."，而是直接变成一条简单的指令：“如果你看到 $x$ 在 $A$ 和 $B$ 的交集里，你就知道 $x$ 在 $A$ 里，也在 $B$ 里。”
- 这就像把复杂的乐高说明书，简化成了“第一步放这块，第二步放那块”的直观步骤。

3. 如何控制难度？（核心魔法：同构证明）

这是论文最精彩的部分。他们定义了一种叫**“证明同构”（Proof-isomorphic）**的概念。

比喻：
- 题目 A：用红色积木搭一个塔。
- 题目 B：用蓝色积木搭一个塔。
- 如果搭这两个塔所需的步骤完全一样（先放底座，再放中间，最后封顶），只是颜色（具体的数学符号）不同，那么这两个题目在“脑力消耗”上就是一模一样的。
电脑怎么做？
1. 老师先给电脑一个**“标准题目”**（比如：证明集合 A 和 B 的交集包含于 A）。
2. 电脑用上面的“专用规则”把这个题目拆解，算出它需要几步，每一步用了什么规则。这就得到了一个**“标准搭建蓝图”**。
3. 然后，电脑开始“换皮”：它保持“蓝图”不变，只是把里面的符号（比如把“交集”换成“差集”，把“属于”换成“包含”）进行替换。
4. 只要替换后的题目能套用同一个“蓝图”（即证明步骤结构完全一致），电脑就认为：“这道新题和原题难度相当！”

4. 为什么要这么做？（教育意义）

个性化教学：老师可以一键生成 10 道难度完全一样的题。如果学生做错了，老师可以立刻换一道“同难度”的题让他再练，而不是换一道可能突然变难或变简单的题。
公平性：在自适应考试（根据学生表现动态出题）中，系统可以精准地控制难度阶梯，不会因为题目结构不同而误判学生的水平。
解放老师：老师不再需要绞尽脑汁想“这道题会不会太难”，系统会自动保证生成的题目都在同一个难度层级上。

总结

这篇论文就像给自动出题系统装上了一个**“难度校准器”**。

它不再数题目里有多少个词，而是深入分析解题的“思维路径”。通过把复杂的逻辑证明转化为简单的“操作指令”，并寻找那些**“思维路径完全一致”**的新题目，它成功实现了：让电脑像经验丰富的老教师一样，知道什么样的题目对学生来说“难度相当”。

一句话概括：
这就好比电脑不再只是随机发给你不同颜色的乐高积木，而是确保你每次拿到的积木，都能用完全相同的步骤搭成一座城堡，从而保证你每次练习的“脑力强度”都是精准可控的。

Each language version is independently generated for its own context, not a direct translation.

论文技术总结：基于证明复杂度的自动化证明习题生成方法

1. 研究背景与问题 (Problem)

背景：自动习题生成（Automatic Question Generation, AQG）旨在减轻教师手动设计习题的负担。然而，将自动化技术整合到教学实践中的主要障碍在于难以控制生成习题的难度。
核心问题：

现有的 AQG 工具缺乏对“证明复杂度”（proving complexity）的细粒度控制。
现有的难度控制方法（如基于文本的机器学习预测、基于命题逻辑的句法结构参数）存在局限性：
- 机器学习方法：依赖人工标注，存在主观不一致性，且缺乏可解释性。
- 句法结构方法：仅关注公式的抽象结构（如原子数量、连接词深度），忽略了实际证明过程中的逻辑步骤和策略。两个句法结构相似的公式，其证明难度可能截然不同。
在形式化领域（如一阶逻辑、离散数学），缺乏一种基于证明结构本身来量化和比较习题难度的有效方法。

2. 方法论 (Methodology)

本文提出了一种针对一阶语言（特别是离散数学课程中的集合论和数论）的自动化证明习题生成方法。该方法的核心思想是：两个习题具有可比的证明复杂度，当且仅当它们的最小证明在“推导同构”（deductive isomorphism）意义下是相同的。

2.1 理论基础：基于切割的特定理论表列 (Cut-based Theory-specific Tableaux)

特定理论证明 (Theory-specific Proofs)：为了模拟学生非形式化的证明过程（通常不显式使用逻辑符号），作者引入了不含逻辑符号（如 $\neg, \land, \to$ ）的表列证明。
定义理论 (Definitional Theories)：通过定义理论 $\langle L, Ax, < \rangle$ 来刻画数学理论片段（如集合论）。其中 $Ax$ 是定义公理， $<$ 是谓词符号上的良基关系。
规则提取 (Rule Extraction)：
- 将定义公理转换为规则蕴含范式 (RINF)： $(l_1 \land \dots \land l_{n-1}) \to l_n$ 。
- 从 RINF 公式中提取特定理论规则 (Theory-specific Rules)。这些规则是线性的（单结论），且满足三个解析限制：
  1. 结论中的变量必须出现在前提中。
  2. 结论中的谓词符号在 $<$ 关系下小于至少一个前提中的谓词符号。
  3. 若谓词符号相同，则结论公式的深度必须小于前提。
- 这种设计确保了证明过程的解析性（analyticity）和终止性。
切割规则 (Cut Rules)：引入基于“次要共前提”（minor co-premise）的切割规则，允许在证明中引入中间步骤，同时保持证明的有限性。

2.2 证明复杂度的形式化定义

推导同构 (Deductive Isomorphism)：
- 不仅比较表列树的结构，还比较证明树 (Justification Trees) 的结构。
- 两个证明是推导同构的，如果它们之间存在一一对应，使得对应的分支具有同构的证明树，且节点上的公式是句法同构的（抽象结构相同且变量集相同）。
最小证明 (Minimal Proof)：在给定规则集下，具有最小“推导大小”（节点总数）的干净（clean）证明。
复杂度可比性：两个习题集 $SF_1$ 和 $SF_2$ 具有可比的证明复杂度，如果它们存在最小证明 $P_1$ 和 $P_2$ ，且 $P_1$ 与 $P_2$ 是推导同构的，同时 $SF_1$ 和 $SF_2$ 之间存在保持符号和句法结构的双射。

2.3 生成算法流程

算法分为两个主要步骤：

搜索最小证明：
- 输入：一个习题的逻辑描述（带符号公式集）和特定理论规则集。
- 过程：迭代构建应用 $n$ 次规则的表列集合 $T_n$ ，寻找第一个封闭表列（证明）。
- 优化：一旦找到最小证明，记录其大小作为上界，继续搜索直到穷尽该上界内的所有可能性，收集所有最小证明。
搜索证明同构的公式集：
- 输入：上述找到的最小证明 $P$ 。
- 过程：基于 $P$ 的结构和规则集，生成证明同构候选集。
- 关键机制：利用推导匹配符号 (Deductive Matching Symbols)。
  - 对于证明树中的每个符号，分析其在规则前提中的位置。
  - 确定哪些其他符号可以替换当前符号而不破坏证明结构（即保持推导同构）。
  - 通过限制替换空间（仅允许在特定规则下匹配的符号间替换），大幅减少搜索空间（例如，将 $5625 $种可能减少到$ 144$ 种）。
- 输出：所有能生成与输入习题具有相同最小证明结构的公式集，即生成具有可比复杂度的新习题。

3. 关键贡献 (Key Contributions)

基于证明结构的难度度量：提出了一种不依赖人工标注、基于证明树结构同构性的客观难度度量方法，解决了传统句法参数无法准确反映一阶逻辑证明难度的问题。
无逻辑符号的特定理论表列：设计了一套从定义公理自动提取规则的方法，生成的证明不含逻辑连接词，更贴近人类（特别是初学者）的数学证明直觉。
推导同构与匹配符号机制：定义了“推导同构”概念，并提出了“推导匹配符号”算法，使得系统能够自动识别并替换习题中的符号（如将 $\cap$ 替换为 $\cup$ 或 $\setminus$ ），同时保持证明难度不变。
自动化生成原型：开发了一个名为 GePECC 的原型系统（GitHub 开源），实现了从输入习题到生成一系列难度相当的新习题的全流程。

4. 实验结果与示例 (Results)

案例研究：以集合论为例，输入习题为证明 $x \in y \cap (w \cup z) \implies x \in (y \cap w) \cup z$ 。
生成效果：系统成功生成了多个具有相同最小证明结构的变体，例如：
- $x \in y \setminus (w \triangle z) \implies x \in (y \setminus w) \cup z$
- $x \in y \cap (w \triangle z) \implies x \in (y \cap w) \cup z$
效率提升：通过利用证明结构约束符号替换，搜索空间减少了约 40 倍（从数千种组合减少到百种级别），证明了该方法在计算上的可行性。
验证：生成的习题在逻辑上被证明具有“推导同构”的最小证明，从而在理论上保证了难度的可比性。

5. 意义与局限性 (Significance & Limitations)

意义：

教学价值：为教师提供了生成个性化、难度可控的练习的工具，支持自适应测试和形成性评估。
理论创新：将逻辑证明的结构性特征（如表列树的同构性）转化为可计算的难度指标，为形式化教育中的 AQG 提供了新的理论框架。
可解释性：生成的习题难度由最小证明的结构决定，而非黑盒模型，教师可以清晰理解难度来源。

局限性与未来工作：

公理限制：某些定义公理因无法满足解析限制（如变量出现位置或深度要求）而无法提取规则。未来计划放宽这些限制。
STSNF 限制：目前方法仅适用于能转换为“带符号特定理论范式 (STSNF)"的习题。对于无法转换的复杂逻辑描述，需要进一步研究分解策略。
感知差异：虽然结构同构保证了理论上的难度一致，但学生可能因多前提规则的使用或特定符号的熟悉度而感到不同。未来计划在实际教学环境中进行实证研究，验证“推导复杂度”与学生实际感知难度的相关性。

总结：该论文提出了一种严谨的、基于形式化逻辑的方法，通过模拟人类证明的解析结构来量化和生成难度可控的数学证明习题，填补了自动习题生成领域在形式化难度控制方面的空白。

A method for the automated generation of proof exercises with comparable levels of proving complexity