AI được sử dụng để xác minh bằng chứng toán học khó nhất từ ​​trước đến nay

Đánh dấu một cột mốc quan trọng trong nghiên cứu toán học được AI hỗ trợ, một nhóm tại Axiom Math đã tự động xác minh bằng chứng của một định lý liên quan đến số nguyên tố—thường được gọi là “định lý 246”—lần đầu tiên sử dụng hệ thống AI AxiomProver của công ty. Trong xác minh chính thức, các nhà toán học giao nhiệm vụ cho máy tính kiểm tra phiên bản chứng minh có thể đọc được bằng máy. Quá trình này không đảm bảo 100% rằng bằng chứng là chính xác, như một minh chứng gần đây đã cho thấy, cho thấy cách khai thác một lỗi trong phương pháp để chấp nhận bằng chứng sai do AI tạo ra. Tuy nhiên, phương pháp tính toán gần giống như một con tem cao su mà bạn có thể có được. Việc xác minh cụ thể này chính thức hóa một bước tiến quan trọng trong lý thuyết số. Ngoài bằng chứng cụ thể này, nó còn cho thấy cách sử dụng xác minh AI tự động trong tương lai để đảm bảo tính chính xác của mã máy tính do AI tạo ra sẽ sớm làm nền tảng cho phần mềm trên toàn cầu. Hình thức hóa hữu ích theo thiết kế Đây không phải là cuộc đua ngựa đầu tiên của AxiomProver. Axiom Math đã sử dụng hệ thống đa tác nhân tự động của mình để biến các câu lệnh toán học thành các bằng chứng có thể kiểm tra được bằng máy nhằm giải quyết một số vấn đề toán học chưa được giải quyết và xác minh nhiều bằng chứng khác trong năm nay. Nhưng việc chứng minh chính thức hóa định lý 246 cho đến nay là quan trọng nhất, như Ken Ono, nhà toán học sáng lập Axiom Math, giải thích: “Định lý này hiện đại diện cho ngưỡng hiểu biết của con người về số nguyên tố”. Đầu năm nay, đối thủ cạnh tranh của Axiom Math Math, Inc. đã sử dụng tác nhân Gauss của mình để chính thức hóa bằng chứng đoạt Huy chương Fields năm 2022 của Maryna Viazovska về bài toán đóng gói hình cầu trong 8 và 24 chiều. Sidharth Hariharan, tiến sĩ. sinh viên tại Đại học Carnegie Mellon, người dẫn đầu nỗ lực của con người trong kế hoạch chi tiết nhằm chính thức hóa chứng minh của Viazovska, nói rằng việc chính thức hóa định lý 246 là một thành tựu toàn diện và hữu ích hơn. LIÊN QUAN: Bước ngoặt cho sự hợp tác giữa AI và con người trong môn toán Hiện là thực tập sinh tại Axiom Math, Hariharan đã tham gia rất nhiều vào việc chính thức hóa chứng minh định lý 246 của công ty. Ông nói rằng một trong những điểm khác biệt chính ở đây là thay vì là cách tiếp cận một lần liên quan đến một vấn đề duy nhất, Axiom Math đã nhắm mục tiêu rõ ràng là làm cho các thành phần của quá trình hình thức hóa có thể tái sử dụng được cho các nhiệm vụ hình thức hóa khác và nghiên cứu toán học. Nhóm đã sử dụng AxiomProver để xây dựng một thư viện kết quả về các khoảng trống trong số nguyên tố. Định lý 246 là kết quả hàng đầu trong thư viện đó. Định lý 246 là gì? Một số số nguyên tố đầu tiên gần nhau: 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, .... Và có một số trường hợp chúng cách nhau bởi hiệu hai: 3:5, 5:7, 11:13, 17:19, .... Những cặp số nguyên tố này được gọi là số nguyên tố sinh đôi. Các số nguyên tố sinh đôi càng trở nên hiếm hơn khi bạn càng tiến xa hơn từ số 0, nhưng chúng dường như thỉnh thoảng vẫn xuất hiện. Giả thuyết số nguyên tố sinh đôi, lần đầu tiên được nhà toán học người Pháp Alphonse de Polignac đưa ra một cách chính xác vào thế kỷ 19, thừa nhận rằng chúng sẽ tiếp tục xuất hiện bất kể bạn nhìn dọc theo trục số bao xa. Nói cách khác, có vô số số nguyên tố sinh đôi. Mặc dù dễ phát biểu nhưng giả thuyết số nguyên tố sinh đôi đáng kính vẫn chưa được chứng minh. Bước tiến đầu tiên trong việc giải quyết nó chỉ xảy ra vào năm 2013 khi Yitang Zhang, hiện là giáo sư tại Đại học Tôn Trung Sơn, ở Quảng Châu, Trung Quốc, chứng minh rằng có vô số cặp số nguyên tố cách nhau 70 triệu. Vài tháng sau, sử dụng một kỹ thuật khác, giáo sư James Maynard của Đại học Oxford đã lly giảm khoảng cách này từ 70 triệu xuống chỉ còn 600; một kỳ tích góp phần quan trọng giúp Maynard được trao Huy chương Fields năm 2022—được nhiều người coi là giải Nobel về toán học. Là thành viên của một nhóm các nhà toán học được biết đến với tên gọi cộng tác Polymath8b, Maynard và người đồng nghiệp đoạt Huy chương Fields Terence Tao, giáo sư tại Đại học California, Los Angeles, đã giảm khoảng cách xuống chỉ còn 246, các nhà toán học gần nhất đã đạt được khoảng cách mục tiêu là hai. Chính định lý 246 này—trong đó phát biểu rằng có vô số số nguyên tố khác nhau 246—mà AxiomProver đã xác minh là đúng. Mã do AI tạo an toàn và chính xác Các kỹ thuật được chính thức hóa trong công trình này rất quan trọng trong lý thuyết số, nhánh toán học làm nền tảng cho tất cả an ninh mạng và mật mã ngày nay. Do đó, chúng có thể tỏ ra hữu ích trong việc xác minh những cách cụ thể để chúng ta giữ an toàn cho dữ liệu kỹ thuật số của mình trong tương lai. Nhưng Ono của Axiom Math lại hào hứng hơn với bức tranh lớn hơn. Ông coi việc chính thức hóa các bằng chứng toán học là bước đệm để xác minh mã do AI tạo ra, mã này đang bắt đầu được sử dụng trên toàn xã hội trong các hệ thống vận hành cơ sở hạ tầng, quản lý tài chính và bảo vệ dữ liệu của chúng ta. Điều này bất chấp những lo ngại về an toàn xung quanh ảo giác, lỗi và các lỗ hổng ngoài ý muốn khác. Nếu các thuộc tính của mã—chẳng hạn như thuật toán có kết thúc hay không hoặc liệu đầu ra của chương trình có đúng với bất kỳ đầu vào nào—có thể được chuyển thành các câu lệnh toán học chính xác hay không, thì các công nghệ có nguồn gốc từ AxiomProver sẽ phù hợp một cách lý tưởng để phát biểu và chứng minh chúng một cách chính thức. Bằng cách này, việc xác minh về mặt toán học tính chính xác của mã do AI tạo ra sẽ giúp mã này an toàn khi sử dụng. Ono kết luận: “Thế giới sắp chạy trên những mã máy tính mà chưa ai đọc được”. “AI đã ở đây và chúng ta không thể rời mắt được nữa—chính thức hóa bằng chứng là nơi thử nghiệm để giải quyết những gì tôi nghĩ là thách thức quan trọng nhất mà chúng ta sẽ phải đối mặt từ AI.”