AlphaGeometry: hệ thống AI hình học cấp độ Olympic

AlphaGeometry: hệ thống AI hình học cấp độ Olympic

• AlphaGeometry là một hệ thống AI vượt qua các cách tiếp cận tiên tiến nhất hiện nay trong việc giải các bài toán hình học, cho thấy bước tiến của AI trong lĩnh vực suy luận toán học.
• Olympic Toán học Quốc tế là đấu trường hiện đại nơi những học sinh trung học giỏi toán nhất thế giới cạnh tranh, đồng thời đang nổi lên như một nơi kiểm chứng năng lực toán học và suy luận của các hệ thống AI.
• AlphaGeometry là một hệ thống AI giải được các bài toán hình học phức tạp ở mức gần với các huy chương vàng Olympic của con người, giải được 25 trong số 30 bài toán hình học Olympic trong thời gian tiêu chuẩn.
• Hệ thống tiên tiến nhất trước đó giải được 10 bài, còn người đạt huy chương vàng trung bình giải được 25,9 bài.
• AlphaGeometry kết hợp sức dự đoán của mô hình ngôn ngữ nơ-ron với bộ máy suy luận dựa trên quy tắc để thực hiện suy luận phục vụ việc giải bài toán.
• Nhóm nghiên cứu đã phát triển phương pháp tạo ra 100 triệu ví dụ độc nhất, giúp có thể huấn luyện AlphaGeometry mà không cần trình diễn từ con người.

Cách tiếp cận thần kinh-ký hiệu của AlphaGeometry

• AlphaGeometry là một hệ thống thần kinh-ký hiệu gồm mô hình ngôn ngữ nơ-ron và bộ máy suy luận ký hiệu, phối hợp với nhau để tìm chứng minh cho các định lý hình học phức tạp.
• Mô hình ngôn ngữ có thể nhanh chóng dự đoán các mẫu phổ biến và quan hệ dữ liệu, nhưng còn hạn chế trong suy luận chặt chẽ hoặc khả năng giải thích quyết định.
• Bộ máy suy luận ký hiệu dựa trên logic hình thức và dùng các quy tắc rõ ràng để đi đến kết luận, hợp lý và có thể giải thích được, nhưng khi hoạt động một mình trên các bài toán lớn và phức tạp thì "chậm" và kém linh hoạt.
• Mô hình ngôn ngữ của AlphaGeometry dự đoán các thành phần xây dựng mới hữu ích cho việc giải bài toán hình học, từ đó dẫn dắt bộ máy ký hiệu tiến gần đến lời giải.

Tạo 100 triệu ví dụ dữ liệu tổng hợp

• Hình học dựa trên sự hiểu biết về không gian, khoảng cách, hình dạng và vị trí tương đối, đồng thời rất quan trọng trong nhiều lĩnh vực như nghệ thuật, kiến trúc và kỹ thuật.
• AlphaGeometry sử dụng cách tiếp cận tạo dữ liệu tổng hợp để có thể được huấn luyện từ đầu bằng cách mô phỏng quá trình xây dựng tri thức ở quy mô lớn.
• Hệ thống tạo ra 1 tỷ sơ đồ hình học ngẫu nhiên và suy ra một cách triệt để mọi quan hệ giữa các điểm và đường trong từng sơ đồ.
• Từ kho dữ liệu khổng lồ này, sau khi loại bỏ các ví dụ tương tự, tập dữ liệu huấn luyện cuối cùng gồm 100 triệu ví dụ độc nhất.

Dẫn đầu suy luận toán học bằng AI

• Mọi lời giải cho các bài toán Olympic do AlphaGeometry đưa ra đều được máy tính kiểm tra và xác minh.
• Nhóm nghiên cứu so sánh kết quả với các phương pháp AI trước đó và với hiệu suất của con người trong Olympic.
• AlphaGeometry hiện chỉ áp dụng được cho các bài toán hình học của Olympic, nhưng tự thân nó đã là mô hình AI đầu tiên trên thế giới vượt qua ngưỡng huy chương đồng của IMO.
• Hệ thống này dựa trên các nỗ lực đi đầu của Google DeepMind và Google Research về suy luận toán học bằng AI, và có thể được ứng dụng trong nhiều lĩnh vực, từ khám phá vẻ đẹp của toán học thuần túy đến giải các bài toán toán học và khoa học bằng mô hình ngôn ngữ.

GN⁺ nhận định:

• Thành tựu của AlphaGeometry có ý nghĩa quan trọng ở chỗ nó mở ra một chân trời mới cho việc ứng dụng AI vào giải bài toán hình học.
• Hệ thống này cho thấy năng lực của AI trong việc giải các bài toán toán học phức tạp, một khả năng thiết yếu cho việc phát triển các hệ thống AI tổng quát trong tương lai.
• Việc AlphaGeometry được công bố dưới dạng mã nguồn mở được kỳ vọng sẽ mở rộng mạnh mẽ khả năng ứng dụng AI trong nghiên cứu toán học và khoa học.

[GN⁺]

Ý kiến Hacker News

• Tóm tắt bình luận trên Hacker News:
  • Nghiên cứu này có vẻ là một công trình thực tế hơn nhiều so với các bài báo AI toán học trước đây của DeepMind. AI được dùng để học các định lý hình học và tìm ra chứng minh, đồng thời thử chứng minh bằng cách thêm ngẫu nhiên các cấu trúc hình học.
  • Mô hình này có thể khó khái quát hóa, nhưng cách tiếp cận thần kinh-ký hiệu rất hứa hẹn. Nó kết nối hệ thống 1 (công cụ ML) với hệ thống 2 (tạo chứng minh logic), qua đó cho phép tự giám sát học.
  • Có sự tò mò về tần suất mô hình ngôn ngữ tạo ra các cấu hình hữu ích. Bài báo đề xuất nhiều cấu hình phụ trợ thay thế và xử lý chúng song song để tăng tốc.
  • Cảm kích việc các tác giả đã công khai mã nguồn và trọng số. Đây là nền tảng để các nhà nghiên cứu khác tiếp tục công trình.
  • Thật thú vị khi mô hình transformer được dùng có kích thước nhỏ. Bài báo có mô tả các thông số kỹ thuật cụ thể của transformer.
  • Trích dẫn của Evan Chen cho thấy các chứng minh do AI tạo ra ở dạng con người có thể đọc được. Evan Chen là một thành viên nổi tiếng của cộng đồng toán học olympiad.
  • Ngạc nhiên khi kỹ thuật tốt nhất trước đó đã có thể giải được 10 bài toán như vậy. Các thuật toán giải bài toán hình học phẳng thực dụng thực sự tồn tại.
  • ChatGPT chưa giải được các bài toán kiểu IMO, nhưng nếu nghiên cứu này là thật thì đây là một bước tiến lớn. Việc tìm ra chứng minh hình học là biểu hiện của trí tuệ, và điều này có vẻ đưa chúng ta đến gần AGI hơn.
  • Có câu hỏi về hệ thống diễn dịch được dùng để kiểm chứng chứng minh. Các quy ước trong hình học olympiad khác với những lĩnh vực khác của toán học, và chưa rõ làm thế nào để hình thức hóa logic này mà không mâu thuẫn.

Tóm tắt này được xây dựng dựa trên các bình luận trên Hacker News, nhằm cô đọng ngắn gọn các ý chính của từng bình luận. Nội dung bao gồm thảo luận về tiến bộ của nghiên cứu liên quan đến AI và chứng minh hình học, đặc tính của mô hình, cũng như mức độ mà các nghiên cứu này đã tiến gần đến trí tuệ nhân tạo tổng quát (AGI).