AI giải mã sổ tay Gödel, phát hiện hàng trăm định lý

Một dự án kéo dài nhiều năm nhằm giải mã 16 cuốn sổ tay của nhà logic học Kurt Gödel vừa có bước ngoặt bất ngờ nhờ trí tuệ nhân tạo. Chỉ trong vài ngày, mô hình Claude đã đưa ra bản tổng hợp toàn bộ 1.009 trang ghi chép viết bằng thứ tốc ký đã lỗi thời, cho thấy Gödel đã chứng minh hàng trăm định lý mà không ai hay biết.

Chân dung nhà logic học Kurt Gödel

Ký hiệu tốc ký cổ và bế tắc kéo dài nhiều năm

Kurt Gödel là một trong những nhà tư tưởng độc đáo nhất thế kỷ 20. Hai định lý bất toàn của ông, công bố năm 1931, đã thay đổi nền toán học và mở đường cho kỷ nguyên số.

Sau những kết quả nền tảng của thập niên 1930, Gödel chỉ công bố một vài bài báo. Tuy nhiên, khối tác phẩm chưa xuất bản của ông lên tới hàng chục nghìn trang và là mối quan tâm lớn của giới sử học khoa học.

Từ năm 2017, nhà logic học người Phần Lan Jan von Plato dẫn dắt một dự án tại Đại học Helsinki nhằm tìm hiểu nội dung 16 cuốn sổ tay Gödel viết vào đầu thập niên 1940. Tư liệu này – được gọi là các "workbook" – gồm 1.009 trang viết dày đặc về toán học và logic. Phần lớn được ghi bằng tốc ký tiếng Đức Gabelsberger, một hệ thống đã lỗi thời ngay cả khi Gödel còn sử dụng.

Tiến độ hiểu nội dung toán học diễn ra cực kỳ chậm – khoảng một trang mỗi tuần – cho đến tháng 9, khi von Plato nhờ đến sự trợ giúp của mô hình AI Claude. Chỉ trong vài ngày, Claude đã cung cấp một bản tóm tắt toàn diện cho toàn bộ tư liệu, hé lộ rằng Gödel đã chứng minh hàng trăm định lý mà không ai từng biết.

"Tôi sững sờ," von Plato nói. "Các cuốn sổ tay không chỉ chứa hàng chục dự báo về những kết quả mãi đến thập niên 70 và 80 mới được biết, mà còn có 14 chủ đề logic chưa từng được theo đuổi. Gödel đã đi trước thời đại rất xa."

Từ định lý bất toàn đến dấu vết của một chứng minh thất lạc

Gödel đã thay đổi cục diện logic học khi chỉ ra những giới hạn của tri thức toán học. Các định lý bất toàn của ông chứng minh rằng trong mọi hệ toán học đều tồn tại những mệnh đề đúng nhưng không thể chứng minh cũng không thể bác bỏ. Kết quả này giáng một đòn vào thế hệ nhà logic học trước đó, những người từng hy vọng mọi chân lý đều có thể kiểm chứng, nhưng đồng thời đẩy lĩnh vực này sang hướng mới, truyền cảm hứng để Alan Turing viết bài báo năm 1936 mở đầu lý thuyết tính toán hiện đại.

Năm 1940, Gödel trốn khỏi Áo dưới thời Đức Quốc xã. Ông định cư tại Princeton, New Jersey, và trở thành bạn thân của Albert Einstein tại Viện Nghiên cứu Cao cấp. Về sau, ông ngày càng hoang tưởng, từ chối ăn thức ăn không do vợ nấu và qua đời vì đói năm 1978.

Einstein trao giải thưởng cho Gödel tại Đại học Princeton

Von Plato cho biết ông khởi động dự án Gödel năm 2017 vì sắp đến tuổi nghỉ hưu bắt buộc tại Đại học Helsinki. "Tôi nên làm gì để khiến mình trở nên không thể thiếu? À đúng rồi, tôi sẽ bắt đầu đọc những trang tốc ký bí ẩn của Gödel!" Ông nhận khoản tài trợ 2,5 triệu euro (khoảng 2,1 triệu bảng Anh) từ Hội đồng Nghiên cứu Châu Âu, tự học tốc ký Gabelsberger – "tôi là một trong chỉ sáu người trên thế giới đọc được nó" – và lập nên một nhóm nhỏ.

Tháng 8, tại một hội nghị ở Pháp về AI và chứng minh định lý, von Plato gặp các nhà khoa học máy tính, những người gợi ý ông tranh thủ sự trợ giúp của Claude để hiểu các cuốn sổ tay. Trở về Helsinki, ông bắt đầu quá trình này, đưa cho Claude các bản ghi chép của mình cùng sáu cuốn sách ông từng viết về Gödel và các tài liệu khoa học thứ cấp khác.

"Trong vài ngày, tôi nhận được một bản giải thích dài 650 trang về các cuốn sổ tay. Nó phải được kiểm tra từng trang, nhưng về cơ bản đây là công việc con người không thể làm nổi," ông nói. "Con người đọc từng trang một và chúng ta có xu hướng quên. Mất một năm để đọc khoảng 50 trang. Chúng ta không thể ghi nhớ tất cả các phần khác nhau. AI có thể kết nối mọi mảnh ghép trong một nghìn trang. Nó có thể nhìn toàn bộ tác phẩm của Gödel như một chỉnh thể."

Một trang sổ tay với ký hiệu tốc ký của Gödel trên vi phim

Bài kiểm tra đầu tiên: tiên đề chọn

Các định lý bất toàn của Gödel cho thấy tồn tại những mệnh đề có chân lý độc lập với hệ thống mà chúng được viết ra: nghĩa là chúng không thể chứng minh hay bác bỏ trong nội bộ hệ thống. Năm 1966, nhà toán học người Mỹ Paul Cohen giành Huy chương Fields – vinh dự cao nhất trong toán học – nhờ chứng minh tính độc lập của hai mệnh đề toán học nổi tiếng: giả thuyết continuum và tiên đề chọn.

Gödel phản ứng trước Huy chương Fields của Cohen bằng cách nói rằng ông đã chứng minh kết quả này từ thập niên 1940. Nhưng khi đồng nghiệp yêu cầu đưa ra chứng minh, Gödel không thể tái dựng lại từ ghi chú của mình.

Nhiệm vụ đầu tiên von Plato giao cho Claude là tìm xem các cuốn sổ tay có chứa chứng minh về tính độc lập của tiên đề chọn hay không – điều sẽ chứng tỏ Gödel đã nói thật năm 1966. Câu trả lời là: gần như có. "Ông ấy chỉ còn cách một bước," von Plato nói. "Có một định nghĩa Gödel làm sai, nhưng ông đã có định nghĩa đúng hai năm trước đó, nên suy luận là ông sẽ đến được định nghĩa đúng nếu tiếp tục thêm vài tháng. Với tôi, kiến trúc chứng minh của ông thật tuyệt vời. Nó khiến toàn bộ các kết quả lý thuyết tập hợp tuân theo một khuôn mẫu thống nhất."

"Điều khiến tôi ấn tượng đặc biệt là ông bắt đầu từ các ý tưởng. Ông không giống người chơi đùa với công thức và hy vọng đến được đâu đó. Ông có những ý tưởng rất, rất rõ ràng, rồi làm việc có phương pháp. Từng bước một, ông tiến lên và hoàn thành các mục tiêu trong công trình hình thức này."

Von Plato cho biết khi Claude trình bày chứng minh tái dựng về tính độc lập của tiên đề chọn, ông đưa nó qua Coq – một trình hỗ trợ chứng minh (proof assistant) kiểm tra tính hợp lệ của các chứng minh toán học – và nó đã vượt qua. Von Plato tin rằng nếu Gödel công bố công trình về tiên đề chọn, ông hẳn đã giành Huy chương Fields năm 1940. "Có lẽ ông cảm thấy khi Cohen nhận huy chương, đó là điều gì đó ông đã bỏ lỡ."

663 định lý và giới hạn của điều AI có thể làm

Trong các cuộc trao đổi tiếp theo với Claude, von Plato yêu cầu mô hình AI trích xuất mọi định lý trong các cuốn sổ tay mà Gödel có chứng minh, phác thảo chứng minh hoặc có ý tưởng chứng minh. Claude tìm được 663 định lý. Khi đưa các kết quả này vào Coq: khoảng 400 được xác nhận đúng như đã nêu, khoảng 200 được sửa chữa – nghĩa là có thể phải làm phát biểu định lý chính xác hơn hoặc thêm một giả thiết – và khoảng 50 là sai. Điều này không có gì lạ, vì chính Gödel khi đọc lại ghi chú đôi khi thêm ghi chú bên lề: falsch! (sai!) hoặc schlecht! (tệ!).

Von Plato nói thêm: "Tôi chắc chắn rằng việc tiếp tục nghiên cứu các bản thảo của Gödel sẽ hé lộ thêm nhiều kho báu. Theo Claude, các cuốn sổ tay chứa hơn một chục chủ đề logic và nền tảng toán học chưa từng được tìm thấy trong hơn 80 năm kể từ khi chúng được ghi lại. Đó là một hướng để khám phá. Nhưng còn nhiều hướng khác. Các cuốn sổ tay vật lý và vũ trụ học của ông là vùng đất chưa biết mà tôi dự định bắt đầu khám phá khi xong các dự án logic hiện tại."

Joel David Hamkins, giáo sư logic tại Đại học Notre Dame, Indiana, chưa xem bản tái dựng của Claude về chứng minh tính độc lập của tiên đề chọn, nhưng cho rằng nếu nó đứng vững thì "đó là điều đáng chú ý và thú vị về mặt lịch sử. Tuy nhiên, bao nhiêu phần là Claude và bao nhiêu phần là Gödel lại là việc của các nhà sử học."

Hamkins nói: "Việc trong đó có những thứ giống [chứng minh của Cohen] không có nghĩa ông đã có nó. Nó cho thấy ông đang đi đúng đường. Bạn không được ghi công cho công trình mà bạn không nói với ai. Nhưng Gödel có quá nhiều ý tưởng đột phá đến mức có lẽ không ngạc nhiên khi sổ tay của ông đầy những điều thú vị."

Góc nhìn

Câu chuyện này cho thấy một hướng ứng dụng AI rất khác với việc sinh mã hay viết nội dung: xử lý khối tư liệu khổng lồ mà con người không thể giữ trong đầu cùng lúc. Với các nhóm nghiên cứu và doanh nghiệp Việt Nam đang có kho tài liệu cũ, bản thảo, log hệ thống hay hồ sơ kỹ thuật chưa số hóa hoàn chỉnh, mô hình ngôn ngữ lớn có thể đóng vai trò "người đọc toàn bộ" để kết nối các mảnh thông tin rải rác.

Tuy nhiên, ví dụ của von Plato cũng chỉ ra giới hạn: AI đưa ra gợi ý, còn con người phải kiểm chứng từng trang và dùng công cụ hình thức như Coq để xác nhận. Khoảng 50 định lý sai trong 663 kết quả là lời nhắc rằng đầu ra của AI cần được đối chiếu nghiêm ngặt trước khi dùng cho bất kỳ quyết định kỹ thuật hay học thuật nào.