构建可验证的跨语言程序翻译系统，确保答案可信且可追溯。
Untrusted Authors, Trusted Answers: A Calculus of Fidelity-Graded Translations
- 用图形化计算模型描述翻译过程，支持逐层合约组合与验证。
- 在July 2026快照中实现构造级覆盖率达98%，双路径分支一致率超95%。
- 适合需高可靠性验证的LLM辅助编程场景，尤其适用于形式化检查需求。
为回答程序相关问题，将程序移至问题可判定的位置——每一次移动即为一次翻译，而每次翻译都可能出错。本文将翻译视为图结构：多种语言、少数推理目标，各自独立构建信任度不同的路径。提出一套计算体系：近似交换方阵对，具有方向性（精确性是过近似的一种特例），每条程序可验证且可组合；路径的契约由各跳契约的分量交集决定——包括保证等级、方向、保留可观测性及测量成本。一个不对称机制组织信任：携带证明的答案可在源端回放自证；通用答案则通过等级、独立分支和重新验证的证书来证明其代价。组合核心包含松弛望远镜，在Lean 4中机械化实现。hurdy-gurdy以两平面交汇于一注册表的形式实现该体系：使用平面读取声明并生成带证据的回答，其构建者与目标用户均为不被信任的LLM；演化平面扩展图谱：未满足的问题记为需求，基于证据推荐配对并由人工注册，棘轮机制确保所有先前判决永久有效。答案从不写入；演化从不回答。无限运行下，系统收敛于所有可约简判定的问题，且保真度持续提升。我们测量了2026年7月快照数据：构造级联合覆盖率、两条路径对两个ISA的一致性、源码级证明回放、经形式化验证检查器复核的不可达性、门控逃逸率，并报告了架构自身发现的作者代码缺陷。
原文摘要 · Abstract (English)
To answer a question about a program, move the program to where the question is decidable. Every such move is a translation, and every translation is a place to be wrong. We study translation as a graph -- many languages, a few reasoning targets, independently built routes of honestly different trustworthiness -- and give it a calculus: pairs of languages close commuting squares that are directional (exactness is the identity-embedding special case of over-approximation), checkable per program, and composable, a route's contract being the componentwise meet of its hops' contracts -- assurance class, direction, kept observables, measured cost. One asymmetry organizes trust: witness-carrying answers are self-certifying by replay at the source; universal answers are where grades, independent branches, and re-checked certificates earn their cost. The compositional core, lax telescope included, is mechanized in Lean 4. hurdy-gurdy implements the calculus as two planes meeting in one registry. The use plane reads declarations and produces evidence-carrying answers; its builders and its intended player are both LLMs, untrusted by construction. The evolution plane grows the graph: unmet questions are recorded as demand, pairs are recommended by evidence and registered by humans, and a ratchet keeps every prior verdict standing. Answers never write; growth never answers. Run indefinitely, the loop converges on every reducibly decidable question, at fidelity that only rises. We measure the July 2026 snapshot -- per-construct conjoined coverage, dual-route branch agreement for two ISAs, source-level witness replay, certified unreachability re-validated by a formally verified checker, escape rates for the gate itself -- and report the defects the architecture caught in its own authors' work.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。