# Mô hình năng lượng (EBM) và tư duy logic không dùng ngôn ngữ

> Phân tích toán học và kiến trúc mô hình năng lượng thay thế LLM tự hồi quy trong suy luận logic, tối ưu hóa liên tục và kiểm chứng hình thức Lean 4.

Nguồn: https://camnangai.com/ky-thuat/mo-hinh-nang-luong-ebm-la-gi  
Xuất bản: 2026-10-17

Nếu bạn từng cố gắng ép một mô hình ngôn ngữ tự hồi quy (Autoregressive LLM) giải bài toán Sudoku, lập lịch sản xuất nhà máy hay kiểm chứng mã nguồn điều khiển thiết bị y tế, bạn sẽ nhận ra một sự thật phũ phàng: việc bắt hệ thống "tư duy" bằng cách nhả từng token văn bản rời rạc theo xác suất `P(y_t | y_0, ..., y_{t-1}, x)` là một sai lầm về mặt kiến trúc. LLM không thực sự tư duy logic; chúng chỉ đang dự đoán ký tự tiếp theo dựa trên sự tương quan chuỗi. Khi gặp các hệ ràng buộc cứng, chỉ cần một lựa chọn token sai lệch ở thời điểm ban đầu, toàn bộ chuỗi suy luận sau đó sẽ sụp đổ dây chuyền mà không có cách nào tự sửa lỗi mượt mà.

Suy luận logic bản chất không phải là một chuỗi câu từ tuyến tính. Đó là quá trình tối ưu hóa liên tục trên một bề mặt ràng buộc toán học khắt khe. Để giải quyết triệt để bế tắc này, giới kỹ thuật hệ thống đang quay trở lại với nền tảng của **mô hình năng lượng** (Energy-Based Model - EBM), định nghĩa một hàm vô hướng đo đạc độ tương thích giữa bài toán và câu trả lời thay vì gán xác suất cho từng từ ngữ.


  Bằng cách dịch chuyển quy trình tư duy sang không gian biểu diễn liên tục và kiểm chứng qua [Lean
  4](https://lean-lang.org/), hệ thống giải quyết các ràng buộc phức tạp với độ chính xác tuyệt đối
  mà không cần chuỗi suy luận CoT vô ích.


![Minh họa mô hình năng lượng EBM và cảnh quan tối ưu hóa liên tục](https://camnangai.com/articles/mo-hinh-nang-luong-ebm-la-gi/01-infographic-vn.webp)

## Vì sao mô hình ngôn ngữ tự hồi quy thất bại trước bài toán ràng buộc

![So sánh điểm nghẽn chuỗi token rời rạc của LLM với cơ chế đánh giá toàn cục của EBM](https://camnangai.com/articles/mo-hinh-nang-luong-ebm-la-gi/02-vn.webp)

Để hiểu tại sao mô hình ngôn ngữ tự hồi quy bế tắc trước logic phức tạp, bạn cần nhìn vào công thức nền tảng của chúng:

```text
P(y | x) = ∏ P(y_t | y_0, ..., y_{t-1}, x)
```

Mô hình chọn token `y_t` dựa trên phân bố xác suất điều kiện được huấn luyện từ tập dữ liệu văn bản. Cơ chế này hoạt động rất tốt đối với văn bản tự do, nơi ranh giới đúng/sai mang tính tương đối. Tuy nhiên, trong các bài toán thỏa mãn ràng buộc (Constraint Satisfaction Problems - CSP), chỉ một biến sai lệch sẽ vô hiệu hóa toàn bộ nghiệm.

Khi bạn ép LLM sinh token theo cách tham lam (greedy search) hoặc lấy mẫu xác suất, nó phải đối mặt với hiện tượng lệch phân bố tích tụ (exposure bias). Nếu ở bước `t = 3`, mô hình chọn một token sai, ngữ cảnh tiếp theo bị nhiễm độc. Trong không gian token rời rạc (discrete token space), việc quay lui (backtracking) đòi hỏi các thuật toán tìm kiếm trên cây như Beam Search hay Monte Carlo Tree Search (MCTS) với chi phí tính toán bùng nổ theo lũy thừa `O(b^d)`, trong đó `b` là độ rộng chùm và `d` là chiều sâu suy luận. Bạn sẽ thấy mô hình bị sa lầy vào các nhánh cây sai lầm mà không cách nào trượt mượt mà về vùng nghiệm đúng.

Hiện tượng này xuất hiện liên tục trong thực tế:

- **Bài toán Sudoku & Lập lịch công nghiệp:** Một bảng Sudoku 9x9 hay một hệ thống lập lịch máy móc nhà máy đòi hỏi thỏa mãn đồng thời hàng trăm ràng buộc bất đẳng thức và tính duy nhất. LLM thường vi phạm ràng buộc ở các ô cuối cùng vì không thể nhìn thấy bức tranh tổng thể liên tục.
- **Quy hoạch hành động Robot (Robot Motion Planning):** Robot di chuyển trong không gian thực cần tránh vật cản và tối ưu động năng. Chuỗi token "đi trái", "đi thẳng" không thể biểu diễn mịn các tham số vận tốc, gia tốc và vị trí liên tục.
- **Xác thực mã nguồn và an ninh phần mềm:** Lỗi bộ nhớ hay lỗ hổng phân quyền yêu cầu kiểm chứng chính xác đến từng bit logic. Một token sai lệch trong điều kiện rẽ nhánh sẽ biến một thuật toán an toàn thành một lỗ hổng nghiêm trọng.

Nhiều đội ngũ kỹ thuật cố gắng giải quyết bằng cách dùng kỹ thuật chuỗi suy luận (Chain-of-Thought - CoT), bắt LLM "hãy suy nghĩ từng bước". Hãy nhìn dưới góc độ chi phí tính toán: bạn đang bắt một mạng nơ-ron hàng trăm tỷ tham số thực hiện hàng chục ngàn phép nhân ma trận đắt đỏ chỉ để nhả ra các câu văn giải thích từng bước trung gian. Đây là một sự lãng phí tài nguyên máy tính vô lý để giải một bài toán mà đáng lẽ ra có thể được quy về một hệ phương trình tối ưu hóa liên tục. Chuỗi CoT càng dài, xác suất xuất hiện một token ảo giác ở giữa chuỗi càng tiến gần đến 100%.

## Mô hình năng lượng EBM: Bản chất toán học và cảnh quan năng lượng

![Cấu trúc cảnh quan năng lượng: thung lũng năng lượng cho đáp án đúng và vùng năng lượng cao cho vi phạm](https://camnangai.com/articles/mo-hinh-nang-luong-ebm-la-gi/03-vn.webp)

**Mô hình năng lượng** tiếp cận bài toán theo một triết lý hoàn toàn khác. Thay vì gán một phân bố xác suất chuẩn hóa cho đầu ra, EBM thiết lập một hàm năng lượng vô hướng `E(W, Y, X) ∈ ℝ`, trong đó `X` là biến quan sát (đầu vào), `Y` là biến dự đoán (đầu ra), và `W` là tập tham số mạng.

Giá trị năng lượng đo đạc độ "không tương thích" (uncompatibility) giữa `X` và `Y`:

- Cấu hình `Y` thỏa mãn tốt các ràng buộc của `X` dẫn tới `E(W, Y, X)` có giá trị rất thấp.
- Cấu hình `Y` vi phạm ràng buộc hoặc không hợp lý với `X` dẫn tới `E(W, Y, X)` có giá trị rất cao.

Sự khác biệt mang tính cách mạng giữa EBM và các mô hình xác suất chuẩn hóa nằm ở mẫu số chuẩn hóa. Trong mô hình xác suất chuẩn, bạn bắt buộc phải tính phân bố Gibbs:

```text
P(Y|X) = exp(-β · E(W, Y, X)) / Z(X)

với hàm phân hoạch (Partition Function):
Z(X) = ∫ exp(-β · E(W, y, X)) dy
```

Ở đây, `Z(X)` được gọi là hàm phân hoạch (Partition Function), còn `β` là hằng số nhiệt độ nghịch đảo. Khi không gian đầu ra `Y` là không gian liên tục nhiều chiều (`ℝ^d`) hoặc không gian rời rạc tổ hợp khổng lồ, việc tính tích phân hay lấy tổng `Z(X)` trên toàn bộ không gian là bất khả thi (NP-hard). Phép tính xấp xỉ bằng lấy mẫu MCMC (Markov Chain Monte Carlo) hay MCMC chạy trong chuỗi dài cực kỳ tốn kém và dễ bị mắc kẹt tại các vùng phân bố hẹp.

EBM loại bỏ hoàn toàn yêu cầu tính `Z(X)`. Nhờ không cần chuẩn hóa về tổng bằng 1, bạn có quyền tự do thiết kế kiến trúc mạng nơ-ron `E(W, Y, X)` một cách tùy ý mà không bị gò bó bởi các điều kiện tích phân.

Mục tiêu của quá trình huấn luyện EBM là kiến tạo nên một cảnh quan năng lượng (energy landscape). Bạn cần điều chỉnh `W` sao cho điểm dữ liệu đúng `Y_i` bị "ấn xuống" (push down) đáy thung lũng năng lượng, trong khi các điểm dữ liệu sai `Y ≠ Y_i` bị "kéo lên" (pull up).

Dưới đây là so sánh giữa các dạng hàm mất mát (loss function) phổ biến trong huấn luyện EBM:

- **Energy Loss:** `L = E(W, Y_i, X_i)`. Dạng này chỉ kéo năng lượng của đáp án đúng xuống mà không đẩy đáp án sai lên, dễ dẫn đến hiện tượng "sụp đổ năng lượng" (collapse solution) khi mô hình học cách gán `E(W, Y, X) = 0` cho mọi điểm.
- **Hinge Loss:** `L = max(0, m + E(W, Y_i, X_i) - E(W, Y_bar_i, X_i))`, tạo ra một khoảng lề `m` giữa đáp án đúng `Y_i` và đáp án sai nhất `Y_bar_i`.
- **Negative Log-Likelihood (NLL) Loss:** Kéo `Y_i` xuống và kéo tất cả `Y` khác lên thông qua tích phân Free Energy: `F_β(X) = -(1/β) · log ∫ exp(-β · E(y, X)) dy`.
- **Square-Square Loss (L_sq-sq):** Khống chế tuyệt đối năng lượng bằng cách ghim điểm đúng về 0 và đẩy điểm sai vượt qua khoảng lề `m`.

Đoạn mã PyTorch dưới đây minh họa cách cài đặt Square-Square Loss để huấn luyện cảnh quan năng lượng:

```python
import torch
import torch.nn as nn

class SquareSquareLoss(nn.Module):
    def __init__(self, margin: float = 1.0):
        super(SquareSquareLoss, self).__init__()
        self.margin = margin

    def forward(self, energy_correct: torch.Tensor, energy_incorrect: torch.Tensor) -> torch.Tensor:
        """
        energy_correct: E(W, Y_i, X_i) - Năng lượng của đáp án đúng (cần ép về 0)
        energy_incorrect: E(W, Y_bar_i, X_i) - Năng lượng của đáp án sai nhất (cần đẩy vượt lề m)
        """
        loss_pos = torch.pow(energy_correct, 2)
        margin_violation = torch.clamp(self.margin - energy_incorrect, min=0.0)
        loss_neg = torch.pow(margin_violation, 2)
        return torch.mean(loss_pos + loss_neg)
```

## Cơ chế suy luận EBM: Hạ dốc gradient trong không gian liên tục

Khi bạn thực hiện suy luận (inference) trên một **mô hình năng lượng**, bạn không đi tìm token tiếp theo. Bạn đang giải một bài toán tối ưu hóa tìm điểm cực tiểu trên bề mặt năng lượng liên tục:

```text
Y* = argmin_{Y ∈ 𝒴} E(W, Y, X)
```

Nếu `Y` là biến liên tục (chẳng hạn như vị trí tọa độ, vectơ đặc trưng ẩn, hay tham số điều khiển), bạn có thể bắt đầu từ một điểm `Y_0` ngẫu nhiên và cho mô hình "trượt" dần xuống thung lũng năng lượng bằng thuật toán hạ dốc gradient (Gradient Descent). Tại mỗi bước thời gian `t`, trạng thái được cập nhật:

```text
Y_{t+1} = Y_t - η · ∇_Y E(W, Y_t, X)
```

Tuy nhiên, nếu bề mặt năng lượng có nhiều điểm cực tiểu cục bộ (local minima), thuật toán hạ dốc gradient thuần túy có thể bị kẹt tại một đáp án sai. Để khắc phục, chúng ta áp dụng **động lực học Langevin (Langevin Dynamics)** — phương pháp chèn thêm nhiễu Gauss ngẫu nhiên vào quy trình trượt dốc:

```text
Y_{t+1} = Y_t - η · ∇_Y E(W, Y_t, X) + √(2η / β) · ε_t    (với ε_t ~ 𝒩(0, I))
```

Thành phần nhiễu `√(2η / β) · ε_t` đóng vai trò như động năng nhiệt. Nhờ có nhiễu này, vectơ trạng thái `Y` có khả năng "nhảy" thoát khỏi các bẫy cực tiểu cục bộ cạn để rơi vào điểm cực tiểu toàn cục (global minimum) có năng lượng thấp nhất.

```
          CẢNH QUAN NĂNG LƯỢNG VÀ ĐỘNG LỰC HỌC LANGEVIN
   Năng lượng E
        ^
        |      \                                  /
  Lớn   |       \   Trạng thái ban đầu Y_0       /
        |        \        o                     /
        |         \        \  <- Hạ dốc        /
        |          \        v    Gradient     /
        |           \------> o               /
        |           | Cực tiểu|  \          /
        |           | cục bộ  |   v Langevin/ (vượt rào cản nhờ nhiễu)
  Nhỏ   |           \________/     \_______/
        |                          |  Y*  |  <-- Điểm cực tiểu toàn cục
        +---------------------------------------------------------> Không gian trạng thái Y
```

So sánh chi phí tính toán giữa hai phương pháp:

- **Suy luận rời rạc trên LLM:** Bạn phải duy trì ma trận KV-cache khổng lồ, chạy qua hàng trăm tầng Transformer rời rạc chỉ để sinh từng token. Khi phát hiện vi phạm ràng buộc ở token thứ 50, bạn phải hủy bỏ toàn bộ và quay lui trên cây tìm kiếm rời rạc.
- **Suy luận liên tục trên EBM:** Mạng nơ-ron `E(W, Y, X)` được thiết kế rất gọn nhẹ. Gradient `∇_Y E(W, Y, X)` được tính toán cực nhanh thông qua lan truyền ngược (backpropagation) theo biến đầu ra `Y` (chứ không phải theo tham số `W`). Vectơ `Y` liên tục điều chỉnh mịn màng mọi chiều cùng một lúc. Bạn dịch chuyển toàn bộ giải pháp về trạng thái tối ưu chỉ sau 20-50 bước lặp gradient mà không tốn tài nguyên cho chuỗi token văn bản.

## Suy luận trong không gian ẩn: Tư duy logic không cần token ngôn ngữ

![Kiến trúc H-JEPA thực hiện suy luận liên tục trong không gian biểu diễn ẩn thông qua biến ẩn Z](https://camnangai.com/articles/mo-hinh-nang-luong-ebm-la-gi/04-vn.webp)

Một rào cản lớn khi xử lý các bài toán thế giới thực là sự tồn tại của các thông tin ẩn không thể quan sát trực tiếp. Để giải quyết điều này, dòng Mô hình Năng lượng Biến ẩn (Latent Variable EBMs) và Kiến trúc Dự đoán Nhúng chung Phân cấp (Hierarchical Joint Embedding Predictive Architecture - H-JEPA) đưa ra lời giải kiến trúc đột phá.

Trong mô hình này, hàm năng lượng tích hợp thêm biến ẩn `Z ∈ 𝒵`:

```text
E(Y, X) = min_{Z ∈ 𝒵} E(Z, Y, X)
```

Biến ẩn `Z` đại diện cho các bước tư duy trung gian, các biến kế hoạch chưa biết hoặc các giả định logic cần thiết để nối liền từ quan sát `X` đến kết quả `Y`. Quá trình tư duy thực chất là việc tối ưu hóa đồng thời cả `Y` và `Z` trên bề mặt năng lượng liên tục.

Khái niệm "tư duy không token" (token-free reasoning) đạt đến mức hoàn thiện ở kiến trúc H-JEPA: mô hình thực hiện mọi dự đoán và suy luận trực tiếp trong **không gian biểu diễn ẩn (representation space)**, thay vì không gian điểm ảnh (pixel space) hay không gian từ ngữ (token space). Khi bạn loại bỏ việc sinh token, bạn loại bỏ luôn việc phải dự đoán các chi tiết bề mặt không liên quan, chỉ tập trung giữ lại các đặc trưng logic mang tính bản chất.

Tuy nhiên, thách thức lớn nhất của các kiến trúc nhúng chung (Joint-Embedding) là **sụp đổ biểu diễn (representation collapse)**. Đây là trạng thái lỗi khi mạng nơ-ron học cách gán mọi đầu vào `X` và `Y` về cùng một vectơ hằng số, làm cho năng lượng `E(Z, Y, X) = 0` ở mọi nơi.

Để ngăn chặn sụp đổ biểu diễn mà không cần dùng đến các mẫu âm (negative samples) tốn kém, các kiến trúc hiện đại áp dụng các thành phần điều hòa cứng như VICReg (Variance-Covariance-Invariance):

1. **Ràng buộc Biến thiên (Variance Constraint):** Bắt độ lệch chuẩn của các chiều trong vectơ biểu diễn phải lớn hơn một ngưỡng cố định, ngăn các chiều bị teo về 0.
2. **Ràng buộc Hiệp biến thiên (Covariance Constraint):** Ép hiệp biến giữa các cặp chiều biểu diễn về 0, đảm bảo mỗi chiều thông tin chứa thông tin độc lập, tránh dư thừa.
3. **Ràng buộc Bất biến (Invariance Constraint):** Giữ khoảng cách giữa biểu diễn của các biến thể cùng ngữ cảnh trong phạm vi tối ưu.

Thử nghiệm thực nghiệm chứng minh rõ sức mạnh của tư duy trong không gian ẩn:

- **Kiểm chứng biểu diễn (Probing):** Đạt độ chính xác **91%** khi đánh giá tuyến tính trên tập dữ liệu benchmark mà không cần tinh chỉnh sâu.
- **Dự đoán chuỗi thời gian:** Thực hiện thành công dự đoán đa bước (multi-step prediction) trên tập dữ liệu chuỗi, nắm bắt mượt mà động lực học thời gian mà không bị suy hao chất lượng như các mô hình sinh điểm ảnh.
- **Lập kế hoạch hành động:** Đạt tỷ lệ thành công **97%** trong các bài toán điều hướng không gian phức tạp (Robot tìm đường qua các phòng có cửa hẹp), thể hiện khả năng lập kế hoạch conditioning theo hành động chuẩn xác trong không gian ẩn.

## Kiểm chứng hình thức và Lean 4: Bảo đảm tính đúng đắn tuyệt đối

![Quy trình kiểm chứng hình thức tuyệt đối của Lean 4 dựa trên nhân kiểm chứng tối thiểu](https://camnangai.com/articles/mo-hinh-nang-luong-ebm-la-gi/05-vn.webp)

Mặc dù EBM giúp bạn tìm nghiệm tối ưu mượt mà trong không gian liên tục, đối với các hệ thống an toàn cốt lõi (critical systems), chúng ta vẫn cần một cơ chế bảo chứng tính đúng đắn tuyệt đối về mặt logic rời rạc. Đây là lúc ngôn ngữ lập trình và trợ lý chứng minh hình thức **Lean 4** thể hiện vai trò quyết định.

Lean 4 vận hành dựa trên Lý thuyết Kiểu phụ thuộc (Dependent Type Theory) và Đẳng cấu Curry-Howard — nguyên lý toán học khẳng định một chứng minh toán học chính là một chương trình máy tính, và một mệnh đề logic chính là một kiểu dữ liệu. Trọng tâm của Lean 4 là một **nhân kiểm chứng tối thiểu (minimal trusted kernel)**. Nhân này chỉ gồm một đoạn mã nguồn nhỏ được kiểm tra nghiêm ngặt, chịu trách nhiệm xác minh tính hợp lệ của toàn bộ cây chứng minh. Nếu nhân Lean 4 xác nhận một chứng minh là đúng, nó đảm bảo tính đúng đắn toán học tuyệt đối 100%, loại bỏ hoàn toàn khả năng xảy ra ảo giác.

Trong các kiến trúc suy luận thế hệ mới, mô hình AI/EBM và Lean 4 phối hợp theo một vòng lặp khép kín:

- **Mô hình EBM / Latent AI (Reasoning Engine):** Đóng vai trò là "máy đề xuất". Mạng nơ-ron trượt trên cảnh quan năng lượng để đề xuất các cấu trúc chứng minh, các bước biến đổi đại số, hoặc các đường đi tiềm năng trong không gian ẩn.
- **Môi trường Lean 4 (Validation Layer):** Đóng vai trò là "lớp kiểm chứng". Mỗi bước do AI đề xuất lập tức được đưa qua nhân của Lean 4. Nếu Lean 4 chấp nhận, bước đi được xác nhận. Nếu Lean 4 báo lỗi, phản hồi lỗi (error trace) được chuyển hóa thành một khoản phạt năng lượng cực lớn (energy penalty) dội ngược lại, ép EBM phải điều hướng dốc gradient sang nhánh logic khác.

```
+-----------------------------------+        Đề xuất bước chứng minh /        +-----------------------------------+
|    Mô hình EBM / Latent AI        |  ---- Đường đi trong không gian ẩn ---> |  Trợ lý chứng minh Lean 4         |
|   (Reasoning & Search Engine)     |                                         |  (Kernel kiểm chứng tối thiểu)    |
+-----------------------------------+  <--- Phạt năng lượng khi vi phạm ----- +-----------------------------------+
                                            (Phản hồi lỗi logic từ Kernel)
```

Kiến trúc kiểm chứng hình thức kết hợp Lean 4 đang được triển khai mạnh mẽ trong các dự án quy mô công nghiệp:

- **AWS Cedar:** Amazon Web Services sử dụng Lean 4 để hình thức hóa và kiểm chứng ngôn ngữ phân quyền Cedar. Toàn bộ chính sách truy cập tài nguyên đám mây được xác minh tính an toàn tuyệt đối trước khi chạy thực tế, loại bỏ nguy cơ rò rỉ dữ liệu do lỗi logic phân quyền.
- **Aeneas:** Công cụ chuyển đổi mã nguồn Rust sang mô hình toán học trong Lean 4. Bằng cách tận dụng hệ thống kiểu khắt khe của Rust, Aeneas loại bỏ hoàn toàn gánh nặng lý luận bộ nhớ phức tạp, giúp kiểm chứng mã nguồn phần mềm với tốc độ vượt trội.
- **ArkLib:** Dự án dùng Lean 4 để kiểm chứng hình thức các hệ thống chứng minh không tiết lộ thông tin (SNARKs/zk-proofs), đảm bảo các hợp đồng thông minh tài chính không tồn tại lỗ hổng toán học.
- **Toán học đỉnh cao:** Lean 4 đã kiểm chứng thành công các dự án hình thức hóa phương trình Navier-Stokes và bài toán khoảng cách đơn vị Erdos.

Sức mạnh thực thi của Lean 4 còn nằm ở tactic `grind` — công cụ tự động hóa mạnh mẽ tích hợp sẵn, giúp tự động giải quyết các hệ bất phương trình tuyến tính, phân tích trường hợp và khớp mẫu tổ hợp phức tạp:

```lean
-- Minh họa tactic grind trong Lean 4 tự động kiểm chứng hệ bất phương trình tuyến tính
example (x y : Int) : 27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45 → -10 ≤ 7*x - 9*y → 7*x - 9*y > 4 := by grind
```

## Phân chia kiến trúc: EBM làm tư duy suy luận, LLM làm giao diện giao tiếp

Thực tế công nghiệp cho thấy bạn không nên bỏ rơi hoàn toàn LLM, mà cần đặt nó vào đúng vị trí trong một hệ thống lai (Hybrid Architecture) hoàn chỉnh.

Sự phân tách kiến trúc tối ưu nhất hiện nay được chia làm ba lớp chuyên biệt:

```
                  +---------------------------------------------------+
                  |                   NGƯỜI DÙNG                      |
                  +---------------------------------------------------+
                                    ^               |
            Văn bản tự nhiên        |               | Yêu cầu bằng
            đã được kiểm chứng      |               | ngôn ngữ tự nhiên
                                    |               v
                  +---------------------------------------------------+
                  |              MÔ HÌNH NGÔN NGỮ (LLM)               |
                  |             (Interface Engine - LLM)              |
                  +---------------------------------------------------+
                                    ^               |
               Kết quả đã           |               | Dịch thành tham số/
               kiểm chứng           |               | ma trận ràng buộc DSL
                                    |               v
                  +---------------------------------------------------+
                  |            MÔ HÌNH NĂNG LƯỢNG (EBM)               |
                  |           (Reasoning Engine - EBM)                |
                  +---------------------------------------------------+
                                    ^               |
             Xác thực               |               | Đề xuất cấu trúc/
             tính đúng đắn          |               | Lời giải hình thức
                                    |               v
                  +---------------------------------------------------+
                  |              MÔ TRƯỜNG LEAN 4                     |
                  |              (Validation Layer)                   |
                  +---------------------------------------------------+
```

Vai trò của từng thành phần trong luồng vận hành:

1. **LLM - Giao diện ngôn ngữ (Interface Engine):** Chịu trách nhiệm giao tiếp với con người. LLM tiếp nhận yêu cầu bằng ngôn ngữ tự nhiên, trích xuất ý định và biên dịch chúng thành một DSL (Domain-Specific Language) cấu trúc hoặc một ma trận ràng buộc toán học rõ ràng (JSON Schema/Constraint Matrix).
2. **EBM - Bộ não suy luận (Reasoning Engine):** Nhận ma trận ràng buộc từ LLM. EBM thực hiện hạ dốc gradient Langevin trong không gian ẩn liên tục, tối ưu hóa cảnh quan năng lượng để tìm ra nghiệm hoặc kế hoạch hành động thỏa mãn 100% các điều kiện mà không tốn một token văn bản nào.
3. **Lean 4 - Lớp xác thực hình thức (Validation Layer):** Nhận đề xuất giải pháp từ EBM, chạy qua nhân kiểm chứng tối thiểu để xác nhận tính đúng đắn logic. Kết quả đã xác minh được gửi ngược lại cho LLM để dịch thành câu trả lời văn bản tự nhiên mượt mà cho người dùng.

Lợi ích kỹ thuật của sự phân tách này:

- **Giảm thiểu tối đa chi phí tính toán:** Bạn loại bỏ được 90% số lượng token CoT không cần thiết. LLM chỉ chạy ở bước dịch thuật đầu-cuối.
- **Triệt tiêu hoàn toàn vi phạm ràng buộc:** EBM đảm bảo giải pháp luôn nằm ở điểm cực tiểu năng lượng. Nếu không tìm được nghiệm thỏa mãn, hệ thống sẽ báo không thể giải thay vì sinh ra một nghiệm giả tạo.
- **An toàn tuyệt đối cho hệ thống cốt lõi:** Mọi đầu ra trước khi thực thi trên phần cứng đều đã đi qua nhân Lean 4, đảm bảo an toàn tính mạng và tài sản trong các ứng dụng hàng không, y tế và hạ tầng tài chính.

## Khi nào bài toán kỹ thuật của bạn cần mô hình năng lượng thay vì LLM

Là một kỹ sư trưởng hệ thống, bạn cần quyết định công nghệ dựa trên bản chất toán học của bài toán thay vì chạy theo xu hướng tiếp thị.

Tiếp tục sử dụng **mô hình ngôn ngữ (LLM)** khi:

- Tác vụ mang tính sáng tạo văn bản, tóm tắt tài liệu, viết email, hoặc dịch thuật ngôn ngữ tự nhiên.
- Bài toán không có một nghiệm đúng/sai tuyệt đối, chấp nhận được sự linh hoạt và tính ngẫu nhiên của xác suất `P(y_t | y_0, ..., y_{t-1}, x)`.

Chuyển sang **mô hình năng lượng (EBM)** hoặc kiến trúc suy luận không gian ẩn khi:

- Bài toán đòi hỏi tuân thủ **100% ràng buộc cứng (hard constraints)** như lập lịch nhà máy, quy hoạch đường đi robot, tối ưu hóa danh mục đầu tư hoặc xác thực mã nguồn.
- Không gian giải pháp mang tính **mượt mà liên tục (continuous space)** hoặc có chiều dữ liệu cực lớn, nơi phép tìm kiếm rời rạc bị bùng nổ chi phí lũy thừa.
- Hệ thống không chấp nhận bất kỳ sai số tích tụ nào trong quy trình suy luận đa bước.
- Đầu ra của AI bắt buộc phải có **chứng minh hình thức (formal proof)** được kiểm chứng qua nhân Lean 4 trước khi can thiệp vào các hệ thống vận hành thực tế.

## Tài liệu tham khảo

- [A Tutorial on Energy-Based Learning — Yann LeCun et al.](http://yann.lecun.com/exdb/publis/pdf/lecun-06.pdf)
- [How to Build Models Without Language, with Logical Intelligence — ByteByteGo](https://blog.bytebytego.com/p/how-to-build-models-without-language)
- [Introduction to Latent Variable Energy-Based Models: A Path Towards Autonomous Machine Intelligence — Dawid & LeCun (arXiv:2306.02572)](https://arxiv.org/abs/2306.02572)
- [A Lightweight Library for Energy-Based Joint-Embedding Predictive Architectures — Terver, LeCun et al. (arXiv:2602.03604)](https://arxiv.org/abs/2602.03604)
- [Logical Intelligence · AI Certainty for Critical Systems — Logical Intelligence](https://logicalintelligence.com/)
- [The Lean 4 Programming Language and Theorem Prover — Lean Community](https://lean-lang.org/)