Kết hợp Type Theory và Neural Networks: Chìa khóa cho tương lai của sinh mã AI

Các mạng nơ-ron ngày càng được sử dụng để tạo ra mã nguồn trong các ngôn ngữ lập trình cho phép tính tổng quát hóa cao và khả năng chứng minh tính đúng đắn (provably correct), điển hình là Idris, Lean và Agda. Tuy nhiên, hầu hết các mô hình tiên phong hiện nay — các Mô hình Ngôn ngữ Lớn (LLM) — lại tách biệt quá trình huấn luyện khỏi quá trình kiểm tra kiểu (typechecking).

Chúng được huấn luyện để tạo ra đầu ra có kiểu cố định là List Token (danh sách các token). Để có được mã hợp lệ, đầu ra này sau đó được phân tích cú pháp (parse) theo nhiều cách thủ công sau khi huấn luyện để phù hợp với kiểu của một ngôn ngữ cụ thể. Điều này đặt ra câu hỏi lớn: Liệu chúng ta có thể xây dựng lại LLM từ nền tảng để chúng được huấn luyện để tạo ra đầu có kiểu (typed output) ngay từ đầu không?

Những hạn chế của các phương pháp hiện tại

Hiện tại, có hai cách tiếp cận chính để xử lý vấn đề này, nhưng cả hai đều có những điểm yếu cố hữu.

Cách tiếp cận đầu tiên là vòng lặp thử lại (retry loops). Tương tự như cách một lập trình viên viết code và chạy compiler để kiểm tra lỗi, LLM sẽ tạo ra một ứng viên, trình kiểm tra kiểu sẽ xác thực nó. Nếu thất bại, thông báo lỗi được trả lại cho model để thử lại. Mặc dù cung cấp nhiều thông tin (băng thông cao), phương pháp này có độ chi tiết thấp (kiểm tra sau khi đã tạo xong) và cực kỳ lãng phí tài nguyên nếu lỗi xảy ra từ những token đầu tiên.

Cách tiếp cận thứ hai là giải mã bị giới hạn (constrained decoding). Ở đây, trình kiểm tra kiểu được consulted trước khi mỗi token được lấy mẫu (sample), và các token dẫn đến kết quả sai kiểu sẽ bị che (mask). Điều này đảm bảo đầu ra luôn đúng kiểu (độ chi tiết tối đa), nhưng lại có băng thông thấp. Vấn đề lớn là nó chỉ ngăn model nói những điều sai, nhưng không thay đổi những gì model muốn nói. Điều này có thể dẫn đến việc model bị ép vào các nhánh xác suất thấp, tạo ra kết quả đúng cú pháp nhưng vô nghĩa.

Đáng chú ý, cả hai phương pháp trên đều không cho phép gradient (đạo hàm) chảy qua quá trình kiểm tra kiểu, nghĩa là model không bao giờ thực sự học được cách sinh ra mã đúng kiểu thông qua việc cập nhật trọng số (weights).

Đề xuất mới: Khác biệt hóa theo cấu trúc

Bài viết đề xuất một hướng đi khác biệt: Thay vì cố định cấu trúc kiểu bên ngoài model, hãy để mạng nơ-ron học cấu trúc đó.

Trong lý thuyết toán học và lập trình hàm, việc tạo ra một giá trị thuộc kiểu A + B (tổng của hai kiểu, ví dụ Either) thường đòi hỏi một sự phân chia cố định của không gian đầu vào. Nếu model đoán sai nhánh ngay từ đầu, nó không thể sửa sai qua các lần cập nhật gradient.

Thay vào đó, tác giả đề xuất việc học cách phân chia này. Chúng ta không cần phân biệt qua các lựa chọn rời rạc, mà thu thập bằng chứng cho mỗi lựa chọn, chuẩn hóa chúng, sau đó mới lấy mẫu để quyết định. Cụ thể, model sẽ trở thành một ánh xạ từ đầu vào đến một phân phối xác suất trên cả lựa chọn kiểu và giá trị của nó.

Quá trình huấn luyện sau đó sẽ chỉ lan truyền gradient (backpropagate) qua nhánh đã được chọn. Điều này cho phép model học được xác suất đúng cho việc lựa chọn kiểu dữ liệu, đồng thời sinh ra nội dung chính xác bên trong kiểu đó.

Bài học từ AlphaZero và tương lai của sinh mã

Sự khác biệt giữa "khác biệt hóa qua cấu trúc" và "khác biệt hóa theo cấu trúc" tương tự như việc coi các lựa chọn ở mức kiểu là một giàn giáo cố định hay là thứ mà mạng có thể học được.

Cách tiếp cận này gợi nhớ đến thành công của AlphaZero trong cờ vua. Thay vì chỉ học các nước đi từ dữ liệu phẳng như GPT-4, AlphaZero đã mã hóa các luật chơi vào quá trình huấn luyện, đạt được hiệu suất siêu phàm với ít tham số hơn nhiều.

Tương tự, việc mã hóa chính ngôn ngữ lập trình vào quá trình huấn luyện sẽ mang lại bước nhảy vọt mà không một kỹ thuật tìm kiếm tại thời điểm suy luận (inference-time search) nào có thể sánh kịp. Token không còn là các ký tự vô nghĩa, mà được gắn liền với ý nghĩa của lĩnh vực chúng ta đang sinh ra.

Kết luận là: Việc kết hợp chặt chẽ lý thuyết kiểu (Type Theory) với mạng nơ-ron không chỉ giúp tạo ra mã chính xác hơn, mà còn mở đường cho việc xây dựng các hệ thống AI thực sự hiểu được cấu trúc của lập trình.