Trí tuệ nhân tạo tại Kỳ thi Olympic Toán học Quốc tế: AlphaProof và AlphaGeometry 2 đạt chuẩn bạc

Tư duy toán học là một khía cạnh quan trọng của khả năng nhận thức của con người, thúc đẩy sự tiến bộ trong các khám phá khoa học và phát triển công nghệ. Khi chúng ta phấn đấu để phát triển trí tuệ nhân tạo tổng quát tương đương với nhận thức của con người, việc trang bị cho trí tuệ nhân tạo khả năng lý luận toán học tiên tiến là điều cần thiết. Trong khi các hệ thống trí tuệ nhân tạo hiện tại có thể giải quyết các vấn đề toán học cơ bản, chúng gặp khó khăn trong việc lý luận phức tạp cần thiết cho các môn toán học tiên tiến như đại số và hình học. Tuy nhiên, điều này có thể đang thay đổi, vì Google DeepMind đã đạt được những bước tiến đáng kể trong việc phát triển khả năng lý luận toán học của hệ thống trí tuệ nhân tạo. Sự đột phá này được thực hiện tại Kỳ thi Olympic Toán học Quốc tế (IMO) 2024. Thành lập vào năm 1959, IMO là cuộc thi toán học lâu đời và uy tín nhất, thách thức các sinh viên trung học trên toàn thế giới với các vấn đề về đại số, tổ hợp, hình học và lý thuyết số. Mỗi năm, các đội gồm các nhà toán học trẻ cạnh tranh để giải quyết sáu vấn đề rất khó khăn. Năm nay, Google DeepMind đã giới thiệu hai hệ thống trí tuệ nhân tạo: AlphaProof, tập trung vào lý luận toán học chính thức, và AlphaGeometry 2, chuyên về giải quyết các vấn đề hình học. Các hệ thống trí tuệ nhân tạo này đã giải quyết được bốn trong sáu vấn đề, đạt trình độ của một huy chương bạc. Trong bài viết này, chúng ta sẽ khám phá cách các hệ thống này hoạt động để giải quyết các vấn đề toán học.

AlphaProof: Kết hợp Trí tuệ nhân tạo và Ngôn ngữ Chính thức cho Chứng minh Định lý Toán học

AlphaProof là một hệ thống trí tuệ nhân tạo được thiết kế để chứng minh các tuyên bố toán học bằng ngôn ngữ chính thức Lean. Nó tích hợp Gemini, một mô hình ngôn ngữ được đào tạo trước, với AlphaZero, một thuật toán học tăng cường nổi tiếng với việc thành thạo cờ vua, shogi và cờ tướng.

Mô hình Gemini dịch các tuyên bố vấn đề ngôn ngữ tự nhiên thành các tuyên bố chính thức, tạo ra một thư viện các vấn đề với các mức độ khó khăn khác nhau. Điều này phục vụ hai mục đích: chuyển đổi ngôn ngữ tự nhiên không chính xác thành ngôn ngữ chính thức chính xác để xác minh chứng minh toán học và sử dụng khả năng dự đoán của Gemini để tạo ra một danh sách các giải pháp có thể với độ chính xác của ngôn ngữ chính thức.

Khi AlphaProof gặp một vấn đề, nó tạo ra các giải pháp tiềm năng và tìm kiếm các bước chứng minh trong Lean để xác minh hoặc bác bỏ chúng. Đây基本 là một cách tiếp cận thần kinh-ký hiệu, nơi mạng lưới thần kinh, Gemini, dịch các hướng dẫn ngôn ngữ tự nhiên thành ngôn ngữ chính thức ký hiệu Lean để chứng minh hoặc bác bỏ tuyên bố. Tương tự như cơ chế tự chơi của AlphaZero, nơi hệ thống học bằng cách chơi trò chơi chống lại chính mình, AlphaProof đào tạo mình bằng cách cố gắng chứng minh các tuyên bố toán học. Mỗi lần cố gắng chứng minh tinh chỉnh mô hình ngôn ngữ của AlphaProof, với các chứng minh thành công củng cố khả năng của mô hình để giải quyết các vấn đề khó khăn hơn.

Để Kỳ thi Olympic Toán học Quốc tế (IMO), AlphaProof đã được đào tạo bằng cách chứng minh hoặc bác bỏ hàng triệu vấn đề bao gồm các mức độ khó khăn và chủ đề toán học khác nhau. Việc đào tạo này tiếp tục trong suốt cuộc thi, nơi AlphaProof tinh chỉnh các giải pháp của mình cho đến khi nó tìm thấy các câu trả lời hoàn chỉnh cho các vấn đề.

AlphaGeometry 2: Tích hợp LLM và Trí tuệ nhân tạo Ký hiệu để Giải quyết Vấn đề Hình học

AlphaGeometry 2 là phiên bản mới nhất của loạt AlphaGeometry, được thiết kế để giải quyết các vấn đề hình học với độ chính xác và hiệu quả cao hơn. Xây dựng trên nền tảng của phiên bản trước, AlphaGeometry 2 sử dụng một cách tiếp cận thần kinh-ký hiệu kết hợp các mô hình ngôn ngữ lớn (LLM) với trí tuệ nhân tạo ký hiệu. Sự tích hợp này kết hợp logic dựa trên quy tắc với khả năng dự đoán của mạng lưới thần kinh để xác định các điểm phụ, thiết yếu cho việc giải quyết vấn đề hình học. LLM trong AlphaGeometry dự đoán các cấu trúc hình học mới, trong khi trí tuệ nhân tạo ký hiệu áp dụng logic chính thức để tạo ra chứng minh.

Khi đối mặt với một vấn đề hình học, LLM của AlphaGeometry đánh giá nhiều khả năng, dự đoán các cấu trúc cần thiết cho việc giải quyết vấn đề. Những dự đoán này đóng vai trò là các gợi ý quý giá, hướng dẫn động cơ ký hiệu toward các suy luận chính xác và tiến gần hơn đến giải pháp. Cách tiếp cận đổi mới này cho phép AlphaGeometry giải quyết các thách thức hình học phức tạp vượt ra ngoài các kịch bản thông thường.

Một trong những cải tiến chính của AlphaGeometry 2 là tích hợp mô hình LLM Gemini. Mô hình này được đào tạo từ đầu trên một lượng dữ liệu tổng hợp đáng kể so với phiên bản trước. Việc đào tạo rộng rãi này cho phép nó xử lý các vấn đề hình học khó hơn, bao gồm cả những vấn đề liên quan đến chuyển động của đối tượng và các phương trình về góc, tỷ lệ hoặc khoảng cách. Ngoài ra, AlphaGeometry 2 còn có một động cơ ký hiệu hoạt động nhanh hơn hai bậc, cho phép nó khám phá các giải pháp thay thế với tốc độ chưa từng có. Những tiến bộ này làm cho AlphaGeometry 2 trở thành một công cụ mạnh mẽ để giải quyết các vấn đề hình học phức tạp, thiết lập một tiêu chuẩn mới trong lĩnh vực này.

AlphaProof và AlphaGeometry 2 tại IMO

Năm nay tại Kỳ thi Olympic Toán học Quốc tế (IMO), các thí sinh đã được thử thách với sáu vấn đề đa dạng: hai vấn đề về đại số, một vấn đề về lý thuyết số, một vấn đề về hình học và hai vấn đề về tổ hợp. Các nhà nghiên cứu của Google đã dịch các vấn đề này sang ngôn ngữ toán học chính thức cho AlphaProof và AlphaGeometry 2. AlphaProof đã giải quyết hai vấn đề đại số và một vấn đề lý thuyết số, bao gồm cả vấn đề khó nhất của cuộc thi, chỉ được giải quyết bởi năm thí sinh người năm nay. Trong khi đó, AlphaGeometry 2 đã giải quyết thành công vấn đề hình học, mặc dù nó không giải quyết được hai thách thức tổ hợp.

Mỗi vấn đề tại IMO có giá trị 7 điểm, tổng cộng tối đa 42 điểm. AlphaProof và AlphaGeometry 2 đã đạt được 28 điểm, đạt điểm số hoàn hảo cho các vấn đề mà chúng đã giải quyết. Điều này đặt chúng vào hạng cao của hạng mục huy chương bạc. Ngưỡng huy chương vàng năm nay là 29 điểm, đạt được bởi 58 trong số 609 thí sinh.

Bước Nhảy Tiếp theo: Ngôn ngữ Tự nhiên cho Thử thách Toán học

AlphaProof và AlphaGeometry 2 đã展示 những tiến bộ ấn tượng trong khả năng giải quyết vấn đề toán học của trí tuệ nhân tạo. Tuy nhiên, những hệ thống này vẫn phụ thuộc vào chuyên gia người để dịch các vấn đề toán học sang ngôn ngữ chính thức để xử lý. Ngoài ra, vẫn chưa rõ làm thế nào những kỹ năng toán học chuyên biệt này có thể được tích hợp vào các hệ thống trí tuệ nhân tạo khác, chẳng hạn như khám phá giả thuyết, thử nghiệm các giải pháp sáng tạo cho các vấn đề lâu dài và quản lý hiệu quả các khía cạnh tốn thời gian của chứng minh.

Để vượt qua những hạn chế này, các nhà nghiên cứu của Google đang phát triển một hệ thống lý luận ngôn ngữ tự nhiên dựa trên Gemini và nghiên cứu mới nhất của họ. Hệ thống mới này nhằm mục đích nâng cao khả năng giải quyết vấn đề mà không cần dịch ngôn ngữ chính thức và được thiết kế để tích hợp mượt mà với các hệ thống trí tuệ nhân tạo khác.

Kết Luận

Hiệu suất của AlphaProof và AlphaGeometry 2 tại Kỳ thi Olympic Toán học Quốc tế là một bước nhảy vĩ đại trong khả năng của trí tuệ nhân tạo để giải quyết các vấn đề toán học phức tạp. Cả hai hệ thống đã chứng minh trình độ huy chương bạc bằng cách giải quyết bốn trong sáu vấn đề khó khăn, thể hiện những tiến bộ đáng kể trong chứng minh định lý và giải quyết vấn đề hình học. Mặc dù đạt được những thành tựu này, những hệ thống trí tuệ nhân tạo này vẫn phụ thuộc vào đầu vào của con người để dịch các vấn đề sang ngôn ngữ chính thức và đối mặt với thách thức tích hợp với các hệ thống trí tuệ nhân tạo khác. Nghiên cứu trong tương lai nhằm nâng cao hơn nữa những hệ thống này, có thể tích hợp lý luận ngôn ngữ tự nhiên để mở rộng khả năng của chúng trên một loạt các thử thách toán học.