Thuật giải Suy diễn tiến - Dạy máy tính làm toán

Suy Diễn Tiến (Forward Chaining) thường được sử dụng trong các hệ chuyên gia (Expert System), AI và các tình huống cần phân tích dữ kiện từ nhiều nguồn. Đây là một giải thuật đã có lâu đời và được sử dụng như một phần nhỏ của Mạng Ngữ Nghĩa (Semantic Network). Bài viết này mình xin giới thiệu với các bạn thuật giải đơn giản và thú vị này và có một demo nhỏ để minh họa cho cách máy tính giải toán với bộ quy tắc về tính toán trong tam giác.

Ý tưởng chính

• Có một tập hợp các quy tắc suy luận (rules).

• Đầu vào là một tập hợp các dữ kiện đã biết (facts)

• Đầu ra là tìm kiếm một quá trình suy luận (inferred rules) để tìm dữ kiện yêu cầu (target) dựa trên tập hợp các quy tắc (rules) đã cung cấp

Ví dụ: Chúng ta có một tập hợp các công thức tính toán để tính diện tích tam giác, đầu vào là cạnh a,b, và diện tích S, đầu ra là tìm cách tính c là chiều dài cạnh còn lại. Suy khi suy luận máy tính sẽ đưa ra cách tính c như sau:

$$\begin{align*} a,b,S \Rightarrow C \quad \text{ since }S=\frac 1 2 ab\sin C\\a,b,C \Rightarrow c \quad \text{ since }c^2=a^2+b^2-2ab\cos C \end{align*}$$

Bộ quy tắc - Rule

Quy tắc có dạng IF <điều kiện> THEN <kết luận>, sẽ được biểu diễn dưới dạng: \(fact_1,fact_2,\dots \Rightarrow conclusion\). Ví dụ: \(a,h_a \Rightarrow S\) có nghĩa là nếu biết chiều dài cạnh đáy và chiều dài đường cao hạ xuống cạnh đáy đó thì có thể tính được diện tích.

Nói chung rule có 2 thành phần:

• Premises: là tập hợp các facts

• Conclusion: là kết luận dựa trên facts

Giải thuật

Khởi tạo:

• Xây dựng tập quy tắc rules

• Xác định dữ kiện ban đầu facts

• Xác định dữ kiện mục tiêu target

const kb = new KnowledgeBase();
kb.rules.push(new Rule('a, ha => S // S=\\frac{1}{2}a \\cdot h_a'));
kb.rules.push(new Rule('a, S => ha // S=\\frac{1}{2}a \\cdot h_a'));
kb.rules.push(new Rule('ha, S => a // S=\\frac{1}{2}a \\cdot h_a'));
// ...

Suy diễn tiến (forward chaining) từ facts:

• Tập các rule đã xem xét checkedRules = {}

• Tập các facts đã suy luận được inferredFacts = facts

• Lặp:

  • Kiểm tra lần lượt từng rule trong tập hợp rules

  • Nếu rule nằm trong tập checkedRules, bỏ qua

  • Nếu rule có thể suy suy ra được từ inferredFacts:

    • Bổ sung conclusion vào: inferredFacts.push(rule.conclusion)

    • Đánh dấu conclusion.inferredBy = rule để sau này trace back

    • Đưa rule vào checkedRules

  • Nếu không thể tìm thấy rule nào có thể đưa vào tập facts nữa thì ngừng lặp

• return inferredFacts

forwardChaining(facts) {
        // add inferred facts to the list
        const inferred = facts.map(f => ({ content: f, inferredBy: null }));
        // check if we can infer more facts
        const checkedRules = [];
        let canInfer = true;
        while (canInfer) {
            canInfer = false;
            // check each rule
            for (const rule of this.rules) {
                // skip if the rule has been checked
                if (checkedRules.includes(rule)) continue;
                // if the rule matches the inferred facts, add the conclusion to the inferred facts
                if (rule.matches(inferred)) {
                    // add the inferred fact, mark that it is inferred by the rule
                    const newFact = { content: rule.conclusion, inferredBy: rule };
                    // if the fact is not already in the inferred list, add it
                    if (!inferred.some(f => f.content === newFact.content)) {
                        inferred.push(newFact);
                        canInfer = true;
                        checkedRules.push(rule);
                    }
                }
            } 
            if (!canInfer) break;           
        }
        return inferred;
    }

Dò tìm lại kết quả target

• Gọi tập inferredFacts là tập hợp đã suy diễn được từ facts sau quá trình suy diễn

• Nếu target nằm trong inferredFacts nghĩa là tìm được solution:

  • Gọi queue q = [solution]

  • Gọi result = {} là tập chứa các rule kết quả của suy diễn

  • Lặp:

    • Gọi current = q.dequeue()

    • Kiểm tra current được suy diễn từ rule nào (current.inferredBy)

    • Đưa tất cả các premises của rule đó vào queue q

    • Đưa luật ấy vào result

• Ngược lại, không thể suy diễn được target từ facts và rules

• return result

solve(facts, target){
        // infer all possible facts
        const inferredFacts = this.forwardChaining(facts);            

        // check if the target fact is in the inferred facts
        let solution = inferredFacts.find(f => f.content === target);
        if (!solution) {
            console.log(`No solution found for ${target}`);
            return null;
        } else {
            let q = [solution];
            let result = [];
            do {
                let current = q.shift();
                // skip if the fact is not inferred by any rule
                if (!current.inferredBy) continue;
                // add the rule to the result
                result.push(current.inferredBy);                
                // now, add the premises of the rule to the queue
                for (let i = 0; i < current.inferredBy.premises.length; i++) {
                    // find the fact that matches the premise
                    const premise = current.inferredBy.premises[i];
                    const fact = inferredFacts.find(f => f.content === premise);

                    // if the fact is not already in the queue, add it
                    if (!q.includes(fact)) {
                        q.push(fact);
                    }
                } 
            } while (q.length > 0);
            return result;
        }               

    }

Demo

Bạn hoàn toàn có thể view source và update lại tập rule theo ý mình!