将eval从语言原语改为受控执行,提升AI系统安全性
Governed Metaprogramming for Intelligent Systems: Reclassifying Eval as a Governed Effect
- 程序结构作为一等值,执行前需经权限与资源审查
- 通过形式化判断确保代码转换不绕过安全检查
- 适用于需要可验证、可审计的智能系统开发
AI系统在运行时越来越多地动态生成可执行结构:大模型生成代码,智能体构建工作流,自进化系统修改自身行为。在传统同像性和分阶段语言中,代码表示到执行的转换是无限制的,eval作为语言原语,并非受控操作。我们认为,在受控智能系统中,这一转换实为权限放大:将符号结构转化为可执行权限,必须像其他效应一样受到中介控制。我们提出受控元编程,一种语言设计,其中程序表示(机器形式)为一等值,形式操作为纯计算,而材料化(从形式到可执行机器的转换)是受控效应,须经过结构检查。治理系统在允许执行前分析程序的能力需求、策略合规性及资源估算。我们形式化两种判断:纯形式评估(不发出指令)和受控材料化(仅发出一个受控指令)。证明了三个性质:形式操作的纯净性、无绕过定理和边界保持性。我们在mashinTalk中实现该设计,这是一个编译为BEAM字节码的AI工作流领域特定语言,并报告了与454个已验证Rocq定理的集成。核心贡献是将eval重新归类为受控效应。
原文摘要 · Abstract (English)
AI systems increasingly synthesize executable structure at runtime: LLMs generate programs, agents construct workflows,self-improving systems modify their own behavior. In classical homoiconic and staged languages, the transition from code representation to execution is unrestricted. eval is a language primitive, not a governed operation. We argue that in governed intelligent systems, this transition is an authority amplification: it converts symbolic structure into executable authority and must be mediated like any other effect. We present governed metaprogramming, a language design where program representations (machine forms) are first-class values, form manipulation is pure computation, and materialization (the transition from form to executable machine) is a governed effect subject to structural inspection. The governance system analyzes the proposed program's capability requirements, policy compliance, and resource estimates before permitting execution. We formalize two judgments: pure form evaluation (which emits no directives) and governed materialization (which emits exactly one governed directive). We prove three properties: purity of form manipulation, the no-bypass theorem, and boundary preservation. We implement the design in mashinTalk, a DSL for AI workflows compiling to BEAM byte code, and report on integration with 454 existing machine-checked Rocq theorems. The central contribution is reclassifying eval from a language primitive into a governed effect.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。