Chúng tôi đã xây dựng một trình chứng minh định lý thần kinh cho Lean (mở trong cửa sổ mới) đã học cách giải quyết nhiều bài toán khó trong kỳ thi Olympic cấp trung học, bao gồm các bài toán từ AMC12 (mở trong cửa sổ mới) và AIME (mở trong cửa sổ mới) các cuộc thi, cũng như hai bài toán được điều chỉnh từ IMO (mở trong cửa sổ mới). Người chứng minh sử dụng mô hình ngôn ngữ để tìm bằng chứng cho các tuyên bố chính thức. Mỗi lần chúng ta tìm thấy một bằng chứng mới, chúng ta sử dụng nó như dữ liệu đào tạo mới, giúp cải thiện mạng nơ-ron và cho phép nó lặp đi lặp lại tìm ra giải pháp cho các tuyên bố ngày càng khó hơn.

Chúng tôi đã đạt được trình độ tiên tiến mới (41,2% so với 29,3%) trên miniF2F (mở trong cửa sổ mới) benchmark, một bộ sưu tập đầy thử thách các bài toán olympiad cấp 3. Phương pháp tiếp cận của chúng tôi, mà chúng tôi gọi là statement curriculum learning , bao gồm việc thu thập thủ công một tập hợp các câu lệnh có mức độ khó khác nhau (không có bằng chứng) trong đó các câu lệnh khó nhất tương tự như chuẩn mực mà chúng tôi nhắm tới. Ban đầu, trình chứng minh thần kinh của chúng tôi yếu và chỉ có thể chứng minh một số ít trong số chúng. Chúng tôi lặp đi lặp lại tìm kiếm các bằng chứng mới và đào tạo lại mạng lưới thần kinh của mình trên các bằng chứng mới được phát hiện và sau 8 lần lặp, trình chứng minh của chúng tôi trở nên vượt trội hơn hẳn khi được thử nghiệm trên miniF2F.

Toán học chính thức là một lĩnh vực thú vị để nghiên cứu vì tính phong phú của nó, cho phép bạn chứng minh các định lý tùy ý đòi hỏi lý luận, sự sáng tạo và hiểu biết sâu sắc và tính tương tự của nó với trò chơi—nơi AI đã thành công ngoạn mục—ở chỗ nó có một cách tự động để xác định xem một bằng chứng có thành công hay không (tức là được xác minh bởi hệ thống chính thức). Như đã chứng minh trong ví dụ tầm thường dưới đây, việc chứng minh một tuyên bố chính thức đòi hỏi phải tạo ra một chuỗi các bước chứng minh, mỗi bước chứng minh bao gồm một lời kêu gọi đến một chiến thuật.

Những chiến thuật này lấy các thuật ngữ toán học làm đối số và mỗi lần gọi chiến thuật sẽ biến đổi câu lệnh hiện tại cần chứng minh thành những câu lệnh dễ chứng minh hơn, cho đến khi không còn gì để chứng minh nữa.

BÀI TOÁN 1

Chuyển thể từ AMC12 2000 Bài toán 5

Chứng minh rằng nếu∣????−2∣=????∣ x−2∣=P, Ở đâu????<2x<2, sau đó????−????=2−2????x−P=2−2 trang.

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

Chúng tôi nhận thấy rằng khả năng tạo ra các thuật ngữ toán học gốc cần thiết làm đối số cho chiến thuật, điều không thể thực hiện được nếu không có mô hình ngôn ngữ thần kinh, xuất hiện từ quy trình đào tạo của chúng tôi. Bằng chứng dưới đây là một ví dụ về nó: bước chứng minh use n + 1 (hoàn toàn do mô hình của chúng tôi tạo ra) đề xuất sử dụng n + 1 như một giải pháp, phần còn lại của bằng chứng chính thức dựa vào [ring_exp](https://leanprover-community.github.io/mathlib_docs/tactic/ring_exp.html) chiến thuật để xác minh rằng nó thực sự hợp lệ.

BÀI TOÁN 2

Chuyển thể từ AMC12B 2020 Bài toán 6

Đối với tất cả các số nguyên????≥9N≥9, chứng minh rằng((????+2)!−(????+1)!)/????!(( N+2 )!−( N+1 )!) / không !là một hình vuông hoàn hảo.

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

Chúng tôi cũng quan sát thấy rằng các mô hình và quy trình tìm kiếm của chúng tôi có khả năng tạo ra các bằng chứng kết nối nhiều bước suy luận không tầm thường. Trong bằng chứng dưới đây, mô hình bắt đầu bằng cách sử dụng phép đối lập dẫn đến câu lệnh hiện sinh ( ∃ (x : ℝ), f x ≠ a * x + b). Sau đó, nó tạo ra một nhân chứng cho nó bằng use (0 : ℝ) và hoàn thành bằng chứng bằng cách tận dụng [norm_num](https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num) chiến thuật.

BÀI TOÁN 3

Chuyển thể từ tập dữ liệu MATH

Cho phépnếu(????)=MỘT????+????f ( x )=Một x+BVà????(????)=????????+MỘTg ( x )=Bx+MỘT, Ở đâuMỘTVà????MỘTvà B. Nếu nhưnếu(????(????))−????(nếu(????))=????−MỘTf ( g ( x ))−g ( f ( x ))=B−MỘT, chứng minh rằngMỘT+????=0MỘT+B=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

Các mô hình của chúng tôi, được đào tạo bằng cách học chương trình giảng dạy phát biểu , có thể giải quyết nhiều vấn đề khác nhau từ sách giáo khoa đào tạo cũng như AMC12 (mở trong cửa sổ mới) và AIME (mở trong cửa sổ mới) cuộc thi và 2 bài toán được điều chỉnh từ IMO (mở trong cửa sổ mới). Chúng tôi trình bày dưới đây ba ví dụ về những bằng chứng được tạo ra như vậy.

BÀI TOÁN 4

Chuyển thể từ IMO 1964 Bài toán 2

Giả địnhMộtMột,????b,????clà các cạnh của một tam giác.

Chứng minh rằngMột2(????+????−Một)+????2(????+Một−????)+????2(Một+????−????)≤3Một????????Một2( b+c−Một )+b2( c+Một−b )+c2( Một+b−c )≤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

BÀI TOÁN 5

Chuyển thể từ AIME 1984 Bài toán 1

Chứng minh rằngMột2+Một4+Một6+Một8+...+Một98=93a2+số 4+số 6+a8+...+một 98=93nếu nhưMột1một 1,Một2a2,Một3...một 3...là một cấp số cộng có hiệu chung11, VàMột1+Một2+Một3+...+Một98=137một 1+a2+a3+...+một 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

BÀI TOÁN 6

Chuyển thể từ IMO Longlist 1990 Bài toán 77

VìMột,????,????Một ,b ,csố thực, chứng minh rằng(Một2+Một????+????2)(????2+????????+????2)(????2+????Một+Một2)≥(Một????+????????+????Một)3( Một2+b+b2) ( b2+b c+c2) ( c2+c a+Một2)≥( từ+b c+c a )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

Toán học chính thức liên quan đến hai thách thức chính khiến cho việc áp dụng học tăng cường một cách ngây thơ khó có thể thành công.

+ Không gian hành động vô hạn : toán học hình thức không chỉ có không gian tìm kiếm cực lớn (ví dụ như Go), mà còn có không gian hành động vô hạn. Ở mỗi bước tìm kiếm bằng chứng, mô hình phải chọn không phải từ một tập hợp hữu hạn các hành động có hành vi tốt, mà là một tập hợp phức tạp và vô hạn các chiến thuật, bao gồm các thuật ngữ toán học ngoại sinh phải được tạo ra (ví dụ, tạo ra một câu lệnh toán học để sử dụng làm bằng chứng, một đối tượng được sử dụng trong các bước như "tồn tại một x st ..." hoặc một vết cắt, phần giới thiệu và chuỗi của một bổ đề ở giữa một bằng chứng).

+ Thiếu tự chơi : ngược lại với trò chơi 2 người chơi, người chứng minh không chơi với đối thủ mà chơi với một tập hợp các tuyên bố cần chứng minh. Khi đối mặt với một tuyên bố quá khó, không có sự thay đổi rõ ràng nào cho phép người chứng minh tạo ra các tuyên bố trung gian dễ giải quyết hơn trước. Sự bất đối xứng này ngăn cản việc áp dụng ngây thơ các thuật toán tự chơi đã thành công với trò chơi 2 người chơi.

Trong công trình của mình, chúng tôi giải quyết vấn đề không gian hành động vô hạn bằng cách lấy mẫu các hành động từ một mô hình ngôn ngữ khi chúng tôi tìm kiếm bằng chứng. Các mô hình ngôn ngữ có khả năng tạo ra các lệnh gọi chiến thuật cũng như các thuật ngữ toán học ban đầu thường được yêu cầu làm đối số. Cơ sở của chúng tôi để giải quyết tình trạng thiếu tự chơi là quan sát rằng vai trò chính của tự chơi trong các trò chơi 2 người chơi là cung cấp một chương trình giảng dạy không giám sát. Phương pháp luận của chúng tôi đề xuất thay thế chương trình giảng dạy không giám sát này bằng một tập hợp các câu lệnh bài toán bổ trợ (không yêu cầu bằng chứng) có độ khó khác nhau. Chúng tôi chứng minh bằng kinh nghiệm rằng, khi độ khó của các bài toán bổ trợ này đủ thay đổi, quy trình đào tạo của chúng tôi có thể giải quyết một chương trình giảng dạy gồm các bài toán ngày càng khó hơn, cuối cùng là khái quát hóa thành tập hợp các bài toán mà chúng tôi quan tâm.

Mặc dù những kết quả này cực kỳ thú vị, vì chúng chứng minh rằng các mô hình học sâu có khả năng suy luận toán học phi tầm thường khi tương tác với một hệ thống chính thức, chúng ta vẫn còn rất xa mới đạt được thành tích học sinh giỏi nhất trong các cuộc thi này, chỉ thỉnh thoảng, thay vì liên tục, mới giải quyết được các bài toán olympiad đầy thách thức. Tuy nhiên, chúng tôi hy vọng rằng công trình của mình sẽ thúc đẩy nghiên cứu trong lĩnh vực này, đặc biệt là hướng tới IMO Grand Challenge (mở trong cửa sổ mới) và rằng phương pháp học tập theo chương trình giảng dạy mà chúng tôi đề xuất sẽ giúp đẩy nhanh tiến độ trong lý luận tự động nói chung.

Tài khoản ChatGPT 4 là gì?

Họ tên (*)	Số điện thoại (*)
Email (*)	Dịch vụ

Giải quyết (một số) bài toán thi Olympic toán học chính thức