Claude Opus 4.8 tạo ra thuật toán giao đa giác được kiểm chứng chính thức trong một lần

Trong một bước tiến đáng chú ý kết hợp giữa hình học tính toán và trí tuệ nhân tạo, một nhà phát triển đã giới thiệu thuật toán giao đa giác (polygon intersection) đầu tiên được kiểm chứng chính thức (formally verified). Dự án này sử dụng ngôn ngữ Lean 4 cùng với sự hỗ trợ của các tác nhân AI hiện đại, đặc biệt là Claude Opus 4.8, để tạo ra một thuật toán có độ chính xác toán học tuyệt đối.

Ví dụ về giao đa giác

Thách thức trong hình học tính toán

Giao đa giác là một tính năng tiêu chuẩn trong các trình chỉnh sửa đồ họa vector như Illustrator hay Inkscape. Tuy nhiên, việc triển khai thuật toán này cực kỳ phức tạp do có vô số cấu hình đầu vào khác nhau. Với phương pháp kiểm thử cổ điển, không thể nào bao quát hết mọi trường hợp đặc biệt, đặc biệt là khi xử lý các đa giác tổ hợp (multipolygons) có lỗ, tự giao nhau hoặc các cạnh chồng chéo.

Trong dự án này, thuật toán giao đa giác được định nghĩa và kiểm chứng hoàn toàn bằng Lean 4 – một trợ lý chứng minh (proof assistant). Điều này cho phép đảm bảo rằng tập hợp các điểm bên trong của đa giác kết quả thực sự bằng giao của hai tập hợp điểm đầu vào, bất kể cấu hình phức tạp đến đâu.

Ví dụ phức tạp về giao đa giác

Bước nhảy vọt của Claude Opus 4.8

Điểm thú vị nhất của dự án nằm ở cách thức sử dụng AI. Tác giả chia sẻ rằng trải nghiệm làm việc với các tác nhân AI đã thay đổi hoàn toàn với các bản phát hành mô hình gần đây:

• Các phiên bản cũ (Opus 4.5, 4.7): Yêu cầu con người phải phác thảo chiến lược chứng minh chi tiết từng bước. AI chỉ đóng vai trò dịch các ý tưởng của con người sang mã Lean khi chiến lược đã hoàn hảo.
• Claude Opus 4.8 (Ultracode mode): Có khả năng cung cấp triển khai thuật toán kèm theo chứng minh chính thức chỉ trong một lần chạy (oneshot). Mô hình này tự xây dựng và thực thi các chiến lược chứng minh lớn, thậm chí tự điều hướng khi phát hiện các định lý trung gian có thể sai.

Opus 4.8 đã chứng minh khả năng xử lý rủi ro khi chứng minh các định lý lớn bằng cách tự động chuyển đổi chiến lược hoặc chạy các tác nhân con song song để thử nhiều cách tiếp cận khác nhau.

Độ tin cậy và quy trình kiểm chứng

Một khía cạnh quan trọng của dự án này là sự tách biệt giữa việc tạo mã và việc kiểm chứng tính đúng đắn:

Sự tin cậy vào tính chính xác đến hoàn toàn từ bộ kiểm tra Lean và sự xem xét của con người đối với một bộ thông số kỹ thuật nhỏ gọn, không phải từ LLM.

Con người chỉ cần xem xét 3 tệp định nghĩa Lean (tổng cộng khoảng 87 dòng mã) để hiểu các khái niệm hình học cơ bản. Toàn bộ mã triển khai thuật toán và các bằng chứng phức tạp (có thể lên tới hàng nghìn dòng) được viết tự động bởi AI và không cần con người xem xét lại. Điều này có thể thực hiện được nhờ bộ kiểm tra Lean sẽ xác minh tính logic của mã, đảm bảo không có lỗi nào tồn tại.

Bạn có thể trải nghiệm thuật toán này thông qua bản demo web được xây dựng dựa trên lõi đã được kiểm chứng, cho phép vẽ và giao các đa giác trực tiếp trên trình duyệt.