什麼是自動推理？
自動推理是電腦科學的領域，試圖提供有關系統或程式將做什麼或絕對不會做什麼的保證。此保證是以數學證明為基礎。人們藉由使用定理和推論等邏輯策略來解決數學、科學和運算中的許多邏輯問題。自動推理利用使用相同工具的電腦來解決複雜的挑戰。自動推理工具試圖藉由使用已知的數學技術來回答有關程式（或邏輯公式）的問題。這些工具可幫助您檢查語句或表達式的真實性。
自動推理可以解決哪些問題？
科學家和軟體開發人員使用自動推理來證明兩件事。首先，他們證明系統設計或實作遵守其規格。其次，他們證明系統按照預期的方式運作。
自動推理透過以數學定理或已知真理支持的形式邏輯產生證明來實現這一目標。自動推理使用以邏輯為基礎的數學演算法驗證方法，為所有可能的行為產生安全性或正確性證明。
自動推理也可以用來證明用於設定網路的系統允許網路存取或授予許可，或者保持資料的隱私性和安全性如預期運作。
使用自動推理時，您首先向系統提出問題陳述式。然後，自動推理系統使用問題陳述式計算和驗證假設。軟體執行此動作，直到用盡所有選項。
自動推理的範例問題
為了更全面地理解自動推理，請考慮問題陳述式貓是否生活在陸地上？和以下聲明：
- 貓是哺乳動物
- 哺乳動物生活在陸地上
自動推理系統評估問題陳述式是否為真。 具體來說，該系統使用邏輯推論。在此案例中，貓是哺乳動物，而哺乳動物生活在陸地上。因此，系統將驗證貓生活在陸地上。
自動推理的局限性
自動推理不會進行預測或概括。例如，我們可以使用自動推理來建立這樣的引數：
- 貓有毛髮
- Fluffy 是一隻貓
- 因此，Fluffy 有毛髮
我們不能使用自動推理來建立這樣的引數：
- 貓是哺乳動物
- 貓生活在陸地上
- 因此，所有哺乳動物都生活在陸地上
此類應用在定理證明器中很常見，其在執行推論性推理任務時需要人為指引。
有哪些自動推理使用案例？
自動推理逐步進行邏輯推論的能力在幾個領域很有幫助。藉由使用自動推理，您可以證明大型架構的安全性、合規性、可用性、耐久性和安全性特性。
以下是自動推理的其他一些使用案例。
數學建模
科學家、工程師和數學家透過在科學應用中套用代數公式來解決問題並驗證數學證明。在此類實務中，他們使用依賴於幾個變數來推斷問題可能解決方案的數學模型。
硬體驗證
自動推理可協助硬體工程師建置可靠的產品。藉助該技術，他們能夠發現傳統測試方法忽略的潛在缺陷。
例如，電子設計工程師使用嚴格的數學自動推理分析來取得確定性證明，表明特定硬體設計符合其規格，例如系統行為或執行。
此驗證表明系統的所有可能行為都滿足構成規格的暫時性屬性。它還可以表明系統實作的每種可能行為與其高階規格的某些行為一致。
軟體驗證
軟體開發人員使用自動推理功能來協助確保應用程式具有強大功能，以防止意外的安全性問題，並且軟體可按預期或設計運作。類似於硬體驗證，自動推理可讓開發人員針對各種政策驗證軟體安全性措施。
例如，Amazon Web Services (AWS) 的工程師透過自動推理，證明每個啟動組態的啟動程式碼都是安全的。另一個範例是，他們證明在 Amazon Simple Storage Service (Amazon S3) 上存儲和處理的資料是受到保護的。在此範例中，它們仰賴自動推理來進行複寫、一致性、自動擴展、負載平衡和其他協調任務。
人类推理建模
電腦科學家使用自動推理技術來設定存取。為此，他們會撰寫描述何時允許和拒絕使用者存取資源要求的政策。這會驗證只有預定的使用者才能存取資源，這對資源的安全性和隱私性很重要。
例如，電腦科學家使用可滿足性模組理論 (SMT) 公式和 SMT 求解器來證明安全性屬性。
有哪些自動推理工具和技術？
接下來，我們分享幾種自動化推論方法，這些方法使運算系統能夠執行人為推論。
經典邏輯
經典邏輯是一種數學哲學，為自動邏輯推理程式提供基本推理模型。此邏輯基於以下原則：每個命題都有真或假的真值，但不是兩者都有。
此原則主要側重於一階邏輯，即允許數學家在句子中用像存在這樣的數量詞表示像 x 這樣的未知變數。例如，科學家在邏輯程式設計中套用經典邏輯來在此句子中找到 x：存在 x，使得 x 生活在陸地上，並且 x 是哺乳動物。
命题逻辑
命題邏輯是一個邏輯系統，其中包含可以為真或假的命題以及它們之間關係的建構模組，稱為引數。
命題邏輯中參數的經典陳述式為如果 P，則 Q。例如，如果是週六，則為週末。
自動推理使用稱為 SAT 求解的技術。該技術使用稱為 SAT 求解器的工具搜尋符合命題邏輯中引數的指派。這意味著使引數為真的變數。
自動推理和人工智慧有什麼區別？
自動推理是人工智慧 (AI) 的特定學科，它將邏輯推論套用至電腦系統。
人工智慧是一門科學，其在電腦解決問題期間教導電腦像人類一樣思考。人工智慧的最新發展導致了各個學科的進步，包括深度學習、資料分析和機器學習。
自動推理與其他 AI 技術不同，例如自然語言處理 (NLP)，後者側重於訓練電腦以理解書面或口頭演講。相反，自動推理使用邏輯模型和證明來推理系統或程式的可能行為，包括其可以或永遠不會達到的狀態。
自動推理和深度學習有什麼區別？
自動推理證明程式或系統的屬性。它使用程式或系統本身，以及採用形式邏輯的系統模型或規格。
深度學習會依據將統計模型套用至大型資料集來進行預測。
深度學習是一種進階的機器學習技術，可模擬人類大腦的運作方式。該技術使用不同的神經網路模型，此模型由擷取、比較和分析相關資訊的多層神經元組成。資料科學家將深度學習用於複雜的應用場景，例如在自動駕駛汽車中處理攝像頭和感測器資料。
自動推理是機器學習嗎？
自動推理並不同於機器學習。簡而言之，機器學習可以做出預測和推論。自動推理則是提供證明。
機器學習是 AI 的子集，可訓練電腦使用大型資料範例做出決策。例如，資料科學家使用機器學習來訓練銀行軟體以辨識欺詐活動。他們使用大量的財務資料範例，以確保軟體依據先前學到的結果輕鬆辨識異常模式。
自動推理不使用資料訓練模型，而是允許模型依據數學真理和證明推斷出結果。
AWS 如何使用自動推理來改善服務產品？
AWS 使用自動推理來改善多種服務產品。以下是我們給出的一些範例：
- Amazon CodeGuru Reviewer 使用自動推理和機器學習來幫助開發人員辨識軟體漏洞。
- Amazon Inspector Classic 具備網路連線功能，可自動分析 EC2 執行個體，找出潛在的安全漏洞和設定錯誤。
- AWS Identity and Access Management (IAM) Access Analyzer 透過自動推理來管理帳戶許可。
- Amazon Virtual Private Cloud (Amazon VPC) Reachability Analyzer 套用自動推理來幫助您了解和視覺化自己的 AWS 網路。
如需 AWS 服務自動推理的詳細資訊，請造訪可證明的安全性。我們使用數學推理為您的安全工作負載提供強大的安全保證。
立即建立帳戶，開始使用 AWS 上的安全性。
