Terrence Tao: AI trở thành ‘bạn đồng hành’ của các nhà toán học
Nhà toán học Terrence Tao giải thích vì sao các chương trình kiểm tra chứng minh và trí tuệ nhân tạo (AI) đang thay đổi toán học một cách mạnh mẽ.
Toán học có truyền thống là một ngành khoa học đơn độc. Năm 1986, Andrew Wiles đã chìm đắm suốt bảy năm một mình trong phòng làm việc để chứng minh Định lý (lớn) Fermat. Các kết quả chứng minh của ông vẫn khiến một số đồng nghiệp thấy khó hiểu và một số hiện vẫn đang gây tranh cãi. Nhưng trong những năm gần đây, ngày càng nhiều chưa từng thấy những địa hạt của toán học bị chia nhỏ thành những thành phần cấu tạo riêng lẻ (“hình thức hóa”), nhờ đó các máy tính có thể kiểm tra và xác nhận các phép chứng minh.
Trong cuộc trả lời phỏng vấn mới đây trên tờ Spektrum der Wissenschaft ở Đức, một phiên bản “chị em” của tờ Scientific American, nhà toán học Terrence Tao ở Đại học California, Los Angeles, cho rằng sự kết hợp cùng những tiến bộ mới nhất trong ngành Trí tuệ nhân tạo, toán học sẽ thiết lập được những cách làm việc hoàn toàn mới trong những năm tới. Với sự giúp đỡ của máy tính, những vấn đề mở, lớn, sẽ được giải quyết.
Trong một bài nói chuyện của anh ở Joint Mathematics Meetings tại San Francisco, dường như anh đã ngụ ý rằng các nhà toán học không tin tưởng nhau. Ý anh là gì?
Tôi cho là, chúng tôi có tin tưởng nhau, nhưng phải quen biết nhau cơ. Thật khó để hợp tác với người mà anh chưa từng gặp trừ phi anh có thể kiểm tra từng dòng nghiên cứu của họ. Thường thì số lượng [cộng tác viên] lớn nhất là 5.
Chuyện thay đổi ra sao trước sự xuất hiện của phần mềm kiểm tra chứng minh tự động?
Giờ đây anh có thể thực sự cộng tác với hàng trăm người mà anh chưa từng gặp trước đây. Và anh không cần phải tin tưởng họ, vì họ sẽ tải mã lên và trình biên dịch Lean sẽ kiểm tra nó. Anh có thể nghiên cứu toán học ở quy mô lớn hơn rất nhiều so với bình thường. Khi hình thức hóa những kết quả mới nhất của chúng tôi về cái gọi là giả thuyết đa thức Freiman-Ruzsa (PFR), tôi đã làm việc với hơn 20 người. Chúng tôi đã chia phép chứng minh thành rất nhiều các bước nhỏ và mỗi người đóng góp một phép chứng minh cho mỗi bước nhỏ ấy. Và tôi không cần kiểm tra từng dòng để biết rằng mỗi đóng góp đều đúng. Gần giống như tôi chỉ cần quản lý toàn bộ quá trình và đảm bảo rằng mọi thứ diễn ra theo đúng hướng. Đó là một cách làm toán khác, hiện đại hơn.
Cho đến nay, ý tưởng chứng minh vẫn phải xuất phát từ nhà toán học, phải không?
Đúng vậy, cách nhanh nhất để hình thức hóa là trước tiên, tìm một phép chứng minh của con người. Con người đưa ra các ý tưởng, bản nháp đầu tiên cho phép chứng minh. Sau đó anh chuyển nó thành một chứng minh hình thức. Trong tương lai, có thể chuyện sẽ tiến triển khác đi. Có thể có những dự án hợp tác mà ta không biết làm thế nào để chứng minh toàn bộ vấn đề. Nhưng người ta có những ý tưởng về cách chứng minh những phần nhỏ, và họ hình thức hóa chúng rồi cố gắng ghép chúng lại với nhau. Trong tương lai, tôi có thể hình dung một định lý lớn được chứng minh nhờ sự kết hợp của 20 người và một nhóm AI, mỗi cá thể lại chứng minh những phần nhỏ. Và theo thời gian, chúng được kết nối lại với nhau, và anh có thể tạo ra một thứ hay ho nào đó. Chuyện đó thật tuyệt. Sẽ mất thêm nhiều năm nữa trước khi điều đó thành hiện thực. Công nghệ hiện tại vẫn chưa đạt đến mức đó, một phần vì việc hình thức hóa hiện vẫn rất khó khăn.
Tôi đã nói chuyện với những người cố gắng sử dụng các mô hình ngôn ngữ lớn hoặc các công nghệ máy học tương tự để tạo ra những chứng minh mới. Tony Wu và Christian Szegedy, những người gần đây đồng sáng lập Công ty xAI cùng với Elon Musk và cộng sự, đã nói với tôi rằng trong vòng hai đến ba năm, toán học sẽ được “giải quyết” theo cách tương tự như cờ vua đã được giải quyết – rằng các cỗ máy sẽ giỏi hơn bất cứ con người nào trong việc tìm ra lời giải.
Tôi nghĩ rằng trong ba năm tới, AI sẽ trở nên hữu ích cho các nhà toán học. Nó sẽ là một bạn đồng hành tuyệt vời. Anh đang cố gắng chứng minh một định lý, và có một bước mà anh nghĩ là đúng, nhưng anh không hoàn toàn hiểu vì sao lại thế. Và anh có thể bảo, “AI, mày có thể làm việc này cho tao không?” Rồi nó có thể đáp, “Tôi nghĩ tôi có thể chứng minh đấy.” Tôi không nghĩ rằng máy sẽ giải quyết được hết toán học. Có thể sẽ xảy ra một đột phá lớn trong công nghệ AI. Nếu là tôi, tôi sẽ nói rằng trong ba năm tới, người ta sẽ thấy những tiến bộ đáng kể, và thực sự việc sử dụng AI sẽ ngày càng dễ quản lý hơn.
Ngay cả khi AI có thể làm thứ toán học mà con người bây giờ đang làm, thì điều đó có nghĩa là chúng ta sẽ chuyển sang một kiểu toán học cao cấp hơn. Nên hiện tại, chẳng hạn, ta chứng minh từng kết quả một. Giống như các nghệ nhân thủ công làm một con búp bê gỗ chẳng hạn. Anh ta cầm một con búp bê gỗ lên và rất cẩn thận sơn mọi thứ, xong anh ta cầm một con khác lên và tiếp tục. Cách chúng ta làm toán chưa thay đổi quá nhiều. Nhưng ở trong tất cả những lĩnh vực khác, chúng ta đã có sản xuất hàng loạt. Và với AI, ta có thể bắt đầu chứng minh hàng trăm hoặc hàng nghìn định lý cùng một lúc. Các nhà toán học con người sẽ chỉ đạo AI làm các việc khác nhau. Vì vậy, tôi nghĩ rằng cách ta làm toán sẽ thay đổi, nhưng nói là trong hai đến ba năm nữa thì cũng hơi quá đà.
Tôi đã phỏng vấn Peter Scholze khi cậu ấy giành Huy chương Fields vào năm 2018. Tôi đã hỏi cậu ấy, có bao nhiêu người hiểu những gì cậu đang làm? Và cậu ấy nói rằng có khoảng 10 người.
Với những dự án hình thức hóa, cái chúng tôi nhận thấy là bạn có thể hợp tác với những người không hiểu toàn bộ mà chỉ hiểu một phần nhỏ toán học của toàn bộ dự án. Giống như với một thiết bị hiện đại. Không một người đơn lẻ nào có thể tự làm ra một chiếc máy tính, từ việc khai thác quặng kim loại và tinh luyện chúng cho đến tạo ra các phần cứng và phần mềm. Chúng ta có tất cả các chuyên gia cho từng lĩnh vực, có những chuỗi cung ứng hậu cần lớn, rồi cuối cùng ta mới có thể tạo ra một chiếc điện thoại thông minh hay bất cứ thứ gì. Hiện tại, trong một mối hợp tác toán học, mọi người phải biết hầu hết trọn vẹn vấn đề, và đó là một trở ngại, như Scholze đã đề cập. Nhưng với các dự án hình thức hóa này, người ta có thể phân chia công việc và đóng góp vào một dự án mà chỉ cần biết một phần của nó. Tôi cũng nghĩ rằng chúng ta nên bắt đầu hình thức hóa các sách giáo khoa. Nếu một cuốn sách giáo khoa được hình thức hóa, anh có thể tạo ra những cuốn sách giáo khoa tương tác, nơi anh có thể mô tả một kết quả chứng minh rất tổng quát, hàm chứa rất nhiều kiến thức. Nhưng nếu có bước nào đó không hiểu, anh có thể đi sâu vào đó rất chi tiết – tới tận các tiên đề nếu muốn. Không ai làm điều đó cho sách giáo khoa bây giờ vì nó đòi hỏi quá nhiều công sức. Nhưng nếu đã hình thức hóa xong thì máy tính có thể tạo ra những cuốn sách giáo khoa tương tác này cho anh. Nó sẽ giúp một nhà toán học trong một lĩnh vực có thể bắt đầu đóng góp vào một lĩnh vực khác vì anh có thể xác định chính xác các công việc nhỏ của một nhiệm vụ lớn mà không cần phải hiểu mọi thứ.
Một chứng minh toán học không chỉ là việc kiểm tra cái gì đó là đúng. Một chứng minh cũng là để hiểu một điều gì đó, đúng không? Có những chứng minh đẹp và có những chứng minh xấu xí rất kỹ thuật. Một chứng minh tốt giúp anh hiểu vấn đề sâu hơn. Vậy, nếu giao việc đó cho máy móc, chúng ta có thể vẫn hiểu được những gì chúng đã tìm ra không?
Những gì các nhà toán học đang làm là khám phá không gian của những gì là đúng và những gì là sai và tại sao những thứ đó lại đúng. Và chúng ta làm việc đó thông qua các chứng minh. Mọi người đều biết rằng khi điều gì đó là đúng thì ta phải cố gắng chứng minh hoặc bác bỏ nó. Và chuyện đó mất rất nhiều thời gian. Nó tẻ nhạt. Nhưng trong tương lai, có thể ta chỉ cần hỏi một AI, “Kết quả này có đúng hay không?” Rồi chúng ta có thể khám phá không gian kia hiệu quả hơn nhiều, và có thể cố gắng tập trung vào những gì chúng ta thực sự quan tâm. AI sẽ giúp ta rất nhiều bằng cách tăng tốc quá trình này. Chúng ta sẽ vẫn là người dẫn dắt, ít nhất là bây giờ. Có thể trong 50 năm nữa mọi thứ sẽ khác. Nhưng trong tương lai gần, AI sẽ tự động hóa những thứ nhàm chán, tầm thường trước tiên.
AI sẽ giúp chúng ta giải quyết những vấn đề lớn, chưa có lời giải trong toán học chứ?
Nếu muốn chứng minh một giả thuyết chưa có lời giải, một trong những điều đầu tiên anh cần làm là chia nó thành các phần nhỏ hơn – có khả năng chứng minh được cao hơn. Nhưng người ta thường chia một vấn đề thành những vấn đề khó hơn. Rất dễ để biến một vấn đề trở nên khó hơn thay vì đơn giản hơn. Và về mặt này thì AI chưa thể hiện được khả năng tốt hơn con người.
Quá trình phân tích và khám phá vấn đề cũng giúp anh học được nhiều điều mới mẻ. Ví dụ, Định lý cuối cùng của Fermat là một giả thuyết đơn giản về các số tự nhiên, nhưng toán học được phát triển để chứng minh nó không nhất thiết phải liên quan đến các số tự nhiên nữa. Vì vậy, giải quyết một bài toán chứng minh thì ý nghĩa hơn nhiều việc chứng minh chỉ một trường hợp.
Giả sử AI đưa ra một chứng minh khó hiểu và phức tạp. Sau đó, anh có thể nghiên cứu và phân tích nó. Chẳng hạn, chứng minh này sử dụng 10 giả thiết để đi đến một kết luận – nếu tôi xóa một giả thiết, chứng minh này còn đúng hay không? Đó là một ngành khoa học hiện vẫn chưa tồn tại vì chúng ta vẫn chưa có quá nhiều chứng minh do AI tạo ra, nhưng tôi nghĩ sẽ có một kiểu nhà toán học mới, những người có thể tiếp nhận toán học do AI tạo ra và giúp chúng trở nên dễ hiểu hơn. Giống như chúng ta có khoa học thực nghiệm và lý thuyết vậy. Có rất nhiều thứ chúng ta khám phá ra nhờ thực nghiệm, sau đó chúng ta làm thêm nhiều thí nghiệm và khám phá ra các định luật của tự nhiên. Hiện tại, chúng ta chưa làm vậy trong toán học. Nhưng tôi nghĩ sẽ có một ngành công nghiệp gồm những người cố gắng trích xuất thông tin ý nghĩa từ các chứng minh do AI tạo ra mà ban đầu không có mấy ý nghĩa.
Vậy thay vì là kết thúc thì đây có phải một tương lai tươi sáng cho toán học?
Tôi nghĩ sẽ có những cách làm toán khác nhau mà hiện tại chưa tồn tại. Tôi có thể thấy những nhà toán học quản lý dự án có thể tổ chức các dự án rất phức tạp – họ không hiểu tất cả toán học, nhưng họ có thể chia nhỏ mọi thứ thành các phần nhỏ hơn và phân công chúng cho người khác, và họ có kỹ năng giao tiếp tốt. Sau đó, có những chuyên gia làm việc trong các lĩnh vực con. Có những người giỏi huấn luyện AI trong các loại toán học cụ thể, và sau đó có những người có thể chuyển đổi các chứng minh của AI thành thứ gì đó mà con người có thể đọc được. Chuyện sẽ trở nên rất giống với cách hoạt động của hầu hết các ngành công nghiệp hiện đại khác. Chẳng hạn như trong báo chí, không phải ai cũng có cùng bộ kỹ năng. Bạn có biên tập viên, bạn có nhà báo, và bạn có doanh nhân, v.v. – cuối cùng chúng ta sẽ có những thứ tương tự trong toán học.
Toán học chúng ta làm là loại toán học phù hợp với bộ não của chúng ta, đúng không? Và nếu đến một lúc nào đó AI thông minh hơn rất nhiều, nó có thể đi vào những vùng mà chúng ta khó có thể hiểu được.
Toán học vốn đã lớn hơn bất cứ bộ óc con người nào. Các nhà toán học thường xuyên dựa vào các kết quả mà những người khác đã chứng minh. Họ biết đại khái tại sao nó đúng, họ có một số trực giác, nhưng họ không thể chia nó ra tất cả các chi tiết đến các tiên đề. Nhưng họ biết nơi để tìm, hoặc có thể họ biết ai đó có thể làm điều đó. Chúng ta đã có rất nhiều định lý chỉ được kiểm chứng bởi máy tính, trong đó một số tính toán lớn trên máy tính đã kiểm tra hàng triệu trường hợp. Anh có thể xác minh nó bằng tay, nhưng không ai có thời gian để làm điều đó, và không đáng để làm như vậy. Vì vậy, tôi nghĩ chúng ta sẽ thích nghi. Một người không nhất thiết phải kiểm tra mọi thứ. Để máy tính làm việc kiểm tra cho chúng ta, với tôi, cũng ổn.
Ở tiền tuyến của toán học, có rất nhiều thứ đang diễn ra kéo mọi thứ lại với nhau từ các lĩnh vực dường như không liên quan, và theo hiểu biết ngây thơ của tôi, một AI biết tất cả các lĩnh vực này có thể cho bạn một gợi ý và nói, “Tại sao bạn không nhìn vào đó? Nơi đó có thể giúp bạn giải quyết vấn đề của mình.”
Tạo ra các kết nối hoặc ít nhất chỉ ra các kết nối có thể có quả là một tiềm năng rất thú vị của AI. Hiện tại, nó có tỷ lệ thành công rất thấp. Nó có thể cho bạn 10 gợi ý mà trong đó có 1 gợi ý thú vị và 9 gợi ý là rác. Thực tế là nó gần như tệ hơn cả ngẫu nhiên. Nhưng điều này có thể thay đổi trong tương lai.
Những vấn đề gì đang cản trở việc huấn luyện một AI toán học?
Một phần của vấn đề là không có đủ dữ liệu để huấn luyện nó. Anh có thể huấn luyện nó bằng các bài báo đã công bố trực tuyến. Nhưng tôi nghĩ rất nhiều trực giác không được nắm bắt trong các bài báo in trên các tạp chí mà nằm trong các cuộc trò chuyện với các nhà toán học, trong các bài giảng và trong cách chúng tôi hướng dẫn sinh viên. Đôi khi tôi đùa rằng điều chúng ta cần làm là để GPT tham gia một khóa học sau đại học tiêu chuẩn, ngồi trong các lớp học, đặt câu hỏi như một sinh viên và học như con người học toán.
Phiên bản đã công bố của một chứng minh luôn được cô đọng. Và ngay cả khi anh lấy tất cả toán học đã được công bố trong lịch sử loài người, thì nó vẫn nhỏ so với những gì các mô hình này được huấn luyện.
Và mọi người chỉ công bố những câu chuyện thành công. Dữ liệu thực sự quý giá là khi một người thử nghiệm một cái gì đó, và nó không hoàn toàn hoạt động, nhưng họ biết cách sửa nó. Nhưng họ chỉ công bố những thứ thành công, không phải là quá trình.
Có thể anh nên đăng ký những nỗ lực chứng minh điều gì đó, giống như trong các nghiên cứu y tế. Các nhà nghiên cứu sẽ đăng ký nó, và sau đó họ sẽ phải công bố nó ngay cả khi nó không thành công.
Chúng tôi không có văn hóa đó. Có thể trong tương lai hình thức hóa sẽ trở nên rất hiệu quả và anh có thể hình thức hóa nhiều thứ theo thời gian thực. Và có thể nếu anh muốn sử dụng một AI Lean giả tưởng nào đó của năm 2040 trong một dự án nghiên cứu và muốn được tài trợ để sử dụng AI giả tưởng này, anh sẽ phải chấp nhận rằng quá trình thử nghiệm và thất bại của anh sẽ được lưu lại. Và sau đó người ta sẽ sử dụng nó để huấn luyện các AI tương lai. Hoặc có thể một nhóm khác đang làm việc với một vấn đề tương tự và họ có thể thấy, “ồ nhóm này đang thử cùng vấn đề này và đã thất bại”, nên anh không phải mất thời gian lặp lại đúng những sai lầm ấy.
Các nhà toán học có đang lãng phí nhiều thời gian không?
Ồ, rất nhiều. Vì lý do nào đó mà rất nhiều kiến thức bị mắc kẹt trong đầu của mỗi nhà toán học. Và chỉ một phần nhỏ được làm rõ. Nhưng càng hình thức hóa, càng có nhiều kiến thức ẩn của chúng ta trở nên hiển hiện. Vì vậy, sẽ có những lợi ích bất ngờ từ điều đó.□
Tia Sáng lược đăng từ bản dịch của Tuệ Tâm
Bản gốc: https://www.scientificamerican.com/article/ai-will-become-mathematicians-co-pilot/
Bài đăng Tia Sáng số 13/2024