转载

OpenAI研究解决（一些）正式的数学奥林匹克问题

我们为Lean构建了一个神经定理证明器，它学会了解决各种具有挑战性的高中奥林匹克竞赛问题，包括来自 AMC12 和 AIME 竞赛的问题，以及两个改编自 IMO的问题。

我们为 Lean 构建了一个神经定理证明器，它学会了解决各种具有挑战性的高中奥林匹克竞赛问题，包括来自 AMC12 和 AIME 竞赛的问题，以及两个改编自 IMO.A 的问题
[A]
这些问题不是标准的数学练习，它们是用来让来自美国（AMC12、AIME）或世界（IMO）最优秀的高中生相互竞争的。

证明者使用语言模型来寻找形式陈述的证明。每次我们找到新的证明时，我们都会将其用作新的训练数据，这会改进神经网络并使其能够迭代地找到越来越难的陈述的解决方案。

我们在 miniF2F 基准测试上取得了新的最先进水平（41.2% 对 29.3%），这是一组具有挑战性的高中奥林匹克问题。我们的方法，我们称之为语句课程学习，包括手动收集一组不同难度级别的语句（没有证据），其中最难的语句与我们的目标基准相似。最初我们的神经证明器很弱，只能证明其中的几个。我们迭代地搜索新的证明并根据新发现的证明重新训练我们的神经网络，经过 8 次迭代后，我们的证明器最终在 miniF2F 上测试时表现非常出色。

形式数学是一个令人兴奋的研究领域，因为 (i) 它的丰富性，让你可以证明需要推理、创造力和洞察力的任意定理，以及 (ii) 它与游戏的相似性——人工智能在游戏中取得了惊人的成功——因为它有一个自动化的确定证明是否成功的方法（即由正式系统验证）。如下面的简单示例所示，证明正式陈述需要生成一系列证明步骤，每个证明步骤都包含对策略的调用。B
[乙]
正式系统接受的工件是低级的（如汇编代码）并且人类难以生产。策略是从更高级别的指令生成此类工件以协助形式化的搜索过程。

这些策略以数学术语作为参数，每次策略调用都会将当前要证明的语句转换为更容易证明的语句，直到没有任何东西需要证明。

PROBLEM 1

Adapted from AMC12 2000 Problem 5

Prove that if $∣ � - 2 ∣ = �$ ∣x−2∣=p, where $� < 2$ x<2, then $� - � = 2 - 2 �$ x−p=2−2p.

theorem amc12_2000_p5      -- ← theorem name
  (x p : ℝ)                -- ← the statement we want
  (h₀ : x < 2)             --   to prove
  (h₁ : abs (x - 2) = p) :
  x - p = 2 - 2 * p :=
begin                      -- ← formal proof starts here
  -- This first tactic requires that the prover invent
  -- the term: `abs (x - 2) = -(x - 2)`.
  have h₂ : abs (x - 2) = -(x - 2), {
    apply abs_of_neg,
    linarith,
  },
  rw h₁ at h₂,
  -- At this stage the remaining goal to prove is:
  -- `x - p = 2 - 2 * p` knowing that `p = -(x - 2)`.
  linarith,
end

我们观察到，在我们的训练过程中出现了生成战术参数所需的原始数学术语的能力，如果没有神经语言模型，这是无法做到的。下面的证明就是其中的一个例子：proof step use n + 1 (完全由我们的模型生成)建议使用 n + 1 作为解决方案，其余的正式证明依赖于 ring_exp 策略来验证它确实是有效的。

PROBLEM 2

Adapted from AMC12B 2020 Problem 6

For all integers $� \geq 9$ n≥9，证明 $((� + 2个) ！ - (� + 1个) ！) / � ！$ (( ñ+2 ）！−( ñ+1 )!) / n !是一个完美的正方形。

theorem amc12b_2020_p6
  (n : ℕ)
  (h0 : 9 ≤ n) :
  ∃ x : ℕ, (x:ℝ)^2 = 
    (nat.factorial (n + 2) - nat.factorial (n + 1))
    / nat.factorial n :=
begin
  -- The model directly proposes `n + 1` as solution.
  use n + 1,
  field_simp [nat.factorial_ne_zero, pow_succ'],
  ring_exp
end

我们还观察到我们的模型和搜索过程能够产生链接多个非平凡推理步骤的证明。在下面的证明中，模型首先使用导致存在性陈述 ( ∃ (x : ℝ), f x ≠ a * x + b) 的对位。然后它为它生成一个见证 use (0 : ℝ) 并通过利用该策略完成证明 norm_num 。

问题3

改编自 MATH 数据集

让 $� (�) = � � + 乙$ f ( x )=× _+乙和 $� (�) = 乙 � + �$ 克（× ）=× _+A，在哪里 $� < � � / > 电子乙$ A<布拉/ _>e B. 如果 $� (� (�)) - � (� (�)) = 乙 - �$ f ( g ( x ))−g ( f ( x ))=乙−A，证明 $� + 乙 = 0$ A+乙=0.

theorem mathd_train_algebra_217
  (a b : ℝ)
  (f g : ℝ → ℝ)
  (h₀ : ∀ x, f x = a * x + b)
  (h₁ : ∀ x, f x = b * x + a)
  (h₂ : a ≠ b)
  (h₃ : ∀ x, f (g x) - g (f x) = b - a) :
  a + b = 0 :=
begin
  revert h₀ h₁ h₂ h₃,
  -- Initial contraposition.
  contrapose!,
  rintro ⟨h₀, ⟨h₁, h₂⟩⟩,
  -- The model proposes `0` as witness for the current
  -- goal that consists in `∃ (x : ℝ), f x ≠ a * x + b`.
  use (0 : ℝ),
  simp only [sub_eq_iff_eq_add, h₀, mul_zero, zero_add],
  norm_num at h₀,
end

我们的模型经过 statement curriculum learning 训练，能够解决来自培训教科书以及 AMC12 和 AIME 竞赛的各种问题，以及 2 个改编自 IMO的问题。我们在下面展示了此类生成证明的三个示例。

问题4

改编自 IMO 1964 问题 2

认为 $�$ A, $�$ b, $�$ C是三角形的边。

证明 $�^{2个} (� + � - �) + �^{2个} (� + � - �) + �^{2个} (� + � - �) \leq 3个 � � �$ A2个(乙+C−一）+b2个( c+A−二）+C2个（一个+b−三）≤3 AB C.

theorem imo_1964_p2
  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c)
  (h₁ : c < a + b)
  (h₂ : b < a + c)
  (h₃ : a < b + c) :
  a^2 * (b + c - a) + b^2 * (c + a - b) + c^2 * (a + b - c) 
    ≤ 3 * a * b * c :=
begin
  -- Arguments to `nlinarith` are fully invented by our model.
  nlinarith [sq_nonneg (b - a),
             sq_nonneg (c - b),
             sq_nonneg (c - a)]
end

问题5

改编自 AIME 1984 问题 1

证明 $� 2个 + � 4个 + � 6个 + � 8个 + . . . + � 98 = 93$ 一个2+一个4+一个6+一个8+...+一个98=93如果 $� 1个$ 一个1, $� 2个$ 一个2, $� 3...$ 一个3...是具有公差的等差级数 $1个$ 1个，和 $� 1个 + � 2个 + � 3个 + . . . + � 98 = 137$ 一个1+一个2+一个3+...+一个98=137.

theorem aime_1984_p1
  (u : ℕ → ℚ)
  (h₀ : ∀ n, u (n + 1) = u n + 1)
  (h₁ : ∑ k in finset.range 98, u k.succ = 137) :
  ∑ k in finset.range 49, u (2 * k.succ) = 93 :=
begin
  rw finset.sum_eq_multiset_sum,
  dsimp [finset.range] at h₁,
  simp [h₀],
  ring,
  norm_num at h₁,
  norm_num,
  apply eq_of_sub_eq_zero,
  { simp only [*, abs_of_pos, add_zero] at *, linarith },
end

问题6

改编自 IMO Longlist 1990 Problem 77

为了 $�, �, �$ 一个，乙，C实数，证明 $(�^{2个} + � � + �^{2个}) (�^{2个} + � � + �^{2个}) (�^{2个} + � � + �^{2个}) \geq (� � + � � + � �)^{3个}$ （一个2个+ab+b2个) (乙2个+乙丙+C2个) (丙2个+一个_+A2个)≥( ab+乙丙+一） _3个.

theorem imo_longlist_1990_p77
  (a b c : ℝ) :
  (a * b + b * c + c * a)^3 ≤
    (a^2 + a * b + b^2) * (b^2 + b * c + c^2) *
    (c^2 + c * a + a^2) :=
begin
  -- The three initial steps use Cauchy–Schwarz to prove
  -- `(a * b + b * c) ^ 2 ≤ (a ^ 2 + b ^ 2) * (b ^ 2 + c ^ 2)`
  -- which is required for the final call to `nlinarith`.
  let u : euclidean_space ℝ (fin 2) := ![a, b],
  let v : euclidean_space ℝ (fin 2) := ![b, c],
  have h₀ := real_inner_mul_inner_self_le u v,
  simp [u, v, fin.sum_univ_succ, 
        ←pow_two, ←pow_two, le_of_lt, mul_assoc] at h₀,
  -- The model introduces another required cut (i.e. invent
  -- the term `0 ≤ (c + a) * (c + a)` and proves it).
  have h₃ : 0 ≤ (c + a) * (c + a),
  { nlinarith, },
  have h₄ := sq_nonneg (a * b + b * c + c * a),
  simp [sq, h₀, h₃, mul_add, add_mul] at h₄ ⊢,
  nlinarith [sq_nonneg (b - a),
             sq_nonneg (c - b),
             sq_nonneg (a - c)]
end

形式数学涉及两个主要挑战，这使得强化学习的天真应用不太可能成功。

(i) 无限的行动空间：形式数学不仅有一个非常大的搜索空间（比如围棋），它还有一个无限的行动空间。在证明搜索的每一步，模型必须不是从一组行为良好的有限动作中进行选择，而是从一组复杂且无限的策略中进行选择，涉及必须生成的外生数学项（例如，生成一个数学语句是用作见证，在诸如“存在 x st ……”或切割、证明中间的引理的引入和链接等步骤中使用的对象）。
(ii) 缺乏自我对弈：与 2 人游戏相反，证明者不是与对手对弈，而是与一组陈述进行证明。当面对一个太难的陈述时，没有明显的重构可以让证明者生成更容易的中间陈述来首先解决。这种不对称性阻止了 self-play 算法的天真应用，这种算法在 2 人游戏中是成功的。

在我们的工作中，我们通过在搜索证明时从语言模型中采样动作来解决无限动作空间问题。语言模型能够生成策略调用以及通常需要作为参数的原始数学术语。我们解决缺乏自我博弈的基础是观察到自我博弈在 2 人游戏中的关键作用是提供无监督的课程。我们的方法建议用一组不同难度的辅助问题陈述（不需要证明）代替这种无监督课程。我们凭经验表明，当这些辅助问题的难度足够大时，我们的训练过程能够解决越来越难的问题，最终泛化到我们关心的问题集。

虽然这些结果非常令人兴奋，因为它们表明深度学习模型在与正式系统交互时能够进行非平凡的数学推理，但我们距离这些竞赛中的最佳学生表现还很遥远，只是偶尔，而不是始终如一，关闭具有挑战性的奥林匹克问题。尽管如此，我们希望我们的工作能够激发这一领域的研究，特别是针对 IMO 大挑战的研究，并且我们提出的语句课程学习 方法将有助于加快自动推理的总体进展。

脚注

这些问题不是标准的数学练习，它们是用来让来自美国（AMC12、AIME）或世界（IMO）最优秀的高中生相互竞争的。↩︎
正式系统接受的工件是低级的（如汇编代码）并且人类难以生产。策略是从更高级别的指令生成此类工件以协助形式化的搜索过程。↩︎

作者

致谢

感谢我们的论文合著者：Igor Babuschkin、Kunhao Zheng 和 Mantas Baksys。

感谢 Xena Project Discord 的学生，他们帮助我们将证明和陈述形式化（特别是：Antoine Labelle、Hanting Zhang、Shing Tak Lam、Paul Lezeau、Sara Diaz、Nikita Golikov、Yael Dillies、Artem Vasilyev、Ollie Perree 和 Yourong藏）。

特别感谢 Kevin Buzzard 和 Daniel Selsam 自本项目开始以来的支持和周到的反馈。

详细论文

OpenAI研究

OpenAI研究解决（一些）正式的数学奥林匹克问题

PROBLEM 1

Prove that if $∣ � - 2 ∣ = �$ ∣x−2∣=p, where $� < 2$ x<2, then $� - � = 2 - 2 �$ x−p=2−2p.

PROBLEM 2

For all integers $� \geq 9$ n≥9，证明 $((� + 2个) ！ - (� + 1个) ！) / � ！$ (( ñ+2 ）！−( ñ+1 )!) / n !是一个完美的正方形。

问题3

让 $� (�) = � � + 乙$ f ( x )=× _+乙和 $� (�) = 乙 � + �$ 克（× ）=× _+A，在哪里 $� < � � / > 电子乙$ A<布拉/ _>e B. 如果 $� (� (�)) - � (� (�)) = 乙 - �$ f ( g ( x ))−g ( f ( x ))=乙−A，证明 $� + 乙 = 0$ A+乙=0.

问题4

认为 $�$ A, $�$ b, $�$ C是三角形的边。

证明 $�^{2个} (� + � - �) + �^{2个} (� + � - �) + �^{2个} (� + � - �) \leq 3个 � � �$ A2个(乙+C−一）+b2个( c+A−二）+C2个（一个+b−三）≤3 AB C.

问题5

问题6

脚注

作者

致谢

相关文章

本文目录

标签

近期评论

OpenAI研究 解决（一些）正式的数学奥林匹克问题

PROBLEM 1

Prove that if ∣�−2∣=�∣x−2∣=p, where �<2x<2, then �−�=2−2�x−p=2−2p.

PROBLEM 2

For all integers �≥9n≥9， 证明((�+2个)！−(�+1个)！)/�！(( ñ+2 ）！−( ñ+1 )!) / n !是一个完美的正方形。

问题3

让�(�)=��+乙f ( x )=× _+乙和�(�)=乙�+�克（× ）=× _+A， 在哪里�<��/>电子乙A<布拉/ _>e B. 如果�(�(�))−�(�(�))=乙−�f ( g ( x ))−g ( f ( x ))=乙−A， 证明�+乙=0A+乙=0.

问题4

认为�A,�b,�C是三角形的边。证明�2个(�+�−�)+�2个(�+�−�)+�2个(�+�−�)≤3个���A2个(乙+C−一）+b2个( c+A−二）+C2个（一个+b−三）≤3 AB C.

问题5

证明�2个+�4个+�6个+�8个+...+�98=93一个2+一个4+一个6+一个8+...+一个98=93如果�1个一个1,�2个一个2,�3...一个3...是具有公差的等差级数1个1个， 和�1个+�2个+�3个+...+�98=137一个1+一个2+一个3+...+一个98=137.

问题6

为了�,�,�一个，乙，C实数，证明(�2个+��+�2个)(�2个+��+�2个)(�2个+��+�2个)≥(��+��+��)3个（一个2个+ab+b2个) (乙2个+乙丙+C2个) (丙2个+一个_+A2个)≥( ab+乙丙+一） _3个.

脚注

作者

致谢

相关文章

本文目录

标签

近期评论

OpenAI研究解决（一些）正式的数学奥林匹克问题

Prove that if $∣ � - 2 ∣ = �$ ∣x−2∣=p, where $� < 2$ x<2, then $� - � = 2 - 2 �$ x−p=2−2p.

For all integers $� \geq 9$ n≥9，证明 $((� + 2个) ！ - (� + 1个) ！) / � ！$ (( ñ+2 ）！−( ñ+1 )!) / n !是一个完美的正方形。

让 $� (�) = � � + 乙$ f ( x )=× _+乙和 $� (�) = 乙 � + �$ 克（× ）=× _+A，在哪里 $� < � � / > 电子乙$ A<布拉/ _>e B. 如果 $� (� (�)) - � (� (�)) = 乙 - �$ f ( g ( x ))−g ( f ( x ))=乙−A，证明 $� + 乙 = 0$ A+乙=0.

认为 $�$ A, $�$ b, $�$ C是三角形的边。

证明 $�^{2个} (� + � - �) + �^{2个} (� + � - �) + �^{2个} (� + � - �) \leq 3个 � � �$ A2个(乙+C−一）+b2个( c+A−二）+C2个（一个+b−三）≤3 AB C.