Formal Methods

Recent Signals

• 2026-07-25
• 의미: LLM reasoning을 기계적으로 검증 가능한 증명/형식 시스템과 연결하려는 흐름입니다.
• 팔로업: Lean 같은 형식언어에서 실제 proof success rate와 agent loop 설계를 확인해야 합니다.
• Euclid-MCP: A Model Context Protocol Server for Deterministic Logical Reasoning via Prolog (arXiv cs.AI)
• Agentic coding without the cloud: evaluating open-weight large language models on longitudinal data preparation tasks (arXiv cs.AI)