发表机构
University of Salzburg; Czech Technical University（萨尔茨堡大学; 捷克技术大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究翻译问题，提出保真度分级翻译演算，该演算可按程序检查、通过粘贴组合，核心在Lean 4中机械化，在hurdy - gurdy平台实现，报告了多项实验结果，其增长模型通过任何人贡献语言对扩展语言支持。
AI 中文摘要
经过验证的翻译有两个经过充分研究的极端情况：一次性证明翻译器（经过认证的编译），或验证一个翻译器的每次运行（翻译验证）。两者都孤立地处理单个翻译。我们将翻译视为一个图——多种源语言、多个推理目标、多条独立构建的路径——其中对于“这个翻译正确吗？”的诚实答案因边而异。我们提出了一种保真度分级翻译演算：语言对接近可交换方块，可按程序检查并通过粘贴组合；声明的保真度等级按最弱链接组合，通过内联检查在每次运行时重新建立，并通过独立派生路径之间的一致性来超越；一个端到端定理分离出一个基本的不对称性——携带见证的答案在源处是自我认证的，而通用答案是等级、分支和证书产生成本的地方。组合核心在Lean 4中实现机械化。该演算在hurdy - gurdy中实现，hurdy - gurdy是一个围绕两个推理中心的包含13种语言和13对语言的平台，作为LLM生成正确性的双向实验构建：独立的LLM代理在很大程度上无监督地编写每一对语言，架构的交叉检查作为唯一的语义门，并且该平台的目标参与者本身就是一个LLM。所有代码以及本文的大部分内容都是由LLM生成的；人类的贡献是架构。相同的门是预期的增长模型：hurdy - gurdy通过任何人贡献的语言对（通过LLM、代理或手动）来扩展语言支持，这些语言对由架构而非作者身份认可。我们报告了联合覆盖、分支一致性、基于合规性推导的带有机器推导的基本事实的基准、见证重放、经过认证的不可达性以及针对该门的逃逸率实验。
英文摘要
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.
Comments29 pages. v2: rewritten on the two-plane principle; directional squares primary (exactness = the identity-embedding case, mechanized incl. the lax telescope); the answerability loop and its economy (demand books, recommended-then-registered); post-snapshot exhibits. Code, evidence, Lean mechanization: https://github.com/cksystemsgroup/hurdy-gurdy (tag arxiv.2)
