基于人类编写的本体构建可审计、安全的智能体，确保决策可追溯且正确。
Provably Auditable and Safe LLM Agents from Human-Authored Ontologies
- 用类型化λ演算证明智能体在特定领域执行时语义正确。
- 所有决策记录在不可篡改的追加日志中，支持线性审计。
- 适用于医疗账单合规与安全漏洞披露，适合高风险场景使用。
我们提出一种名为 Agentic Redux 的大语言模型智能体架构，适用于需要线性审计的复杂问题领域。通过类型化λ演算，证明在适当领域运行时，Agentic Redux 的执行在语义上保证正确，所有决策均记录于不可篡改的追加日志中。本文展示了两个生产级适用领域：医疗账单合规与安全漏洞披露。配套代码仓库已公开，可在两个领域中运行 Agentic Redux。此外，我们提出「本体优先智能体设计」方法论：由人类专家使用基本形式本体（Basic Formal Ontology）对问题领域进行形式化建模，再将 LLM 分配以推导出人类与智能体可协作的角色，共同解决领域内问题。
原文摘要 · Abstract (English)
We introduce the LLM agent architecture Agentic Redux, intended for use with nontrivial problem domains that require linear auditability. Using the typed lambda calculus, we prove that, run on appropriate domains, Agentic Redux executions are semantically guaranteed to be correct, with all decisions recorded in an append-only ledger. We present two production-grade appropriate domains, in healthcare billing compliance, and security vulnerability disclosure. Working code for Agentic Redux run on both domains is available in a supporting code repository. We also introduce Ontology-First Agent Design, a methodology for creation of agent frameworks on a problem domain, in which a human expert ontologizes the problem domain with Basic Formal Ontology, and then assigns an LLM to derive roles that agents and humans-in-the-loop can fill, in order to work the problems in the domain.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。