Cựu nhà nghiên cứu Axiom Math và Kimi hợp tác khởi nghiệp, dùng AI giải quyết bài toán xác minh chip

Động Sát Beating Tin nhanh AI, một trong những điều mà thiết kế chip sợ nhất là sau khi sản xuất mới phát hiện lỗi logic. Một khi sự cố xảy ra, có thể cần phải thiết kế lại, tape-out lại, trả giá đắt. Xác minh chip chính là để trước khi sản xuất, cố gắng tìm ra những lỗi ẩn này càng nhiều càng tốt.

Xác minh chip truyền thống chủ yếu dựa vào kiểm thử mô phỏng, nhưng các tổ hợp trạng thái vận hành bên trong chip có thể đạt tới con số thiên văn, hoàn toàn không thể kiểm thử từng cái một. Xác minh hình thức thì sử dụng phương pháp toán học để chứng minh chip luôn tuân thủ một quy tắc nào đó trong điều kiện quy định. Ví dụ, hai mạch vốn không thể bật đồng thời, tuyệt đối không được cùng bật do một thao tác đặc biệt nào đó.

Phương pháp này đã tồn tại từ lâu, nhưng chứng minh toán học cho chip phức tạp rất khó khăn. Nhiều vấn đề cần chuyên gia xử lý thủ công, các công cụ hiện có cũng có thể không đưa ra kết luận do quy mô tính toán quá lớn.

Theo báo cáo của Leiphone, Trương Cự Kiến, cựu trưởng bộ phận xác minh hình thức của Axiom Math, cùng Lưu Tuấn Kỷ, người từng nghiên cứu toán học AI tại Moonshot AI, đã thành lập Công ty TNHH Công nghệ Hữu Lý Số Bắc Kinh, sử dụng AI để tự động hoàn thành nhiều công việc chứng minh hình thức chip hơn. Công ty đã hoàn thành vòng gọi vốn hạt giống.

Cả hai đều có nền tảng chứng minh toán học mạnh mẽ. Trương Cự Kiến đã tham gia phát triển Mathlib và AxiomProver. Lưu Tuấn Kỷ là tác giả cốt lõi của Numina-Lean-Agent, hệ thống này đã chứng minh thành công toàn bộ 12 bài toán của Kỳ thi Toán Putnam 2025, và xác minh quá trình chứng minh thông qua công cụ Lean.

Hiện tại, Hữu Lý Số đã chạy thông qua nguyên mẫu kỹ thuật, trong dự án chip liên quan đến hàng trăm nghìn dòng mã RTL, đã xác minh một số khẳng định mà công cụ EDA hiện có không thể phán định. Nhóm đang hợp tác với khách hàng chip, cố gắng biến năng lực này thành dịch vụ xác minh thương mại hóa.