[Giới thiệu] Chỉ một tia lửa cũng có thể gây ra cả một đám cháy thảo nguyên! Giá trị của bằng chứng nằm ở khả năng kiểm chứng; lần này, GPT-5 đưa bằng chứng toán học vào mã nguồn.
ChatGPT khôi phục danh tiếng của OpenAI bằng cách chứng minh điều đó!
Sau khi bị Hassabis chỉ trích là quá đáng xấu hổ, GPT-5 thực sự đã truyền cảm hứng cho những kết luận toán học mới.
Nhà khoa học Sebastien Bubeck của OpenAI đã trở thành tâm điểm chú ý khi GPT-5 giải quyết được mười bài toán Erdős.
Tuy nhiên, người ta chỉ ra rằng GPT không giải quyết được vấn đề của Erdős mà tìm thấy tài liệu đã giải quyết được những vấn đề này.
Sau đó, anh đã xóa dòng tweet đó và tuyên bố rằng anh không có ý định gây hiểu lầm cho bất kỳ ai.
Yann LeCun lên án OpenAI là "gieo gió gặt bão": OpenAI đã bị chính GPTard của mình gây hại.
Sau đó, các bài đăng của anh trên LinkedIn trở nên ít nổi bật hơn hẳn:
Bây giờ, mọi thứ đã có bước chuyển biến tốt đẹp hơn—
Sebastien Bubeck đã bị "buộc tội oan"; AI thực sự đang thúc đẩy tiến bộ khoa học.
Một diễn biến bất ngờ: ChatGPT "minh oan" cho OpenAI.
Ngày hôm qua, câu chuyện đã có một bước ngoặt—
Boris Alexeev (ảnh bên trái), tiến sĩ toán học của Đại học Princeton, và Dustin G. Mixon (ảnh bên phải), phó giáo sư tại Đại học bang Ohio, đã phát hiện ra rằng Bài toán số 707 của Erdő, với phần thưởng trị giá 1.000 đô la, đã được giải quyết 30 năm trước khi được đề xuất.
Liên kết bài báo: https://borisalexeev.com/pdf/erdos707.pdf
Vấn đề này có phần vô lý, gần giống với "cuộc tìm kiếm trống rỗng" của nhà toán học—
Câu trả lời đã có từ 30 năm trước, nhưng cho đến gần đây, người ta vẫn tin rằng vấn đề này vẫn chưa được giải quyết!
Hiện tại, bài toán số 707 của Erdő đã được đánh dấu là "Bị bác bỏ".
Liên kết: https://www.erdosproblems.com/go_to/707
Lần, Sebastien Bubeck đã đảo ngược tình thế khi đăng dòng tweet:
Có vẻ như việc tìm kiếm tài liệu văn học không phải là một nhiệm vụ đơn giản 😅.
Ý nghĩa ẩn dụ ở đây là việc tìm ra 10 giải pháp hiện có trong quá khứ bằng GPT-5 không phải là việc dễ dàng.
Nhưng những gì diễn ra sau đó thậm chí còn thú vị hơn.
Các bằng chứng toán học được hỗ trợ bởi ChatGPT - Terence Tao đánh giá cao
Hai nhà toán học cũng hoài nghi về kết quả, nên họ quyết định sử dụng GPT5 để tạo ra một bằng chứng chính thức trong Lean. Cuối cùng, họ đã thành công!
Lưu ý⚠️: ChatGPT và Lean được liệt kê là những bên cộng tác, nhưng nội dung của bài báo vẫn do chính các tác giả viết.
Tuy nhiên, con người đã nỗ lực rất nhiều trong quá trình này, liên tục cung cấp phản hồi cho GPT5 hoàn thiện các đối số chính thức của nó.
Trên trang web "Vấn đề Erdős", nhiều trường hợp thành công gần đây đã xuất hiện, trong đó các nhà nghiên cứu đã sử dụng các mô hình ngôn ngữ lớn để tìm ra giải pháp cho vấn đề Erdős trong các tài liệu hiện có.
Điều đáng nói là Terence Tao trước đây đã chứng minh thành công bằng chứng khái niệm bằng cách sử dụng AI để tìm ra "câu trả lời hiện có" cho vấn đề của Erdős.
Terence Tao cũng lưu ý đến bằng chứng mới lần, cho rằng đây là một ví dụ thú vị về bằng chứng có sự hỗ trợ của máy tính.
Trong quá trình nghiên cứu, hai nhà toán học tin rằng Lean có thể giúp xác minh tính xác thực của các bài báo hiện có, nhưng vào thời điểm đó, họ không quen thuộc với Lean cũng như không thấy giao diện người dùng của nó thân thiện.
Tuy nhiên, vì ChatGPT có khả năng viết mã Lean nên họ quyết định chính thức hóa toàn bộ bằng chứng thông qua mã hóa vibe.
Quá trình này mất khoảng một tuần và trải nghiệm mệt mỏi, nhưng cuối cùng thì nó đã thành công ngoài mong đợi.
Trong các hệ thống chính thức, ChatGPT đã chứng minh một cách nghiêm ngặt sự phủ định của giả thuyết Erdős .
Bản chứng minh cuối cùng bao gồm hơn 6.000 dòng mã, bao gồm 26 định nghĩa, 169 bổ đề và 4 định lý (phần xác minh phản ví dụ cuối cùng). Trên một máy tính xách tay thông thường, việc xác minh mã mất chưa đến nửa phút.
Sau nhiều vòng tương tác, Boris và Dustin cho rằng rằng nhiều vấn đề sẽ được giải quyết đáng kể nếu giao diện của mô hình ngôn ngữ lớn có thể được tích hợp độ sâu với Lean và được tinh chỉnh phù hợp cho phương pháp tương tác này.
Ngay cả những tối ưu hóa nhỏ, có mục tiêu cũng đủ để khiến trải nghiệm"bằng chứng hợp tác giữa con người và máy móc" này trở nên mượt mà và tự nhiên hơn.
Terence Tao đánh giá cao bằng chứng được hỗ trợ bởi AI lần. Ông cho rằng đây là một trong những trường hợp hiếm hoi sử dụng kết quả LLM một cách có trách nhiệm trong một bài nghiên cứu:
Điều quan trọng là không có đầu ra nào do LLM tạo ra được đưa trực tiếp vào văn bản (ngoại trừ việc tham chiếu các đoạn mã Lean do LLM tạo ra cho mục đích minh họa).
Thay vào đó, đầu ra này chỉ được sử dụng trong bối cảnh có thể xác minh đầy đủ (trong trường hợp này, để tạo mã có thể được Lean kiểm tra kiểu).
Tuy nhiên, Terence Tao nhấn mạnh: "Chính thức hóa tinh gọn chỉ là sự bổ sung cho bằng chứng của con người và không thể thay thế nó."
Hơn nữa, ông gần như có thể đoán trước được một số báo cáo phóng đại—"Lần này, LLM thực sự đã giải quyết được vấn đề của Erdős!"
Nhưng sự thật phức tạp và tinh tế hơn nhiều. Để rút ra bất kỳ kết luận nào, chúng ta cần xem xét kỹ lưỡng toàn bộ câu chuyện.
GPT-5 đang thúc đẩy nghiên cứu và những dấu hiệu ban đầu đang xuất hiện.
Paata Ivanisvili, giáo sư toán học tại Đại học California, Irvine, cũng liệt kê ChatGPT là đồng tác giả của bài báo.
Bài báo mới được đồng tác giả bởi giáo sư toán học Paata Ivanisvili và Xinyuan Xie, cựu sinh viên năm 2022 của Đại học Khoa học và Công nghệ Trung Quốc (USTC). ChatGPT là tác giả đầu tiên.
Cuộc khám phá này bắt đầu khi hai người yêu cầu GPT-5 Pro tìm kiếm các phản ví dụ trong các bài toán chưa được giải quyết công khai (xem bên dưới 👇).
- Liên kết: https://simons.berkeley.edu/sites/default/files/openprobsmerged.pdf
- Tiêu đề: Phân tích thực tế trong khoa học máy tính: Tuyển tập các bài toán mở
Sau một số thí nghiệm số, nó đề xuất một phản ví dụ cho bài toán chưng cất tương quan không tương tác (NICD) với phép xóa:
Hàm Boolean được xác định trên 5 bit có giá trị E|f(z)| lớn hơn giá trị tương ứng của hàm đa số 5 bit khi tham số xóa p = 0,40.
Họ đã ghi lại quá trình khám phá và xác minh toàn bộ quá trình tính toán.
Kết quả này phản ánh phản ví dụ kinh điển "Đa số là ít ổn định nhất" trong các hàm ngưỡng tuyến tính: ngay cả khi AI chỉ áp dụng các mẫu phản ví dụ đã biết vào các tình huống mới và xác minh chúng, thì đóng góp của nó vẫn đáng được ghi nhận.
Liên kết: https://arxiv.org/abs/1703.07657
Đây chính là "tia lửa" của AI trong khoa học máy tính lý thuyết: trước đây, các mô hình ngôn ngữ lớn (LLM) chủ yếu được sử dụng để tìm kiếm tài liệu hoặc hỗ trợ số, nhưng lần, một phản ví dụ cụ thể, có giới hạn và có thể xác minh được đã được tạo ra .
Ngoài ra, giáo sư toán học Ernest Ryu của UCLA đã giải quyết một vấn đề mở trong lĩnh vực tối ưu hóa lồi bằng cách sử dụng GPT-5 Pro.
Mặc dù khoảng 80% nỗ lực chứng minh mô hình này là sai, nhưng nó đã đề xuất một số ý tưởng mới.
Những đóng góp cụ thể của GPT-5 Pro:
- Phương pháp chứng minh khả thi cuối cùng và khuôn khổ lập luận được đưa ra.
- Bằng cách nhanh chóng loại bỏ các tuyến đường không hợp lệ, quá trình khám phá đã được đẩy nhanh đáng kể.
Nhiệm vụ này mất khoảng 12 giờ và hoàn thành trong 3 ngày. Nhìn lại, Ernest Ryu nhận ra rằng bằng chứng thực ra khá đơn giản.
Các bước chính trong bằng chứng được tạo ra bởi ChatGPT:
Ernest Ryu đã tóm tắt những đóng góp của mình:
- Lọc ra những lập luận không chính xác và tích lũy sê-ri các sự kiện chính xác.
- Xác định những ý tưởng lý luận mới đầy triển vọng và hướng dẫn ChatGPT khám phá sâu hơn những ý tưởng này.
- Nhận biết khi nào một chiến lược đã được khám phá đầy đủ và quyết định khi nào nên chuyển sang hướng khác.
Ông sẽ tiếp tục phát triển dự án này, công bố kết quả trên tạp chí lý thuyết tối ưu hóa chuyên nghiệp và chia sẻ các thông tin cập nhật và phát triển trong tương lai.
Sebastien Bubeck, nhà khoa học của OpenAI bị chỉ trích, cũng đã tái hiện một kịch bản tương tự—
GPT-5 có thể đưa ra những kết luận toán học thú vị.
Tuy nhiên, con người thực sự đã đánh bại GPT-5 :-). Một tác giả khác đã lấp đầy khoảng trống này, chứng minh một giới hạn mới.
Bằng chứng được đề xuất bởi GPT-5:
GPT-5 đã đề xuất một số ý tưởng mới có giá trị nghiên cứu. Hơn nữa, nó thực sự tự tạo ra hầu hết các từ gợi ý.
Liên kết: https://github.com/Dicklesworthstone/model_guided_research
Cánh cửa cho nghiên cứu được hỗ trợ bởi AI đang mở ra.
Có lẽ lịch sử sẽ không nhớ đến câu nói "Thật là xấu hổ", mà là dòng mã được biên dịch âm thầm thành qed.
Tham khảo:
https://x.com/SebastienBubeck/status/1980804267524116569
https://x.com/PI010101/status/1981014478969033156
https://borisalexeev.com/pdf/erdos707.pdf
https://mathstodon.xyz/@tao/115416211466664814
https://x.com/slow_developer/status/1980990021248160009
Bài viết này được trích từ tài khoản WeChat chính thức "New Intelligence" , do KingHZ biên tập và được xuất bản với sự cho phép của 36Kr.
