Jane Street, một trong những công ty giao dịch định lượng lớn nhất thế giới, vừa gây bất ngờ khi tuyên bố thành lập đội ngũ chuyên về formal methods (phương pháp hình thức) sau 25 năm không mặn mà với công nghệ này. Lý do chính là sự trỗi dậy của agentic coding , tức mã do AI tự động sinh ra.

Tác động của AI tới chi phí và lợi ích

Trước đây, formal methods quá đắt đỏ: dự án seL4 (một microkernel được xác minh chính thức) mất 25 người-năm để xác minh chỉ vỏn vẹn 8.700 dòng C. Mỗi dòng code tương ứng 23 dòng chứng minh và nửa ngày công. Jane Street cho rằng mô hình AI, đặc biệt là các LLM, đã thay đổi hoàn toàn cục diện. Agent AI có thể hỗ trợ lập trình viên viết và xác minh code nhanh hơn, mở rộng đối tượng sử dụng công cụ formal methods vốn chỉ dành cho chuyên gia.

Lợi ích kép: chi phí giảm, giá trị tăng

Không chỉ giảm chi phí, lợi ích của formal methods cũng tăng lên. Khi AI tạo ra code ngày càng nhiều, chất lượng code lại có xu hướng "slop": phức tạp, lỗi vặt, không tuân thủ bất biến (invariants) của hệ thống. Formal methods giúp kiểm soát chất lượng đó, biến code do AI sinh ra thành sản phẩm có thể đưa vào sản xuất. Jane Street hy vọng biến formal methods thành công cụ phổ biến như type systems hiện nay.

Bước tiến cho ngành công nghệ và AI

Sự thay đổi của Jane Street phản ánh xu hướng lớn: các công ty tài chính và startup đang tận dụng AI để giải quyết bài toán chất lượng phần mềm. Nếu thành công, bước đi này có thể giúp giảm thiểu rủi ro trong các hệ thống giao dịch, ngân hàng, và cả ứng dụng hàng ngày mà người dùng phụ thuộc vào.