Entailment và Model Checking - Knowledge Base suy ra điều gì?

Ở bài trước, ta đã biết cách biểu diễn facts và rules thành Knowledge Base. Bây giờ ta cần phân biệt hai câu hỏi rất khác nhau:

Kết luận này có thể đúng không?
Kết luận này có bắt buộc đúng từ KB không?

AI suy luận logic quan tâm mạnh đến câu hỏi thứ hai.

Mục tiêu

Sau bài này, bạn cần:

hiểu entailment $KB \models \alpha$ ;
phân biệt entailment với implication $P \to Q$ ;
hiểu inference là quá trình sinh tri thức mới;
mô tả được Model Checking;
tự kiểm tra một ví dụ nhỏ bằng truth table;
hiểu vì sao brute-force Model Checking tăng theo khoảng $2^n$ model.

Entailment - hệ quả logic

Ký hiệu:

KB \models \alpha

Đọc là:

KB entails $\alpha$ .

Ý nghĩa chính xác:

Trong mọi model mà KB đúng, $\alpha$ cũng đúng.

Ví dụ:

P \land Q \models P

Nếu một thế giới thỏa P AND Q, thì chắc chắn P đúng.

Entailment khác Implication

Hai ký hiệu dễ nhầm:

P -> Q
P ⊨ Q

$\to$ là connective nằm bên trong một logical sentence.

$\models$ là quan hệ giữa hai sentence hoặc giữa KB và query.

Ví dụ:

P \land (P \to Q) \models Q

Bên trái là knowledge. Dấu $\models$ nói rằng knowledge đó bắt buộc dẫn tới $Q$ .

Inference - suy luận

Inference là quá trình sinh ra sentence mới từ các sentence đã biết.

Ví dụ:

Nếu nộp bài muộn thì bị trừ điểm.
An nộp bài muộn.
=> An bị trừ điểm.

Có nhiều cách thực hiện inference. CS50 AI giới thiệu hai hướng quan trọng:

Model Checking - kiểm tra mọi model;
Inference Rules / Resolution - biến đổi và suy ra trực tiếp bằng luật logic.

Model Checking - kiểm tra tất cả model

Câu hỏi cần trả lời:

KB \models \alpha\;?

Ý tưởng của Model Checking:

liệt kê mọi model có thể;
chỉ quan tâm những model làm cho KB đúng;
kiểm tra query $\alpha$ trong tất cả các model đó;
nếu $\alpha$ luôn đúng, kết luận $KB \models \alpha$ .

Ví dụ Model Checking từng bước

Đặt:

P: Có tiết AI.
Q: Có thông báo nghỉ.
R: Tôi tới trường.

Knowledge Base:

KB = P \land \neg Q \land ((P \land \neg Q) \to R)

Query:

R

Có 3 symbol nên có:

2^3 = 8

model.

$P$	$Q$	$R$	$KB$
False	False	False	False
False	False	True	False
False	True	False	False
False	True	True	False
True	False	False	False
True	False	True	True
True	True	False	False
True	True	True	False

Chỉ có một model làm KB đúng:

P = True
Q = False
R = True

Trong model đó, query R cũng True.

Vì vậy:

KB \models R

Điều cần chú ý

Ta không yêu cầu query đúng trong mọi model có thể.

Ta chỉ yêu cầu query đúng trong mọi model thỏa Knowledge Base.

Các model làm KB False không mô tả thế giới phù hợp với những gì agent đang biết, nên không dùng chúng để bác bỏ entailment.

Model Checking bằng đệ quy

Ta không nhất thiết phải tạo sẵn một list chứa toàn bộ $2^n$ model. Có thể sinh model từng bước bằng recursion.

Pseudo-code:

CHECK-ALL(KB, query, symbols, model):
    nếu không còn symbol:
        nếu KB đúng trong model:
            trả về query đúng trong model
        ngược lại:
            trả về True

    lấy một symbol P

    model_true  = model + {P = True}
    model_false = model + {P = False}

    return CHECK-ALL(... model_true)
       AND CHECK-ALL(... model_false)

Điểm khó nhất là dòng:

nếu KB False thì return True

Lý do: entailment chỉ bị phá vỡ nếu tồn tại một model thỏa KB nhưng query False. Model không thỏa KB không phải counterexample.

Python rút gọn theo ý tưởng CS50

def check_all(knowledge, query, symbols, model):
    if not symbols:
        if knowledge.evaluate(model):
            return query.evaluate(model)
        return True

    remaining = symbols.copy()
    symbol = remaining.pop()

    model_true = model.copy()
    model_true[symbol] = True

    model_false = model.copy()
    model_false[symbol] = False

    return (
        check_all(knowledge, query, remaining, model_true)
        and check_all(knowledge, query, remaining, model_false)
    )

Hàm này xây một cây nhị phân của các truth assignment:

Với mỗi symbol mới, số nhánh tăng gấp đôi.

Độ phức tạp của Model Checking

Nếu có $n$ propositional symbol, số model tối đa là:

2^n

Do đó brute-force model checking có độ phức tạp tăng theo hàm mũ theo số symbol.

Điều này không làm Model Checking “vô dụng”. Nó vẫn rất tốt để:

hiểu định nghĩa entailment;
giải bài nhỏ;
làm baseline dễ kiểm tra;
kiểm chứng logic khi số symbol ít.

Nhưng với knowledge base lớn, ta cần các cách inference thông minh hơn.

Chốt lại

Entailment không hỏi query có đúng ở một thế giới nào đó hay không. Nó hỏi:

Trong mọi model phù hợp với Knowledge Base, query có luôn đúng không?

Model Checking trả lời câu hỏi này bằng cách xét các model. Cách làm rất rõ ràng, nhưng số model tăng theo $2^n$ , vì vậy ta cần các phương pháp suy luận có cấu trúc hơn ở bài tiếp theo.

Bản tiếng Anh đang soạn.