AI dùng được để kiểm chứng minh ở vai người đọc thử: chỉ ra bước thiếu lý do, trường hợp bị bỏ sót, chỗ dùng sai định nghĩa; nhưng nó không đáng tin ở vai người phán quyết cuối cùng, vì nó có thể khen một chứng minh sai và chê một chứng minh đúng với cùng một giọng tự tin. Khác biệt giữa hai vai đó quyết định bạn học được gì hay chỉ nhận về một cảm giác yên tâm giả.
Bài này liệt kê những chỗ chatbot hay sai khi đọc và viết chứng minh, đưa một quy trình bảy bước để kiểm chứng minh của chính bạn bằng AI, một bài thử để đánh giá công cụ bạn đang dùng, phân biệt chatbot với các trợ lý chứng minh hình thức, và nói rõ ranh giới liêm chính học thuật.
Những chỗ chatbot hay sai khi làm việc với chứng minh
Bước sai viết bằng giọng chắc chắn. Mô hình ngôn ngữ sinh ra câu chữ trôi chảy, và một bất đẳng thức đảo chiều hay một phép chia cho số có thể bằng 0 được viết với cùng độ tự tin như một bước đúng. Không có tín hiệu nào trong văn phong cho biết bước nào đáng ngờ.
Dễ đồng ý với người hỏi. Khi bạn gửi một chứng minh và hỏi "đúng không", chatbot có xu hướng xác nhận, nhất là khi chứng minh trông giống một dạng quen. Hỏi theo kiểu trung lập, hoặc bảo nó tìm lỗi, cho kết quả tốt hơn.
Lắp khuôn quen. Với bài trông giống bài kinh điển, AI hay viết lại lời giải kinh điển dù đề đã đổi một chi tiết làm khuôn cũ không còn chạy. Ví dụ đổi căn bậc hai của 2 thành căn bậc hai của 4.
Đổi thứ tự lượng từ. Trong giải tích, chuyển "với mọi ε tồn tại N" thành "tồn tại N với mọi ε" là thay đổi ý nghĩa hoàn toàn, và đây là loại lỗi tinh vi chatbot có thể mắc khi diễn đạt lại.
Dùng định lý mà quên kiểm giả thiết. Áp dụng một định lý về hàm liên tục cho một hàm không liên tục, hoặc định lý về khoảng đóng cho khoảng mở. Kết luận nghe rất hợp lý nhưng không có cơ sở.
Bịa tên định lý hoặc tài liệu. Khi bị hỏi "theo định lý nào", AI đôi khi đưa ra một cái tên nghe như thật hoặc một trích dẫn không tồn tại. Mọi tên định lý lạ đều cần tra lại trong giáo trình.
Quy trình bảy bước kiểm một chứng minh bằng AI
Quy trình dưới đây giữ phần suy nghĩ ở phía bạn và dùng AI ở đúng chỗ nó có ích:
- Tự kiểm trước. Đọc lại chứng minh theo danh sách kiểm của riêng bạn. Bước này không được bỏ, vì nếu bỏ, bạn sẽ dần giao luôn việc suy nghĩ.
- Cung cấp đủ ngữ cảnh. Gửi nguyên phát biểu, các định nghĩa giáo trình dùng, và chứng minh của bạn, đánh số từng dòng. Thiếu định nghĩa, AI sẽ dùng định nghĩa nó quen, có thể khác giáo trình.
- Yêu cầu đánh giá từng dòng, không viết lại. Câu lệnh mẫu: "Với mỗi dòng đánh số, cho biết dòng đó suy ra từ đâu và có hợp lệ không. Chỉ nêu nhận xét, không viết chứng minh mới."
- Hỏi phản ví dụ cho từng bước đáng ngờ. "Dòng 4 có đúng với mọi x thoả giả thiết không? Nếu không, cho một phản ví dụ cụ thể." Một phản ví dụ cụ thể kiểm được bằng tay, còn một lời khẳng định thì không.
- Tự kiểm mọi nhận xét. Với mỗi chỗ AI chỉ ra, tự xác minh bằng định nghĩa hoặc bằng tính toán. Nhận xét sai thì ghi lại, đó cũng là thông tin về độ tin cậy của công cụ.
- Đối chiếu chéo. Với chứng minh quan trọng, hỏi lại trong một cuộc trò chuyện mới, hoặc một công cụ khác, mà không kèm nhận xét cũ. Hai lần độc lập cùng chỉ một chỗ thì chỗ đó đáng xem kỹ.
- Hỏi người thật ở chỗ còn tranh cãi. Giảng viên, trợ giảng, nhóm học. AI giúp bạn đến giờ thảo luận với câu hỏi sắc hơn, không thay giờ thảo luận.
Nếu dán chứng minh từ tài liệu không công khai, như đề kiểm tra chưa tới hạn hay bản thảo nghiên cứu của nhóm, hãy cân nhắc quy định của lớp hoặc nhóm trước. Với tài liệu nghiên cứu, che tên người và chi tiết chưa công bố.
Bài thử nhanh: chứng minh 1 = 2
Trước khi tin một công cụ để kiểm chứng minh, hãy thử nó với một chứng minh sai kinh điển mà bạn biết lỗi. Chứng minh sau được dùng nhiều trong lớp học: cho a = b, với b khác 0. Nhân hai vế với a được a² = ab. Trừ hai vế cho b² được a² − b² = ab − b². Phân tích: (a + b)(a − b) = b(a − b). Chia hai vế cho a − b được a + b = b. Vì a = b nên 2b = b, chia cho b được 2 = 1.
Lỗi nằm ở bước chia cho a − b, vì a = b nên a − b = 0. Mọi bước trước đó đều đúng; đẳng thức (a + b)(a − b) = b(a − b) đúng vì cả hai vế bằng 0. Phép chia cho 0 là chỗ duy nhất gãy.
Chatbot phổ biến hiện nay gần như chắc chắn nhận ra chứng minh này vì nó quá nổi tiếng. Bài thử có giá trị hơn là bạn tự ngụy trang nó: đổi tên biến, đặt nó trong một bài toán khác, hoặc giấu phép chia cho 0 trong một bước rút gọn phân thức. Ví dụ rút gọn (x² − 1)/(x − 1) thành x + 1 rồi thay x = 1. Xem công cụ có còn tìm ra lỗi không khi nó không thể nhận mặt bài quen. Kết quả của vài bài thử như vậy cho bạn cảm giác thực tế về mức tin cậy, tốt hơn mọi lời quảng cáo.
Chatbot khác trợ lý chứng minh hình thức thế nào
Ngoài chatbot, có một loại phần mềm khác là trợ lý chứng minh hình thức, nơi chứng minh được viết bằng một ngôn ngữ chính xác và máy kiểm từng bước theo quy tắc logic. Lean, Coq và Isabelle là vài cái tên được nhắc nhiều. Hai loại công cụ này khác nhau về bản chất:
| Tiêu chí | Chatbot | Trợ lý chứng minh hình thức |
|---|---|---|
| Đầu vào | Chữ và ký hiệu tự do | Ngôn ngữ hình thức chặt chẽ, phải học riêng |
| Cách kiểm | Đánh giá dựa trên mẫu đã học, có thể sai | Kiểm từng bước theo quy tắc logic cố định |
| Khi nói "đúng" | Là một ý kiến | Là kết quả kiểm máy, đúng tương đối với định nghĩa đã khai báo |
| Độ khó bắt đầu | Dùng ngay | Mất nhiều tuần để quen |
| Hợp với | Tìm ý, góp ý, giải thích | Xác nhận chặt chẽ, dự án nghiên cứu, thư viện toán |
Có những hướng kết hợp hai loại: AI đề xuất các bước, trợ lý hình thức kiểm. Hướng này đang phát triển nhanh, tính năng thay đổi theo từng phiên bản, nên khi tìm hiểu hãy kiểm tài liệu hiện hành của từng công cụ. Với sinh viên năm đầu, biết rằng có sự khác biệt giữa "AI nói đúng" và "máy đã kiểm" là đủ để không nhầm hai thứ với nhau.
Máy tính trong chứng minh: không phải chuyện mới
Dùng máy tính để chứng minh toán học có lịch sử dài hơn chatbot. Định lý bốn màu, khẳng định mọi bản đồ phẳng tô được bằng bốn màu sao cho hai vùng kề nhau khác màu, được Kenneth Appel và Wolfgang Haken chứng minh năm 1976 với phần kiểm một số lượng rất lớn cấu hình giao cho máy tính. Chứng minh này gây tranh luận nhiều năm, vì không ai kiểm toàn bộ bằng tay được. Về sau, định lý cũng được kiểm lại trong một trợ lý chứng minh hình thức.
Câu chuyện đó cho thấy một điểm quan trọng khi bạn nghĩ về AI: vấn đề chưa bao giờ là máy có được tham gia chứng minh hay không, mà là phần máy làm có kiểm được hay không. Một phép tính máy làm theo chương trình rõ ràng thì người khác chạy lại và kiểm được. Một nhận xét "chứng minh này đúng" của chatbot thì không chạy lại được theo nghĩa đó; hỏi lại có thể ra câu trả lời khác.
Vì vậy, khi dùng AI trong việc học chứng minh, hãy ưu tiên những đầu ra kiểm được: một phản ví dụ cụ thể, một phép tính, một trích dẫn tới định lý trong giáo trình mà bạn tra được. Những đầu ra không kiểm được, như lời khen chung chung, nên được coi là không có giá trị. Một câu lệnh giúp đẩy AI về phía đầu ra kiểm được: "Với mỗi nhận xét, kèm một phép tính hoặc một phản ví dụ cụ thể mà mình tự kiểm được bằng tay; nhận xét nào không kèm được thì bỏ."
Liêm chính học thuật: ranh giới rõ ràng
Phần lớn trường đại học coi việc nộp bài làm do người khác hoặc công cụ khác viết, mà không khai báo, là vi phạm liêm chính học thuật. Quy định về AI cụ thể khác nhau giữa các trường và giữa các môn, có môn cấm hẳn, có môn cho phép dùng để góp ý nếu ghi rõ. Việc đầu tiên là đọc đề cương môn học hoặc hỏi giảng viên.
Ngoài chuyện quy định, có một lý do thực tế hơn. Kỹ năng chứng minh chỉ hình thành khi bạn tự vật lộn với lập luận. Một học kỳ nộp chứng minh do AI viết có thể qua được bài tập về nhà, nhưng sẽ lộ ra ngay trong bài thi viết tay, và lộ ra rõ hơn nữa ở các môn năm sau, nơi mọi thứ xây trên nền đó.
Ranh giới dễ nhớ: AI được hỏi, được góp ý, được ra đề luyện, được giải thích một dòng bạn không hiểu. Chữ trên bài nộp, và lập luận đằng sau nó, là của bạn. Không dùng AI trong phòng thi hoặc trong bài kiểm tra mà quy định không cho phép, dưới bất kỳ hình thức nào.
Câu hỏi thường gặp
Chatbot nói chứng minh của mình đúng thì có tin được không?
Không nên coi đó là phán quyết. Chatbot có thể xác nhận một chứng minh sai, nhất là khi bạn hỏi kiểu đúng không. Hãy yêu cầu nó đánh giá từng dòng và đưa phản ví dụ cụ thể, rồi tự kiểm mọi nhận xét.
Câu lệnh nào giúp AI kiểm chứng minh tốt hơn?
Gửi đủ phát biểu, định nghĩa và chứng minh đánh số dòng; yêu cầu cho biết mỗi dòng suy ra từ đâu và có hợp lệ không; cấm viết lại chứng minh; hỏi phản ví dụ cụ thể cho bước đáng ngờ.
Trợ lý chứng minh hình thức khác chatbot thế nào?
Trợ lý chứng minh hình thức kiểm từng bước theo quy tắc logic cố định với chứng minh viết bằng ngôn ngữ chính xác. Chatbot chỉ đưa ra ý kiến dựa trên mẫu đã học, có thể sai và hỏi lại có thể ra kết quả khác.
Có nên nhờ AI viết chứng minh để nộp bài tập không?
Không. Ở hầu hết các trường đó là vi phạm liêm chính học thuật nếu không được phép và không khai báo. Kỹ năng chứng minh cũng chỉ hình thành khi bạn tự làm; bài thi viết tay sẽ cho thấy khoảng trống đó.
Làm sao biết một công cụ AI có đáng tin để kiểm chứng minh không?
Thử nó với vài chứng minh sai mà bạn biết lỗi, nhất là những chứng minh được ngụy trang để nó không nhận ra bài quen. Tỷ lệ bắt đúng lỗi của các bài thử đó cho bạn cảm giác thực tế về độ tin cậy.
AI đưa ra tên một định lý lạ thì xử lý thế nào?
Tra lại trong giáo trình hoặc tài liệu chính thống trước khi dùng. AI đôi khi bịa tên định lý hoặc trích dẫn nghe như thật. Nếu không tra được, coi như bước đó chưa có cơ sở.