【2026 最新】TwIL-LM3-Pro 怎麼測？十組假規則驗收 CPU 邏輯小模型（量化比較＋例外判定）

你想把 TwIL-LM3-Pro 放在自己的電腦，替一段流程檢查「這個結論能不能從規則推出」。第一題答對了，第二題加上「停權會員例外」，它還會放行嗎？再刪掉停權資料，它會說不知道，還是自己補一個答案？

這篇專為第一次評估本機模型、沒有邏輯學背景的讀者寫。先把規則變成一張有標準答案的考卷，再核對權重、模板與執行設定，用十組假規則分開檢查正確、例外、矛盾與資訊不足。願意貼指令的讀者可以走到 CPU 首跑；還沒準備好環境，也能先完成題集。

截至 2026 年 10 月 14 日，本文核對官方模型卡、權重目錄與 llama.cpp 文件。以下是供你執行的驗收方法，沒有預填這十題的模型成績。TwIL-LM3-Pro 的 授權第 3.3 節限定非商業研究與教育；本文練習使用自建假資料。要接進公司的收費服務或業務流程，應先取得另行允許該用途的授權。

先說結論：TwIL-LM3-Pro 要用四張成績單驗收

邏輯驗收＝事先寫正解＋固定執行條件＋保留完整回答＋獨立檢查。把模型當成來應徵的規則解讀員：考卷由你出，答案由規則決定，交卷時間和漏答另算。

• 先用十題小考找出錯誤種類，再擴充未見題，別直接拿總分代表所有用途。
• Q4 比較省權重儲存空間；品質是否符合你的規則，需用同題對照確認。
• 缺少前提、推出否定，以及題目本身矛盾，是三種不同結果。
• 可寫成明確公式的部分，交給真值表或求解器檢查；自然語言翻譯另驗。

TwIL-LM3-Pro 是什麼？先分清模型與驗證器

webAI 在 2026 年 9 月 30 日的發布文把它定位為小型形式邏輯推理模型。它基於 IBM Granite 4.2 3B，官方列出約 36.6 億參數，提供完整權重與 GGUF（方便本機推論程式載入的檔案格式）。

形式邏輯像把校規改寫成積木：「若 A 且 B，則 C」。模型擅長的候選工作，是把句子翻成這些積木、判斷前提與結論的關係、協助整理推論。你真正要問的，是它在你的句型與例外上，能否穩定交出正確標籤。

模型生成一段看起來合理的解釋；符號驗證器則在明確公式與指定語意下找反例。兩者工作不同。即使驗證器判定公式成立，仍要檢查「會員」是否被翻成正確變數、例外是否漏寫。想理解這個分工，可接著讀 確定性核心與機率性邊緣。

①「先訂考規」：不知道、反駁、矛盾分開

本篇使用嚴格條件規則與開放世界：沒有提供的事實保持未知。「沒寫停權」不等於「確定未停權」。所有題目互相獨立，不繼承上一題的資料；若要表達一般規則的例外，把條件寫成「會員且明確未停權」，不要靠模型猜優先順序。

• ENTAILED：所有符合規則與事實的可能情況，都支持問題中的結論。
• CONTRADICTED：所有符合規則與事實的可能情況，都支持結論的否定。
• UNKNOWN：仍存在結論為真與為假的兩種可能，資料不足以選邊。
• INCONSISTENT：規則與事實互相衝突，找不到同時成立的情況；先回報輸入衝突。

最後一種是我們為本篇驗收加的出口，不是宣稱模型原生提供四分類。先查一致性，再做前三種判定，可避免把「同時准許與禁止」錯讀成某一邊勝出。這個次序也符合 Z3 命題邏輯指南所示的可滿足性與邏輯蘊涵檢查方式。

②「先寫答案」：十組假規則考卷

以下每組都有題目與正解。執行時只貼規則、事實與問題，把正解放在另一份筆記；不要讓受測模型看到答案。每題加同一段要求：「依嚴格條件規則判定，未提供的事實保持未知；先查一致性，再輸出 ENTAILED、CONTRADICTED、UNKNOWN 或 INCONSISTENT，附最短必要理由。」

1.「基本放行」

會員且未停權 → 可進場；停權 → 不可進場。事實：阿林是會員，且明確未停權。問題：阿林可進場嗎？

事先寫好的正解：ENTAILED。兩個必要前提都已提供。

2.「例外攔截」

會員且未停權 → 可進場；停權 → 不可進場。事實：阿林是會員，且已停權。問題：阿林可進場嗎？

事先寫好的正解：CONTRADICTED。停權規則推出不可進場；會員身分不消除例外。

3.「例外狀態缺失」

會員且未停權 → 可進場；停權 → 不可進場。事實：阿林是會員。問題：阿林可進場嗎？

事先寫好的正解：UNKNOWN。沒有未停權或停權事實，兩種可能仍存在。

4.「別倒著推」

審核通過 → 有票。事實：阿林有票。問題：阿林審核通過嗎？

事先寫好的正解：UNKNOWN。有票可能來自其他途徑，規則未寫反方向。

5.「兩段接力」

紅卡 → 藍卡；藍卡 → 綠卡。事實：阿林有紅卡。問題：阿林有綠卡嗎？

事先寫好的正解：ENTAILED。先推出藍卡，再推出綠卡。

6.「二選一排除」

阿林有紅卡或藍卡，允許同時有兩張。事實：阿林沒有紅卡。問題：阿林有藍卡嗎？

事先寫好的正解：ENTAILED。紅卡可能被排除，藍卡仍需成立。

7.「少一個條件」

有票且成年 → 可進場。事實：阿林有票。問題：阿林可進場嗎？

事先寫好的正解：UNKNOWN。成年資訊缺失，沒有規則保證進場或禁止進場。

8.「輸入互相打架」

事實：阿林可進場；阿林不可進場。問題：阿林可進場嗎？

事先寫好的正解：INCONSISTENT。先攔下同一命題與其否定，勿挑一邊回答。

9.「嚴格規則的逆否」

紅卡 → 藍卡。事實：阿林沒有藍卡。問題：阿林有紅卡嗎？

事先寫好的正解：CONTRADICTED。在本篇嚴格邏輯下，有紅卡會迫使有藍卡，與事實相衝突。

10.「有一人，不是每一人」

阿林與阿梅之中至少一人有票。問題：阿林有票嗎？

事先寫好的正解：UNKNOWN。可能只有阿梅有票，也可能阿林有票，名字不能偷換。

完整追一次第三題：會員是真的；停權狀態未知。假設阿林未停權，規則會放行；假設阿林已停權，規則會禁止。兩種情況都符合目前資料，所以 UNKNOWN 才是正解。模型若答「通常會員能進場」，是在加入生活常識，沒有完成這張考卷。

第九題採用的是邏輯課的嚴格「若…則…」。日常說「下雨通常會塞車」帶有例外，不應直接套逆否。真正業務規則若有優先權、有效日期或預設值，先把那些語意寫清楚，再製作另一份考卷。

③「鎖同一份材料」：權重、模板、版本都留下

從 官方檔案目錄選 TwIL-LM3-Pro-Q4_K_M.gguf，先記下 repository revision，再下載單一檔案。不要把「main」當作永久版本；本次讀取的 revision 為 144a3ccb31264deadcf68bc5a1d58f621e497d03。下載前可用 Hugging Face 下載說明核對指定 revision 的方式。

下載後，macOS 可執行 shasum -a 256 TwIL-LM3-Pro-Q4_K_M.gguf，把輸出的雜湊留在紀錄裡。雜湊像封箱編號：它幫你認出是否同一份檔案，不代表內容已被證明安全或正確。也記 llama-cli --version、CPU、RAM、執行緒、作業系統與完整啟動指令。

官方模型卡列出 Q4 權重約 2.09 GiB；那是檔案大小，不是整個程式的 RAM 上限。載入、上下文快取與執行緩衝也占記憶體。先關掉其他重工作，觀察是否發生大量記憶體交換；發生時把該跑次註明，勿直接歸因模型推理慢。

若尚未安裝 llama.cpp，從 官方 releases取得對應作業系統與 CPU 架構的版本，解壓縮後到含執行檔的目錄。官方建置文件另提供 macOS／Linux 的建置選項。本篇接下來假設 llama-cli已在命令搜尋路徑；若只解壓縮在目前資料夾，改用 ./llama-cli，Windows 使用對應的 llama-cli.exe。

④「先考一題」：CPU 首跑與完整交卷

對已下載的 Q4 檔案，貼入 llama-cli -m TwIL-LM3-Pro-Q4_K_M.gguf -cnv --temp 0 -n 2048 -c 8192 --device none -ngl 0。llama.cpp 參數文件列出模型路徑、上下文與裝置選項；--device none -ngl 0把此輪設定為不將模型層卸載到 GPU。啟動日誌仍要留下，確認實際裝置。

-cnv是對話模式；--temp 0使用貪婪選取；-n 2048是輸出 token 上限；-c 8192是這次指定的上下文容量。Token 是模型切分文字的單位，不等於中文字數。這些值是起始測試設定，不是保證每題夠用。

保留檔案內建對話模板，先貼第一題，看到最後標籤才算交卷。每題結束後重啟對話或程式，避免前題答案進入後題。模型卡說預設模板會先產生 <think>…</think>；如果停在推理途中，把它記為未完成，勿從半段推理猜答案。

以按下送出到完整答案出現的時間作為完整回答延遲，另外記第一次載入時間。模型每秒吐很多 token，但寫了很長的草稿，你仍可能等很久。官方發布文把速度測量限定在伺服器配置，並提醒在自己的硬體量反應時間；這裡不套用它的 GPU 吞吐數字。

若遇輸出上限，保留第一次結果，再用 -n 4096重跑該題，單獨標註「加大預算後完成」。上下文溢出則檢查輸入加輸出的容量，勿把兩種截斷混在一起。兩種設定各算一張成績單，才看得出預算帶來的改變。

⑤「每次只改一項」：TwIL-LM3-Pro 量化怎麼比？

先跑 Q4，再在設備容量允許時，用同 revision 的 Q8 或 F16 當本機參照。更換 -m後保留同樣十題、模板、執行緒、上下文、溫度與輸出上限，重新啟動程式。F16 GGUF 是由發布權重轉換而來，與 BF16 不是位元完全相同的檔案；此輪比較回答「這兩份本機檔在我的題目上差在哪」。

官方模型卡明確說公開分數來自 BF16／vLLM，GGUF 的差異尚未在該卡量化。因此 Q4 全對也不能推出與 BF16 等效；Q4 有錯也要看較高精度參照是否同樣錯。兩邊一起答錯，可能先要修規則表達、翻譯或模型選擇。

• 答案：正確題數／全部十題；無標籤與未完成都保留在分母。另列四類的錯誤，尤其 UNKNOWN 被錯判放行。
• 完成：有幾題交出最後標籤、有幾題撞上輸出上限。不要只報已完成題的正確率。
• 時間：逐題完整延遲、重跑後結果、首輪載入時間。使用暖機後對照，另留首輪觀察。
• 記憶體：用同一個系統監控工具看程式峰值，註明 CPU-only 與是否換頁；檔案大小另列。

溫度為零有助固定選取方式，但跨硬體、版本與數值運算仍應重跑確認。再做一組改名、換詞、換規則順序的未見題；新題先由你另寫正解，勿看模型答案後才修改評分標準。十題只用來找缺陷，不足以估算你的全部任務成功率。

官方卡把主要語言列為英文。繁中先測一輪，再用你核對過、語意相同的英文題逐題配對，分開看語言表達與邏輯能力。翻譯本身若把「且」變成「或」，兩張考卷就已經不同。需要更完整的題集紀律，可讀 AI Evals 新手教學。

⑥「另找裁判」：一個不靠模型的符號驗證

第一題只需要三個布林值：m代表會員，s代表停權，a代表可進場。規則是 (m and not s) → a；事實是 m=True, s=False。把三個開關的所有組合列出，留下符合規則與事實的組合，再問其中是否還有 a=False的反例。

已有 Python 3 的讀者可貼入：python3 -c 'from itertools import product; worlds=[(m,s,a) for m,s,a in product([False,True],repeat=3) if m and not s and ((not (m and not s)) or a)]; print(worlds); print("counterexamples:", [w for w in worlds if not w[2]])'。這個小示範使用 Python 的 product列舉組合；它不是完整自然語言規則解析器，也未處理任意量詞。

你應看到一個成立組合 [(True, False, True)]，反例清單為 []，所以可進場成立。第三題若刪掉程式中的 not s and這個事實條件、保留括號內規則，就會留下進場與不進場的可能。先確認符合前提的組合非空，再找反例；前提若本身矛盾，空清單應判輸入衝突。

規則多時可以進一步使用 Z3：先檢查前提是否可滿足，再測「前提＋否定結論」能否成立。求解器給的是編碼後問題的結果；模型把原句轉錯，求解器也會忠實地解那份錯公式。用第一題、第三題與第八題對照，驗翻譯與判定兩層。

常見坑：一個漂亮總分會藏住什麼？

第一個坑是把 UNKNOWN 算成「保守拒絕」就給分。它的用途是表達資訊不足；若你需要補查資料，應另定義補查流程。第二個坑是讓模型看見標準答案，第三個坑是十題連續聊、前面的例子偷偷教會後面。三者都會讓小考與真正使用情境錯位。

第四個坑是先改量化、又關思考、又縮上下文，最後猜哪一項造成差異。先只換權重，再另外設計思考模式對照。官方模板提供思考控制參數，但不同推論端的傳遞方式需按文件核對；本篇 CPU 首跑保留預設模板，不把提示「只給答案」當成已關閉內部計算。

若模型只幫你整理候選邏輯，再由明確公式檢查，值得繼續做非商業研究。若你的成功條件是商業流程自動放行，這次授權與十題小考都沒有提供採用依據。一般本機決策模型的整合需求，可另讀 本機決策模型的獨立驗收；不要把那篇的部署路線直接移植成 TwIL 的商用許可。

FAQ：TwIL-LM3-Pro 新手八問

1. Q4 能在 CPU 跑，就表示我的電腦一定夠用嗎？

不一定。官方提供 CPU 路線；實際 RAM、上下文快取、程式版本與完整延遲仍要看你的啟動和紀錄。

2. 下載權重，就能放進公司流程嗎？

不能依這份授權直接推定可以。第 3.3 節限定非商業研究與教育，商業用途要有另行授權。

3. Q4 與 BF16 一樣準嗎？

本篇沒有這個結論。官方說 GGUF 差異尚未在卡中量化，應在自己的同題比較裡觀察。

4. 可以把輸出預算縮到很小，只看速度嗎？

可以設計這種對照，但要同時記未完成與正確率。停在推理途中，不算交出最後答案。

5. 沒提到停權，應當作沒停權嗎？

本篇不這樣定義。未給定事實保持未知；若你的系統使用封閉世界，必須另寫考規與正解。

6. 正反答案都能推出來，該挑哪一個？

先標 INCONSISTENT。修正互相衝突的輸入，再做結論判定。

7. 十題全對，就代表可以取代符號驗證器嗎？

這份小考支持的只是十題結果。擴充未見題與邊界情況，並把可形式化的部分獨立驗證。

8. 完全不會寫程式，今天能做什麼？

先把十題存成兩份筆記：一份考題，一份答案。先親手走完第三題的兩種可能，之後再準備本機執行。

給新手的三個重點

• 先寫清楚「不知道」與「規則衝突」的出口，才能判斷模型有沒有擅自補前提。
• 固定權重、模板與預算，答案、完成、時間、記憶體各自留下證據。
• 模型負責候選解讀，形式化部分另有裁判；學會找反例，比背一個跑分更有用。