전공 공부/인공지능(Artificial Intelligence)

[인공지능] Propositional Logic - 5

7_JUN_7 2023. 10. 11. 04:09

SAT Solvers in Practice

SAT 솔버가 실제로 어떻게 다양한 분야에서 사용되는지를 설명합니다.

1. Circuit Verification

  • 주어진 VLSI(매우 대규모 집적 회로) 회로가 올바른 답을 계산하는지 확인한다.
  • 회로 설계의 정확성과 신뢰성을 검증하기 위해 SAT 솔버를 사용한다.
  • does this VLSI circuit compute the right answer?

2. Software Verification

  • 특정 프로그램이 올바른 결과를 계산하는지 확인한다.
  • 코드의 논리적 오류를 찾고, 프로그램이 예상대로 작동하는지 검증한다.
  • does this program compute the right answer?

3. Software Synthesis(합성)

  • 올바른 답을 계산하는 프로그램이 무엇인지 찾는다.
  • 특정 요구 사항을 충족하는 프로그램을 자동으로 생성한다.
  • what program computes the right answer?

4. Protocol Verification

  • 특정 보안 프로토콜이 깨질 수 있는지 확인한다.
  • 프로토콜의 취약점을 식별하고, 보안 메커니즘이 올바르게 작동하는지 검증한다.
  • can this security protocol be broken?

5. Protocol Synthesis(합성)

  • 특정 작업에 대해 안전한 프로토콜이 무엇인지 찾는다.
  • 주어진 보안 요구 사항을 충족하는 프로토콜을 개발합니다.
  • what protocol is secure for this task?

6. Combinatorial Problems

  • 다양한 조합 문제의 해결책을 찾는다.
  • what is the solution?

7. Planning

    • 목표를 달성하기 위한 효율적인 계획을 생성한다.
    • 팩맨의 경우 ) how can I eat all the dots?

Planning as Satisfiability

  • hyper-efficient SAT solver이 주어진 경우, 완전 관측 가능 (fully observable) 하고 결정론적인 경우(deterministic)에만 계획을 수립할 수 있다.
    • 계획 문제(planning problem)는 만족할 수 있는 할당(satisfying assignment)이 있는 경우에만 해결할 수 있다.(solvable)
    • 액션 변수의 진리 값에서 추출된 solution으로 계획을 수립한다.

시간 T = 1부터 ∞까지:

  • T 타임스텝에 대한 PacPhysics(팩맨 물리)로 지식 베이스(KB)를 초기화(intialize)한다.
  • 시간 T에서 목표가 참이라고 주장한다.

SAT 솔버의 solution에서 액션 변수를 읽어(read-off) 계획을 수립한다.

Basic PacPhysics for Planning

"Basic PacPhysics for Planning" 팩맨 게임의 기본 물리학을 계획에 적용하는 방법을 설명한다. 이는 팩맨이 게임 환경에서 어떻게 움직이고 상호작용하는지를 정의한다.

1. Map

  • where the walls are and aren’t, where the food is and isn’t
  • 벽의 위치 : 맵에서 어디에 벽이 있는지, 없는지를 정의한다.
  • 음식의 위치 : 각 위치에 음식이 있는지 없는지를 정의한다.

2. Initial State

  • Pacman start location (exactly one place), ghosts
  • 팩맨 시작 위치: 팩맨이 게임 시작 시점에 정확히 어디 한 위치에 있는지를 정의한다.
  • 고스트: 게임에 등장하는 고스트의 초기 상태와 위치를 정의한다.

3. Actions

  • Pacman does exactly one action at each step
  • 팩맨의 행동: 각 스텝에서 팩맨은 정확히 하나의 행동을 수행한다.

4. Transition Model

  • <at x,y_t>
    • 이는 시간 t에서 팩맨이 위치 (x, y)에 있는지를 나타낸다.
    • <at x,y_t> ⇔ [at x,y_(t-1) and stayed put] v [next to x,y_(t-1) and moved to x,y]
    • 팩맨이 t-1 시간에 (x, y)에 있고 움직이지 않았거나, (x, y)에 바로 이웃위치에 있고 (x, y)로 이동했을 경우 참이다.
  • <food x,y_t>
    • 이는 시간 t에서 위치 (x, y)에 음식이 있는지를 나타낸다.
    • <food x,y_t> ⇔  [food x,y_(t-1) and not eaten]
    • t-1 시간에 (x, y)에 음식이 있고, 그 음식이 먹히지 않았다면 참이다.
  • <ghost_B x,y_t>
    • 이는 고스트의 위치와 움직임을 나타내는 전이 모델이다.
    • <ghost_B x,y_t> ⇔  […..]

Reminder: Partially observable Pacman

 팩맨이 부분적으로 관측 가능한 환경에서 어떻게 작동하는지를 설명다. 이는 팩맨이 환경의 전체를 한 번에 볼 수 없고, 한 시점에 한 방향의 정보만을 얻을 수 있다는 것을 의미합니다. 이전에 설명했던 것을 다시 한번 설명했음.

1. Perception

  • 벽 감지: 팩맨은 각 시간 단위마다 각 방향으로 벽이 있는지 없는지를 감지한다.

2. Variables

  • Blocked_W_0, Blocked_N_0, …, Blocked_W_1, …:
    • 이러한 변수들은 각 시간 단위에서 각 방향으로 벽이 있는지 없는지를 나타낸다.
    • Blocked_W_0은 시간 0에서 서쪽 방향에 벽이 있는지를 나타낸다.

3. Basic Question - Where Am I?

  • 위치 추론: 주어진 감지 정보를 기반으로 팩맨은 현재 위치를 추론해야 한다.
  • 팩맨은 각 시간 단위에서 각 방향의 정보만을 알고 있으므로, 이 정보를 종합하여 현재 위치를 결정해야 합니다.

State Estimation

"State Estimation" 섹션은 주어진 관측 및 행동의 이력을 기반으로 현재 상태를 추적하는 과정을 설명합니다. 상태 추정은 에이전트가 현재 어떤 상태에 있는지를 파악하는 데 중요하다

 

State Estimation의 정의

  • 상태 추정(State Estimation): 관측 및 행동(observation and actions)의 이력(history)을 기반으로 현재 어떤 상태가 참인지를 추적하는 과정

 

논리 에이전트는 자가 질의(ask itself)가 가능하다! : 논리 에이전트는 자신에게 질문하여 상태를 추정할 수 있다.

  • 예: ask whether KB ∧   <actions> ∧   <percepts> |= At_2,2_6
  • logical agent는 KB(지식 베이스)와 행동, 그리고 인지가 At_2,2_6을 함축하는지를 질문한다.
  • 이것은 지연된(lazy) 방식이다: 이 방식은 각 스텝에서 전체 생애 이력( one’s whole life history )을 분석한다.

자가 질의의 방식보다 더 적극적인 방식의 상태 추정 방식이 존재한다.

 

"적극적인"(eager) form의 상태 추정 :

  • 각 행동 및 인지(percept) 후에 :
    • 각 상태 변수 에 대해 다음을 수행한다.
      • If KB ∧  action_(t-1) ∧ percept_t |= X_t, add X_t to KB
      • 만약 이 를 함축한다면, 를 KB에 추가한다.
      • If KB ∧  action_t-1 ∧  percept_t |= ¬ X_t, add ¬ X_t to KB
      • 만약 이 를 함축한다면, ¬를 KB에 추가합니다.

Example: Localization in a Known Map

"Example: Localization in a Known Map" 섹션은 알려진 맵에서의 팩맨의 위치 추정(Localization) 방법을 설명한다.

  • KB 초기화: PacPhysics(+SM)을 사용하여 시간 스텝 동안의 KB를 초기화한다.
  • 시간 스텝 동안 팩맨 에이전트를 실행 :
    • 각 행동과 인지(percept) 후에 :
      • 각 변수 At_x,y_t에 대해 :
        • If KB ∧  action_(t-1) ∧  percept_t |= At_x,y_t, add At_x,y_t to KB
        • 만약 이 를 함축한다면, 를 KB에 추가한다.
        • If KB ∧  action_t-1 ∧  percept_t |=  ¬ At_x,y_t, add ¬ At_x,y_t to KB
        • 만약이 를 함축한다면, 를 KB에 추가한다.
      • 행동(action)을 선택한다.
  • 팩맨의 가능한 위치(possible locations)는 증명 가능하게 거짓이 아닌 위치들( not provably false locations)  이다. 즉, KB에 의해 거짓으로 증명되지 않은 위치들이 팩맨이 있을 수 있는 가능한 위치이다.

and localization demo...

Example: Mapping from a Known Relative Location

팩맨이 초기 위치를 알고 있을 때 주변 환경(즉, 맵)을 어떻게 매핑하는지 설명한다.

  • 초기 위치를 손실 없이(without loss of generality) 이라고 하자. 이는 팩맨이 시작하는 임의의 위치를 으로 설정하여 문제를 단순화하는 것이다.
  • 팩맨은 인식(percept)을 통해 어떤 행동이 효과적인지 안다. 즉, 항상 자신의 위치를 알 수 있다. 이를 "Dead Reckoning"이라고 한다. Dead reckoning은 초기 위치에서의 이동을 측정하여 현재 위치를 추정 ( from chatGPT )
  • 시간 스텝 동안 에서 시작하는 PacPhysics를 사용하여 KB를 초기화한다.
  • 시간 스텝 동안 팩맨 에이전트를 실행 :
    • 각 시간 스텝에서:
      • 이전 행동과 새로운 인식 사실로 KB를 업데이트한다.
      • 각 벽 변수 Wall_x,y에 대해:
        • If Wall_x,y is entailed, add to KB
        • 만약 Wall_x,y가 함축되면, KB에 추가한다.
        • If ¬ Wall_x,y is entailed, add to KB
        • 만약 가 함축되면, KB에 추가한다.
      • 행동을 선택한다.
  • 벽 변수( The wall variables )들이 맵을 구성( constitute )한다.

Mapping Demo

Simultaneous Localization and Mapping

 

Dead Reckoning의 한계

  • 실제 세계에서 Dead Reckoning은 항상 효과적이지 않다.
  • 예를 들어, 센서가 인접한 벽( adjacent walls )의 수만 계산할 수 있을 때(0, 1, 2, 3 중 하나로 표현됨) 이 방법이 제한된다. (0,1,2,3 = 2 bits)

Pacman doesn’t know which actions work, so he’s “lost”

  • 팩맨은 어떤 행동이 효과적인지 모르며, 그의 정확한 위치도 모른다. 이 상태에서 팩맨은 어떻게 맵을 생성할 수 있겠는가?

에서 시작하여 시간 스텝 동안 PacPhysics를 사용하여 KB를 초기화한다.

 

시간 스텝 동안 팩맨 에이전트를 실행한다.

  • 각 시간 스텝에서:
    • 이전 행동과 새로운 인식 사실로 KB를 업데이트한다.
    • For each x,y, add either Wall_x,y or ¬ Wall_x,y to KB, if entailed
    • 각  에 대해, Wall_x,y 또는 중 하나를 KB에 추가한다. (만약 함축된다면)
    • For each x,y, add either At_x,y_t or ¬ At_x,y_t to KB, if entailed
    • 각 에 대해, At_x,y_t 또는 중 하나를 KB에 추가한다. (만약 함축된다면)
    • 행동을 선택한다.

Simple Theorem Proving: Forward Chaining

Forward Chaining이라는 추론 방법을 설명한다. 이 방법은 새로운 사실을 생성하기 위해 Modus Ponens 규칙을 적용합니다.

  • Forward Chaining은 Modus Ponens를 적용하여 새로운 사실을 생성한다.
    • Given X_1​∧X_2​∧…∧X_n​ ⇒ Y  and X_1​,X_2​,…,X_n​ ,  infer Y
    • 주어진 및 이 있을 때, 를 추론한다.
  • 이 규칙을 계속 적용하여 새로운 사실을 추가한다. 더 이상 추가할 사실이 없을 때까지 이 과정을 반복한다.
  • 지식 베이스(KB)에는 오직 definite clauses만 포함되어야 한다. :
    • Definite clause는 심볼들의 결합(Conjunction of symbols)이 하나의 심볼을 함축하는 형태 ( (Conjunction of symbols) ⇒ symbol ) 이거나,
    • 단일 심볼이어야 한다.. (여기서 는 와 동일하다.)

Summary

1. One possible agent architecture : knowledge + inference

  • 지식과 추론을 결합한 에이전트 아키텍처를 고려할 수 있다.

2. Logics provide a formal way to encode knowledge

  • 논리(logic)는 지식을 인코딩하는 공식적인 방법을 제공한다.
    • 논리는 구문(syntax), 가능한 세계의 집합( set of possible worlds ), 진리 조건(truth condition)에 의해 정의된다.

3. 팩맨을 위한 간단한 지식 베이스 (KB)

  • 팩맨을 위한 간단한 KB는 초기 상태( initial state ), 센서 모델( sensor model ), 그리고 전이 모델(transition model)을 포함한다.

4. 논리적 추론의 역할

  • 논리적 추론(Logical inferenece)은 문장들 사이의 함축 관계(entailment relations)를 계산한다. 이를 통해 다양한 작업( a wide range of tasks )이 해결될 수 있다.

5. DPLL 기반 SAT 솔버의 효율성

  • DPLL 알고리즘을 기반으로 한 SAT 솔버는 놀랍도록 효율적인 추론( inference )을 제공한다.

6. 논리 에이전트의 다양한 기능

  • 논리 에이전트는 하나의 지식 베이스( one knowledge base )에 대한 하나의 일반적인 추론 알고리즘( one generic inference algorithm )을 사용하여 위치 추정(localization), 매핑(mapping), SLAM, 계획 수립(planning) 등 많은 작업을 수행할 수 있다.