AlphaGeometry, hệ thống AI hình học ở trình độ Olympic
(deepmind.google)- Khi Olympic Toán học Quốc tế trở thành phép thử cho suy luận toán học của AI, AlphaGeometry đã giải được 25 trong số 30 bài hình học trong thời gian giới hạn, tiệm cận mức trung bình 25,9 bài của các thí sinh đạt huy chương vàng
- Cốt lõi là sự kết hợp giữa mô hình ngôn ngữ mạng nơ-ron và bộ máy suy luận ký hiệu dựa trên quy tắc, xử lý việc đề xuất cấu hình mang tính trực giác và xác minh logic hình thức trong cùng một vòng lặp
- 100 triệu ví dụ tổng hợp độc nhất được tạo mà không cần trình diễn của con người đã giảm nút thắt dữ liệu học, trong đó 9 triệu ví dụ bao gồm các cấu hình bổ trợ cần thiết cho chứng minh
- Mọi lời giải Olympic đều đã được máy tính xác minh; Evan Chen đánh giá rằng đầu ra vừa có thể kiểm chứng bằng máy, vừa con người có thể đọc được, đồng thời tuân theo các quy tắc hình học cổ điển mà học sinh sử dụng
- Dù phạm vi áp dụng còn hạn chế vì trong một kỳ IMO thường chỉ có 2 trên 6 bài là hình học, đây là mô hình AI đầu tiên chỉ với năng lực hình học đã có thể vượt chuẩn huy chương đồng IMO năm 2000 và 2015
Thành tích trên benchmark hình học IMO
- AlphaGeometry, được công bố trên Nature, giải các bài hình học phức tạp ở mức gần với thí sinh đạt huy chương vàng Olympic của con người
- Benchmark gồm 30 bài hình học IMO-AG-30 được chọn từ các kỳ Olympic từ năm 2000 đến 2022
- AlphaGeometry: giải 25 bài trong thời gian giới hạn
- Cách tiếp cận tốt nhất trước đó, Wu’s method: giải 10 bài
- Trung bình thí sinh đạt huy chương vàng: giải 25,9 bài
- Google DeepMind đã mở mã nguồn mã và mô hình AlphaGeometry
Cấu trúc hệ thống nơ-ron-ký hiệu
- AlphaGeometry là một hệ thống nơ-ron-ký hiệu, trong đó mô hình ngôn ngữ mạng nơ-ron và bộ máy suy luận ký hiệu cùng tìm chứng minh cho các định lý hình học phức tạp
- Mô hình ngôn ngữ nhanh chóng nhận diện các mẫu và quan hệ chung từ dữ liệu, dự đoán những cấu hình có khả năng hữu ích
- Tuy nhiên, khả năng suy luận chặt chẽ hoặc giải thích quyết định có thể còn thiếu
- Bộ máy suy luận ký hiệu đi đến kết luận theo logic hình thức và các quy tắc rõ ràng
- Có thể giải thích được và hợp lý, nhưng khi tự xử lý các bài toán lớn thì có thể chậm và kém linh hoạt
- Khi dùng hai thành phần cùng nhau, mô hình ngôn ngữ đề xuất các thành phần bổ trợ như điểm, đường thẳng, đường tròn mới, còn bộ máy suy luận dựa trên đó để rút ra thêm kết luận về hình
Vòng lặp giải bài để tìm cấu hình bổ trợ
- Các bài hình học Olympic đôi khi không thể giải ngay chỉ với hình đã cho, mà cần thêm các thành phần hình học mới cần thiết cho lời giải
- Quy trình giải của AlphaGeometry vận hành bằng cách luân phiên giữa suy luận ký hiệu và đề xuất của mô hình ngôn ngữ
- Từ hình đã cho và các tiền đề của định lý, bộ máy suy luận ký hiệu suy ra các mệnh đề mới
- Nếu không tìm được lời giải hoặc không thể tạo thêm mệnh đề mới, mô hình ngôn ngữ thêm một thành phần bổ trợ có khả năng hữu ích
- Thành phần được thêm mở ra đường đi mới cho bộ máy suy luận, và quá trình này được lặp lại cho đến khi tìm ra lời giải
- Trong bài số 3 của Olympic Toán học Quốc tế năm 2015, lời giải của AlphaGeometry gồm 109 bước logic
Tạo 100 triệu dữ liệu tổng hợp
- Hình học dựa trên việc hiểu không gian, khoảng cách, hình dạng và vị trí tương đối, đồng thời là nền tảng của nhiều lĩnh vực như nghệ thuật, kiến trúc và kỹ thuật
- Cách tạo dữ liệu tổng hợp của AlphaGeometry mô phỏng ở quy mô lớn quá trình con người quan sát hình vẽ và dùng tri thức sẵn có để tìm các tính chất và quan hệ hình học mới
- Hệ thống tạo 1 tỷ hình ngẫu nhiên bằng điện toán song song hóa cao
- Suy ra toàn bộ các quan hệ giữa điểm và đường thẳng trong mỗi hình
- Tìm tất cả các chứng minh có trong mỗi hình
- Truy ngược để xác định cần những thành phần bổ sung nào để đi đến chứng minh đó
- Quá trình này được gọi là suy luận ký hiệu và truy ngược (symbolic deduction and traceback)
- Kho dữ liệu khổng lồ được lọc để loại các ví dụ tương tự, cuối cùng trở thành 100 triệu ví dụ học độc nhất với độ khó đa dạng
- Trong đó 9 triệu ví dụ là các trường hợp có thêm thành phần bổ trợ
- Mô hình ngôn ngữ học nhiều ví dụ trong đó cấu hình bổ trợ dẫn đến chứng minh, nhờ đó có thể đề xuất cấu hình mới cả trong các bài Olympic
Khả năng xác minh và giới hạn áp dụng
- Tất cả lời giải bài Olympic do AlphaGeometry cung cấp đều đã được máy tính kiểm tra và xác minh
- Kết quả được so sánh với các phương pháp AI trước đây và thành tích của con người tại Olympic
- Evan Chen, huấn luyện viên toán học và cựu thí sinh đạt huy chương vàng Olympic, đã đánh giá một số lời giải
- Đầu ra của AlphaGeometry có thể xác minh được và gọn gàng
- Trước đây, lời giải AI cho các bài thi dựa trên chứng minh khi thì đúng khi thì sai, nên có thể cần con người kiểm tra
- Lời giải của AlphaGeometry có cấu trúc có thể kiểm chứng bằng máy nhưng vẫn con người có thể đọc được
- Thay vì đẩy mạnh các phép tính đại số khổng lồ bằng hệ tọa độ, hệ thống dùng các quy tắc hình học cổ điển như góc và tam giác đồng dạng giống như học sinh
- Một kỳ IMO gồm 6 bài, và thường chỉ 2 bài trong số đó tập trung vào hình học
- Vì vậy AlphaGeometry chỉ có thể áp dụng cho khoảng một phần ba số bài của một kỳ
- Dù vậy, đây là mô hình AI đầu tiên chỉ với năng lực hình học đã có thể vượt chuẩn huy chương đồng IMO năm 2000 và 2015
Mở rộng sang AI suy luận toán học
- AlphaGeometry cho thấy AI ngày càng có năng lực suy luận logic và khám phá, xác minh tri thức mới
- Giải các bài hình học ở trình độ Olympic là một cột mốc quan trọng hướng tới suy luận toán học sâu hơn và các hệ thống AI đa dụng tiên tiến hơn
- Cách tiếp cận huấn luyện AI từ đầu bằng dữ liệu tổng hợp quy mô lớn có thể tác động đến cách khám phá tri thức mới trong khoa học và AI, vượt ra ngoài toán học
- AlphaGeometry nằm trong dòng công việc về AI suy luận toán học của Google DeepMind và Google Research
- Khám phá vẻ đẹp của toán học thuần túy theo những cách mới
- Dùng mô hình ngôn ngữ với Minerva để giải các bài toán và khoa học
- FunSearch sử dụng mô hình ngôn ngữ lớn để tạo ra phát hiện đầu tiên trong một bài toán mở của khoa học toán học
- Mục tiêu dài hạn là tạo ra các hệ thống AI có thể khái quát hóa trên nhiều lĩnh vực toán học, phát triển năng lực giải quyết vấn đề và suy luận tinh vi cần thiết cho các hệ thống AI đa dụng, đồng thời mở rộng ranh giới tri thức của con người
1 bình luận
Ý kiến trên Hacker News
Từ góc nhìn của một người từng ra đề cho các kỳ thi như IMO, tôi đọc bài báo này với rất nhiều hứng thú. Đồng thời, tôi cho rằng trong AI, tức là các chỉ mục tri thức thông minh và chỉ mục phương thức suy luận, chủ đề đầu tiên bị “đánh sập” chắc chắn phải là hình học
Trong các chủ đề Olympic toán, bài hình học nhìn chung là “máy móc” nhất. Nếu có thể biểu diễn bài toán bằng tọa độ, chẳng hạn tọa độ XY hoặc mặt phẳng phức, thì sẽ có một tập hữu hạn các bước mà máy tính có thể dùng để tìm lời giải. Tất nhiên, tại IMO thực tế, giới hạn thời gian và sai sót của con người khiến cách này khó khả thi. Trước đây tôi từng dùng WolframAlpha theo cách này để kiểm chứng chứng minh cho các bài hình học và phỏng đoán do tôi tạo ra
Đại số, đặc biệt là bất đẳng thức, cũng tương tự: nếu đẩy mạnh tính toán đủ lớn thì trong nhiều trường hợp sẽ ra đáp án
Những lĩnh vực mà tôi muốn thấy hệ thống thông minh thật sự tiến bộ là lý thuyết số và tổ hợp. Không gian tìm kiếm phức tạp hơn nhiều, và thường đòi hỏi chứng minh rằng một điều gì đó là bất khả thi. Những bài toán như vậy khó giải bằng tính toán vét cạn
Tôi đồng ý rằng hình học sẽ là lĩnh vực đầu tiên. Theo những gì thấy ở đây, đây không phải là “vét cạn” theo nghĩa dựa vào hình học đại số, vector hay lời giải bằng số phức, nhưng khá gần với tìm kiếm vét cạn theo nghĩa rà soát mọi phép dựng phụ “thú vị”
Hình học luôn là môn tệ nhất của tôi, nhưng tôi từng cảm thấy rằng nếu được cho đúng phép dựng, bài toán sẽ dễ hơn nhiều. Chỉ là tôi không học được trực giác để nhanh chóng nghĩ ra phép dựng như vậy. AI này dường như cũng không có trực giác đó, nhưng có thể tuôn ra chúng nhanh hơn nhiều. Các ứng viên có thể dựng được như đường vuông góc, đường song song, đường phân giác rốt cuộc cũng hữu hạn, và có thể đánh giá khá máy móc bằng cách trải hết các góc và tỉ số, hoặc thử dùng lũy thừa của điểm
Rất ấn tượng, nhưng theo nghĩa “engine so với AI” thì có vẻ như DeepMind:Kasparov::AlphaGeo:Terry Tao
Tôi đồng ý rằng đại số rất có thể là lĩnh vực tiếp theo. Cũng như hình học, thường chỉ cần tìm được một, hai hoặc ba phép thế thông minh, và các lựa chọn thì có giới hạn
Một số bài tổ hợp cũng có thể phù hợp với chiến lược tìm kiếm này. Ví dụ như các bài đếm cùng một đối tượng theo hai cách. Tuy nhiên đó là một cây cầu xa hơn, và chỉ bắt được một phần trong toàn bộ các bài toán
Lý thuyết số có lẽ sẽ là ranh giới cuối cùng trước khi đạt điểm tối đa 42
Sau khi kiểm chứng rằng bài giải được, tôi cũng tò mò họ chọn các bài cụ thể để đưa vào bộ đề cuối cùng như thế nào. Là bỏ phiếu hay dùng một cách đánh giá khác?
Ai đó nên biến hình học tổng hợp thành một game phiêu lưu. Có thể dùng một ngôn ngữ viết chứng minh đơn giản hơn Lean, và cũng có thể làm cho nó trông đẹp mắt về mặt trực quan
Nếu tôi đọc bài báo đúng thì đây có vẻ là một công trình thật sự. Nó chính đáng hơn nhiều so với bài báo toán học AI mà DeepMind tháng trước đã quảng bá sai là giải được một vấn đề nghiên cứu toán học mở. Dù vậy, cấu trúc của nó khác với thứ người ta thường nghĩ là suy luận/trí tuệ tự động đến mức khá đáng chú ý
Tôi hiểu là họ huấn luyện Transformer bằng hàng triệu định lý hình học sơ cấp rồi dùng nó để tìm kiếm vét cạn các chứng minh. Do bối cảnh là hình học sơ cấp nên cấu trúc tất yếu cũng sơ cấp, và đúng/sai có thể được phán định bằng ký hiệu một cách dễ dàng. Tôi nghĩ cách làm là: nếu tìm kiếm vét cạn thất bại, họ ngẫu nhiên thêm các dựng hình phụ như thêm trung điểm, rồi xem với vật liệu bổ sung đó có tìm kiếm được không
Chỉnh sửa: Như phần đính chính của Imnimo, tôi đã hiểu ngược. Tìm kiếm vét cạn là tìm kiếm vét cạn thuần túy, còn Transformer được dùng để dự đoán nên thêm dựng hình phụ nào
Ngoài ra, dù bài blog không nói, các phát biểu bài toán thực tế cũng phải được sửa/chuyển thể. Ví dụ một câu gốc kiểu “Gọi các đường cao của tam giác ABC là AH1, BH2, CH3…” được đổi thành một danh sách định nghĩa tường minh hơn nhiều, kiểu “Gọi ABC là một tam giác. AI định nghĩa điểm I sao cho nó là tia phân giác của góc BAC và CI là tia phân giác của góc ACB…”, và cuối cùng thành dạng “Chứng minh T1I=IZ”
Quy trình bạn mô tả chính xác là quy trình con người dùng. Phỏng đoán thứ có vẻ hữu ích, rồi giải các chi tiết một cách cơ học. Nếu bị kẹt thì đưa ra phỏng đoán khác. Rốt cuộc nó giống như duyệt một cái cây
Con người đã nhận ra quy trình này từ năm 1955 và còn tạo ra một nguyên mẫu hoạt động có thể chứng minh định lý: https://en.wikipedia.org/wiki/Logic_Theorist Điểm cốt lõi nằm ở việc dùng heuristic tốt. Mạng nơ-ron có thể rút ra heuristic từ dữ liệu, nên ở đây nó có ý nghĩa
Tôi tò mò bạn nghĩ ý tưởng thông thường về “suy luận tự động” là gì. Một thiết bị ma thuật giải mọi bài toán chỉ trong một lượt tuyến tính sao?
Chỉ sau khi vào khoa toán ở đại học tôi mới học được cách làm đúng và bắt đầu thấy thích
Lĩnh vực này vẫn còn ở giai đoạn đầu, và có vẻ còn nhiều việc dang dở. Phần tìm kiếm nên được thay bằng một mạng nơ-ron nhỏ, còn phần suy luận thì không khó và dường như cũng không cần cải thiện nhiều
Giờ là lúc nâng hiệu năng bằng tự chơi. Trong các bài toán hình học phẳng, có thể xem kết luận cần chứng minh là một điểm của hình, các điều kiện là điểm khác, rồi để hai người chơi di chuyển tối đa về phía nhau và chia sẻ dữ liệu. Trong quá trình đó, đóng góp của mỗi người chơi có thể được ví với cách tính thắng thua trong cờ vây để dùng cho cải thiện hiệu năng
Tôi không thấy mô hình cụ thể này có vẻ khái quát hóa được, nhưng cách tiếp cận thần kinh-ký hiệu thì trông rất hứa hẹn
Đây là cách nối các công cụ “hệ thống 1” ngày càng mạnh — vốn chiếm phần lớn học máy hiện nay — với các công cụ “hệ thống 2” có cấu trúc, như sinh chứng minh logic. Hệ thống 2 có thể lập kế hoạch và kiểm tra tính đúng đắn hoặc giá trị của đầu ra
Hệ thống 2 tiếp tục cho đến khi bị kẹt; khi kẹt, hệ thống 1 cung cấp phỏng đoán trực giác về phần nào của không gian trạng thái nên được kiểm tra tiếp theo
Ở đây họ tận dụng việc máy tính có thể sinh chứng minh để tạo một tập dữ liệu 100 triệu chứng minh, qua đó cho phép học tự giám sát có khả năng mở rộng. Các miền ký hiệu có vẻ là dạng rất phù hợp cho kiểu tạo dữ liệu này. Dù giá trị của từng mẫu riêng lẻ thấp, khi gom lại chúng có thể cho phép tiền huấn luyện hữu ích
Kết hợp các yếu tố này lại thì đây là một cách tiếp cận có thể đi khá xa
Cột mốc then chốt là thoát khỏi nhu cầu phải phụ thuộc vào một miền hình thức/ký hiệu cụ thể, và tạo ra một hệ thống tiền huấn luyện có thể khái quát hóa các kỹ năng học được trong miền đó
Ngoài ra, trong phạm vi các miền áp dụng được, nó giải quyết hoàn toàn một vấn đề căn bản mà làn sóng AI hiện nay gọi là “ảo giác”. Tuy nhiên, cách giải quyết đó khả thi vì có một hệ thống phi AI chứng minh tính chính xác
Nhìn rộng ra, cách tiếp cận này không quá mới. Trong sinh hóa, người ta đã dùng AI để tìm phân tử ứng viên rồi kiểm chứng bằng thí nghiệm vật lý
AI cho trò chơi tổ hợp cũng từ lâu đã dùng AI làm đầu vào cho tìm kiếm Monte Carlo kiểu cũ
Tôi rất cảm kích việc họ công bố mã và trọng số cùng với bài báo. Theo tôi nhớ, đây là bài báo nổi tiếng đầu tiên của DeepMind công bố mã suy luận chạy được và checkpoint. Nếu có ví dụ sớm hơn thì tôi sẵn sàng được đính chính
Tôi vẫn chưa thấy tập huấn luyện công khai hay mã huấn luyện mẫu nào, nhưng dù sao đây cũng là một bước tiến tốt vì họ đã cung cấp thứ gì đó để các nhà nghiên cứu khác có thể xây tiếp lên đó. Suy cho cùng, đó cũng là mục đích của bài báo học thuật
Nếu tôi không nhầm thì họ dùng mô hình t5 phải không? Ít nhất có vẻ họ dùng từ vựng SentencePiece t5
Tôi cũng tò mò họ đã dùng bao nhiêu thời gian GPU để huấn luyện mô hình này, và dùng những tham số huấn luyện nào
Mong đừng hiểu lầm. Hệ thống này rất cuốn hút và cho thấy kỹ thuật ứng dụng nên trông như thế nào. Chỉ là tôi muốn biết thêm về chi tiết huấn luyện, dữ liệu ban đầu và cách tạo dữ liệu tổng hợp
Tôi rất tò mò không biết mô hình ngôn ngữ tạo ra các phép dựng hữu ích thường xuyên đến mức nào. Chắc chắn là tốt hơn ngẫu nhiên, nhưng tôi không rõ liệu nó ném ra hàng nghìn phép dựng cho đến khi tìm được cái tốt, hay đưa ra các đề xuất hữu ích với tỷ lệ tương tự chuyên gia con người
Trong bài báo có nói: “Vì quá trình giải mã của mô hình ngôn ngữ trả về k chuỗi khác nhau mô tả k phép dựng phụ trợ thay thế, chúng tôi dùng điểm của từng beam làm hàm giá trị để thực hiện beam search trên k lựa chọn này. Thiết lập này rất dễ song song hóa giữa các beam, nên tăng tốc đáng kể khi có tài nguyên tính toán song song. Trong thí nghiệm, chúng tôi dùng kích thước beam k=512, số vòng lặp tối đa 16, hệ số phân nhánh ở mỗi nút, tức kích thước batch giải mã, là 32”
Nhưng tôi vẫn chưa hiểu hoàn toàn 512 và 16 quy đổi thành tổng số phép dựng được đề xuất như thế nào. Họ cũng nói rằng ngay cả khi bỏ kích thước beam và số vòng lặp tối đa thì hiệu năng chỉ giảm ở mức nào đó. Điều này có nghĩa là mô hình thực sự xếp các phép dựng hữu ích lên khá cao, và chỉ những bài khó nhất mới cần hàng nghìn cái?
Dù vậy, nếu thử tóm tắt thì con số là 262.144, nhưng không nên hiểu theo nghĩa đen
Đầu ra của hàm giải mã là token, xấp xỉ khoảng 3/4 một từ, nhưng cứ coi là 1 từ đi
Số token được xét cho mỗi token đầu ra là
beam_size * branching_factor * max_iterations = 512 * 32 * 16 = 262.144Có thể đếm số từ trong lời giải mẫu: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
Tổng số token của lời giải là 2289, và tổng số token đã được xét là
262.144 * 2289 = 600.047.616Nếu gượng ép tính “số lời giải đã xét” là tổng số token đã xét / tổng số token của lời giải thì ra 262.144. Nó cũng hợp lý ở chỗ bằng với số token được xem ở mỗi bước lặp
Điều thú vị là Transformer được dùng khá nhỏ. Theo bài báo, họ huấn luyện với cấu hình mặc định của thư viện Meliad, gồm 12 tầng, chiều embedding 1.024, 8 attention head, và các tầng dense giữa attention có chiều 4.096 dùng kích hoạt ReLU
Nếu loại trừ các tầng embedding của input và output head, toàn bộ Transformer có 151 triệu tham số. Tokenizer tùy chỉnh được huấn luyện ở chế độ ‘word’ của SentencePiece và kích thước từ vựng là 757. Độ dài ngữ cảnh tối đa được giới hạn ở 1.024 token và dùng embedding vị trí tương đối kiểu T5. Vì hơn 90% chuỗi có độ dài dưới 200, họ cũng dùng sequence packing
Điều thực sự mới với tôi là ngay cả hệ thống tốt nhất trước đây cũng đã giải được tới 10 bài kiểu này. Tôi từng nghe nói có thuật toán quyết định cho các bài hình học phẳng, nhưng không biết là có thuật toán thực dụng. Tìm thử thì thấy tài liệu tham khảo này: http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf
Tôi vốn đã chuẩn bị nghi ngờ những kết quả kiểu này vì thường chúng bị nói là “không giống chứng minh của con người”, nhưng khi thấy Evan Chen nói đây thực sự là các chứng minh gọn gàng và con người đọc được, tôi đã đổi ý
Evan Chen là nhân vật nổi tiếng trong cộng đồng toán olympiad và cũng là tác giả một cuốn sách hình học olympiad nổi tiếng[1], nên lần này có lẽ phải thừa nhận rằng máy đã thực sự chinh phục một phần các bài IMO
[1]: https://web.evanchen.cc/geombook.html
Dù vậy, ý tưởng O2 nằm trên đường tròn chín điểm là đúng
Chỉnh sửa: tôi rút lại lời trên. Có vẻ họ dùng góc có hướng[2], và nếu vậy thì câu đó đúng
[1]: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
[2]: https://web.evanchen.cc/handouts/Directed-Angles/Directed-An...
Liên quan, https://www.nytimes.com/2024/01/17/science/ai-computers-math... cũng đáng xem
Bài này được dẫn đến qua https://news.ycombinator.com/item?id=39030186, và thread đó dự kiến sẽ được gộp vào đây
Có liên quan: https://aimoprize.com/
Đây là giải thưởng 10 triệu USD dành cho mô hình thể hiện tốt tại IMO