Thuật toán tìm đường đi ngắn nhất mới nhanh hơn Dijkstra, được chứng minh bằng Lean

Bài toán tìm đường đi ngắn nhất là một trong những bài toán kinh điển và đơn giản nhất của khoa học máy tính. Cho một đồ thị gồm các đỉnh và các cạnh có hướng (hoặc vô hướng) với trọng số là số thực, xuất phát từ một đỉnh nguồn, ta cần tìm tổng trọng số nhỏ nhất của đường đi tới mọi đỉnh còn lại — hoặc báo rằng đỉnh đó không thể tiếp cận được.

Trong phiên bản được xét lần này, đồ thị là có hướng, yêu cầu đáp án chính xác tuyệt đối và trọng số các cạnh là số thực không âm. Mọi thao tác mà thuật toán thực hiện trong nội bộ — như đếm số đỉnh đã thăm hay lưu khoảng cách tạm thời — đều được tính vào thời gian chạy.

Bối cảnh: Dijkstra và các cột mốc gần đây

Với thiết lập trên, thuật toán Dijkstra kinh điển chạy trong thời gian O(m + n log n), với n là số đỉnh và m là số cạnh, đạt được nhờ cấu trúc dữ liệu hàng đợi ưu tiên phù hợp như Fibonacci heap.

Trong trường hợp m ≥ n, một số thuật toán tất định khác đã đạt được các cận tốt hơn:

• O(m log^(2/3) n) — lần đầu được giới thiệu trong một bài báo đột phá năm 2025
• O(m √log n + √(mn log n log log n)) — công trình tiếp nối năm 2026

Tuy nhiên, giữa các cận này vẫn tồn tại một vùng rộng trong không gian tham số — nơi m được biểu diễn như hàm của n — mà tại đó Dijkstra vẫn tỏ ra tốt hơn. Đây chính là khoảng trống mà nhóm nghiên cứu nhắm tới.

Thuật toán C-HD ra đời như thế nào?

Sau khoảng 15 giờ và 733 tin nhắn trên bảng tin nội bộ, một nhóm gồm 10 agent Claude Opus 5.5 đã hoàn thành đề xuất thuật toán mới mang tên C-HD cho bài toán tìm khoảng cách đường đi ngắn nhất chính xác trên đồ thị có hướng.

Điểm đáng chú ý: toàn bộ chứng minh tính đúng đắn và hiệu quả của thuật toán đều được thực hiện bằng Lean — công cụ xác minh hình thức (formal verification) hàng đầu hiện nay.

C-HD xử lý khá tốt việc tìm kiếm cục bộ gặp phải các cạnh "không sinh lợi". Thuật toán vẫn dùng so sánh ưu tiên, nhưng một đỉnh mới gặp có thể được tính vào giới hạn kích thước tìm kiếm như một lá chưa khám phá. Nó duy trì các bất biến cục bộ — tức các quy tắc luôn đúng sau mỗi lần cập nhật — kết hợp với việc xóa cạnh cẩn thận và tìm kiếm cục bộ có giới hạn.

Cận độ phức tạp đạt được

Trong vùng được chứng minh, thuật toán đạt cận:

O(n + m + m log(2 + m/(n+1)) + m^(1/3) · (n log(n+2))^(2/3))

với điều kiện mật độ m ≤ n · ⌊⌊log₂ n⌋^(3/4)⌋. Phân tích này cũng tính đến cả chi phí cấp phát bộ nhớ, sắp xếp cạnh, đọc đồ thị đầu vào và xuất kết quả.

Ý tưởng cốt lõi giúp C-HD vượt qua Dijkstra trong vùng liên quan là nó giảm công việc tìm kiếm và thao tác trên cấu trúc dữ liệu lặp lại:

• Xuất phát từ đỉnh nguồn và biên hiện tại của các đỉnh
• Chạy các tìm kiếm cục bộ có giới hạn dọc theo các cạnh đi ra
• Đếm các đỉnh mới gặp vào giới hạn tìm kiếm, kể cả những lá chưa khám phá khi một cạnh không cải thiện được ước lượng khoảng cách
• Dùng các cây tìm kiếm và điểm xoay thu được để tổ chức công việc đệ quy

Thuật toán vẫn đọc toàn bộ đồ thị đầu vào và phụ thuộc vào danh sách cạnh đi ra đã được sắp xếp — phần tiền xử lý này được tính vào chi phí của chính nó.

So sánh với các công trình trước

Để thấy rõ lợi thế, hãy xét đồ thị có khoảng m ≈ n log^(3/4) n cạnh:

• Dijkstra: O(n log n)
• C-HD: O(n log^(11/12) n)

Thoạt nhìn, mức cải thiện có vẻ nhỏ. Nhưng về mặt tiệm cận, nó thực sự tốt hơn khi đồ thị lớn dần. Ví dụ, với n = 2^1000, tỷ lệ giữa hai biểu thức dẫn đầu là 1000^(1/12) ≈ 1,78 (bỏ qua hằng số và các số hạng bậc thấp hơn).

Đáng lưu ý rằng đây không phải là tốc độ đo được trên thực tế, mà là cải thiện về cận tiệm cận. Mức cải thiện này tăng theo hàm polylogarit của kích thước đầu vào: nhân đôi n sẽ nhân tỷ lệ đó lên thêm 2^(1/12).

Hiệu năng thực tế và giới hạn

Cần nhấn mạnh một cách thẳng thắn: kết quả trên chỉ là cận trên của độ phức tạp — một lời hứa toán học. Hoàn toàn có thể xảy ra trường hợp dù tốt hơn về lý thuyết trong vùng này, thuật toán lại chạy chậm hơn khi triển khai thực tế.

Trong lần chạy này, nhóm chỉ thực hiện các mô phỏng nhỏ để kiểm tra tính đúng đắn, chứ không đo chuẩn (benchmark) trên đồ thị lớn thực tế. Các hằng số trong xây dựng hình thức là cực kỳ lớn, nên kết quả này không thiết lập được một tốc độ cải thiện thực dụng.

Khi m = 10n, đồ thị nằm ở vùng mật độ khác và kết quả này không chứng minh được cải thiện so với các cận tốt nhất đã biết ở vùng đó. Ngoài ra, với đầu vào nhỏ hoặc nằm ngoài vùng mật độ được chứng minh, nhóm bổ sung một thuật toán riêng là Bellman–Ford với thời gian chạy O((n+1)(m+1)), được chọn ngay từ đầu quá trình thực thi. Bellman–Ford ở đây không phải là một biến thể của Dijkstra.

Xác minh hình thức bằng Lean

Đoạn mã chứng minh then chốt trong namespace Frontier.CHD.Final khẳng định mục tiêu thời gian chạy đã đạt được:

theorem chd_CHDTarget : GateCTarget.CHDTarget GateCCalc.F :=
⟨chdProgram, chd_exact_within.1,
bodyC KcC + 65536 * 9 + 100, chd_exact_within.2⟩

theorem chd_gateC : Frontier.GateC :=
GateCTarget.chdTarget_F_imp_gateC chd_CHDTarget

Chứng minh được kiểm tra bằng công cụ Lean Comparator, đảm bảo ba điều:

• Chứng minh thực sự chứng minh định lý đã chỉ định
• Chỉ sử dụng các tiên đề được phép
• Được nhân (kernel) của Lean chấp nhận

Chứng minh này thiết lập cả cận thời gian chạy lẫn việc cải thiện tiệm cận chặt chẽ so với n log n dọc theo biên mật độ đã nêu. Khi thay biên đó vào các cận đã công bố, nó cũng cho thấy cận mới nhỏ hơn cả m log^(2/3) n lẫn m√log n + √(mn log n log log n).

Cách các agent phối hợp

Điều thú vị nhất có lẽ nằm ở phương pháp. Nhóm nghiên cứu đã tạo ra 10 agent Claude Opus 5.5 hoạt động ở mức nỗ lực tối đa, kết nối với nhau qua một bảng tin đơn giản. Các agent có vai trò ban đầu nhưng được tự do tổ chức lại công việc, chia sẻ phát hiện, phản biện ý tưởng của nhau và dồn nguồn lực vào hướng đi hứa hẹn nhất.

Chúng được giao một đề bài khá dài, yêu cầu cụ thể: tìm cải thiện lý thuyết đáng kể cho bài toán đường đi ngắn nhất chính xác trên đồ thị có hướng với trọng số thực không âm, kèm chứng minh Lean hoàn chỉnh. Các hướng được phép theo đuổi gồm loại bỏ các nhân tử logarit, tìm số mũ tốt hơn, tìm thuật toán thời gian tuyến tính, hoặc chứng minh cận dưới cơ bản cho mọi thuật toán.

Nhóm cũng được yêu cầu ghi lại các hướng tiếp cận thất bại để đồng đội không lặp lại, phản biện lẫn nhau, và trước khi tuyên bố thành công phải có bản build Lean tái lập được cùng hai vòng đánh giá độc lập. Nếu không chứng minh được cải thiện, chúng phải bảo toàn tiến độ một phần và nêu rõ điều gì còn bỏ ngỏ.

Toàn bộ gói chứng minh — mã nguồn Lean, bài báo không chính thức và hồ sơ xác minh — được công khai tại github.com/spicylemonade/c-hd-proof.

Ý nghĩa với cộng đồng công nghệ Việt Nam

Câu chuyện này đáng chú ý ở hai điểm. Thứ nhất, về mặt kỹ thuật, đây là một bước tiến nhỏ nhưng có thật trong lý thuyết thuật toán đồ thị — lĩnh vực đã tưởng như bão hòa sau nhiều thập kỷ. Thứ hai, về mặt phương pháp, nó cho thấy các agent AI có thể nén đáng kể thời gian nghiên cứu khi được tổ chức đúng cách và có công cụ xác minh chặt chẽ như Lean.

Với các kỹ sư và sinh viên Việt Nam đang làm việc trong lĩnh vực tối ưu hóa, logistics, bản đồ số hay hệ thống định tuyến, đây là lời nhắc rằng nền tảng lý thuyết bên dưới vẫn đang tiến hóa — và các công cụ AI hiện đại có thể trở thành trợ thủ đắc lực cho nghiên cứu hình thức.

Một quốc gia của những thiên tài trong một trung tâm dữ liệu — dự đoán đó hóa ra không quá xa vời.