하이브리드 기호 + 신경 에이전트

순수 LLM을 넘어서

기호 도구의 예

패턴: LLM을 번역기로 사용하기

user_query = 'Three students, three rooms, each room one student, Alice not in room 3, Bob in room 1 or 2...'
formal_constraints = llm_to_smt(user_query)   # produces Z3 input
solution = z3_solve(formal_constraints)
explanation = llm_explain(solution)

패턴: 기호 계획 수립기 + LLM 실행기

plan = pddl_planner.solve(domain, initial_state, goal)
for step in plan:
    llm_execute(step)   # LLM figures out HOW to do it

패턴: LLM이 정리 증명기를 호출하기

패턴: 지식 그래프 + LLM

facts = kg.query('SELECT ?spouse WHERE { :Einstein :spouse ?spouse }')
answer = llm.invoke(f'Format these facts: {facts}')

패턴: 규칙 기반 fallback

if rules.match(query):
    return rules.apply(query)
return llm_fallback(query)

하이브리드가 필요한 이유

순수 기호 방식만으로는 실패하는 이유

신경 기호 연구

직접 구축하기

tools = [
    {'name': 'sat_solver', 'description': 'Solve a SAT problem in DIMACS format', 'parameters': ...},
    {'name': 'symbolic_math', 'description': 'Solve an equation symbolically with sympy', 'parameters': ...}
]

Tool: Sympy for Math

import sympy
from sympy import solve, symbols

x, y = symbols('x y')
result = solve([2*x + y - 5, x - y - 1], [x, y])
print(result)
# {x: 2, y: 1}

Tool: Z3 for Constraints

from z3 import Solver, Int, And
s = Solver()
x = Int('x')
s.add(And(x > 5, x < 15, x % 3 == 0))
print(s.check())  # sat
print(s.model())

프로덕션 고려 사항

하이브리드의 이점

복습