Vào ngày 17 tháng 1 năm 2024, nhóm DeepMind đã xuất bản một bài báo có tiêu đề “Giải hình học Olympic mà không cần sự chứng minh của con người” trên tạp chí Nature.
Bài viết này giới thiệu AlphaGeometry, hệ thống trí tuệ nhân tạo mới nhất của nhóm DeepMind. Như tiêu đề của bài báo đã nêu, AlphaGeometry có thể tự mình giải các bài toán hình học phẳng độ khó Olympic Toán quốc tế. Theo bài báo, trong bài kiểm tra điểm chuẩn của 30 câu hỏi hình học Olympic, AlphaGeometry đã giải được 25 câu trong số đó trong thời gian tiêu chuẩn của Olympic. Để so sánh, hệ thống tiên tiến trước đây đã giải được 10 bài toán hình học này. Tương ứng, những người đoạt huy chương vàng con người giải được trung bình 25,9 vấn đề, những người đoạt huy chương bạc giải được trung bình 22,9 vấn đề và những người đoạt huy chương đồng giải được trung bình 19,3 vấn đề.
Đó là sau khi AlphaGo, cũng do nhóm DeepMind phát triển, đã đánh bại Li Shishi và Ke Jie trong môn cờ vây vào tháng 3 năm 2016 và tháng 5 năm 2017. Đây là lần đầu tiên một hệ thống trí tuệ nhân tạo đạt tới đỉnh cao của người chơi trong lĩnh vực trí tuệ thuần túy cạnh tranh. cấp độ. Đây cũng là thành công đáng kinh ngạc nhất mà hệ thống trí tuệ nhân tạo đạt được trong việc giải quyết các vấn đề toán học kể từ làn sóng hệ thống trí tuệ nhân tạo mô hình ngôn ngữ quy mô lớn mới do ChatGPT kích hoạt vào năm 2022.
Một đặc điểm chính của toán học hiện đại là tiên đề. Cái gọi là toán học tiên đề trước tiên phải thống nhất về một số tiên đề hoặc định đề "không thể bác bỏ". Sau đó dùng điều này làm cơ sở để suy ra các bổ đề, định lý và suy luận thông qua quá trình suy luận logic và toán học, từ đó suy ra toàn bộ hệ thống toán học. Miễn là các tiên đề được chấp nhận thì tất cả các kết quả suy ra phải tự động đúng. Trong hơn một trăm năm qua, các nhà toán học đã dần hoàn thiện việc tiên đề hóa các nhánh khác nhau của toán học. Ví dụ, việc tiên đề hóa lý thuyết xác suất đã được nhà toán học Liên Xô Kolmogorov hoàn thành vào những năm 1930.
Tiên đề hóa hình học phẳng đã xảy ra ở Hy Lạp cổ đại hơn hai nghìn năm trước. Ngay từ năm 300 trước Công nguyên, Euclid đã đưa ra năm tiên đề về hình học phẳng trong cuốn “Các phần tử của hình học”, và dựa vào đó, ông đã chứng minh một cách chặt chẽ hàng chục định lý về hình học phẳng. Vì vậy, hình học phẳng còn được gọi là hình học Euclide.
Việc tiên đề hóa được hoàn thành cực kỳ sớm đã giúp hình học Euclide đạt được những tiến bộ vượt bậc trong thời kỳ Hy Lạp cổ đại. Khi khung lý thuyết của một nhánh toán học được xây dựng và tất cả các vấn đề có thể giải được đều được giải quyết, đối với các nhà toán học, nhánh này mất đi giá trị của việc tiếp tục nghiên cứu. Vì vậy, sự phát triển và trưởng thành quá sớm cũng khiến hình học Euclide trở thành nhánh toán học “chết” đầu tiên.
Tuy nhiên, giống như tiếng Latin chết đã trở thành ngôn ngữ được chỉ định duy nhất để đặt tên các loài trong sinh học vì nó không còn thay đổi nữa, hình học Euclide chết cũng đã đóng một vai trò sâu sắc và lâu dài trong các khía cạnh khác của toán học.
Nhờ hệ thống năm tiên đề trực quan, dễ hiểu của hình học Euclide và quy trình suy luận mệnh đề rõ ràng và ngắn gọn, hình học Euclide đã trở thành khuôn mẫu tốt nhất để học các tiên đề toán học và phương pháp chứng minh. Chính vì vậy, hình học Euclide luôn là một môn học rất quan trọng trong chương trình toán THCS ở giai đoạn giáo dục phổ thông.
Mặt khác, quy trình suy luận rõ ràng của hình học Euclide và các nội dung liên quan đã được nghiên cứu kỹ lưỡng từ rất sớm, khiến hình học Euclide trở thành một nguồn tài nguyên tuyệt vời cho các nhà toán học “Lĩnh vực thực nghiệm”. Trong lịch sử toán học, nhiều phát triển mới về lý thuyết, công cụ và khái niệm toán học lần đầu tiên được thực hiện thông qua các thí nghiệm và suy luận về hình học Euclide.
“Chương trình hình thức chủ nghĩa” do Hilbert đưa ra cách đây hơn một trăm năm cũng bắt đầu với hình học Euclide.
Hệ tiên đề toán học hình thức mà Hilbert muốn thiết lập phải thỏa mãn ba điều kiện. Đó là: tính đầy đủ: tất cả các mệnh đề toán học thực sự đều có thể được phát hiện; tính tự nhất quán: không có mâu thuẫn trong toán học; tính quyết định: khả năng phán đoán tính đúng hay sai của mọi mệnh đề toán học.
Theo yêu cầu của chủ nghĩa hình thức, trước tiên cần có một bảng ký hiệu chỉ với một số lượng ký hiệu hạn chế và những ký hiệu này nên được sử dụng để thay thế ngôn ngữ tự nhiên dùng để thảo luận các vấn đề toán học. Bằng cách sử dụng các ký hiệu này, bạn có thể "đánh vần" các công thức mệnh đề có ý nghĩa giống như bạn sử dụng các chữ cái để đánh vần các từ, tức là "các công thức hình thức". Sau khi xác định các mệnh đề tương ứng là tiên đề, quá trình suy luận logic trong toán học có thể được thay thế bằng các suy luận tượng trưng trong ngôn ngữ và được biểu thị một cách hình thức dưới dạng so sánh giữa các “từ” được tạo thành từ các chuỗi ký hiệu. Nhờ đó, quá trình suy luận toán học đã hoàn toàn trở thành một phép toán biểu tượng “hình thức”.
Theo quan điểm của các nhà toán học theo chủ nghĩa hình thức như Hilbert, tất cả các định lý toán học đã được khám phá và chưa được khám phá đều có thể được viết dưới dạng một chuỗi ký hiệu dài hoặc ngắn như thế này.
Mặc dù định lý về tính bất toàn của Gödel sau đó đã chứng minh rằng bức tranh tổng thể của Hilbert là không thể đạt được đối với toàn bộ hệ thống toán học. Nhưng nếu chỉ giới hạn trong nhánh toán học như hình học Euclide thì hệ tiên đề hình thức Hilbert đã hoàn toàn được thiết lập. Điều này là do hệ tiên đề hình học Euclid không chứa đựng lý thuyết số cơ bản, đây là điều kiện để hình thành định lý bất toàn của Gödel, do đó hệ tiên đề hình học Euclid đã hoàn chỉnh.
Hình học Euclide được hình thức hóa bởi Hilbert được gọi là hình học Hilbert.
Vào những năm 1970, Wu Wenjun đã sử dụng phương pháp đại số và ký hiệu này để kết hợp hình học Euclide với khoa học máy tính, đi tiên phong trong hướng chứng minh định lý hình học máy và thúc đẩy sự phát triển của các chứng minh toán học tự động được cơ giới hóa. Bộ chứng minh tự động được cơ giới hóa này, được cộng đồng toán học gọi là "phương pháp Wu", thay thế lý luận toán học trừu tượng bằng các phép tính và suy luận hình thức và ký hiệu phức tạp, từ đó sử dụng máy tính để hỗ trợ các nhà toán học khám phá các cấu trúc tự nhiên và thu được các chân lý toán học.
Việc chứng minh định lý hình học tự động dựa trên phương pháp của Wu trước tiên cần đại số hóa bài toán hình học, chuyển các điều kiện hình học và kết luận hình học đưa ra trong mệnh đề thành các phương trình đa thức, sau đó sử dụng các thuật toán máy tính cụ thể để tính các đa thức này và cuối cùng xác định xem mệnh đề hình học có là đúng. .
Bởi vì hình học Euclide là hoàn chỉnh nên tất cả các mệnh đề trong hình học Euclide đều có thể được chứng minh hoặc chứng minh sai trong một số bước giới hạn bằng cách sử dụng ngôn ngữ hình thức tượng trưng. Vì vậy, về mặt lý thuyết, phương pháp Wu do Wu Wenjun phát minh có thể chứng minh hoàn toàn tất cả các định lý của hình học Euclide.
Cái gọi là "về mặt lý thuyết" ở đây cũng giống như nói về mặt lý thuyết, chỉ có một số cách hạn chế để chơi cờ vây theo luật, vì vậy bạn có thể tìm ra chiến lược chiến thắng bằng cách làm hết tất cả các bước. Trong hoạt động thực tế, phương pháp của Wu chỉ có thể giải được một số bài toán hình học nhất định do hạn chế về khả năng tính toán và thời gian.
Mặc dù vậy, trước sự bùng nổ của trí tuệ nhân tạo trong những năm gần đây, phương pháp của Wu và các phiên bản cải tiến liên quan của nó vẫn là phương pháp hiệu quả nhất để máy móc chứng minh các mệnh đề hình học Euclide. "Hệ thống tiên tiến nhất trước đây" được đề cập ở đầu bài viết này và được dùng để so sánh với AlphaGeometry, hệ thống "giải được 10 bài toán hình học", là phương pháp của Wu.
AlphaGeometry là một hệ thống ký hiệu thần kinh, chủ yếu bao gồm mô hình ngôn ngữ thần kinh (mô hình ngôn ngữ lớn) và công cụ suy luận ký hiệu.
Trong hai phần này, các mô hình ngôn ngữ lớn rất giỏi trong việc xác định các mẫu và mối quan hệ chung trong dữ liệu, do đó chúng có thể nhanh chóng dự đoán các cấu trúc có thể hữu ích. Nhưng thông thường, các mô hình ngôn ngữ lớn thiếu khả năng suy luận hoặc giải thích chặt chẽ. Đây cũng là lý do khiến các mô hình ngôn ngữ quy mô lớn trước đây, trong đó có ChatGPT và GPT-4, có hiệu suất không đạt yêu cầu về mặt khả năng toán học.
Trong AlphaGeometry, điểm yếu này của các mô hình ngôn ngữ lớn được giải quyết bằng một phần khác, đó là công cụ suy luận tượng trưng. Công cụ suy luận tượng trưng dựa trên logic hình thức và sử dụng các quy tắc rõ ràng để đưa ra kết luận. Hai phần này phối hợp với nhau, tương tự như các khái niệm của Hệ thống 1 và Hệ thống 2 được đề cập trong cuốn sách “Tư duy, nhanh và chậm” của Kahneman. Hệ thống 1 cung cấp những ý tưởng nhanh chóng, “trực quan”, trong khi Hệ thống 2 cung cấp “những quyết định chu đáo hơn, hợp lý hơn” ý tưởng.
Để đào tạo các mô hình ngôn ngữ lớn, DeepMind đã xây dựng một mô hình chứa 151 triệu tham số cho AlphaGeometry. Việc đào tạo trước được tiến hành về "mệnh đề, kết luận và chứng minh" và 500 triệu chứng minh hình học đã được tổng hợp, trong đó có 9 triệu câu hỏi có các dòng phụ trợ.
Thông qua khóa đào tạo này, DeepMind đã dạy thành công mô hình ngôn ngữ lớn của AlphaGeometry những kỹ năng quan trọng nhất trong chứng minh hình học: cộng và sử dụng các đường phụ.
AlphaGeometry có thể liệt kê đầy đủ các mệnh đề có thể thu được từ mỗi hình hình học. Và lần lượt có thể truy ngược lại tập hợp các hình hình học có trong mỗi mệnh đề. Trong quá trình giải quyết vấn đề, AlphaGeometry sẽ tìm kiếm các mệnh đề có thể thu được từ các hình hình học trong các điều kiện của bài toán, cũng như tập hợp các hình hình học chứa các mệnh đề kết luận cần được chứng minh bằng bài toán. Tìm vị trí của đường phụ bằng cách so sánh sự khác biệt giữa các đối tượng bộ sưu tập trong hai bộ sưu tập.
Mặc dù AlphaGeometry là hiện thân của giai đoạn hiện tại của các mô hình ngôn ngữ lớn, "dữ liệu đủ tốt có nghĩa là trí thông minh đủ tốt", tính năng thẩm mỹ bạo lực này sử dụng một số lượng lớn tham số và bộ mẫu lớn để giải quyết vấn đề. Tuy nhiên, bản thân AlphaGeometry phụ thuộc rất nhiều vào các đặc điểm của hình học Euclide. Như đã đề cập ở trên, hình học Euclide là một nhánh rất đặc biệt của toán học. Liệu cách tiếp cận này của AlphaGeometry có thể được mở rộng sang các nhánh toán học khác hay không vẫn chưa được biết.
Hơn nữa, như Yang Likun và những người khác đã đề cập nhiều lần, tỷ lệ sử dụng dữ liệu của các mô hình ngôn ngữ lớn ở giai đoạn này khá thấp. Đơn giản chỉ để giải các bài toán hình học, các tham số và tập huấn luyện của AlphaGeometry đã đạt đến cấp độ này. Do đó, ngay cả khi cách tiếp cận của AlphaGeometry có thể được mở rộng sang các bài toán tổng quát theo một cách nào đó, đối mặt với nhiều loại bài toán khác nhau, thì số lượng tham số và tập huấn luyện mà một hệ thống trí tuệ nhân tạo như vậy yêu cầu vẫn còn rất hạn chế ở cấp độ thực tế hiện nay. không thể đạt được.
Tuy nhiên, khả năng suy luận logic ngày càng tăng của trí tuệ nhân tạo cũng như khả năng khám phá và xác minh kiến thức mới do AlphaGeometry thể hiện vẫn đủ ấn tượng.
Như một trong những tác giả của AlphaGeometry đã nói trên mạng xã hội: "Vẫn còn những ngày đầu để chính thức hóa tổ hợp và việc xây dựng các công cụ biểu tượng mạnh mẽ cho các lĩnh vực khác nhau đòi hỏi phải có kiến
thức chuyên môn sâu về miền. Chúng tôi xem xét việc áp dụng khuôn khổ này cho phạm vi rộng hơn trong tương lai." làm việc và mong muốn có những đổi mới hơn nữa để giải quyết những thách thức này."
Đánh giá từ nội dung trong bài viết, ý tưởng về AlphaGeometry rất đơn giản, nhưng những khó khăn về mặt kỹ thuật trong các chi tiết khác nhau và phương pháp giải quyết những khó khăn này là rất phi thường. Điều này phản ánh đầy đủ khả năng và sự kiên trì bền bỉ của tác giả. Vì vậy, rõ ràng là còn quá sớm để đưa ra kết luận về AlphaGeometry, nhưng tất cả những gì đã thể hiện trong việc hoàn thành tác phẩm của AlphaGeometry cho chúng ta lý do để mong chờ vào tác phẩm trong tương lai của tác giả.
Bài viết này giới thiệu AlphaGeometry, hệ thống trí tuệ nhân tạo mới nhất của nhóm DeepMind. Như tiêu đề của bài báo đã nêu, AlphaGeometry có thể tự mình giải các bài toán hình học phẳng độ khó Olympic Toán quốc tế. Theo bài báo, trong bài kiểm tra điểm chuẩn của 30 câu hỏi hình học Olympic, AlphaGeometry đã giải được 25 câu trong số đó trong thời gian tiêu chuẩn của Olympic. Để so sánh, hệ thống tiên tiến trước đây đã giải được 10 bài toán hình học này. Tương ứng, những người đoạt huy chương vàng con người giải được trung bình 25,9 vấn đề, những người đoạt huy chương bạc giải được trung bình 22,9 vấn đề và những người đoạt huy chương đồng giải được trung bình 19,3 vấn đề.
Đặc điểm của hình học phẳng
Khác với Leandojo, một hệ thống trí tuệ nhân tạo giải quyết tất cả các bài toán toán học được nêu trong một bài báo do các học giả từ Caltech, NVIDIA, MIT và các tổ chức khác đồng viết vào năm 2023, hệ thống trí tuệ nhân tạo do DeepMind phát hành lần này được thiết kế đặc biệt để giải hình học phẳng trong toán học. Điều này có thể được nhìn thấy từ tên của AlphaGeometry, Alpha Geometry. Điều này là do, trong số tất cả các nhánh của toán học, hình học phẳng là cực kỳ đặc biệt.Một đặc điểm chính của toán học hiện đại là tiên đề. Cái gọi là toán học tiên đề trước tiên phải thống nhất về một số tiên đề hoặc định đề "không thể bác bỏ". Sau đó dùng điều này làm cơ sở để suy ra các bổ đề, định lý và suy luận thông qua quá trình suy luận logic và toán học, từ đó suy ra toàn bộ hệ thống toán học. Miễn là các tiên đề được chấp nhận thì tất cả các kết quả suy ra phải tự động đúng. Trong hơn một trăm năm qua, các nhà toán học đã dần hoàn thiện việc tiên đề hóa các nhánh khác nhau của toán học. Ví dụ, việc tiên đề hóa lý thuyết xác suất đã được nhà toán học Liên Xô Kolmogorov hoàn thành vào những năm 1930.
Tiên đề hóa hình học phẳng đã xảy ra ở Hy Lạp cổ đại hơn hai nghìn năm trước. Ngay từ năm 300 trước Công nguyên, Euclid đã đưa ra năm tiên đề về hình học phẳng trong cuốn “Các phần tử của hình học”, và dựa vào đó, ông đã chứng minh một cách chặt chẽ hàng chục định lý về hình học phẳng. Vì vậy, hình học phẳng còn được gọi là hình học Euclide.
Việc tiên đề hóa được hoàn thành cực kỳ sớm đã giúp hình học Euclide đạt được những tiến bộ vượt bậc trong thời kỳ Hy Lạp cổ đại. Khi khung lý thuyết của một nhánh toán học được xây dựng và tất cả các vấn đề có thể giải được đều được giải quyết, đối với các nhà toán học, nhánh này mất đi giá trị của việc tiếp tục nghiên cứu. Vì vậy, sự phát triển và trưởng thành quá sớm cũng khiến hình học Euclide trở thành nhánh toán học “chết” đầu tiên.
Tuy nhiên, giống như tiếng Latin chết đã trở thành ngôn ngữ được chỉ định duy nhất để đặt tên các loài trong sinh học vì nó không còn thay đổi nữa, hình học Euclide chết cũng đã đóng một vai trò sâu sắc và lâu dài trong các khía cạnh khác của toán học.
Nhờ hệ thống năm tiên đề trực quan, dễ hiểu của hình học Euclide và quy trình suy luận mệnh đề rõ ràng và ngắn gọn, hình học Euclide đã trở thành khuôn mẫu tốt nhất để học các tiên đề toán học và phương pháp chứng minh. Chính vì vậy, hình học Euclide luôn là một môn học rất quan trọng trong chương trình toán THCS ở giai đoạn giáo dục phổ thông.
Mặt khác, quy trình suy luận rõ ràng của hình học Euclide và các nội dung liên quan đã được nghiên cứu kỹ lưỡng từ rất sớm, khiến hình học Euclide trở thành một nguồn tài nguyên tuyệt vời cho các nhà toán học “Lĩnh vực thực nghiệm”. Trong lịch sử toán học, nhiều phát triển mới về lý thuyết, công cụ và khái niệm toán học lần đầu tiên được thực hiện thông qua các thí nghiệm và suy luận về hình học Euclide.
Đại số hóa, tọa độ, ký hiệu hóa và cơ giới hóa
Về mặt lịch sử, "sự biến đổi" hoàn chỉnh đầu tiên của hình học Euclide đến từ Descartes. Bằng cách đưa ra các khái niệm số học về hệ tọa độ và các đoạn thẳng, Descartes coi một điểm trên mặt phẳng là một cặp số thực có thứ tự, trong khi các hình hình học như đường thẳng và đường tròn có thể được biểu diễn bằng một mối quan hệ đại số cụ thể. Trong cuốn sách Hình học của mình, Descartes đã chứng minh rằng các bài toán hình học có thể được quy giản thành các bài toán đại số. Hơn nữa, các tính chất hình học có thể được phát hiện và chứng minh thông qua các phép toán đại số. Kết quả là Descartes đã tích hợp thành công đại số và hình học, hai môn hoàn toàn tách biệt vào thời điểm đó, và thành lập nên một nhánh toán học mà sau này được gọi là hình học giải tích.“Chương trình hình thức chủ nghĩa” do Hilbert đưa ra cách đây hơn một trăm năm cũng bắt đầu với hình học Euclide.
Hệ tiên đề toán học hình thức mà Hilbert muốn thiết lập phải thỏa mãn ba điều kiện. Đó là: tính đầy đủ: tất cả các mệnh đề toán học thực sự đều có thể được phát hiện; tính tự nhất quán: không có mâu thuẫn trong toán học; tính quyết định: khả năng phán đoán tính đúng hay sai của mọi mệnh đề toán học.
Theo yêu cầu của chủ nghĩa hình thức, trước tiên cần có một bảng ký hiệu chỉ với một số lượng ký hiệu hạn chế và những ký hiệu này nên được sử dụng để thay thế ngôn ngữ tự nhiên dùng để thảo luận các vấn đề toán học. Bằng cách sử dụng các ký hiệu này, bạn có thể "đánh vần" các công thức mệnh đề có ý nghĩa giống như bạn sử dụng các chữ cái để đánh vần các từ, tức là "các công thức hình thức". Sau khi xác định các mệnh đề tương ứng là tiên đề, quá trình suy luận logic trong toán học có thể được thay thế bằng các suy luận tượng trưng trong ngôn ngữ và được biểu thị một cách hình thức dưới dạng so sánh giữa các “từ” được tạo thành từ các chuỗi ký hiệu. Nhờ đó, quá trình suy luận toán học đã hoàn toàn trở thành một phép toán biểu tượng “hình thức”.
Theo quan điểm của các nhà toán học theo chủ nghĩa hình thức như Hilbert, tất cả các định lý toán học đã được khám phá và chưa được khám phá đều có thể được viết dưới dạng một chuỗi ký hiệu dài hoặc ngắn như thế này.
Mặc dù định lý về tính bất toàn của Gödel sau đó đã chứng minh rằng bức tranh tổng thể của Hilbert là không thể đạt được đối với toàn bộ hệ thống toán học. Nhưng nếu chỉ giới hạn trong nhánh toán học như hình học Euclide thì hệ tiên đề hình thức Hilbert đã hoàn toàn được thiết lập. Điều này là do hệ tiên đề hình học Euclid không chứa đựng lý thuyết số cơ bản, đây là điều kiện để hình thành định lý bất toàn của Gödel, do đó hệ tiên đề hình học Euclid đã hoàn chỉnh.
Hình học Euclide được hình thức hóa bởi Hilbert được gọi là hình học Hilbert.
Vào những năm 1970, Wu Wenjun đã sử dụng phương pháp đại số và ký hiệu này để kết hợp hình học Euclide với khoa học máy tính, đi tiên phong trong hướng chứng minh định lý hình học máy và thúc đẩy sự phát triển của các chứng minh toán học tự động được cơ giới hóa. Bộ chứng minh tự động được cơ giới hóa này, được cộng đồng toán học gọi là "phương pháp Wu", thay thế lý luận toán học trừu tượng bằng các phép tính và suy luận hình thức và ký hiệu phức tạp, từ đó sử dụng máy tính để hỗ trợ các nhà toán học khám phá các cấu trúc tự nhiên và thu được các chân lý toán học.
Việc chứng minh định lý hình học tự động dựa trên phương pháp của Wu trước tiên cần đại số hóa bài toán hình học, chuyển các điều kiện hình học và kết luận hình học đưa ra trong mệnh đề thành các phương trình đa thức, sau đó sử dụng các thuật toán máy tính cụ thể để tính các đa thức này và cuối cùng xác định xem mệnh đề hình học có là đúng. .
Bởi vì hình học Euclide là hoàn chỉnh nên tất cả các mệnh đề trong hình học Euclide đều có thể được chứng minh hoặc chứng minh sai trong một số bước giới hạn bằng cách sử dụng ngôn ngữ hình thức tượng trưng. Vì vậy, về mặt lý thuyết, phương pháp Wu do Wu Wenjun phát minh có thể chứng minh hoàn toàn tất cả các định lý của hình học Euclide.
Cái gọi là "về mặt lý thuyết" ở đây cũng giống như nói về mặt lý thuyết, chỉ có một số cách hạn chế để chơi cờ vây theo luật, vì vậy bạn có thể tìm ra chiến lược chiến thắng bằng cách làm hết tất cả các bước. Trong hoạt động thực tế, phương pháp của Wu chỉ có thể giải được một số bài toán hình học nhất định do hạn chế về khả năng tính toán và thời gian.
Mặc dù vậy, trước sự bùng nổ của trí tuệ nhân tạo trong những năm gần đây, phương pháp của Wu và các phiên bản cải tiến liên quan của nó vẫn là phương pháp hiệu quả nhất để máy móc chứng minh các mệnh đề hình học Euclide. "Hệ thống tiên tiến nhất trước đây" được đề cập ở đầu bài viết này và được dùng để so sánh với AlphaGeometry, hệ thống "giải được 10 bài toán hình học", là phương pháp của Wu.
AlphaGeometry làm gì
Sự cải tiến vượt bậc của AlphaGeometry so với "hệ thống tiên tiến nhất trước đây" thể hiện sự tích lũy công nghệ trước đây của DeepMind, bao gồm AlphaGo, kết hợp với mô hình ngôn ngữ quy mô lớn hiện tại, thuộc nhánh toán học cụ thể của hình học Euclide.AlphaGeometry là một hệ thống ký hiệu thần kinh, chủ yếu bao gồm mô hình ngôn ngữ thần kinh (mô hình ngôn ngữ lớn) và công cụ suy luận ký hiệu.
Trong hai phần này, các mô hình ngôn ngữ lớn rất giỏi trong việc xác định các mẫu và mối quan hệ chung trong dữ liệu, do đó chúng có thể nhanh chóng dự đoán các cấu trúc có thể hữu ích. Nhưng thông thường, các mô hình ngôn ngữ lớn thiếu khả năng suy luận hoặc giải thích chặt chẽ. Đây cũng là lý do khiến các mô hình ngôn ngữ quy mô lớn trước đây, trong đó có ChatGPT và GPT-4, có hiệu suất không đạt yêu cầu về mặt khả năng toán học.
Trong AlphaGeometry, điểm yếu này của các mô hình ngôn ngữ lớn được giải quyết bằng một phần khác, đó là công cụ suy luận tượng trưng. Công cụ suy luận tượng trưng dựa trên logic hình thức và sử dụng các quy tắc rõ ràng để đưa ra kết luận. Hai phần này phối hợp với nhau, tương tự như các khái niệm của Hệ thống 1 và Hệ thống 2 được đề cập trong cuốn sách “Tư duy, nhanh và chậm” của Kahneman. Hệ thống 1 cung cấp những ý tưởng nhanh chóng, “trực quan”, trong khi Hệ thống 2 cung cấp “những quyết định chu đáo hơn, hợp lý hơn” ý tưởng.
Để đào tạo các mô hình ngôn ngữ lớn, DeepMind đã xây dựng một mô hình chứa 151 triệu tham số cho AlphaGeometry. Việc đào tạo trước được tiến hành về "mệnh đề, kết luận và chứng minh" và 500 triệu chứng minh hình học đã được tổng hợp, trong đó có 9 triệu câu hỏi có các dòng phụ trợ.
Thông qua khóa đào tạo này, DeepMind đã dạy thành công mô hình ngôn ngữ lớn của AlphaGeometry những kỹ năng quan trọng nhất trong chứng minh hình học: cộng và sử dụng các đường phụ.
AlphaGeometry có thể liệt kê đầy đủ các mệnh đề có thể thu được từ mỗi hình hình học. Và lần lượt có thể truy ngược lại tập hợp các hình hình học có trong mỗi mệnh đề. Trong quá trình giải quyết vấn đề, AlphaGeometry sẽ tìm kiếm các mệnh đề có thể thu được từ các hình hình học trong các điều kiện của bài toán, cũng như tập hợp các hình hình học chứa các mệnh đề kết luận cần được chứng minh bằng bài toán. Tìm vị trí của đường phụ bằng cách so sánh sự khác biệt giữa các đối tượng bộ sưu tập trong hai bộ sưu tập.
Đây có phải là tương lai của toán học?
Mặc dù rất ngạc nhiên trước hiệu suất vượt trội của AlphaGeometry nhưng chúng tôi không thể không muốn biết, liệu mô hình AlphaGeometry này có phải là tương lai của sự phát triển toán học không? Nói cách khác, liệu trí tuệ nhân tạo có thể tiến hành nghiên cứu toán học một cách độc lập và tạo ra những kết quả có giá trị trong thời gian dự kiến được không?Mặc dù AlphaGeometry là hiện thân của giai đoạn hiện tại của các mô hình ngôn ngữ lớn, "dữ liệu đủ tốt có nghĩa là trí thông minh đủ tốt", tính năng thẩm mỹ bạo lực này sử dụng một số lượng lớn tham số và bộ mẫu lớn để giải quyết vấn đề. Tuy nhiên, bản thân AlphaGeometry phụ thuộc rất nhiều vào các đặc điểm của hình học Euclide. Như đã đề cập ở trên, hình học Euclide là một nhánh rất đặc biệt của toán học. Liệu cách tiếp cận này của AlphaGeometry có thể được mở rộng sang các nhánh toán học khác hay không vẫn chưa được biết.
Hơn nữa, như Yang Likun và những người khác đã đề cập nhiều lần, tỷ lệ sử dụng dữ liệu của các mô hình ngôn ngữ lớn ở giai đoạn này khá thấp. Đơn giản chỉ để giải các bài toán hình học, các tham số và tập huấn luyện của AlphaGeometry đã đạt đến cấp độ này. Do đó, ngay cả khi cách tiếp cận của AlphaGeometry có thể được mở rộng sang các bài toán tổng quát theo một cách nào đó, đối mặt với nhiều loại bài toán khác nhau, thì số lượng tham số và tập huấn luyện mà một hệ thống trí tuệ nhân tạo như vậy yêu cầu vẫn còn rất hạn chế ở cấp độ thực tế hiện nay. không thể đạt được.
Tuy nhiên, khả năng suy luận logic ngày càng tăng của trí tuệ nhân tạo cũng như khả năng khám phá và xác minh kiến thức mới do AlphaGeometry thể hiện vẫn đủ ấn tượng.
Như một trong những tác giả của AlphaGeometry đã nói trên mạng xã hội: "Vẫn còn những ngày đầu để chính thức hóa tổ hợp và việc xây dựng các công cụ biểu tượng mạnh mẽ cho các lĩnh vực khác nhau đòi hỏi phải có kiến
thức chuyên môn sâu về miền. Chúng tôi xem xét việc áp dụng khuôn khổ này cho phạm vi rộng hơn trong tương lai." làm việc và mong muốn có những đổi mới hơn nữa để giải quyết những thách thức này."
Đánh giá từ nội dung trong bài viết, ý tưởng về AlphaGeometry rất đơn giản, nhưng những khó khăn về mặt kỹ thuật trong các chi tiết khác nhau và phương pháp giải quyết những khó khăn này là rất phi thường. Điều này phản ánh đầy đủ khả năng và sự kiên trì bền bỉ của tác giả. Vì vậy, rõ ràng là còn quá sớm để đưa ra kết luận về AlphaGeometry, nhưng tất cả những gì đã thể hiện trong việc hoàn thành tác phẩm của AlphaGeometry cho chúng ta lý do để mong chờ vào tác phẩm trong tương lai của tác giả.
