AI giải bài toán cờ vua 58 năm

Hệ thống trí tuệ nhân tạo Double Agent tìm ra thế cờ có 63 nước đi hợp lệ đều chiếu, đồng thời chứng minh không thể vượt qua con số này, phá kỷ lục tồn tại từ năm 1968.

Double Agent công bố kết quả nghiên cứu hôm 13/10, giải quyết một bài toán lâu năm trong cờ vua bằng cách kết hợp các phương pháp tìm kiếm, logic toán học và chứng minh được máy tính kiểm tra. Hệ thống xác định số nước đi hợp lệ tối đa trong một thế cờ mà tất cả nước đi đều chiếu vua là 63, vượt kỷ lục 60 nước trước đó của Norbert Ringeltaube.

Double Agent không chỉ tìm được một thế cờ có 63 nước chiếu, còn chứng minh đây là giới hạn tối đa. Nhóm nghiên cứu xác nhận thế cờ đạt kỷ lục có thể xuất hiện thông qua một ván đấu hợp lệ, thay vì chỉ tồn tại trên lý thuyết.

Bài toán đặt ra một điều kiện đặc biệt: bên tới lượt đi phải có ít nhất một nước đi hợp lệ, nhưng mọi nước đi hợp lệ đều phải chiếu vua đối phương. Nếu có dù chỉ một nước đi không chiếu, thế cờ đó không đáp ứng yêu cầu. Vì vậy, việc tăng số quân hoặc tạo thêm khả năng tấn công chưa chắc giúp cải thiện kết quả, bởi mỗi nước đi bổ sung cũng phải thỏa mãn điều kiện trên.

Chiếu vua là tình huống vua bị quân đối phương tấn công trực tiếp. Người chơi buộc phải xử lý mối đe dọa này bằng một nước đi hợp lệ. Bài toán của Double Agent không đơn thuần tìm nhiều cách chiếu nhất có thể, mà yêu cầu toàn bộ nước đi hợp lệ của một bên đều phải tạo ra tình huống đó.

Để đạt 63 nước, thế cờ phải được bố trí chặt chẽ. Các quân trên bàn không chỉ có nhiệm vụ tạo ra những đòn chiếu, còn hạn chế hoặc ngăn cản những nước đi không đáp ứng điều kiện. Một quân có thể bị ghim, khiến việc di chuyển trở nên bất hợp lệ vì sẽ để vua của chính mình bị chiếu. Những quân khác có thể chắn đường hoặc kiểm soát ô cờ, loại bỏ các lựa chọn không phù hợp.

Theo nhóm nghiên cứu, cách giải quyết bằng tìm kiếm vét cạn thông thường không khả thi. Thay vì thử mọi thế cờ có thể có, Double Agent trước tiên chứng minh những đặc điểm cấu trúc về hình học của các đòn chiếu trên bàn cờ. Nhóm sau đó hình thức hóa các kết quả này bằng Lean 4, ngôn ngữ dùng để biểu diễn và kiểm tra chứng minh toán học, rồi chuyển phần còn lại thành bài toán thỏa mãn các điều kiện logic, gọi tắt là SAT.

SAT là phương pháp xác định liệu có tồn tại cách gán giá trị đúng hoặc sai cho một tập hợp biến để thỏa mãn toàn bộ điều kiện đặt ra hay không. Trong bài toán cờ vua, các điều kiện có thể liên quan đến sự hiện diện của quân trên một ô, khả năng di chuyển của quân hoặc việc một ô cờ có bị chiếm hay không. Những ràng buộc này kết hợp với nhau để loại bỏ các thế cờ không hợp lệ.

Nhóm nghiên cứu cho biết các chứng minh đều được kiểm tra bằng máy. Cách tiếp cận này giúp kết quả không phụ thuộc đơn thuần vào việc chương trình tìm thấy một lời giải có vẻ đúng. Hệ thống còn phải cung cấp cơ sở để xác nhận không tồn tại lời giải vượt quá giới hạn đã nêu trong phạm vi bài toán.

Ngoài kỷ lục 63 nước đi, Double Agent còn nghiên cứu một câu hỏi khác. Nếu hai bên liên tục đáp trả một nước chiếu bằng một nước chiếu khác, chuỗi dài nhất có thể kéo dài bao nhiêu nước?

Kỷ lục được biết đến trước nghiên cứu này là 54 nước chiếu liên tiếp, trong một thế cờ do Alexey Khanyan sáng tác năm 2013. Với bài toán mới, hệ thống chứng minh rằng từ bất kỳ thế cờ hợp lệ nào, không thể có quá 364 nước đi liên tiếp mà tất cả đều chiếu.

Tuy nhiên, con số 364 mới là giới hạn trên được chứng minh, không phải số nước tối đa đã được xác định chính xác. Nhóm nghiên cứu cho biết độ dài lớn nhất thực sự của chuỗi chiếu liên tiếp vẫn là câu hỏi bỏ ngỏ.