Các nhà toán học hàng đầu thế giới đã dành kỳ nghỉ lễ Quốc tế Lao động này như thế nào?
Người đoạt huy chương Fields Terence Tao dường như đang bận rộn phát hành dự án mã nguồn mở của riêng mình: "Tôi đã viết một công cụ phần mềm chứng minh khái niệm với sự trợ giúp của một mô hình lớn để xác minh xem ước tính nhất định bao gồm các tham số dương tùy ý có hợp lệ hay không (trong phạm vi các yếu tố hằng số)."
Địa chỉ dự án: https://github.com/teorth/estimates
Trong dự án này, Tao đã phát triển một khuôn khổ để tự động (hoặc bán tự động) biện minh cho các ước tính trong phân tích. Ước tính là một bất đẳng thức có dạng X≲Y (là X=O(Y) theo ký hiệu tiệm cận) hoặc X≪Y (là X=o(Y) theo ký hiệu tiệm cận).
Tại sao lại tạo ra một công cụ như vậy? Điều này phải bắt đầu bằng cuộc thảo luận gần đây giữa Terence Tao và Bjoern Bringmann (cựu nghiên cứu sinh tiến sĩ của Tao, hiện là trợ lý giáo sư tại Đại học Princeton).
Các gói toán học biểu tượng đã được phát triển rất tốt cho nhiều nhiệm vụ toán học trong các lĩnh vực như đại số, phép tính và phân tích số. Nhưng hiện tại vẫn chưa có công cụ tinh vi tương tự nào để xác minh ước tính tiệm cận - bất đẳng thức có thể áp dụng cho các tham số lớn tùy ý trong khi vẫn giữ nguyên mức tổn thất. Đặc biệt quan trọng là ước tính hàm, trong đó các tham số liên quan đến một hàm hoặc chuỗi chưa biết (tồn tại trong một không gian hàm phù hợp, chẳng hạn như một không gian).
Tao đã viết một bài đăng trên blog về cuộc thảo luận của họ, tập trung vào trường hợp đơn giản hơn về ước lượng tiệm cận liên quan đến một số hữu hạn các số thực dương kết hợp bằng cách sử dụng các phép toán số học như cộng, nhân, chia, lũy thừa, cực tiểu và cực đại (nhưng không phải trừ).
“Tôi mong muốn có một công cụ có thể tự động xác định liệu những ước tính đó có đúng hay không (cung cấp bằng chứng nếu đúng và cung cấp phản ví dụ tiệm cận nếu không đúng).”
Bây giờ, mong ước này đã thành hiện thực.
Chúng ta đều biết rằng Terence Tao rất thích sử dụng các mô hình lớn để giải quyết các bài toán. Hầu hết thời gian trong quá khứ, tôi chỉ hoàn thành nhiệm vụ mã hóa tương đối đơn giản, chẳng hạn như tính toán rồi vẽ biểu đồ một số hàm toán học hơi phức tạp hoặc thực hiện một số phân tích dữ liệu cơ bản trên một số tập dữ liệu .
Lần, ông quyết định tự giao cho mình một nhiệm vụ khó khăn hơn: viết một trình xác thực có thể xử lý các bất đẳng thức có dạng trên.
Ví dụ, một bất đẳng thức điển hình có thể là bất đẳng thức trung bình số học-trung bình nhân yếu.
Trong đó abc là bất kỳ số thực dương nào,
chỉ ra rằng chúng ta sẵn sàng mất đi một hằng số (nhân) không xác định trong ước tính.
Về nguyên tắc, các bất đẳng thức đơn giản có dạng này có thể được giải tự động bằng cách phân chia trường hợp theo phương pháp vũ phu. Một bất đẳng thức đơn lẻ thuộc loại này không khó để giải bằng tay, nhưng một số ứng dụng đòi hỏi phải kiểm tra lượng lớn các bất đẳng thức như vậy hoặc chia chúng thành lượng lớn trường hợp. Nhiệm vụ này có vẻ hoàn hảo để tự động hóa, đặc biệt là với sự trợ giúp của công nghệ hiện đại.
Công cụ AI được Terence Tao sử dụng lần vẫn là ChatGPT. Sau khoảng bốn giờ lập trình, với sự hỗ trợ thường xuyên từ mô hình lớn, anh đã có một công cụ chứng minh khái niệm.
Đồng thời, Tao cũng tung ra quy trình trò chuyện với ChatGPT. Không khó để nhận ra rằng quá trình trò chuyện khá dài.
Liên kết: https://chatgpt.com/share/68143a97-9424-800e-b43a-ea9690485bd8
Lúc đầu, Terence Tao đưa ra yêu cầu riêng của mình cho ChatGPT: "Tôi muốn viết một số lớp Python để vận hành các biểu thức tượng trưng. Và tôi hy vọng có một lớp để biểu diễn các biến, chẳng hạn như x, y, z... Bạn có thể giúp tôi viết một số lớp cơ bản với hàm này để bắt đầu không?"
ChatGPT suy nghĩ trong 6 giây và đưa ra câu trả lời.
Sau khi hoàn tất bước này, vòng trò chuyện tiếp theo sẽ bắt đầu. Đào Triết Tuyền hỏi tiếp: "Tôi thấy anh dùng add để thực hiện phép toán +. Tuyệt lắm. Vậy phương pháp tương ứng để thực hiện * và / là gì?"
ChatGPT cũng đưa ra câu trả lời:
Trong suốt quá trình, Tao liên tục đặt câu hỏi và ChatGPT đã trả lời tất cả, dù đó là những câu hỏi đơn giản hay phức tạp:
「Làm thế nào để nhập một tệp python vào cùng mục lục với tệp python hiện tại?」
Cuối cùng, với sự hỗ trợ đắc lực của ChatGPT, Tao đã hoàn thiện công cụ phần mềm chứng minh khái niệm này.
Trên thực tế, trong số nhiều nhà toán học có tiếng, Terence Tao là một trong những người đầu tiên chấp nhận và khám phá ra giá trị toán học của các mô hình AI lớn như ChatGPT. Ông từng dự đoán rằng "nếu được sử dụng đúng cách, đến năm 2026, AI sẽ trở thành đồng tác giả đáng tin cậy trong nghiên cứu toán học và nhiều lĩnh vực khác".
Terence Tao đã sử dụng các mô hình lớn để nghiên cứu nhiều lần. Ông đã từng giải thành công một bài toán chứng minh với sự trợ giúp của GPT-4 (GPT4 đề xuất 8 phương pháp, trong đó 1 phương pháp giải thành công bài toán) và cũng phát hiện ra một lỗi ẩn trong bài báo của mình với sự trợ giúp của AI.
Ông Tao cũng gợi ý rằng nếu mọi người muốn phát triển loại phần mềm này thì tốt nhất là các nhà toán học và lập trình viên chuyên nghiệp nên hợp tác với nhau để có thể bổ sung thế mạnh cho nhau.
“Tất nhiên đây là một bằng chứng cực kỳ thiếu tinh tế, nhưng sự tinh tế không phải là vấn đề; vấn đề là nó diễn ra tự động.”
Nhìn lại toàn bộ quá trình, chúng ta có thể lấy cảm hứng từ trải nghiệm của Terence Tao. Việc phát triển và sử dụng các mô hình lớn có thể chỉ là phần nổi của tảng băng chìm, và còn nhiều chức năng khác đang chờ mọi người khám phá.
Liên kết tham khảo:
https://terrytao.wordpress.com/2025/05/01/a-proof-of-concept-tool-to-verify-estimates/
Bài viết này trích từ tài khoản công khai WeChat "Machine Heart" , do Danjiang và Chenchen biên tập và được 36Kr xuất bản với sự cho phép.
