Mikhail-Balari/Ledge

GitHub: Mikhail-Balari/Ledge

Ledge 是一个实验性的 DSL 和运行时,通过静态类型检查和哈希链审计日志,强制开发者在 AI 输出进入业务决策前显式处理不确定性。

Stars: 0 | Forks: 0

# Ledge [![PyPI version](https://img.shields.io/pypi/v/ledge-lang.svg)](https://pypi.org/project/ledge-lang/) [![CI](https://static.pigsec.cn/wp-content/uploads/repos/2026/06/41c63db6cf183308.svg)](https://github.com/Mikhail-Balari/Ledge/actions/workflows/ci.yml) [![License: MIT](https://img.shields.io/badge/license-MIT-blue.svg)](LICENSE) ![Status: alpha / experimental](https://img.shields.io/badge/status-alpha%20%2F%20experimental-orange) **Ledge 是一个实验性的 runtime 和 DSL,用于可审计的 AI 决策边界。** 它并不能证明一个模型是正确的。它有助于在未经检查的 AI 不确定性变成实际行动之前,使其变得可见、可执行和可审计。Ledge 在 AI 调用周围环绕了一个静态分析过程,该过程拒绝直接使用尚未检查置信度的结果,将 AI 决策记录在哈希链审计日志中,随时间推移将声明的置信度与实际结果进行比较,并可以在 AI 输出跨越进入业务行动之前附加结构化的置信度证据。Ledge 1.7.0 Alpha 添加了用于语义 AI 决策边界事件的防篡改决策账本:本地追加导向的记录,以及用于检查不确定的 AI 输出如何成为(或被阻止成为)系统操作的验证、导出和 AI 可读的审查包。 Ledge 是 alpha 软件。它不是 AI 模型,不是形式化验证系统,不是合规产品,也不能替代评估、监控或人工审查。其他所有事情都使用正常的 Python 和你正常的技术栈;仅在 AI 输出可能成为决策或操作的边界处使用 Ledge。请参阅[限制和非目标](#limitations-and-non-goals)。 ## 一段话契约 Ledge 并不证明 AI 输出是正确的。置信度并不等于正确性。Ledge 所做的是静态拒绝直接使用类型为 `Uncertain[T]` 的值,除非它通过了该语言认可的几种处理结构之一:置信度守卫(`if confidence_of(x) >= t:` 或 `if is_confident(x):`),运行时检查的提取(`when(x, t, fallback)`),或者显式的 `unsafe_value_of(x)` 逃生舱。静态检查器是一个单文件、流敏感的 AST 遍历器,具有文档化的限制(过程内、对反转/提前返回的守卫持保守态度、除了单个 `define c as confidence_of(x)` 模式外没有别名分析)。运行时将每次 AI 调用记录在 SHA-256 链式审计日志中,并锚定到外部文件,以便可以检测到删除和重建攻击。这一切都不能证明关于模型的任何事情;它只是让“我忘记检查了”变成一个静态错误。 ## 这不是什么 - **不是形式化验证系统。** 没有机械化的健全性定理。静态检查器是一个 AST 遍历器,具有下面列出的限制。 - **不是校准的不确定性框架。** 后端置信度得分(OpenAI logprobs,Anthropic 结构化自我评估)是信号,而不是经过校准的正确性概率。校准必须经过测量。 - **不能替代评估、监控或人工审查。** - **不是法律合规产品。** 监管导出旨在支持结构化的证据审查,但并不能确立合规性。它是否对任何特定制度有用,取决于你和你的律师。 - **不是防篡改、防审计、不可变的存储或区块链。** 决策账本是本地追加导向的记录加上验证;它本身并不是安全的存储。 - **不是抵御恶意本地操作员的安全边界。** 审计追踪可以检测到拥有 DB 访问权限但没有锚文件访问权限的攻击者所进行的事后修改;同时拥有两者的攻击者可以伪造干净的历史记录。 - **不是 Python 的通用替代品。** 其他所有事情都使用 Python;仅在做出 AI 决策的层使用 Ledge。 ## 2 分钟内安装并运行 从 PyPI: ``` pip install ledge-lang==1.7.0 ledge demo ledge demo medical_triage ledge demo loan_approval ledge pilot-dry-run loan_approval ledge python-integration-demo ``` 从源代码检出: ``` python scripts/run_pilot_dry_run.py pilot_templates/loan_approval python examples/python_integration/app.py python scripts/ledge_check_ci.py ledge_lang/demos examples/python_integration ``` 预期输出(无 API key,无 clone,无 setup): ``` === MEDICAL TRIAGE DEMO === PATIENT P001: ESCALATE TO HUMAN (confidence=0) PATIENT P002: ESCALATE TO HUMAN (confidence=0) PATIENT P003: ESCALATE TO HUMAN (confidence=0) Decisions logged in audit trail: 3 Cryptographic chain intact: true ``` 如果没有连接真实的 AI 后端,每个患者都会被升级到人工审查——这就是安全失败的默认设置。连接真实的后端,它将使用后端提供的置信度估计进行分类。 要查看捆绑演示在源代码中的形式: ``` python -c "from ledge_lang import demos; print(open(demos.demo_path('medical_triage')).read())" ``` 要运行最清晰的以安全为导向的展示示例,目前你需要 clone 该存储库: ``` git clone https://github.com/Mikhail-Balari/Ledge cd Ledge ledge run examples/showcase/loan_approval.ledge ledge run examples/showcase/medical_triage.ledge ``` `examples/showcase/financial_analysis.ledge` 是一个混合了确定性和 AI 的示例:即使 AI 历史置信度为 0,债务比率规则也可能产生初步的基于规则的决策,并且输出会标出这种区别。 捆绑的 `loan_approval` 演示是合成的。它不是信用模型,也不是贷款决策系统。它演示了确定性规则检查、置信度控制的 AI 使用、人工审查回退和审计链验证。 `ledge run` 在执行前运行静态 Uncertain 检查器。如果你是故意尝试未检查的提取,请使用 `ledge run program.ledge --unsafe` 绕过检查器。 Python API 注意:`from ledge_lang import checked_run` 是安全门控的编程执行助手。它在执行前运行相同的静态检查器,如果发现类型问题,将抛出 `LedgeError` 而不执行程序。`from ledge_lang import run` 仍然是用于解释器和测试工具使用的低级直接执行 API;它在设计上绕过了静态检查器。 Python SDK 核心:`from ledge_lang.sdk import Uncertain, DecisionPolicy` 提供了一个最小化的 alpha SDK 表面,用于在正常的 Python 代码中对不确定值和决策策略进行建模。这并不能替代 DSL 静态检查器。它是 API 级别和 runtime 级别的处理。Ledge 1.5.0 Alpha 添加了 `ledge lint-python`,用于对常见的危险 Python 决策边界模式进行基于 AST 的 CI 强制执行。Ledge 1.6.0 Alpha 添加了置信度证据引擎:在 AI 输出跨越进入业务行动之前,为置信度得分提供结构化的、感知脱敏的、可哈希的证据。Ledge 1.7.0 Alpha 添加了用于语义决策边界事件、验证、本地审计审查导出包、AI 可读审查包以及面向 SDK 的记录助手的防篡改决策账本。它不提供完整的 Python 语义验证、完整的跨文件/过程间数据流分析、真值保证、防止幻觉、法律合规、生产就绪、企业就绪、防篡改存储、审计保证、不可变存储或区块链。 参见 [`examples/sdk_decision_boundary`](examples/sdk_decision_boundary/) 和 [`examples/confidence`](examples/confidence/)。有关端到端的账本工作流,请参见 [`examples/ledger`](examples/ledger/)。 对于安装包后的极简 Python 集成和 CI 检查器示例: ``` ledge python-integration-demo ledge ci-check path/to/your/ledge/files ledge lint-python path/to/your/python/files --config ledge.toml ``` 在源代码检出中,包装器和存储库路径的 CI 检查仍然可用: ``` python examples/python_integration/app.py python scripts/ledge_check_ci.py ledge_lang/demos examples/python_integration ledge ci-check ledge_lang/demos examples/python_integration ledge lint-python examples/python_linter --config examples/python_linter/ledge.toml ``` 使用存储库 fixture 文件的置信度证据引擎示例也需要源代码检出,以便 `examples/confidence/` 可用: ``` ledge confidence-eval examples/confidence/fixture.json ledge confidence-eval examples/confidence/fixture.json --format json ledge calibration-report examples/confidence/outcomes.json ledge calibration-report examples/confidence/outcomes.json --format json ``` 使用存储库路径的决策账本示例也需要源代码检出,以便 `examples/ledger/` 可用: ``` python examples/ledger/sdk_decision_result_to_ledger.py ledge ledger-verify --store examples/ledger/out/support_ticket_ledger.jsonl --manifest examples/ledger/out/ledger_manifest.json ledge ledger-export --store examples/ledger/out/support_ticket_ledger.jsonl --manifest examples/ledger/out/ledger_manifest.json --out examples/ledger/out/audit_export --force ledge ledger-review-pack --store examples/ledger/out/support_ticket_ledger.jsonl --manifest examples/ledger/out/ledger_manifest.json --out examples/ledger/out/ai_review_pack.json --force ``` 有关详细的检查器契约,请参见 [`docs/STATIC_CHECKER.md`](docs/STATIC_CHECKER.md)。 有关 Python 集成指南,请参见 [`docs/PYTHON_INTEGRATION.md`](docs/PYTHON_INTEGRATION.md)。 有关在正常 Python 中的 SDK 级别不确定值,请参见 [`examples/sdk_decision_boundary`](examples/sdk_decision_boundary/)。 有关当前和未来的不确定性语义,请参见 [`docs/UNCERTAINTY_MODEL.md`](docs/UNCERTAINTY_MODEL.md)。 有关置信度证据记录、信号生成、报告和限制,请参见 [`docs/CONFIDENCE_EVIDENCE_ENGINE.md`](docs/CONFIDENCE_EVIDENCE_ENGINE.md)。 有关防篡改决策账本、schema、验证契约、SDK 集成和限制,请参见 [`docs/DECISION_LEDGER.md`](docs/DECISION_LEDGER.md)。 有关部署假设和非目标,请参见 [`docs/THREAT_MODEL.md`](docs/THREAT_MODEL.md)。 有关未来的审计锚定设计,请参见 [`docs/AUDIT_ANCHORING.md`](docs/AUDIT_ANCHORING.md)。 有关从 alpha 软件走向生产关键型就绪的路径,请参见 [`docs/ROADMAP.md`](docs/ROADMAP.md)。 有关简短的技术审查路径,请参见 [`EXPERT_REVIEW.md`](EXPERT_REVIEW.md)。 有关演示和试点计划材料,请参见 [`DEMO.md`](DEMO.md)、[`COMMERCIAL.md`](COMMERCIAL.md) 和 [`PILOT_PACK.md`](PILOT_PACK.md)。 对于安装包后的合成试点试运行: ``` ledge pilot-dry-run loan_approval ``` 在源代码检出中,包装器仍然可用: ``` python scripts/run_pilot_dry_run.py pilot_templates/loan_approval ``` ## Ledge 的适用位置 Ledge 属于 AI 或模型输出可以成为业务操作的边界:批准、拒绝、升级、计费、退款、路由、写入、发布或触发工具/API。它目前适用于演示、概念验证和影子模式试点,其目标是使不确定性处理变得明确且可审查。 生产关键型或受监管的使用需要额外的集成、安全审查、监控、校准、操作测试、法律/合规审查以及适合该领域的人工监督。Ledge 是围绕一个决策边界的一种控制措施,而不是一个完整的治理系统。 ## 检查器的契约,精确版 类型为 `Uncertain[T]` 的值(由 `analyze`、`classify`、`generate`、`ask`、`embed` 返回)不能直接使用。检查器接受以下形式: ``` define r as classify(symptoms) using ["urgent", "routine"] # (1) 置信度防护 —— 识别出的缩窄模式: if confidence_of(r) >= 0.85: show value_of(r) # OK inside this block if is_confident(r): show value_of(r) # OK inside this block # (2) 别名感知防护(检查器会记住别名): define c as confidence_of(r) if c >= 0.85: show value_of(r) # OK inside this block # (3) 带有 fallback 的运行时检查提取: show when(r, 0.85, "fallback for low-confidence") # (4) 显式逃生舱 —— 故意起的难看名字: show unsafe_value_of(r) # OK anywhere; reader is warned ``` 检查器拒绝以下情况: ``` define r as classify(symptoms) using ["urgent", "routine"] show r # ERROR: unsafe use of Uncertain show value_of(r) # ERROR: value_of outside guard show upper(r) # ERROR: Uncertain in function call define x: text as r # ERROR: Uncertain to typed var ``` 这是核心的强制执行。其他一切——审计追踪、校准、监管导出——都是支持性基础设施。 ## 你可以在终端中验证的四个属性 自己运行这些。无需 API key。无需设置。不到 5 分钟。每个演示都是一个运行某项 runtime 行为的小型 Python 脚本;该脚本会打印出自己的通过/失败状态。 ### G1 -- 没有后端时的零置信度 ``` python demo_guarantee1.py ``` 如果没有连接真实的模型,每个 AI 原语都会返回 `confidence = 0.0`。系统无法虚构确定性。这是一个 runtime 属性,而不是静态属性。 ### G2 -- 危险的使用在执行前被拒绝 ``` python demo_guarantee2.py ``` 静态分析器在任何代码运行之前就会拒绝 `Uncertain[T]` 的危险使用(参见上面的契约)。如果检查器本身崩溃,它会抛出带有堆栈跟踪的 `TypecheckerInternalError`,而不是返回空的结果列表。 ### G3 -- 带有外部锚点的哈希链审计追踪 ``` python demo_guarantee3.py ``` 每个 AI 决策都使用 SHA-256 哈希链进行记录。更改任何字段(置信度、时间戳、操作)都会破坏链条。外部锚文件(`~/.ledge/anchors.jsonl`)每 10 次决策记录一次链状态;如果 SQLite 数据库被删除并重建,锚点将检测到不连续性。 **威胁模型。** 这可以检测到能够读/写 SQLite 存储但不能访问锚文件的操作者所进行的事后修改。控制数据库和锚文件的攻击者可以伪造干净的历史记录。这无法抵御控制这两个文件的恶意本地操作员。有关完整的威胁模型,请参见 `GUARANTEES.md`。 ``` ledge audit --verify-anchors # cross-check anchor file against the store ``` ### G4 -- 未配置后端时的安全失败 ``` python demo_guarantee4.py ``` G1 的一个后果:没有后端时,`confidence = 0.0`,因此任何 `> 0.0` 的决策阈值都会导致系统升级。它不会根据虚构的确定性采取行动。 ## 置信度并不等于正确性 Ledge 不信任置信度得分。它会记录它们,并随着时间的推移将它们与实际结果进行比较。 每个后端的置信度来源: ``` # OpenAI:基于分类标签的 token 对数概率,被用作 # 基于 token 概率推导出的置信度估计。对以下因素敏感: # - 首 token 分类(多 token 标签会优雅降级) # - top-logprob 截断(低概率标签会从列表中掉落) # - prompt 表述和标签顺序 # - 模型特定行为(gpt-4o-mini 与 gpt-4o 存在差异) # - 随着提供商更新模型,随时间推移产生的漂移 # 这些都是信号。它们不是经过校准的正确性概率。 backend = openai_backend(api_key="sk-...", model="gpt-4o-mini") # Anthropic:结构化自我评估 —— 模型在给出答案的同时返回一个置信度 # 分数。这是自我报告的,并非从 # 模型权重或 token 概率推导得出。 backend = anthropic_backend(api_key="sk-ant-...", model="claude-3-haiku-20240307") ``` 将两者都视为校准的输入,而不是基准事实。校准层(下面的第 3 层)测量每个模型和领域的实际准确率: ``` ledge audit --calibration gpt-4 medical ledge audit --calibration-metrics gpt-4 medical ``` ``` Calibration Report: gpt-4 / medical (n=30) RANGE COUNT MEAN_CONF ACCURACY CAL_ERROR 0.8-0.9 20 0.848 0.850 0.002 0.9-1.0 10 0.924 0.700 0.224 <- overconfident Brier score : 0.1711 (lower is better; 0.0 is perfect) ECE : 0.0756 (lower is better; <0.10 is a rough heuristic) False accept rate : 0.1429 (accepted when wrong) False reject rate : 0.7826 (rejected when right) Calibrated threshold: 0.921 (provisional -- only 10 samples > 0.9) Well calibrated : False (overconfident in 0.9-1.0 range) ``` 有关最小样本要求(默认 30)、自我报告结果的注意事项以及漂移处理,请参见 [CALIBRATION_GUIDE.md](CALIBRATION_GUIDE.md)。 ## 各个部分是如何组合在一起的 ``` Uncertain output -> static check -> logged decision -> recorded outcome -> calibrated threshold -> safer future decision ``` **多步链。** 置信度在推理步骤中会降低。如果每一步的置信度都是 0.85,那么五步之后的结果是 `0.85^5 = 0.44`。`chain_confidence()` 内置函数应用位置加权衰减并对弱步骤进行惩罚;其结果是该链的一个传播置信度值,受制于与任何其他 Uncertain 值相同的处理规则。 **第 1 层 -- 执行前静态检查。** 直接使用 `Uncertain[T]` 会被拒绝。(参见上面的*检查器契约*。) **第 2 层 -- Runtime 置信度来源。** 置信度来自你连接的后端;如果没有后端,它确切地说是 0.0。`AIDerived` 包装器通过提取保留了 AI 原始来源,因此调用者仍然可以检测到它。 **第 3 层 -- 领域准。** 测量每个模型和领域的实际准确率。校准阈值是根据观察到的结果计算出来的,而不是根据后端自己的置信度声明。如果样本量低于 `min_samples`(默认 30),则回退到默认的 0.85 并发出警告。 **第 4 层 -- 自适应阈值 API。** ``` from ledge_lang.calibration import DomainCalibrator threshold = calibrator.get_calibrated_threshold( 'gpt-4', 'medical', desired_accuracy=0.90, min_samples=30 ) ``` **第 5 层 -- 结构化证据导出。** JSON-LD 输出旨在支持 AI 日志记录、监控和透明度工作的结构化证据审查。生成导出并不能在任何司法管辖区建立法律合规性;这需要由合格的法律顾问进行适当的审查。 ``` ledge audit --export-regulatory report.json ledge audit --validate-regulatory report.json ``` ## 为什么选择 DSL 加 SDK,而不是仅仅使用 Python 库、mypy 插件、Pyright 插件、linter 或框架? 直截了当的版本,没有夸大的声明。 **普通的 Python 库**可以帮助团队对不确定性进行建模、应用策略,并使决策处理变得明确。这就是为什么 Ledge 现在包含一个 Python SDK 核心。但是,仅靠一个库并不能阻止开发者忘记使用它、绕过它,或者直接将不确定的值传递到操作路径中。 **Ledge DSL** 的存在是为了应对更严格的情况:一个更小、受控的表面,在这里危险的提取可以在 runtime 之前变成一个静态错误。 **mypy 或 Pyright 插件**可以在正常的 Python 中覆盖这个问题的一部分,特别是围绕 `Uncertain[T]`。这条路径很有价值,但它仍然依赖于插件的安装、项目的配置,以及通过 Python 的类型系统表达置信度守卫提取的局限性。 **linter** 可以捕获 Python 代码中明显的不安全模式。Ledge 包含了 `ledge lint-python`,用于基于 AST 的 CI 强制执行常见的不安全 SDK 决策边界模式。其局限性在于 linter 主要是通过语法和约定来工作,因此跨文件流、过程间流、别名和框架特定的行为需要谨慎处理。 **框架或 SDK** 可以要求特定的类和方法签名。当团队一致采用该 SDK 或框架时,这会非常有效。Ledge 的 SDK 遵循这条路径进行采用和集成,而 DSL 仍然是更严格的边界层。 **Ledge 实际上为你带来的是这种组合。** 一个用于最受控决策边界层的 DSL,一个用于正常应用程序集成的 Python SDK,用于常见 Python 不安全使用模式的基于 AST 的 CI 强制执行,以及通往更丰富证据捕获的路线图。权衡是诚实的:DSL 是一个新的表面,目前还没有广泛的生态系统,而 SDK 和 linter 更容易采用,但本身无法提供完整的语义验证。 ### 相关工作和相邻工具 这些项目相关且有用;Ledge 并不能替代它们。 - [Model Context Protocol](https://modelcontextprotocol.io/) 标准化了 AI 应用程序如何公开和使用工具、资源和上下文。Ledge 专注于 AI 结果进入决策流程之后的程序边界。 - [Guardrails AI](https://guardrailsai.com/docs) 和 [NVIDIA NeMo Guardrails](https://docs.nvidia.com/nemo/guardrails/latest/) 提供了用于验证或约束模型行为的护栏框架。Ledge 较窄的实验是使代码中的不确定结果变得明确,并在执行前拒绝未检查的使用。 - [LangChain](https://docs.langchain.com/) 和 [LangGraph](https://docs.langchain.com/oss/python/langgraph) 有助于构建 LLM 应用程序和 agent 工作流。Ledge 可以位于决策边界;它不是一个编排框架。 - [mypy](https://mypy.readthedocs.io/) 和 [Pyright](https://microsoft.github.io/pyright/#/) 是 Python 类型检查器;[Ruff](https://docs.astral.sh/ruff/) 和 [Pylint](https://pylint.pycqa.org/) 是 Python 代码检查/静态分析工具。成熟的 Python 插件或 linter 可以覆盖这个领域的部分内容。Ledge 测试了一个较小的 DSL 表面,其中 `Uncertain[T]` 和置信度守卫内置在检查的执行路径中。 - 结构化输出和 schema 验证,例如 [OpenAI Structured Outputs](https://platform.openai.com/docs/guides/structured-outputs) 和 [JSON Schema](https://json-schema.org/),有助于确保输出具有预期的形状。Ledge 解决的是另一个不同的问题:程序是否被允许在不检查置信度并记录决策路径的情况下使用 AI 派生的值。 当前的实验是将 AI 输出表示为 `Uncertain[T]`,在执行前拒绝未检查的使用,并将决策与审计和校准证据联系起来。这里并没有声称自己是首创、独特或革命性的。 **什么时候你不应该使用 Ledge。** 如果你的团队已经有了一套关于不确定性处理的有效规范;如果你的 AI 调用足够隔离,以至于 linter 或轻量级包装库就足够了;如果你的技术栈限制使得单独的语言层变得不可接受;如果你需要生产级的工具、IDE 支持或生态系统成熟度。Ledge 是一个实验,而不是基础设施。 ## 限制和非目标 Ledge 没有声称的事情,并预先解决了最常见的技术异议。 **Ledge 能证明 AI 的答案是正确的吗?** 不能。它只拒绝特定语法模式的未检查使用。 **高置信度意味着答案是正确的吗?** 不是。后端置信度得分是信号,而不是校准过的概率。校准层的存在是为了测量声明的准确率和观察到的准确率之间的差距。 **它能防止对不确定值的所有误用吗?** 仅根据已实现的检查器规则。请参阅下面的*已知检查器限制*。 **这是一个完整的形式化类型系统吗?** 不是。它是一个单文件、流敏感的 AST 分析。没有机械化的健全性定理,也没有声称这些规则构成了一个健全或完整的系统。 **审计追踪对恶意管理员是不可变的吗?** 不是。哈希链加上外部锚文件可以检测到具有 DB 访问权限但没有锚访问权限的攻击者所做的修改。控制这两者的攻击者可以伪造干净的历史记录。 **它会取代评估、校准监控或人工审查吗?** 不会。校准很有帮助,但不能替代评估、行为测试,或者在错误答案成本很高的情况下的回路中的人工干预。 **它能保证符合 EU AI Act、GDPR、HIPAA 或任何其他合规要求吗?** 不能。监管导出旨在支持结构化的证据审查,但它并不能确立合规性。任何特定司法管辖区的合规性都需要法律顾问。 **为什么不直接使用 Python + mypy/Pyright?** 参见上面的*为什么选择 DSL 加 SDK* —— 这对于许多团队来说是一个合理的选择。Ledge 将一个可采用的 Python SDK 与一个更窄的 DSL 边界配对,适用于需要更严格检查执行的情况。 ### 已知的检查器限制 这些是静态分析过程的局限性,而不是 bug: - **仅限过程内。** 检查器在函数体内追踪 Uncertain。它不会跨函数边界追踪值。在边界处会尊重标记为 `uncertain[T]` 的函数参数/返回值;`AIDerived` runtime 包装器通过提取保留了 AI 的来源。 - **对提前返回的守卫持保守态度。** 诸如 `if confidence_of(x) < t: return; use(x)` 之类的模式目前不被识别为缩小了块的其余部分。请使用 `if ... >= t: ... else:` 形式,或者如果你已经通过带外方式满足了要求,请使用 `unsafe_value_of(x)`。 - **没有 `not is_uncertain(x)`。** 只有肯定的形式(`is_confident(x)`,`confidence_of(x) >= t`)被识别为缩小范围。 - **除了单个 `define c as confidence_of(x)` 之外没有别名分析。** 更复杂的别名(例如,通过 map 读取置信度)不会被缩小范围。 - **没有 lambda 流程缩小。** 在 lambda 主体内的置信度检查不会为后续表达式缩小 lambda 参数的范围。 - **`map(...)` 中的 lambda 会传播内部的 Uncertain。** `list[uncertain[T]]` 会被识别,并且对这种列表的迭代会触发相同的检查。可能无法识别更复杂的高阶模式。 如果你遇到了检查器应该识别但却没有识别的情况,请提交一个 issue。 ## Ledge 与现有工作的关系 **Turn** -- Kizito, 2024 ([arxiv:2603.08755](https://arxiv.org/abs/2603.08755)) 将类型化的 LLM 推理作为带有置信度操作符的语言原语,专为 LLM 编写代码的 agentic 系统而设计。Ledge 面向构建*使用* LLM 的系统的开发者,并增加了领域校准、结果追踪和链式审计追踪。 **QUASAR** -- 2025 ([arxiv:2506.12202](https://arxiv.org/abs/2506.12202) | [OpenReview](https://openreview.net/forum?id=TvpaeQVTGQ)) 一种用于 LLM 代码操作的语言,通过共形预测进行不确定性量化,从 LLM 编写的 Python 转译而来。Ledge 由开发者编写,并在静态分析时强制执行处理。QUASAR 的不确定性基于共形预测理论;Ledge 的校准是经验性的。 **IMMACULATE** -- Guo et al., 2026 ([arxiv:2602.22700](https://arxiv.org/abs/2602.22700)) 审计 LLM API 提供商是否执行了他们声称的模型。Ledge 审计*使用*这些模型的代码是否安全地处理了它们的输出。互补关系。 **SAUP** -- Zhao et al., 2024 ([arxiv:2412.01033](https://arxiv.org/abs/2412.01033)) 在 runtime 使用情境权重,通过多步 LLM agent 推理传播不确定性。Ledge 在语言级别(`chain_confidence()`)实现了传递性不确定性传播(位置加权衰减、弱步骤惩罚),并将其呈现给静态检查器。 如果你知道我们遗漏的相关工作,请提交一个 issue。 ## 安全模型 没有 Python 的 `eval()` 或 `exec()`。Ledge 使用自定义的树遍历解释器,因此 Python 的对象内省逃逸路径不适用。 在安全模式下,默认阻止 Python FFI 导入: ``` ledge run program.ledge --safe-mode # block all imports + cap iterations ledge run program.ledge --allow-import=math,json # whitelist specific modules ``` 这些执行标志仍然会首先运行静态检查器。仅当你明确希望跳过 Uncertain 契约检查时,才添加 `--unsafe`。 对于用户提交 Ledge 代码的服务器部署,请在 Docker 或类似的操作系统级别隔离内运行。`--safe-mode` 不能替代它。 ## 测试 ``` python tests/conformance.py # 284/284 passed python -m pytest tests/unit/ # 373 passed ``` 测试计数会随时间变化。一致性测试工具和单元套件是事实来源。 ## 常见问题 **这是为谁准备的?** 为在生产中使用 AI 模型构建系统的开发者准备,特别是在受监管的行业中,“我忘记检查置信度”是一种真实的失败模式。 **它会替代 Python 吗?** 不会。Ledge 用于做出 AI 决策的层。其他所有内容都保留在你现有的语言中。 **置信度得分实际上准确吗?** 不准确。校准层测量的是它随着时间的推移以及在您的数据上的准确程度。参见 [CALIBRATION_GUIDE.md](CALIBRATION_GUIDE.md)。 **审计追踪在法律上可以接受吗?** 导出可以支持结构化的证据审查,但它并不能确立法律合规性。它是否对特定流程有用,由你的法律顾问决定。 **我可以将此用于生产关键型决策吗?** 还不能。它是一个具有可检查 runtime 属性的工作原型。 今天可用的功能: - 上面的静态契约(由 `tests/unit/test_typechecker.py` 中的测试强制执行) - 带有外部锚点验证的哈希链审计追踪 - 使用 token 对数概率作为置信度的 OpenAI 后端 - 具有 Brier score、ECE 和错误接受/拒绝率的领域校准 - 具有弱步骤惩罚的位置加权链式置信度 - 用于证据审查的结构化监管导出 不可用的功能: - 分布式审计存储 - 成熟的包生态系统 - 已知的生产部署 - 除了捆绑的 LSP server 之外的 IDE 工具 - 类型规则的机械化证明 **零生产部署——我为什么要信任这个?** 你不应该。你应该去验证它。本文档中的每个属性都可以在 5 分钟内检查完毕,无需 API key。这些属性在你运行它们时要么成立,要么不成立。 ## License MIT ## 问题和反馈 如果某些东西损坏了,某个声明不成立,或者你知道有现有的工作做得更好——请提交一个 issue。如果你在一个真实的系统中使用 Ledge,即使是实验性的,我们也想听到关于它的反馈。
标签:AI安全与合规, DSL领域特定语言, Python, 云安全监控, 人工智能, 可靠性设计, 审计日志, 无后门, 用户模式Hook绕过, 自动化payload嵌入, 逆向工具, 静态分析