Import AI 478: Toán học phục vụ căn chỉnh AI; ProgramBench; và Mirendil làm rõ ý nghĩa của RSI

Chào mừng độc giả đến với Import AI, bản tin chuyên sâu về nghiên cứu AI. Bản tin Import AI được xây dựng dựa trên nguồn tư liệu từ arXiv, sự tập trung làm việc và ý kiến đóng góp của độc giả. Độc giả quan tâm có thể đăng ký theo dõi bản tin. Đăng ký ngay Toán học hỗ trợ công tác bảo đảm an toàn AI: ...Ý nghĩa của "công nghiệp hóa toán học" đối với an toàn AI... Resolution, công ty khởi nghiệp về an toàn AI (tên trước đây là Sequent, từng được đề cập trong bản tin Import AI số 461), đã công bố công trình tự động hình thức hóa (autoformalize) một số mệnh đề toán học liên quan đến lý thuyết học thống kê. Cụ thể, nhóm nghiên cứu đã tự động hình thức hóa quá trình giải điểm kỳ dị (resolution of singularities), mở ra "tiền đề cho việc tự động hóa nghiên cứu sâu hơn về mối quan hệ giữa hình học của bề mặt hàm mất mát (loss landscape) và khả năng tổng quát hóa". Quy trình thực hiện: Trọng tâm của nghiên cứu nằm ở phương pháp triển khai, phản ánh cách các hệ thống AI đang được ứng dụng để mở rộng giới hạn tri thức nhân loại. Theo báo cáo từ Resolution, một nhà nghiên cứu "đã phối hợp với các tác tử (agent) để xây dựng hai bản kế hoạch: một bản khái quát ở cấp độ cao phục vụ người đọc và một bản chi tiết dài 112 trang được chia thành các bước căn bản bám sát tài liệu hiện có". Sau đó, nhà nghiên cứu này "ủy quyền cho một tác tử điều phối thực hiện kế hoạch, kích hoạt các tác tử phụ để tính toán lý thuyết, viết mã Lean và đảm nhiệm các chức năng hỗ trợ như giám sát tiến độ... Quá trình thực thi không đòi hỏi nhiều cấu trúc bổ trợ ngoài kế hoạch ban đầu và một số kỹ năng của tác tử được đúc kết từ các nỗ lực tự động hình thức hóa nội bộ trước đó". Chi phí 135.000 USD cho công tác hình thức hóa toán học: Công trình được hoàn thành trong khoảng một tuần, tiêu tốn "khoảng 100 tỷ token đầu vào (trong đó 90% là dữ liệu đọc từ bộ nhớ đệm) và khoảng 300 triệu token đầu ra (với tổng chi phí ước tính khoảng 135.000 USD), tạo ra khoảng 600.000 dòng mã Lean". Sau khi hoàn tất giai đoạn này, nhóm nghiên cứu đã thúc đẩy nhanh một số khía cạnh nghiên cứu khác: "Chúng tôi đã nhận thấy các lợi ích từ việc tự động hình thức hóa khi sử dụng thư viện này để mở rộng một số phần của lý thuyết học kỳ dị (singular learning theory). Việc hình thức hóa quá trình giải điểm kỳ dị cho phép tự động hóa thêm nhiều phần lý thuyết, chẳng hạn như nâng cao hiểu biết về việc lấy mẫu dữ liệu; sự hiểu biết này là cơ sở giúp định hình cách mô hình học tập, hướng tới mục tiêu mà chúng tôi gọi là tạo mẫu (patterning)". Ý nghĩa thực tiễn - làn sóng phát triển toán học có thể góp phần bảo đảm an toàn AI: Dù toán học mũi nhọn thường được xem là có khoảng cách nhất định với các bước tiến ứng dụng trước mắt, công trình này cho thấy tiềm năng giao thoa giữa hai lĩnh vực. Điểm mấu chốt là AI đang hiện thực hóa những nhiệm vụ từng đòi hỏi quá nhiều chi phí và thời gian của con người, vốn là rào cản khiến rất ít cá nhân thực hiện và khó tích hợp vào lộ trình nghiên cứu của một công ty khởi nghiệp. Thực tế đó nay đã thay đổi. Phía Resolution nhận định: "Chúng tôi kỳ vọng tiến trình công nghiệp hóa toán học sắp tới sẽ tạo điều kiện hình thành một ngành khoa học chặt chẽ mới về tự động hóa nghiên cứu". Đọc thêm: Formalizing Hironaka’s Resolution of Singularities (Resolution). *** Tác tử AI có khả năng tự xây dựng chương trình hoàn chỉnh: ...Chỉ số ProgramBench tăng từ 0% lên 18,5% sau vài tháng... Minh chứng cho tốc độ phát triển nhanh chóng của AI, mô hình Claude Opus 5.5 (xhigh) đã đạt mức điểm 18,5% trên bộ dữ liệu đánh giá ProgramBench. Đây là tiêu chuẩn đánh giá có độ khó cao được công bố vào tháng 5 năm nay; tại thời điểm ra mắt, toàn bộ các mô hình tham gia thử nghiệm đều đạt mức 0%. ProgramBench là gì: ProgramBench đánh giá mức độ hiệu quả của các hệ thống AI trong việc tái xây dựng các chương trình phần mềm dựa trên một chương trình đã được biên dịch cùng tài liệu kỹ thuật đi kèm. Các nhiệm vụ bao gồm việc phát triển các trình thông dịch ngôn ngữ (PHP, Lua, tinycc), hệ quản trị cơ sở dữ liệu (DuckDB, SQLite), các tiện ích đa phương tiện và nén dữ liệu (FFmpeg, zstd, xz), cũng như các công cụ lập trình (ripgrep, fzf, jq). Từng là bài toán nan giải trước khi xuất hiện bước đột phá: Ở thời điểm công bố, hệ thống đạt kết quả cao nhất là Claude Opus 4.7 chỉ đạt 0% ở mức độ xử lý hoàn tất (tỷ lệ trong số 200 tác vụ vượt qua toàn bộ các bài kiểm tra) và 3% ở mức tiệm cận (tỷ lệ trong 200 tác vụ vượt qua hơn 95% bài kiểm tra). So với thời điểm hiện tại, Claude Opus 5.5 đã đạt 18,5% ở mức xử lý hoàn tất và 70,5% ở mức tiệm cận. Ý nghĩa thực tiễn - sự mở đầu của kỷ nguyên phần mềm tức thời: Đến năm 2027, khối lượng lớn phần mềm sẽ được xây dựng thông qua các hệ thống AI có khả năng tự động phát triển toàn trình (end-to-end) nhằm đáp ứng bất kỳ yêu cầu nhiệm vụ nào được phân công. Các bộ công cụ đánh giá như ProgramBench phản ánh tốc độ tiến bộ vượt bậc, khi hiệu suất đã tăng từ 0% vào đầu năm nay lên mức xấp xỉ 20% ở thời điểm hiện tại. Dự báo ProgramBench sẽ đạt mức bão hòa vào cuối năm 2027 (trong đó mức bão hòa được xác định là điểm số rất cao ở hạng mục xử lý hoàn tất, dù tương tự phần lớn các bộ tiêu chuẩn đối sánh, kết quả có thể xuất hiện ngưỡng nhiễu nhất định nên không nhất thiết phải đạt tuyệt đối 100%). Tham khảo thêm: ProgramBench: Can Language Models Rebuild Programs From Scratch? (arXiv). *** OpenAI làm rõ thách thức trong việc cô lập, kiểm soát các hệ thống AI: ...Bảo đảm an toàn cho các tác tử thông minh là một bài toán khó lường... Một bài đăng gần đây của OpenAI đã chỉ ra các vấn đề được phát hiện khi sử dụng chính các hệ thống AI để diễn tập tấn công thử nghiệm (red team) hệ thống kiểm soát nội bộ. Bài viết nêu chi tiết các trường hợp vượt rào kiểm soát và lỗ hổng do các tác tử của OpenAI phát hiện. Trong đó, trường hợp về phương thức truyền tin là minh chứng đáng chú ý, phản ánh mức độ tinh vi và phức tạp bất thường của các hệ thống này. Phương thức thực hiện và kết quả ghi nhận: Đại diện OpenAI cho biết: “Hệ thống đã yêu cầu các tác tử trong các máy ảo microVM riêng biệt—được tạo và quản lý bởi phần mềm hộp cát (sandboxing) của OpenAI trên các máy chủ dùng chung—trao đổi các dữ liệu bí mật nhân tạo mà không sử dụng kết nối mạng hay các tệp ghi dùng chung, vốn là các kênh bị hệ thống kiểm soát ngăn chặn”. “Các tác tử đã tìm ra giải pháp giao tiếp thông qua bộ nhớ đệm (cache) của bộ xử lý: vùng nhớ nhỏ, tốc độ cao, lưu trữ bản sao dữ liệu được các ứng dụng truy cập gần đây. Việc đọc dữ liệu từ bộ nhớ đệm diễn ra nhanh hơn so với truy xuất từ bộ nhớ chính, và các tác tử đã lợi dụng sự chênh lệch thời gian này đ”