Startup Pramaana Labs huy động 27 triệu USD, áp dụng xác minh toán học vào AI để tăng độ tin cậy

Khi các doanh nghiệp đang gặp khó khăn trong việc chuyển đổi các chương trình thí điểm AI thành bộ phận vận hành cốt lõi của kinh doanh, vấn đề độ tin cậy đang trở thành tâm điểm chú ý. Một startup mới đây hy vọng sẽ giải quyết bài toán này bằng cách sử dụng các công cụ toán học chính thức, kết hợp một trong những hệ thống đáng tin cậy nhất của khoa học máy tính với một trong những hệ thống hỗn loạn nhất.

Vào thứ Tư vừa qua, Pramaana Labs đã công bố vòng gọi vốn hạt giống (seed round) trị giá 27 triệu USD do Khosla Ventures dẫn đầu, với sự tham gia của các quỹ đầu tư lớn như Accel, Boldcap, Nexus Venture Partners, Premji Invest và Unbound.

Pramaana sẽ tập trung vào các lĩnh vực nhạy cảm cao như pháp lý, phát hiện thuốc và chuẩn bị thuế — nơi sai sót có thể gây tốn kém và độ tin cậy được đặt lên hàng đầu. Việc triển khai AI trong các hệ thống này sẽ yêu cầu các biện pháp bảo vệ mạnh mẽ hơn chống lại các "ảo giác" (hallucinations) và lỗi so với những gì chúng ta hiện có. Tuy nhiên, theo quan điểm của Ranjan Rajagopalan, đồng sáng lập và CEO của Pramaana, các lĩnh vực này cũng rất phù hợp để áp dụng tính chính thức hóa.

"Nó giống như toán học theo nghĩa là bạn có rất nhiều quy tắc cần tuân thủ," ông Rajagopalan chia sẻ với TechCrunch khi mô tả các quy tắc của luật thuế. "Khi bạn có phiên bản được mã hóa của nó, quá trình lý luận trên nền tảng đó bắt đầu trở nên xác định."

Hệ thống của Pramaana vẫn hoạt động dựa trên một Mô hình Ngôn ngữ Lớn (LLM) thông thường, mang lại sự linh hoạt để trả lời các câu hỏi bằng ngôn ngữ tự nhiên và giải quyết các vấn đề phức tạp mà máy tính truyền thống không thể xử lý. Tuy nhiên, điểm khác biệt là có một lớp xác định (deterministic layer) được đặt ở trên cùng LLM để đảm bảo kết quả làm việc của mô hình được kiểm chứng chính xác.

Sự kết hợp giữa động cơ LLM và xác minh xác định là một cấu hình phổ biến hiện nay; cách tiếp cận độc đáo của Pramaana nằm ở việc sử dụng các công cụ xác minh chính thức — dựa trên ngôn ngữ lập trình mã nguồn mở LEAN được dùng để xác minh các chứng minh toán học. Có rất nhiều tiền lệ cho công việc này; ông Rajagopalan chỉ ra dự án CATALA của Pháp, nơi đã chính thức hóa phần lớn hệ thống thuế và phúc lợi của quốc gia này thành mã thực thi.

Đối với từng trường hợp sử dụng, Pramaana sẽ xây dựng hệ thống xác minh chính thức kiểu LEAN của riêng mình, dưới sự giám sát của các chuyên gia trong lĩnh vực. Đối với luật thuế, công ty đang làm việc với cựu ủy viên IRS Danny Werfel, trong khi các giáo sư từ IIT Delhi, IIT Madras và UC Berkeley sẽ giám sát hệ thống an ninh mạng và phát hiện thuốc.

"Những vấn đề khó nhất thế giới không phải là không thể giải quyết. Chúng chỉ chưa được chính thức hóa," ông Rajagopalan khẳng định. "Mọi lĩnh vực mà việc sai lầm có thể khiến ai đó mất sức khỏe, tiền bạc hoặc tự do đều có những quy tắc riêng."

Bây giờ, những quy tắc đó cần được mã hóa hóa thành hiện thực.