Phương pháp Chính thức và Tương lai của Lập trình: Khi AI thay đổi cuộc chơi

Phương pháp Chính thức và Tương lai của Lập trình: Khi AI thay đổi cuộc chơi

Trong suốt 25 năm qua, tôi luôn nói với mọi người rằng Jane Street, với tư cách là một tổ chức, thực sự không quan tâm đến các phương pháp chính thức (formal methods). Nhưng giờ đây, tôi không còn nói như vậy nữa.

Điều này không hẳn vì chúng tôi đã sai trong suốt những năm qua. Để rõ ràng, chúng tôi luôn tin tưởng vào sức mạnh của các công cụ giúp viết mã tốt hơn và đáng tin cậy hơn. Các hệ thống kiểu (type systems) chính là một dạng phương pháp chính thức "nhẹ" mà chúng tôi đã hưởng lợi rất nhiều từ đó. Vì vậy, có thể bạn sẽ nghĩ rằng chúng tôi là những người ủng hộ nhiệt thành cho các phương pháp chính thức đầy đủ hơn.

Tuy nhiên, ngoài một số trường hợp đặc biệt (đáng chú ý là tổng hợp phần cứng), chúng tôi từng cảm thấy các phương pháp chính thức không đáng với chi phí bỏ ra. Và chi phí đó thực sự rất cao! seL4 là một ví dụ điển hình. Đó là một vi hạt nhân được kiểm chứng chính thức, một thành tựu vĩ đại. Nhưng nó cực kỳ tốn kém! Nó đã mất 25 năm nhân lực để kiểm chứng 8.700 dòng mã C, và mỗi dòng mã yêu cầu khoảng 23 dòng chứng minh và nửa ngày công để xác minh.

OxCaml Prover

Loại tiếp cận này có thể đáng giá cho một vi hạt nhân quan trọng về mặt bảo mật, nơi rủi ro cao và thông số kỹ thuật khá rõ ràng. Nhưng nó không hợp lý với hầu hết các phần mềm, và đối với chúng tôi, nó dường như không hợp lý ngay cả với những phần mềm quan trọng nhất của mình.

Tuy nhiên, sự trỗi dậy của lập trình dựa trên tác nhân (agentic coding) đã thay đổi quan điểm của chúng tôi. Chúng tôi đã chuyển từ sự hoài nghi sang phấn khích trước những khả năng này. Kết quả là, chúng tôi hiện đang xây dựng một đội ngũ tập trung vào các phương pháp chính thức. Hy vọng của chúng tôi là biến các phương pháp chính thức trở thành công cụ hữu ích phổ biến để xây dựng phần mềm, giống như cách các hệ thống kiểu tinh vi đang phục vụ chúng tôi ngày nay.

Tại sao sự thay đổi này lại xảy ra?

Lập trình dựa trên tác nhân làm đảo lộn mọi tính toán cũ về các phương pháp chính thức theo một vài cách.

Đầu tiên, nó thay đổi đáng kể chi phí sử dụng các phương pháp chính thức. Không phải là các tác nhân có thể tự mình xây dựng các chứng minh đầy thách thức một cách tùy ý. Nhưng các mô hình AI vô cùng hữu ích và mở rộng tập hợp những người có thể sử dụng các công cụ này một cách hiệu quả. Khi các phương pháp chính thức trở nên dễ sử dụng hơn bao giờ hết, việc xem lại lại tính toán chi phí/lợi ích cũ là hoàn toàn xứng đáng.

Nhưng mọi thứ không chỉ thay đổi ở phía chi phí. Lợi ích dường như cũng lớn hơn hiện nay. Có hai lý do chính cho điều này:

Nút thắt kiểm chứng quan trọng hơn bao giờ hết. Các mô hình ngày càng giỏi trong việc viết mã hữu ích. Nhưng có một khoảng cách lớn giữa mã mà mô hình tạo ra và mã mà bạn thực sự muốn phát hành. Một mức độ nào đó, đây là đặc điểm của cách các mô hình được đào tạo. Chúng đáng ngạc nhiên tốt trong việc đạt được mục tiêu bạn đặt ra, nhưng chúng không làm tốt việc duy trì và thậm chí cải thiện chất lượng cơ sở mã trong quá trình đó. Mã do tác nhân tạo ra đang tốt hơn, nhưng vẫn có xu hướng trở nên lộn xộn: quá phức tạp, đầy những lỗi kỳ lạ và các trường hợp góc (corner cases), thường không tuân theo các bất biến quan trọng của cơ sở mã mà nó là một phần.

Kết quả là, mọi người cần dành nhiều thời gian để xác minh rằng mã do tác nhân tạo ra đạt chuẩn. Và các phương pháp chính thức có thể là một cách để giảm bớt gánh nặng kiểm chứng đó, làm cho quá trình xem xét hiệu quả hơn.

Ngoài ra, các tác nhân phát triển mạnh dựa trên phản hồi (feedback). Điều này đúng cả khi bạn đang đào tạo tác nhân bằng học tăng cường (RL), và khi bạn sử dụng tác nhân để viết mã. Các phương pháp chính thức là một dạng phản hồi mạnh mẽ khác có thể tăng khả năng của tác nhân trong việc giải quyết các vấn đề khó khăn.

Tại sao lại thực hiện điều này tại Jane Street?

Một câu hỏi được đặt ra là: Tại sao Jane Street lại có vị thế tốt để giải quyết vấn đề này? Cả thế giới đang suy nghĩ về việc các tác nhân có ý nghĩa gì đối với tương lai của lập trình, và có vô số startup tìm cách kết hợp các phương pháp chính thức và tác nhân. Tại sao đây là điều chúng tôi muốn thực hiện nội bộ? Và tại sao các chuyên gia về phương pháp chính thức bên ngoài nên hào hứng tham gia vào nỗ lực của chúng tôi?

Một mặt, chúng tôi có sự kiểm soát sâu sắc về ngôn ngữ mà chúng tôi đang sử dụng, và điều đó cho phép chúng tôi điều chỉnh ngôn ngữ đó để biến nó thành một môi trường tốt hơn cho các kỹ thuật định hướng chứng minh. Có rất nhiều hướng tiềm năng để đi ở đây: từ việc tích hợp các thông số kỹ thuật mô-đun của thuộc tính vào hệ thống kiểu, đến việc thêm các ràng buộc ở cấp độ kiểu xung quanh những thứ như quyền sở hữu và tính biến đổi để làm cho một số loại chứng minh dễ dàng hơn, đến việc xây dựng các kỹ thuật chứng minh trực tiếp vào ngôn ngữ.

Chúng tôi cũng có một cộng đồng các lập trình viên đã sẵn sàng cho điều này, hoặc ít nhất là sẵn sàng hơn bất kỳ cộng đồng lập trình nghiêm túc nào tôi từng gặp. Đối với hầu hết những người làm việc về ngôn ngữ lập trình, phần dễ dàng là đưa ra các ý tưởng mới và tốt hơn về cách làm cho lập trình tốt hơn. Phần khó khăn là thuyết phục bất kỳ ai thực sự sử dụng các ý tưởng đó cho công việc thực tế.

Tại Jane Street, mọi chuyện khác biệt! Chúng tôi thường xuyên có người dùng tức giận vì các tính năng hệ thống kiểu mới lạ mà chúng tôi hứa hẹn không đến đủ nhanh. Chúng tôi có nhiều người có nền tảng phù hợp để tận dụng các kỹ thuật này, và rất nhiều sự quan tâm sẵn có trong việc làm đúng và xây dựng phần mềm chất lượng cao.

Chúng tôi nghĩ rằng cơ sở người dùng này sẽ cho chúng tôi tự do thử nghiệm một hỗn hợp các cách tiếp cận; có một số cải thiện ngắn hạn mà chúng tôi nghĩ có thể thực hiện và sẽ có tác động gần như tức thì, và một số tầm nhìn tham vọng hơn, dài hạn cho những gì chúng tôi có thể đạt được trong vài năm tới. Có một cơ sở người dùng nhiệt tình và hào hứng làm cho cả hai cách tiếp cận này trở nên khả thi, và cho phép chúng tôi học hỏi từ cái đầu tiên, trong khi chúng tôi xây dựng hướng tới cái thứ hai.

Không phải là chúng tôi sẽ bỏ qua công việc của thế giới bên ngoài. Chúng tôi hào hứng và được truyền cảm hứng bởi công việc trong nhiều cộng đồng ngôn ngữ lập trình (PL) khác, được xây dựng xung quanh các công cụ như Lean, Dafny, Rocq, Agda, Iris và nhiều công cụ khác nữa. Và chúng tôi hào hứng tìm cách tích hợp OxCaml với một số công cụ này, để tận dụng cơ sở hạ tầng tuyệt vời đã có sẵn. Nhưng chúng tôi cũng nghĩ có một số lợi thế độc đáo chỉ có thể thực hiện được bằng cách tham gia vào ngôn ngữ và các kỹ thuật chứng minh cùng một lúc.

Nếu điều này nghe thấy thú vị với bạn, hãy cân nhắc ứng tuyển! Chúng tôi đang tìm kiếm người ở cả London và New York. Chúng tôi ở giai đoạn đầu phỏng vấn những người cho các vị trí này và xây dựng một đội ngũ, và có một khối lượng công việc khổng lồ phía trước, chúng tôi rất muốn bạn trở thành một phần của nó.