munshi007/aura-statePython 프레임워크로, Z3 정리 증명, CTL 모델 검사 및 적합 예측을 통한 형식 검증과 함께 상태 기계로서 LLM 워크플로우를 구축하여 증명 가능하게 올바른 데이터 추출을 지원합니다.
LLM 워크플로우를 상태 머신으로 구축하기 위한 Python 프레임워크로, 형식 검증이 내장되어 있습니다.
pip install git+https://github.com/munshi007/Aura-State.git
대부분의 LLM 프레임워크는 API 호출을 연결하고 결과를 기대하는 방식입니다. Aura-State는 다른 접근 방식을 취합니다: 워크플로우를 노드 그래프로 정의하고, 각 노드는 특정 작업을 수행하며, 프레임워크가 추출, 검증, 라우팅을 처리합니다.
핵심 차이는 노드 사이에서 일어나는 일입니다:
from aura_state import AuraEngine, Node, CompiledTransition
from pydantic import BaseModel, Field
from openai import OpenAI
# Define what you want to extract
class LeadData(BaseModel):
name: str = Field(description="Full name")
budget: int = Field(description="Budget in USD")
timeline: str = Field(description="Buying timeline")
# Define a node that extracts it
class ExtractLead(Node):
system_prompt = "Extract lead info from a sales call transcript."
extracts = LeadData
def handle(self, user_text, extracted_data=None, memory=None):
return "QualifyBudget", extracted_data.model_dump()
# Define a node that does deterministic math (no LLM)
class QualifyBudget(Node):
system_prompt = "Score the lead."
sandbox_rule = "result = budget > 100000" # runs in sandboxed AST, not LLM
def handle(self, user_text, extracted_data=None, memory=None):
return "END", memory
# Wire it up
engine = AuraEngine(llm_client=OpenAI())
engine.register(ExtractLead, QualifyBudget)
engine.connect([
CompiledTransition(from_node=ExtractLead, to_node=QualifyBudget),
])
# Run
next_state, data = engine.process("ExtractLead", user_text="Hi, I'm Sarah. Budget is $450k.")
engine.process()를 호출하면 다음 단계를 순서대로 실행합니다:
1. Adaptive DAG health check → Should this node be skipped or retried?
2. GraphRAG cache lookup → Have we seen this exact input before? Skip the LLM.
3. Few-shot injection → Find similar past successes, inject as examples.
4. LLM extraction + verification → Extract data, verify with Z3, retry if wrong.
5. Your node's handle() method → Your business logic runs here.
6. MCTS Routing (UCB1) → Score branches using UCB1 + AdaptiveDAG metrics.
7. State serialization → Save state for time-travel debugging.
8. Speculative execution → Pre-compute likely next nodes in parallel.
이 부분이 실제로 Aura-State를 다른 프레임워크와 차별화합니다.
노드 그래프는 Kripke 구조로 컴파일되어 시간 논리 속성과 비교 확인됩니다:
from aura_state import verify_engine, reachability, mutual_exclusion, eventual_completion
results = verify_engine(engine, [
{"description": "QualifyBudget is reachable", "formula": reachability("QualifyBudget")},
{"description": "All paths terminate", "formula": eventual_completion("QualifyBudget")},
])
# Result: PROVEN or VIOLATED, with the exact states that satisfy/violate
이 기술은 하드웨어 회로 및 비행 제어 시스템 검증에 사용되는 것과 동일한 기법입니다(CTL 모델 검사, Clarke et al. 1986).
LLM이 값을 추출한 후, Z3(Microsoft Research의 정리 증명기)가 해당 값이 제약 조건을 만족함을 형식적으로 증명할 수 있습니다:
from aura_state import prove_extraction
result = prove_extraction(
{"budget": 450000, "cost_per_sqft": 3, "total": 1350000},
obligations=["budget > 0", "total == budget * cost_per_sqft"],
)
# result.verified = True
# If False, Z3 gives you a counterexample showing exactly what broke
추출을 여러 번 실행하여 분포 가정 없는 신뢰 구간을 얻을 수 있습니다:
from aura_state import conformal_interval
budgets = [450000, 452000, 448000, 450000, 451000]
ci = conformal_interval(budgets, confidence=0.95)
# ci.lower = 447800, ci.upper = 452200
이는 적합 예측(conformal prediction, Vovk et al., 2005)을 사용하며, 분포 가정이 필요하지 않습니다.
4개의 노드로 구성된 파이프라인에서 GPT-4o-mini를 사용하여 10개의 부동산 판매 대화 기록을 실행했습니다(총 30회 API 호출):
Field Accuracy
────────────── ──────────
name 100%
budget 100%
bedrooms 100%
pre_approved 90%
timeline 90%
city 80%
Temporal properties: 3/3 proven
Z3 proof obligations: 20/20 passed
Routing accuracy: 90%
Avg latency: 1.4s
# Try it yourself — no API key needed
python examples/benchmark/run_benchmark.py
# With real LLM calls (needs OPENAI_API_KEY in .env)
python examples/benchmark/run_live.py --model gpt-4o-mini --runs 3
aura_state/
├── core/
│ ├── engine.py # Main engine — process() + MCTS/UCB1 routing
│ ├── adaptive_graph.py # Node health monitoring
│ ├── verification_loop.py # Extract → verify → retry loop
│ └── providers.py # Multi-model routing + cost tracking
├── compiler/
│ ├── schema_compiler.py # JSON Schema → Node classes
│ └── dspy_tuner.py # KNN few-shot selection
├── verification/
│ ├── temporal_verifier.py # Kripke + CTL model checking
│ ├── conformal.py # Conformal prediction intervals
│ └── proof_engine.py # Z3 proofs
├── execution/
│ ├── tracer.py # State serialization (time-travel debug)
│ └── sandbox.py # Safe math execution (AST validated)
├── memory/
│ ├── trajectory_cache.py # Subgraph isomorphism cache
│ └── pruner.py # Context window optimization
└── consensus/
└── auto_vote.py # Multi-run extraction with voting
pip install git+https://github.com/munshi007/Aura-State.git
Python 3.10+ 필요. 의존성: pydantic, instructor, openai, networkx, pyModelChecking, z3-solver, pyyaml.
python -m pytest tests/ -v
# 65 tests passing
MIT