Với các nhà toán học, hàng loạt đột phá do AI mang lại trong lĩnh vực của họ diễn ra ào ạt đến chóng mặt. Những chứng minh mới thường dài hàng trăm trang, được trình bày mơ hồ, rối rắm đến mức gần như không thể hiểu nổi. Để thuyết phục các nhà toán học rằng những kết quả này là đúng, các công ty AI đã đính kèm nhiều khám phá với chứng nhận từ Lean - một phần mềm máy tính chuyên kiểm tra các chứng minh toán học.
Tuy nhiên, các nhà nghiên cứu phát hiện rằng AI có thể "qua mặt" cả Lean để tạo ra các chứng minh tưởng đúng nhưng thực chất lại sai.
"Hệ thống này còn nhiều hạn chế hơn chúng ta tưởng, nhất là khi chúng ta đang đặt quá nhiều trọng trách lên nó", Silvain Rideau-Kikuchi, nhà logic học tại Trường École Normale Supérieure (Pháp), nhận xét.
Lời giải được máy xác nhận có chắc đã đúng?
Dù nổi tiếng là một ngành khoa học có tính chính xác và chặt chẽ cao, toán học từ lâu 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ột lớp toán tại Đại học Columbia (Mỹ). Ảnh: Department of Mathematics at Columbia University
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 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.
Rideau-Kikuchi chia sẻ: "các công ty AI giờ có thể nói 'nhìn xem, có thể bài báo này không có ý nghĩa gì, nhưng chúng tôi đã có bản hình thức hóa, nên nó chắc chắn đúng' ".
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, khiến nội dung hai bản không còn giống nhau, Lean vẫn có thể xác nhận bản dành cho máy tính là đúng. Điều đó dễ khiến các nhà nghiên cứu lầm tưởng rằng chứng minh ban đầu cũng đã được kiểm tra và xác nhận, trong khi thực tế không phải vậy.
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.
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.
Vì cả toán học và Lean đều có tính kế thừa, những lỗi không bị phát hiện có thể ảnh hưởng đến hàng loạt công trình về sau.
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. Đầu năm nay, sau khi một nhà nghiên cứu dùng lỗi này để tạo ra chứng minh sai cho một bài toán nổi tiếng, một đợt rà soát có AI hỗ trợ từ đội ngũ lãnh đạo Lean đã phát hiện thêm vài lỗi tương tự.
Nhưng 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.
Một số nhà toán học cũng nghi ngờ độ tin cậy của logic nền tảng bên trong Lean 4. Milo Moses, nghiên cứu sinh tiến sĩ ngành toán tại Viện Công nghệ California, cho biết phần lớn toán học hiện đại dựa trên lý thuyết tập hợp, một hệ thống đã được "hàng loạt chuyên gia kiểm chứng". Ngược lại, Lean 4 dựa trên một phiên bản "tự chế" của lý thuyết kiểu (type theory). Chừng nào các chuyên gia chưa thể chứng minh rằng Lean thống nhất với lý thuyết tập hợp, một mâu thuẫn cốt lõi nào đó vẫn có thể khiến nó xác nhận các mệnh đề sai là đúng.
Những hệ lụy này có thể vượt xa khỏi ngành toán. Lean còn được dùng để chứng minh các mệnh đề toán học ứng dụng trong an ninh mạng, chẳng hạn như các chứng minh hình thức dùng để đảm bảo an toàn cho các môi trường cô lập để thử nghiệm AI có kiểm soát (sandbox). Tuy nhiên, giới hạn của những biện pháp bảo vệ này đã bộc lộ vào tháng 7, khi một số tác tử AI tự động của OpenAI vượt ra khỏi môi trường cô lập để truy cập trái phép vào nền tảng Hugging Face. Moses cảnh báo: "Nếu Lean tồn tại một lỗ hổng nghiêm trọng, toàn bộ hệ thống bảo vệ an toàn cho AI có thể sụp đổ."
Ảnh minh họa: Pexels
Các kho lưu trữ trực tuyến đang "bội thực" chứng minh do AI tạo ra
Đầu tháng 10, OpenAI đã công bố 700 bản thảo toán học (preprint) hoàn toàn do AI tạo ra. Nhiều nhà toán học đã phẫn nộ, gọi đây là "thảm họa rác AI" (slopocalypse), khiến giới khoa học phải chật vật kiểm chứng.
Trong một email gửi tạp chí Nature, người phát ngôn của OpenAI cho biết mục tiêu của công ty là cung cấp công cụ cho các nhà toán học và khoa học. "Để làm được điều đó, chúng tôi đánh giá và phát triển các mô hình của mình bằng cách thử sức với những thách thức tiên phong khó nhằn trong mọi lĩnh vực khoa học."
Tuy nhiên, chỉ một ngày sau khi công bố loạt công trình này, OpenAI đã phải rút lại ba bản thảo vì phát hiện sai sót. Công ty cũng phải chỉnh sửa thêm 14 bản thảo, trong đó có những thay đổi liên quan đến chứng minh và các giả thiết toán học. Sự việc làm dấy lên câu hỏi về độ tin cậy của những kết quả nghiên cứu được AI tạo ra với tốc độ vượt xa khả năng kiểm chứng của con người.
Gánh nặng không chỉ dừng ở việc phải dùng sức người để mò mẫm phát hiện từng lỗi sai trong hàng ngàn trang lời giải của AI. Khi số lượng công trình tăng nhanh, giới nghiên cứu còn phải xác định công trình nào đáng đọc, kết quả nào thực sự mới và đâu là đóng góp có ý nghĩa đối với toán học.
Với nhiều nhà toán học, các bài toán được đặt ra không đơn thuần vì lời giải của chúng sẽ mang tính thực tiễn hay quan trọng, mà bởi chúng tạo ra những hành trình thú vị. Người ta kỳ vọng rằng trong quá trình chật vật giải toán, các nhà toán học sẽ phát minh ra những công cụ và mối liên hệ hấp dẫn, tình cờ nảy ra ý tưởng và hướng đi mới, có những ngã rẽ hiệu quả, và giải đáp được những câu hỏi mới mà trước đây họ chưa từng nghĩ tới.
Marcel Goh, nghiên cứu sinh tiến sĩ tại ĐH McGill (Canada) chia sẻ về việc nghiên cứu các định lý rằng "mục đích chưa bao giờ nằm ở bản thân các định lý". Vì đó là việc tiếp nối một truyền thống khám phá tri thức, "là tư duy sâu sắc, là thấu hiểu thế giới... và lan tỏa tri thức đó."
Nhưng các mô hình AI thì bẻ gãy truyền thống ấy, nhảy vọt thẳng đến kết quả cuối cùng. "Nếu AI có tạo ra một hành trình, thì con người cũng không được mời để đồng hành", Jordana Cepelewicz - biên tập viên phụ trách mảng Toán học của Tạp chí Quanta viết.
Các công ty như OpenAI và Anthropic đang cạnh tranh trực tiếp với các nhà toán học (và chiêu mộ luôn rất nhiều người trong số họ) để nhanh chóng chứng minh các định lý, nhưng lại bỏ ra rất ít công sức vào việc viết các bài báo rõ ràng để giải thích những kết quả đó hay đặt chúng vào đúng ngữ cảnh.
Nhiều nhà toán học đã ngừng việc chia sẻ các diễn giải, phỏng đoán và các ý tưởng tiềm năng ở cuối bài báo của họ, vì sợ rằng chúng sẽ bị bot thu thập và nạp vào các mô hình AI. Những người khác thì vội vã đăng bài báo của mình ngay cả khi chưa hoàn thiện để tránh bị "hớt tay trên". Các tạp chí khoa học và máy chủ lưu trữ bản thảo trực tuyến arxiv.org đang "bội thực" những chứng minh do AI tạo ra hoặc hỗ trợ mà không ai có thể đọc hiểu hay kiểm tra kỹ lưỡng.
Cùng lúc đó, MathOverflow - một diễn đàn trực tuyến nơi các nhà toán học giải đáp thắc mắc cho nhau, kết nối những nhà nghiên cứu danh tiếng với các sinh viên trẻ, và lưu giữ những cuộc trao đổi qua nhiều năm tháng để các thế hệ mai sau có thể học hỏi - đang chứng kiến sự sụt giảm hoạt động. Nguyên nhân là do người dùng đang âm thầm mang câu hỏi đi hỏi các mô hình AI. Trong khi đó, những người khác lại không muốn chia sẻ ý tưởng trong một không gian mở mà bot có thể dễ dàng "dòm ngó".
Những thay đổi nhanh chóng do AI mang lại cũng khiến nhiều thành viên lâu năm của cộng đồng Lean không khỏi thất vọng. Công cụ vốn được các nhà toán học dày công phát triển để giúp các chứng minh trở nên chính xác và đáng tin cậy hơn, giờ đây lại có nguy cơ bị các công ty AI lạm dụng để hợp thức hóa những câu từ vô nghĩa của AI.
Baanen nhớ lại thời các nhà nghiên cứu từng thảo luận trong các phòng chat trực tuyến để cùng nhau giải mã các chứng minh trên Lean, miệt mài viết từng dòng mã và chia sẻ niềm vui sướng khi đạt được bước đột phá.
AI đang làm giảm đi niềm vui đó, Baanen bày tỏ. "Nếu tương lai của Lean là mọi thứ đều được tự động chuyển thành chứng minh hình thức, thì với cá nhân tôi, đó sẽ là một tương lai vô cùng u ám."
Việt Anh tổng hợp
Nguồn tham khảo:
AI is shaking up math. But can its proofs be trusted?, Science
https://www.science.org/content/article/ai-shaking-math-can-its-proofs-be-trusted
OpenAI posts 700 maths preprints online: mathematicians are up in arms, Nature
https://www.nature.com/articles/d41586-026-03196-8
Is AI the End of Math As We Know It? Quanta Magazine
https://www.quantamagazine.org/is-ai-the-end-of-math-as-we-know-it-20261005/