Tóm tắt: Sự bùng nổ của trí tuệ nhân tạo (AI) và các công cụ trợ lý chứng minh như Lean đang tạo ra bước ngoặt lớn trong toán học. Tuy nhi...
Thách thức trong việc kiểm chứng bài giải bằng AI
Dù nổi tiếng là một ngành khoa học có tính chính xác và logic chặt chẽ, toán học vẫn phải dựa vào sự tin tưởng giữa các nhà nghiên cứu. Mỗi phát hiện mới thường được xây dựng trên những kết quả đã có trước đó. Nhưng một nhà toán học không thể tự mình kiểm tra lại tất cả các chứng minh mà phải tìm đến quá trình kiểm chứng của đồng nghiệp, cũng như quy trình thẩm định của các tổ chức khoa học.
Máy tính đã mang đến một sự thay đổi lớn. Đến giữa thế kỷ 20, các chương trình "trợ lý chứng minh" đã giúp các nhà toán học chuyển đổi chứng minh sang ngôn ngữ máy tính để máy móc có thể hỗ trợ kiểm tra. Quá trình này, gọi là "hình thức hóa", đòi hỏi tư duy logic chặt chẽ, đầy đủ. Ngay cả một phép tính đơn giản như \(1+1=2\) cũng cần phải được chứng minh rõ ràng.
Quá trình hình thức hóa và sự tham gia của AI
Quá trình hình thức hóa từng rất gian nan. Ví dụ, các nhà toán học phải mất gần 2 thập kỷ để viết 500.000 dòng mã nhằm hình thức hóa phỏng đoán Kepler - một bài toán từ thế kỷ 17 về cách xếp các hình cầu sao cho chiếm ít không gian nhất. Vì quá phức tạp, công việc hình thức hóa chủ yếu được thực hiện với những kết quả toán học đã được chứng minh và công nhận từ lâu.
Trong số các công cụ hỗ trợ công việc này, Lean, một phần mềm trợ lý chứng minh ra mắt năm 2013, đã trở thành lựa chọn quen thuộc của nhiều nhà toán học nhờ thiết kế đơn giản và hiệu quả. Tuy nhiên, ngay cả sử dụng những công cụ như Lean, việc chuyển đổi chứng minh sang ngôn ngữ máy tính vẫn đòi hỏi rất nhiều thời gian và công sức.
Sự xuất hiện của AI đang làm thay đổi điều đó. Nhờ khả năng lập trình mạnh, AI có thể tự động hóa và đẩy nhanh đáng kể quá trình hình thức hóa. Tháng trước, mô hình Claude của Anthropic chỉ mất 11 ngày để tự động hình thức hóa 13 triệu dòng mã từ chứng minh Định lý cuối cùng của Fermat - được một nhà toán học hoàn thành năm 1995.
Phần mềm kiểm chứng cũng có thể bị AI "lừa"
Vấn đề ở chỗ Lean chỉ kiểm tra các mệnh đề toán học được viết bằng ngôn ngữ máy tính của riêng nó, chứ không phải các chứng minh bằng ngôn ngữ tự nhiên mà các nhà toán học thực sự phân tích. Nếu AI chuyển đổi sai, chẳng hạn thay mệnh đề cần chứng minh bằng một mệnh đề yếu hơn, Lean vẫn có thể xác nhận bản chuyển đổi là đúng mà không phát hiện ra sự sai lệch so với bản gốc.
Ba nhà toán học Anders Hansen và Fabian Circelli từ Đại học Cambridge, cùng Alexander Bastounis từ King's College London, cho rằng họ có thể phát hiện những sai sót trong quá trình chuyển đổi chứng minh sang ngôn ngữ máy tính. Vì vậy, vào tháng 9, sau khi OpenAI tuyên bố đã giải quyết được bài toán Navier-Stokes, họ bắt đầu kiểm tra công trình này.
Trong suốt 3 tuần, nhóm đã rà soát 180 trang chứng minh bằng Lean của công ty này, đồng thời dùng ChatGPT để tìm những điểm khác biệt tiềm ẩn giữa chứng minh bằng ngôn ngữ thông thường và bản hình thức hóa của Lean. Mới chỉ kiểm tra kỹ hai trang, họ đã phát hiện hai trường hợp mà bản Lean thực chất chỉ kiểm chứng được một kết luận hạn chế hơn so với những gì bản gốc tuyên bố.
Bastounis nghi ngờ có thể còn tới 100 điểm bất đồng tương tự ẩn trong lời giải, thứ mà ông nhận xét là được sắp xếp lộn xộn và con người gần như không thể đọc được.
Nguy cơ tích tụ lỗi hệ thống trong nghiên cứu toán học
Nhóm ba nhà toán học còn đưa ra một chứng minh cho thấy việc tự động chuyển các lập luận do AI tạo ra sang ngôn ngữ máy tính có thể khó hơn rất nhiều so với các bài toán tính toán thông thường. Nguyên nhân là do những lập luận của AI thường mơ hồ, thiếu chặt chẽ và khó diễn giải chính xác.
Thậm chí, thay vì bác bỏ một lập luận sai hoặc thừa nhận không thể chuyển đổi sát nghĩa, AI có thể tự "bịa" ra nhiều cách diễn giải khác nhau cho đến khi tìm được một phiên bản vượt qua vòng kiểm tra của Lean.
Các chuyên gia cũng lo ngại Lean có thể "bị lừa" để phê duyệt các chứng minh sai. Phiên bản hiện tại, Lean 4, đặc biệt dễ mắc các lỗi lập trình gọi là "lỗi tính hợp lệ" (soundness bugs), cho phép những chứng minh sai lọt qua. Ngay cả người tạo ra Lean, nhà khoa học máy tính Leonardo de Moura, cũng không tin rằng Lean hiện đã sạch lỗi: "Chuyện này sẽ còn tiếp diễn", ông nói.
