OpenAI 形式化数学奥林匹克竞赛问题求解

OpenAI 已经证明其模型可以解决形式化的高中数学奥林匹克竞赛问题。通过在形式化系统中生成证明，这些模型可以为来自美国数学竞赛 (AMC12)、美国数学邀请赛 (AIME) 和国际数学奥林匹克竞赛 (IMO) 等竞赛的复杂问题提供可验证的解决方案。

Formal Proof Generation and Tactics

OpenAI 的方法利用了形式化系统，其中证明是通过使用“tactics”构建的。Tactics 是高层级的搜索程序，用于生成低层级的产物——类似于汇编代码——这些产物是形式化系统验证证明所需的。这使得模型能够从高层级的数学陈述转向可验证的形式化证明。

Solved Problem Examples

这些模型成功解决了不同数学领域的各种问题，展示了特定的推理能力：

Algebra and Arithmetic

AMC12 (2000 Problem 5): 模型通过发明必要的项 abs (x - 2) = -(x - 2) 来推进证明，证明了一个关于绝对值的陈述 ($╴ x - 2 ╵ = p$)。
AMC12B (2020 Problem 6): 模型通过直接提出 n + 1 作为解的见证 (solution witness)，解决了涉及阶乘和完全平方数的问题。
MATH Dataset: 模型使用逆否命题法并提出 0 作为目标的见证 (witness)，证明了一个关于线性函数 $f(x) = Ax + B$ 和 $g(x) = Bx + A$ 的陈述。
AIME (1984 Problem 1): 模型处理了一个涉及等差数列和 98 项范围内的求和问题。

Geometry and Inequalities

IMO (1964 Problem 2): 模型通过为 nlinarith tactic 发明论据，特别是使用平方的非负性 (sq_nonneg)，证明了一个涉及边长 $a, b, c$ 的三角形不等式。
IMO Longlist (1990 Problem 77): 模型通过采用 Cauchy-Schwarz 不等式并引入必要的“切割” (inventing terms like $0 ≤ (c + a) * (c + a)$) 来满足形式化证明器，解决了一个复杂的不等式问题。

Technical Implications

解决这些问题的能力突显了模型在形式化证明语境下的“发明”能力。在若干个实例中，模型不仅是简单地应用现有规则，而是提出了特定的见证 (witnesses)（例如 $n+1$ 或 $0$）或发明了中间引理和项（例如特定的平方差），这些对于完成证明是至关重要的。这表明了在应对形式化验证系统的约束时，所需的战略规划和数学推理能力。