- Terence Tao đã phát hiện một lỗi nhỏ nhưng không hề tầm thường trong bài báo khi thực hiện dự án hình thức hóa bằng Lean4
- Lỗi xuất hiện trong lập luận ở trang 6 của bài báo arXiv
2310.05328, khi1/2 log((n - 1)/(n - k - 1))phân kỳ tạin = 3, k = 2 - Vấn đề chỉ giới hạn ở các giá trị
nnhỏ; vớin >= 8thì lập luận hiện có vẫn hoạt động, còn các giá trịnnhỏ có thể được xử lý trực tiếp bằng phương pháp thô hơn - Lean yêu cầu chứng minh
0 < n - 3, nhưng giả thiết chỉ cón > 2, nên tacticlinarithkhông thể thu được mâu thuẫn cần thiết - Tao sẽ điều chỉnh một số hằng số số học để sửa lập luận, và dự định thêm chú thích vào phiên bản mới rằng sự thiếu chính xác của lập luận trước đó đã được phát hiện trong quá trình thử hình thức hóa bằng Lean
Lỗi được hé lộ bởi việc hình thức hóa bằng Lean4
- Terence Tao đã phát hiện rằng bài báo của mình có một bug nhỏ nhưng không hề tầm thường trong quá trình thực hiện dự án hình thức hóa bằng Lean4
- Đối tượng được hình thức hóa là lập luận ở trang 6 của bài báo arXiv
2310.05328 - Biểu thức có vấn đề có dạng sau
1/2 log((n - 1)/(n - k - 1))
- Biểu thức này phân kỳ trong trường hợp
n = 3, k = 2
Phạm vi lỗi và cách sửa
- Vấn đề này chỉ xảy ra với các giá trị
nnhỏ- Với
n >= 8, lập luận đó vẫn hoạt động - Các giá trị
nnhỏ có thể được xử lý trực tiếp bằng phương pháp thô hơn, nhưng các hằng số sẽ tệ hơn
- Với
- Tao cho rằng có thể sửa lập luận bằng cách thay đổi một số hằng số số học trên trang đó
- Trong phiên bản mới của bài báo, ông dự định thêm một chú thích nói rằng lập luận trước đó hơi thiếu chính xác và điều này được phát hiện khi cố hình thức hóa bằng Lean
Điểm cụ thể khiến Lean bị kẹt
- Tại điểm việc hình thức hóa thất bại, Lean yêu cầu chứng minh
0 < n - 3- Giả thiết khả dụng chỉ là
n > 2 - Tactic
linarithkhông thể suy ra mâu thuẫn từ phủ định của0 < n - 3
- Giả thiết khả dụng chỉ là
1 bình luận
Ý kiến trên Hacker News
Ông ấy đã bắt đầu học Lean4 với sự trợ giúp của GPT-4 từ đầu tháng này: https://mathstodon.xyz/@tao/111208692505811257
Khá nhiều bài đăng Mastodon của ông trong tháng này nói về tiến độ học tập, và đây là một ví dụ thú vị cho thấy mô hình ngôn ngữ lớn có thể tăng tốc công việc của cả những người thuộc nhóm thành tựu hàng đầu đến mức nào
Điều thú vị là nếu chỉ người có kỹ năng cao mới tận dụng hiệu quả được các công cụ này, chúng có thể còn làm gia tăng bất bình đẳng
Nếu muốn tiếp cận Lean4 một cách dễ dàng thì Natural Number Game là lựa chọn tốt: https://adam.math.hhu.de/#/g/hhu-adam/NNG4
Nếu muốn chỉ đọc mà không chơi game thì xem ở đây: https://lean-lang.org/theorem_proving_in_lean4/introduction.html
Ban đầu tôi còn viết Alloy thành Allow
Vài năm trước, khi tìm cách giảm bớt sai sót trong các chương trình mình viết, tôi biết đến TLA+ của Lamport và học cách viết đặc tả hình thức bằng cách suy nghĩ về hành vi chương trình như một máy trạng thái
TLA+ giúp tôi hiểu rõ hơn về trừu tượng hóa, và sau đó tôi cũng phát hiện ra loạt Software Foundations về việc tạo phần mềm đúng đắn một cách hình thức bằng trợ lý chứng minh Coq. Các bài tập được làm như những trò chơi nhỏ nên giải khá vui: https://softwarefoundations.cis.upenn.edu/
Đặc tả hình thức, một dạng trừu tượng hóa ở mức cao, tập trung vào ngôn ngữ chuyên dụng để mô tả mã; còn hợp đồng mã ở mức trừu tượng hóa thấp hơn thì gần giống việc thay thế logic kiểm chứng bằng một mô hình tốt hơn. C# từng có Code Contracts[1], một cách làm đơn giản nhưng mạnh mẽ để kiểm tra hợp đồng ở thời điểm biên dịch bằng bộ giải SMT Z3[2], nhưng vài năm sau đã bị ngừng[3], rồi bị gỡ khỏi .NET Runtime và coi như chấm dứt. Thứ gần nhất trong C# hiện nay có lẽ là Dafny[4], và phía phát triển C# vẫn đang suy nghĩ cách đưa nó trực tiếp vào ngôn ngữ[5]
[1] https://www.microsoft.com/en-us/research/project/code-contracts/
[2] https://github.com/Z3Prover/z3
[3] https://github.com/microsoft/CodeContracts
[4] https://github.com/dafny-lang/dafny
[5] https://github.com/dotnet/csharplang/issues/105
Idris2 có vẻ đang hướng tới một ngôn ngữ đa dụng nhưng vẫn cung cấp hệ thống kiểu tiên tiến hơn cho việc chứng minh định lý: https://github.com/idris-lang/Idris2
Cũng có một cuốn sách khá liên quan dùng Agda thay vì Coq: https://plfa.github.io/
Tôi vẫn chưa đọc, nhưng đã đưa vào danh sách, và tôi nghĩ Agda hay Idris có khả năng mang cảm giác giống một ngôn ngữ lập trình hơn Coq
Kiểu phụ thuộc thực sự rất đáng mong đợi. Chỉ là có lẽ trong thời gian tới vẫn khó xuất hiện rộng rãi
Dependent Haskell vẫn đang được triển khai, nhưng người ta nói việc ghép nó vào một ngôn ngữ đã tồn tại từ trước là rất khó; tác giả của Idris cũng từng nói ông hy vọng Idris sẽ trở thành hình mẫu cho các ngôn ngữ khác chứ việc được chấp nhận rộng rãi thì có vẻ khó. Coq, Agda, F* cũng không được thiết kế như ngôn ngữ đa dụng. Việc hiện thực trình biên dịch thì phức tạp và cú pháp có thể trở nên dài dòng, nhưng điều tôi muốn là sự đơn giản. Tôi muốn mã hóa mọi điều mình biết về đầu vào và đầu ra. Trong các ngôn ngữ chủ đạo hiện nay, thường có nhiều điều ta biết về đối số hoặc kết quả hơn những gì hệ thống kiểu cho phép biểu đạt
Sẽ thật tuyệt nếu có một cách tiếp cận dần dần như TypeScript, nơi bạn không cần phải chứng minh mọi thứ ở mọi chỗ mà vẫn có thể thêm thông tin ràng buộc giá trị ở mức kiểu tại những vị trí tùy ý
Ví dụ, nếu bạn biết một danh sách số và đồng thời biết độ dài của nó, thì với kiểu phụ thuộc bạn có thể tạo ra một kiểu danh sách có chứa độ dài đó một cách tường minh, và bảo đảm ở thời điểm biên dịch rằng các phép toán vẫn giữ nguyên độ dài ấy. Nếu bạn chỉ định một hàm chỉ nhận danh sách dài 3 mà lại truyền vào danh sách dài 4 thì nó sẽ không biên dịch, nhờ đó bắt được lỗi trước khi chạy. Nó giống như một lớp kiểm tra an toàn bổ sung làm cho kiểu trở nên biểu đạt hơn và thậm chí mã hóa được cả những quan hệ phức tạp giữa các biến
Nếu một trong những trí tuệ xuất sắc nhất của thế hệ chúng ta có thể mở rộng phạm vi công việc nhờ sự kết hợp giữa mô hình ngôn ngữ lớn và chứng minh tự động, thì tương lai của tổ hợp công nghệ này có vẻ rất đáng lạc quan.
Khởi đầu là sửa lỗi, tiếp theo là hỗ trợ kiểm chứng, rồi cuối cùng có lẽ sẽ thúc đẩy những khám phá mới và mở rộng các giới hạn. Cần có một thuật ngữ để chỉ hiện tượng những động lực kiểu như định luật Moore “lây nhiễm” sang các lĩnh vực vốn dĩ không có tính tích lũy như vậy. Thêm bối cảnh là Terence Tao đang dùng Copilot để học Lean: https://mathstodon.xyz/@tao/111271244206606941
Có lẽ ông ấy vẫn có thể làm điều đó mà không cần Copilot, nhưng cũng có thể đã không bắt đầu vì ma sát trong việc tiếp nhận một công cụ mới. Các mô hình ngôn ngữ lớn có tiềm năng lớn trong những tình huống kiểu “xe đạp cho tư duy” như thế này
Vài năm trước tôi cũng từng tìm ra một lỗi trong một bài viết trên blog toán học của Terence Tao. Tôi báo cho ông ấy, ông ấy đã sửa và còn cảm ơn tôi.
Tất nhiên chuyện đó đã không thể lên trang nhất Hacker News
Tôi đã lo rằng Lean4 lại là một mô hình ngôn ngữ lớn khác, nhưng thực ra nó là một công cụ khá vững chắc và đáng tin cậy
Tò mò liệu có thể kết hợp trình kiểm tra chứng minh hình thức như Lean proof checker với các mô hình ngôn ngữ tạo ra các cặp giả thuyết-chứng minh tổng hợp bằng một ngôn ngữ hình thức như Lean hay không
Trình kiểm tra chứng minh Lean có thể tự động xác minh xem các chứng minh tổng hợp do mô hình ngôn ngữ viết ra có đúng hay không, rồi dùng thông tin đó làm tín hiệu phần thưởng học tăng cường áp vào chính mô hình ngôn ngữ ban đầu để khiến nó viết chứng minh tốt hơn. Hoặc cũng có thể dùng các chứng minh tổng hợp đúng từ vòng trước làm dữ liệu huấn luyện để đào tạo mô hình mới. Thậm chí còn có thể làm theo hướng đối kháng hơn. Chia hệ thống thành mô hình tạo giả thuyết và mô hình chứng minh/bác bỏ, rồi thêm một mô hình dự đoán liệu chứng minh tổng hợp có được trình kiểm tra chứng minh Lean xác minh hay không. Xác suất được dự đoán là đúng càng thấp thì khi thật sự đưa ra được chứng minh đúng, mô hình tạo chứng minh sẽ nhận phần thưởng càng lớn. Cuối cùng, nếu thêm một mô hình dự đoán phần thưởng mà mô hình tạo chứng minh sẽ nhận được cho một giả thuyết tổng hợp cụ thể, thì mô hình tạo giả thuyết sẽ được thưởng khi tạo ra các giả thuyết có mức phần thưởng kỳ vọng cao nhưng không quá khó cũng không quá dễ đối với mô hình tạo chứng minh. Toàn bộ hệ thống có thể dần tạo ra các chứng minh tổng hợp ngày càng khó hơn, và điều này có thể dẫn tới khả năng tự học tốt hơn của mô hình tạo chứng minh. Về nguyên tắc, nó có thể mở rộng tới năng lực siêu nhân trong việc tạo chứng minh, tương tự GAN hoặc cơ chế tự đấu của AlphaGo Zero. Phần khó là giai đoạn khởi động ban đầu, vì việc huấn luyện đầu tiên của mô hình sinh cần dữ liệu chứng minh Lean do con người cung cấp. Nhưng nếu các chứng minh tổng hợp trở nên đủ tốt thì hệ thống có thể tự động tiếp tục quá trình tự học
Cuối cùng có thể thu được một mô hình biết mọi định lý và mọi chứng minh đúng trong toàn bộ tài liệu toán học
Ở giai đoạn đầu, bắt đầu bằng học có giám sát từ các chứng minh hiện có rồi tìm chứng minh mới, có TacticToe (https://arxiv.org/abs/1804.00596), Tactician (https://arxiv.org/pdf/2008.00120.pdf), CoqGym/ASTactic (https://arxiv.org/abs/1905.09381), Proverbot9001 (https://arxiv.org/abs/1907.07794), Diva (https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms) v.v. Phần lớn đều có một dạng mô hình ngôn ngữ nào đó bên trong, nhưng nếu tìm các mô hình ngôn ngữ lớn gần đây thu hút nhiều chú ý thì có GPT-f (https://arxiv.org/abs/2009.03393), Baldur (https://arxiv.org/abs/2303.04910), COPRA (https://arxiv.org/abs/2310.04353). Tuy nhiên ở thời điểm hiện tại, các mô hình như vậy dường như chưa hiệu quả bằng các công cụ chuyên biệt không phải mô hình ngôn ngữ lớn. Về hướng học bằng tăng cường vượt ra ngoài các chứng minh do con người viết thì có TacticZero (https://openreview.net/forum?id=edmYVRkYZv), bài báo của OpenAI (https://arxiv.org/pdf/2202.01344.pdf), rlCoP (https://arxiv.org/abs/1805.07563), các công trình thuộc dòng HOList (https://arxiv.org/pdf/1905.10006.pdf), HyperTree Proof Search (https://arxiv.org/abs/2205.11491), cùng với công việc đang được nhóm University of Massachusetts và tôi tiến hành
Bối cảnh trước đó về việc Tao đã dùng các công cụ mô hình ngôn ngữ lớn, bao gồm GPT-4 trong hành trình này như thế nào có ở đây: https://mathstodon.xyz/@tao/111233986893287137
Có thể theo dõi tiến độ của ông ấy trên GitHub: https://github.com/teorth/symmetric_project/