Business Information Learning

  1. Trang chủ
  2. Lưu
  3. Thẻ
  4. Hỏi - Đáp

 
 
LeVanLoi'log, ⌚ 2024-10-15
***
☕ Nhàn đàm S&T: IMO
Tác giả: Lê Văn Lợi
Phác họa bài post:
Ⓐ. Đề dẫn.
Ⓑ. Sơ lược về IMO.
Ⓒ. Một vài con số tương quan quốc tế & khu vực.
Ⓓ. “Máy” thi IMO.
Ⓔ. “Máy” giải toán.
Ⓕ. Suy ngẫm chậm.

Để giúp anh/chị quyết định có đọc tiếp hay không, tôi xin phép cung cấp các thông tin liên quan đến bài post này như sau:

  • Chủ đề: Toán sơ cấp, Machine Learning
  • Tính thời sự: tháng 9/2024
  • Thời gian đọc: 10 phút, kể cả thời gian uống cà phê (uống cà phê xong là đọc xong)

Ⓐ. Đề dẫn.

Nhân kỷ niệm 50 năm (1974-2024) Việt Nam tham gia Olympic Toán học Quốc tế, hôm nay xin phép diễn đàn có một vài dòng về International Mathematical Olympiad (IMO). Tôi tin là trên diễn đàn này có rất nhiều người đã từng tham gia thi IMO. Ví dụ như anh Hoàng Lê Minh đoạt huy chương vàng trong lần đầu Việt Nam tham gia. Đoàn Việt Nam năm đó (1974) có 5 người đi thi. Ngoài anh Hoàng Lê Minh còn có anh Vũ Đình Hòa đoạt huy chương bạc, anh Đặng Hoàng Trung và anh Tạ Hồng Quang đoạt huy chương đồng. Đoàn còn có anh Nguyễn Quốc Thắng. Trưởng đoàn là thầy Lê Hải Châu và phó trưởng đoàn là thầy Phan Đức Chính.

-

Bài post này có cấu trúc như sau. Sau phần đề dẫn là phần giới thiệu sơ lược về IMO. Tiếp theo là một vài con số tương quan quốc tế & khu vực. Phần cuối tôi xin bàn luận đến việc “máy đi thi IMO” – nghĩa là máy đang tiệm cận đến việc giải các bài toán IMO trong khung thời gian mà ban tổ chức giải quy định.

-

Toàn bộ thông tin liên quan đến IMO tôi lấy từ các trang sau:

https://en.wikipedia.org/wiki/International_Mathematical_Olympiad

https://www.imo-official.org/results.aspx

https://en.wikipedia.org/wiki/International_Mathematical_Olympiad_selection_process

Ⓑ. Sơ lược về IMO.

Lịch sử

Kì thi IMO đầu tiên được tổ chức tại Romania năm 1959 với sự tham gia của 7 quốc gia Đông Âu là chủ nhà Romania, Bulgaria, Tiệp Khắc, Đông Đức, Hungary, Ba Lan và Liên Xô. Trong giai đoạn đầu, IMO chủ yếu là cuộc thi của các quốc gia thuộc hệ thống xã hội chủ nghĩa và địa điểm tổ chức cũng chỉ trong phạm vi các nước Đông Âu. Bắt đầu từ thập niên 1970, số lượng các đoàn tham gia bắt đầu tăng lên nhanh chóng và IMO thực sự trở thành một kì thi quốc tế về Toán dành cho học sinh.

Cho đến nay kì thi được tổ chức liên tục hàng năm, trừ duy nhất năm 1980. Kì IMO có số lượng đoàn tham gia đông đảo nhất tính đến IMO 2011 chính là kì IMO 2011 tổ chức tại Amsterdam, Hà Lan với 101 đoàn tham dự.

Mỗi đoàn tham dự được phép có tối đa 6 thí sinh, một trưởng đoàn, một phó đoàn và các quan sát viên. Theo quy định, thí sinh tham gia phải dưới 20 tuổi và trình độ không được vượt quá cấp trung học phổ thông (high school trong tiếng Anh, hay lycée trong tiếng Pháp), vì vậy một thí sinh có thể tham gia tới 5 hoặc 6 kì IMO, riêng với Việt Nam do quy định của việc chọn đội tuyển, một thí sinh chỉ tham dự được nhiều nhất là hai kì.

Quy chế thi

Mỗi bài thi IMO bao gồm 6 bài toán, mỗi bài tương đương tối đa là 7 điểm, có nghĩa là thí sinh có thể đạt tối đa 42 điểm cho 6 bài. 6 bài toán này sẽ được giải trong 2 ngày liên tiếp, mỗi ngày thí sinh giải 3 bài trong thời gian 270 phút.

Các bài toán được lựa chọn trong các vấn đề toán học sơ cấp, bao gồm 4 lĩnh vực hình học, số học, đại số  tổ hợp. Bắt đầu từ tháng 3 hàng năm, các nước tham gia thi được đề nghị gửi các đề thi mà họ lựa chọn đến nước chủ nhà, sau đó một ban lựa chọn đề thi của nước chủ nhà sẽ lập ra một danh sách các bài toán rút gọn bao gồm những bài hay nhất, không trùng lặp đề thi IMO các năm trước hoặc kì thi quốc gia của các nước tham gia, không đòi hỏi kiến thức toán cao cấp, không quá khó hoặc quá dễ nhưng yêu cầu được thí sinh phải vận dụng hết khả năng suy luận và kiến thức toán được học. Một vài ngày trước kì thi, các trưởng đoàn sẽ bỏ phiếu lựa chọn 6 bài chính thức, chính họ cũng sẽ là người dịch đề thi sang tiếng nước mình để thí sinh có thể giải toán bằng tiếng mẹ đẻ, sau đó các vị trưởng đoàn sẽ được cách ly hoàn toàn với các thí sinh để tránh gian lận.

Bài thi của thí sinh sẽ được ban giám khảo và trưởng đoàn của thí sinh đó chấm song song, sau đó hai bên sẽ hội ý để đưa ra kết quả cuối cùng. Giám khảo và trưởng đoàn đều có thể phản biện cách chấm của nhau để điểm bài thi đạt được là chính xác nhất. Nếu hai bên không thể đi tới đồng thuận thì người quyết định sẽ là trưởng ban giám khảo và giải pháp cuối cùng là tất cả các trưởng đoàn bỏ phiếu. Riêng bài thi của thí sinh nước chủ nhà sẽ do giám khảo đến từ các nước có đề thi được chọn chấm.

Giải thưởng

Tại IMO việc xét giải chỉ là cho cá nhân từng thí sinh tham gia thi, còn việc xếp hạng thành tích các đoàn đều do các nước tham gia tự tính toán và không có ý nghĩa chính thức.

Giải thưởng của IMO bao gồm huy chương vàng, huy chương bạc và huy chương đồng được trao theo điểm tổng cộng mà thí sinh đạt được. Số thí sinh được trao huy chương là khoảng một nửa tổng số thí sinh, điểm để phân loại huy chương sẽ theo nguyên tắc tỉ lệ thí sinh đạt huy chương vàng, bạc, đồng sẽ là 1:2:3. Các thí sinh không giành được huy chương nhưng giải được trọn vẹn ít nhất 1 bài (7/7 điểm) sẽ được trao bằng danh dự.

Ngoài ra, ban tổ chức IMO còn có thể trao các giải thưởng đặc biệt cho cách giải cực kì sáng tạo hoặc tổng quát hóa vấn đề nêu ra trong bài toán. Giải này phổ biến trong thập niên 1980 nhưng gần đây ít được trao hơn, lần cuối cùng giải thưởng đặc biệt được trao là năm 2005. Thí sinh đoàn Việt Nam từng đạt giải thưởng này là Lê Bá Khánh Trình tại IMO 1979.

Ⓒ. Một vài con số tương quan quốc tế & khu vực.

Mười quốc gia hiện tại có kết quả tốt nhất mọi thời đại:

 

Country
(Quốc gia)

Appearances
(Số lần tham dự)

Gold
(Vàng)

Silver
(Bạc)

Bronze
(Đồng)

Honorable mentions
(bằng danh dự)

1

Trung Quốc

39

185

37

6

0

2

Hoa Kỳ

50

151

120

30

1

3

Nga

30

106

62

12

0

4

Hàn Quốc

37

95

83

28

7

5

Hungary

64

88

174

116

10

6

Romania

65

86

158

111

7

7

Liên Xô (cũ)

29

77

67

45

0

8

Việt Nam

48

69

117

85

3

9

Bulgaria

65

57

130

121

15

10

Vương quốc Anh

57

56

124

131

18

-

Các quốc gia sau đây đã đạt được điểm số đồng đội cao nhất (nhất toàn đoàn):

Trung Quốc, 24 lần: vào các năm 1989, 1990, 1992, 1993, 1995, 1997, 1999, 2000, 2001, 2002, 2004, 2005, 2006, 2008, 2009, 2010, 2011, 2013, 2014, 2019, 2020, 2021, 2022, 2023;

Nga (bao gồm cả Liên Xô), 16 lần: vào các năm 1963, 1964, 1965, 1966, 1967, 1972, 1973, 1974, 1976, 1979, 1984, 1986, 1988, 1991, 1999, 2007;

Hoa Kỳ, 9 lần: vào các năm 1977, 1981, 1986, 1994, 2015, 2016, 2018, 2019, 2024;

Hungary, 6 lần: vào các năm 1961, 1962, 1969, 1970, 1971, 1975;

Romania, 5 lần: vào các năm 1959, 1978, 1985, 1987, 1996;

Tây Đức, hai lần: vào các năm 1982 và 1983;

Hàn Quốc, hai lần: vào các năm 2012 và 2017;

Bulgaria, một lần: năm 2003;

Iran, một lần: năm 1998;

Đông Đức, một lần: năm 1968.

-

Các quốc gia sau đây tất cả thành viên đều đoạt huy chương vàng:

Trung Quốc, 15 lần: vào các năm 1992, 1993, 1997, 2000, 2001, 2002, 2004, 2006, 2009, 2010, 2011, 2019, 2021, 2022 và 2023.

Hoa Kỳ, 4 lần: vào các năm 1994, 2011, 2016 và 2019.

Hàn Quốc, 3 lần: vào các năm 2012, 2017 và 2019.

Nga, hai lần: vào các năm 2002 và 2008.

Bulgaria, một lần: vào năm 2003.

-

Kết quả các quốc gia ASEAN:

 

Country
(Quốc gia)

Appearances
(Số lần tham dự)

Gold
(Vàng)

Silver
(Bạc)

Bronze
(Đồng)

Honorable mentions
(bằng danh dự)

1

Việt Nam

48

69

117

85

3

2

Thái Lan

36

34

70

53

26

3

Singapore

37

25

74

74

23

4

Indonesia

36

6

30

61

37

5

Malaysia

30

6

18

35

43

6

Philippines

36

4

20

43

32

7

Căm-pu-chia

9

0

0

0

14

8

Myanmar

7

0

0

0

11

9

Brunei

1

0

0

0

0

10

Lào

1

0

0

0

0

Timor-Leste chưa tham dự lần nào. Brunei tham dự một lần duy nhất vào năm 2000. Lào tham dự một lần duy nhất vào năm 2016.

-

Xếp hạng cao nhất mà đoàn Việt Nam đạt được là đứng thứ ba toàn đoàn vào các năm 1999, 2007 và 2017. Năm 1974, năm lần đầu tiên Việt Nam tham gia, Việt Nam xếp thứ 13/18 toàn đoàn. Năm 2024, Việt Nam xếp thứ 33/108 toàn đoàn.

-

Việt Nam đăng cai tổ chức 1 lần vào năm 2007. Trong các nước ASEAN có Thái Lan đăng cai tổ chức 1 lần vào năm 2015.

Ⓓ. “Máy” thi IMO, AIME.

Trong một lần nhàn đàm trước (bài post ngày 27-3-2022), tôi đề cập đến việc máy đi thi lập trình. Máy mà đi thi lập trình thì “đúng nghề” rồi, đúng không ạ? Lần này chúng ta nói đến chuyện máy đi thi IMO. Thật ra thì “máy” chưa bao giờ được ban tổ chức IMO cho thi cả. Đây là chúng ta nói đến việc “máy” giải các bài toán của IMO hoặc giải các bài toán nhằm tuyển chọn các thí sinh tham dự IMO.

  • Ngày 25/7/2024, DeepMind (thuộc Google) đăng bài “AI achieves silver-medal standard solving International Mathematical Olympiad problems” (AI đạt chuẩn huy chương bạc khi giải bài toán IMO). Mô hình AlphaProof của họ giải được 2 bài đại số (Bài 1 và Bài 2) 1 bài số học (Bài 6 là bài khó nhất mà chỉ 5 thí sinh giải được) trong kỳ thi IMO năm 2024. Mô hình AlphaGeometry 2 giải được bài hình học (Bài 4). Như vậy, “máy” giải được tổng cộng 4 bài, mỗi bài 7 điểm nên tổng số điểm mà “máy” đạt được là 4*7 = 28 điểm, đạt điểm huy chương bạc “tuyệt đối”. Huy chương vàng là từ 29 điểm trở lên.
  • Ngày 12/9/2024, OpenAI, trong bài giới thiệu mô hình o1-preview, cho biết là mô hình này nằm trong tốp đầu 500 thí sinh thi Olympic Toán Hoa Kỳ. Khác với AlphaProof và AlphaGeometry giải toán IMO, o1-preview giải 15 bài toán trong kỳ thi “American Invitational Mathematics Examination (AIME) ” (Kỳ thi Toán học Mời dự tuyển của Mỹ). o1-preview giải được 13.9/15 bài, tương đương 93%.

-

Để cho “fair” (công bằng) cũng cần phải nói rõ thêm một vài chi tiết:

Thi IMO.    Theo quy định của ban tổ chức, các thí sinh giải 6 bài trong 2 phiên, mỗi phiên 4 tiếng rưỡi đồng hồ. Tuy nhiên, theo bài báo của DeepMind thì giải pháp của họ giải được 1 bài chỉ trong vòng mấy phút nhưng các bài còn lại máy họ phải chạy trong 3 ngày liền. Hơn nữa, các giải pháp của họ (AlphaProof và AlphaGeometry) không tự “đọc hiểu” được đề bài mà người của họ phải “dịch” đề bài sang ngôn ngữ hình thức (xem mục Ⓔ. tiếp theo). Như vậy, xét theo quy chế thi của IMO thì có thể nói “Máy” đã phạm quy! 😊

Thi AIME. Trong kỳ thi AIME năm 2024, nếu o1 chỉ nộp một mẫu duy nhất (đưa ra duy nhất 1 đáp án cho mỗi câu hỏi) thì đạt được kết quả đúng là 11.1/15 bài, tương đương 74%. Nếu máy đưa ra 64 mẫu (64 đáp án cho mỗi câu hỏi) rồi chọn đáp án đồng thuận đúng thì đạt được kết quả đúng là 12.5/15 bài, tương đương 83%. Chỉ khi lấy 1.000 mẫu cho mỗi câu hỏi thì o1 mới đạt được kết quả đúng là 13.9/15 bài, tương đương 93%.
Trong bài báo, họ không nói rõ thế nào là kết quả đồng thuận đúng. Căn cứ vào một số Benchmark, cách tính kết quả đồng thuận đúng có thể hiểu như sau. Giả thiết có N mẫu đáp án và có c mẫu đáp án đúng (c  N) thì kết quả đồng thuận đúng là c/N.

Ⓔ. “Máy” giải toán.

Tất nhiên, chúng ta tò mò tự hỏi: “Máy” giải toán bằng cách nào? Đây là vấn đề hóc búa đối với Machine Learning vì các bài toán được diễn tả bằng ngôn ngữ ký hiệu (Symbolic Language) còn “Máy” (Machine Learning) chỉ chạy với các con số.

DeepMind có 2 giải pháp tách rời nhau, đó là AlphaProof  AlphaGeometry.

AlphaProof.

Đại ý: hệ thống “tự huấn luyện” để chứng minh các mệnh đề toán học bằng ngôn ngữ hình thức Lean. Sau đó, họ kết hợp Gemini với AlphaZero để giải bài toán.

Ngôn ngữ hình thức (như Lean) có một ưu điểm đặc biệt là người ta có thể dùng nó để chứng minh tính đúng đắn của một lập luận toán học. Lean có thư viện Mathlib với khoảng 85,000 định nghĩa và 160,000 mệnh đề toán học đã được chứng minh.

Giải pháp chung của AlphaProof:

  • Khi gặp một bài toán, AlphaProof sử dụng Gemini để “dịch” bài toán từ “ngôn ngữ tự nhiên” sang “ngôn ngữ hình thức” Lean.
  • Tiếp theo, AlphaProof tạo sinh ra một loạt các ứng viên cho lời giải. Sau đó, nó so sánh lời giải vừa tạo sinh với thư viện Mathlib để chứng minh hoặc bác bỏ lời giải đó.
  • Đối với các lời giải được chứng minh, nó bổ sung lời giải vào hệ thống để tăng thêm sức mạnh cho chính nó sau này.

Trước khi thi IMO, AlphaProof đã được pre-training (tiền huấn luyện) với khoảng 1 triệu bài toán (xem hình vẽ ở dưới). Đến khi thi, AlphaProof vẫn sử dụng vòng lặp tự huấn luyện với dữ liệu đầu vào là các bài toán thuộc đề thi của IMO2024.

 Chú ý: không có gì đảm bảo rằng vòng lặp của AlphaProof tìm ra lời giải.

Nguồn

Quy trình vòng lặp huấn luyện AlphaProof bằng Reinforcement Learning.

  • Người ta tập hợp khoảng 1 triệu bài toán được trình bày bằng ngôn ngữ tự nhiên (Informal problems)
  • Tiếp theo, người ta “dịch” (Formalizer network) các bài toán đó sang Lean, được khoảng 100 triệu bài toán trong ngôn ngữ hình thức (Formal problems)
  • Người ta dùng hệ thống AlphaZero để tự huấn luyện: tự tạo sinh các biến thể (Formal proofs) rồi tìm đáp án (chứng minh hoặc bác bỏ) cho đến khi một lời giải đầy đủ được tìm thấy

-

AlphaGeometry.

Ngày 17/1/2024, DeepMind giới thiệu giải pháp AlphaGeometry. Họ quảng bá rằng AlphaGeometry có thể giải được các bài toán hình học trong đề thi IMO: 25/30 bài trong khung thời gian quy định. Cùng lúc đó họ cũng đăng bài báo trên tạp chí Nature. Bản AlphaGeometry mà DeepMind dùng để giải Bài 4 trong đề thi IMO2024 là bản nâng cấp, họ gọi bản này là AlphaGeometry 2.0, còn bản đăng ngày 17/1/2024 là AlphaGeometry 1.0.

AlphaGeometry thuộc lớp phần mềm chứng minh định lý hình học một cách tự động (Automated Geometry Theorem Prover). Chúng ta có thể hình dung thế này: khi cho (Giả thiết, Kết luận) thì AlphaGeometry sẽ tạo sinh ra phần Chứng minh:

 

[Giả thiết, Kết luận] → [AlphaGeometry] → [Chứng minh]

 

Hẳn nhiên, tất cả chúng ta đều đã quá quen với hình học: điểm, đường thẳng, đường song song, đường vuông góc, trung điểm, nội tiếp, đường tròn, tam giác đồng dạng,… Có một điểm gây khó cho phần lập trình là tất cả các phần ⟪Giả thiết⟫, ⟪Kết luận⟫, ⟪Chứng minh⟫ đều được diễn tả bằng ngôn ngữ ký hiệu.

AlphaGeometry tự giới hạn mình trong hình học phẳng (Euclidean plane geometry), đồng thời loại trừ các chủ đề như bất đẳng thức hình học và hình học tổ hợp. Họ tiếp cận theo hướng mã hóa các ký hiệu hình học thành Deductive Database (cơ sở dữ liệu suy diễn, viết tắt là DD). Để đi đến ⟪Kết luận⟫, DD xuất phát từ tập hợp các Giả thiết suy diễn qua các bước trung gian và cuối cùng đi đến Kết luận. Ví dụ, phải cần đến n bước trung gian để chứng minh Kết luận, chúng ta có thể hình dung quy trình suy diễn của DD như sau:

Giả thiết ⇒ ⟪Kết luận 1⟫ ⇒ ⟪Kết luận 2⟫ ⇒ … ⇒ ⟪Kết luận n⟫ ⇒ Kết luận

(Thực tế, AlphaGeometry sử dụng “cây suy diễn” chứ không phải “phẳng” như minh họa trên – tôi đơn giản hóa cho dễ hiểu.)

Ngoài DD, AlphaGeometry còn sử dụng một bộ quy tắc nữa có tên là quy tắc đại số, đặt tên là AR (algebraic rules).

Vì sao phải thêm quy tắc đại số AR? Theo bài báo giải thích thì lý do là vì các bài toán hình học có độ khó ở mức IMO thường liên quan đến phương pháp trong hình học gọi là “angle/ratio/distance chasing”. Tôi tạm dịch là “phương pháp đuổi góc/đuổi tỷ số/đuổi khoảng cách”. Các phương pháp này có liên quan đến tính toán ở mức đơn giản. Ví dụ, hai góc phụ nhau có tổng bằng 90 độ, hai góc bù nhau có tổng bằng 180 độ.

 Khởi tạo dữ liệu.

AlphaGeometry khởi tạo dữ liệu huấn luyện bằng cách tạo sinh ra một tỷ biểu đồ ngẫu nhiên của các đối tượng hình học và suy ra toàn bộ các mối quan hệ giữa các điểm và đường trong mỗi biểu đồ. Từ mỗi biểu đồ vừa được tạo sinh, người ta áp dụng các quy tắc suy diễn để được một “cây suy diễn” và tạo dựng toàn bộ các ⟪Kết luận⟫ có thể có từ biểu đồ này (⟪Kết luận⟫ chính là các nút “nhánh” của “cây”). Từ đó, người ta tạo ra tất cả các ⟪Chứng minh⟫ có thể có từ mỗi biểu đồ. (⟪Chứng minh⟫ là dãy duy diễn xuất phát từ nút gốc đi đến một nút “lá” của “cây”). Sau khi lọc, khử các mẫu trùng lặp hoặc hình đồng dạng, người ta được khoảng 100 triệu mẫu. Chú ý rằng tất cả các mẫu này đều có cấu trúc: (⟪Giả thiết⟫, ⟪Kết luận⟫, ⟪Chứng minh⟫). Với số lượng mẫu khổng lồ như vậy, người ta kỳ vọng các bài toán trong thực tế sẽ giống hoặc tương tự như mẫu tạo sẵn.

 

 Huấn luyện sử dụng mô hình Transformer.

Sau khi có dữ liệu ban đầu 100 triệu mẫu, họ sử dụng một LLM (trên nền mô hình Transformer) để huấn luyện. Người ta xếp một cách tuần tự ‘⟪Giả thiết⟫, ⟪Kết luận⟫, ⟪Chứng minh⟫’, … làm dữ liệu đầu vào cho LLM. Sau khi huấn luyện thì LLM sẽ tạo sinh ra ⟪Chứng minh⟫ với điều kiện là (⟪Giả thiết⟫, ⟪Kết luận⟫).

 

 Kết hợp LLM với Symbolic Engine.

Ở mức tổng quan, việc tìm ⟪Chứng minh⟫ là sự phối hợp nhịp nhàng giữa LLM và Symbolic Deduction Engine (bộ máy suy diễn ký hiệu). Việc tìm (Search) lời giải là một vòng lặp với một trong 2 điều kiện dừng:

  • Nếu “bộ máy suy diễn ký hiệu” tìm ra ⟪Kết luận⟫ thì việc chứng minh hoàn tất – dừng.
  • Nếu số vòng lặp lớn hơn một con số N nào đó – dừng – không tìm ra lời giải.

 

▼ Bên lề: Tác giả của AlphaGeometry 1.0 là ai?

Bài viết trên blog của DeepMind với tiêu đề “AlphaGeometry: An Olympiad-level AI system for geometry” ngày 17/01/2024 có nhóm tác giả là Trieu Trinh and Thang Luong. Đây chính là TS. Trịnh Hoàng Triều và TS. Lương Minh Thắng – người Việt.

Bài trên tờ Nature với tiêu đề “Solving olympiad geometry without human demonstrations” ngày 17/01/2024 có nhóm tác giả gồm Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He & Thang Luong. Ngoài Trieu H. Trinh (Trịnh Hoàng Triều) và Thang Luong (Lương Minh Thắng) chúng ta còn thấy Quoc V. Le: đây chính là TS. Lê Viết Quốc – người Việt.

Mở ngoặc ⦅

TS. Lê Viết Quốc là người đồng sáng lập Google Brain cùng với các huyền thoại về Machine Learning như Jeff Dean, Andrew Ng (Ngô Ân Đạt).

Đóng ngoặc⦆

Căn cứ theo thứ tự các tác giả trong 2 bài báo nói trên thì tôi đoán TS. Trịnh Hoàng Triều là tác giả chính của AlphaGeometry 1.0.

▲ Hết bên lề

-

o1-preview.

OpenAI không nói rõ là o1-preview giải toán bằng cách nào. Họ chỉ nói chung chung là kết hợp Chain of Thought với Reinforcement Learning. Vì OpenAI không nói rõ nên tôi “đoán mò” thông qua các bài báo nói về Chain of Thought  Reinforcement Learning.

 Chain of Thought (CoT)

Bắt chước phương pháp suy luận của con người CoT chia một vấn đề phức tạp thành nhiều vấn đề đơn giản, lần lượt giải các vấn đề đơn giản, sau cùng tổng hợp kết quả của các vấn đề đơn giản để đưa ra lời giải cuối cùng. Trong Prompt Engineering, nếu người dùng muốn sử dụng CoT thì phải yêu cầu LLM thực hiện (nói rõ trong Prompt). Đây được gọi là phương pháp sử dụng CoT một cách thủ công. Tôi đoán là trong o1-preview họ đã tự động hóa CoT. Ví dụ, trong việc giải các bài toán phổ thông, đầu tiên người ta nhận dạng bài toán, tìm CoT tương ứng cho bài toán đó, rồi “áp” CoT đó trong lập luận của mình để giải. Tập hợp các CoT thuộc nhóm “giải các bài toán” đã được huấn luyện từ trước (Pre-training).

 Reinforcement Learning (RL)

Tôi xin phép “diễn nôm” RL: RL là một lĩnh vực con của Machine Learning, nghiên cứu cách thức một Agent trong một môi trường nên chọn thực hiện các hành động (Action) theo một Policy nhằm cực đại hóa một khoản thưởng (Reward) nào đó về lâu dài. Có thể nói một cách đơn giản cho dễ hiểu: RL “mày mò” tìm đường tối ưu để đi đến mục tiêu.

-

Tóm lại: thông qua RL, o1-preview học cách mài giũa CoT (chuỗi suy nghĩ) và tinh chỉnh các Policy (chiến lược) mà nó sử dụng. Nó học cách nhận ra và sửa lỗi của mình. Nó học cách chia nhỏ các bước khó thành các bước đơn giản hơn. Nó học cách thử một cách tiếp cận khác khi cách tiếp cận hiện tại không hiệu quả. Quá trình này làm cho o1 khả năng lập luận của nó được cải tiến theo thời gian.

Ⓕ. Suy ngẫm chậm.

Liệu có mối liên hệ nào giữa giỏi Toán và giỏi Machine Learning không? Tôi cho rằng là có, nhưng không rõ tương quan đạt đến mức nào.

Qua hiện tượng phát triển một cách đột biến của LLM, rồi qua các ví dụ về cách giải toán của AlphaProof và AlphaGeometry, tôi có cảm nhận là khi lượng đổi thì chất đổi. Cách đây không lâu (cuối năm 2022, đầu năm 2023), khi ChatGPT mới ra đời, ít người đoán là LLM có khả năng lập luận. Tuy nhiên, với hàng loạt LLM xuất hiện gần đây, thực tế đang nói lên điều ngược lại.

Khi học toán phổ thông, ngoài kỹ năng lập luận logic, thường chúng ta phải “thuộc” nhiều dạng bài toán. Khi gặp một bài toán thuộc dạng chúng ta đã biết, thì khỏi phải suy nghĩ, chúng ta chấp bút làm ngay. Tôi cảm nhận là AlphaProof và AlphaGeometry tiếp cận theo hướng này. Chúng “nạp” kiến thức càng nhiều càng tốt và khi gặp một bài toán thuộc loại chúng đã làm quen thì trong nháy mắt chúng cho ngay lời giải.

-

Trân trọng & vui nhã

(_/)
( •_•)
/ >☕

LeVanLoi