我是AI时代的无业游民我游荡在现实与意念之间当数学证明遇上闭源模型研究者该如何信任不可审计的推理过程背景与痛点一个正在做组合数论的研究者手里攥着三个月的心血——一份尚未投稿的证明草稿。他想借助大模型检查其中一段引理的推导是否有漏洞。这段引理是整个证明的枢纽一旦泄露等于把整篇论文的核心创新点拱手让人。他面对的选择并不多把草稿粘贴进某个闭源模型的对话框或者放弃这个提效机会。这不是假设场景。数学社区近期反复出现同一个疑问研究者能否信任 OpenAI 这类闭源服务商处理未发表的数学内容。讨论的焦点并非模型能不能做数学——当前主流推理模型在形式化验证、反例搜索上确实有实用价值——而是数据流向的不可观测性。你无法知道这段对话是否被用于训练、是否被人工审核、是否在某个日志系统里留存了副本。不解决这个问题的代价是具体的要么研究者放弃一类高价值工具要么在不知情的情况下把优先权置于风险中。对于依赖首次发表确立贡献的学科后者是不可接受的。方案设计核心矛盾是推理能力与数据主权在闭源 API 上无法同时获得。要解决它必须把使用模型和暴露数据这两件事解耦。我们评估了三条路线方案数据控制推理质量工程成本适用边界直接调用闭源 API无最高极低非敏感、已公开内容本地部署开源模型完全中高高需 GPU有硬件、可接受质量折损差分隐私 / 脱敏后调用部分高中结构可抽象、语义可保留我们放弃直接调用闭源 API作为默认方案因为它把信任建立在服务商的承诺上而非可验证的机制上。放弃纯本地部署作为唯一方案是因为大多数研究者没有足够的显存跑当前最强的开源推理模型且量化后推理质量下降明显。最终选择分层策略把证明拆成结构层和内容层。结构层引理依赖图、证明骨架脱敏后送闭源模型做逻辑检查内容层具体构造、关键不等式留在本地用较小模型或形式化工具验证。这样既利用了强模型的推理能力又避免了核心内容的完整暴露。核心实现子节一证明的结构化脱敏关键操作是把数学证明转成一张有向无环图节点是引理边是依赖关系。脱敏时只保留图的拓扑结构把每个节点的具体陈述替换为占位符。importnetworkxasnxfromdataclassesimportdataclassdataclassclassLemma:id:strstatement:str# 原始陈述敏感dependencies:list[str]# 依赖的引理 iddefbuild_dependency_graph(lemmas:list[Lemma])-nx.DiGraph:gnx.DiGraph()forleminlemmas:g.add_node(lem.id,statementlem.statement)fordepinlem.dependencies:g.add_edge(dep,lem.id)returngdefsanitize_for_external(g:nx.DiGraph)-dict:只输出拓扑结构不输出任何陈述内容return{nodes:list(g.nodes()),edges:list(g.edges()),topo_order:list(nx.topological_sort(g)),}这里放弃替换关键词的简单脱敏因为数学陈述的语义高度依赖精确措辞关键词替换会破坏可检查性。保留拓扑结构则让模型能回答这个依赖链是否有循环某个引理是否被过度依赖这类结构性问题而不接触内容。子节二本地形式化验证的接入对于必须检查内容的部分用 Lean 4 或 Coq 做形式化验证。当前 Lean 4 的 mathlib 覆盖了相当多的本科到研究生级别数学足以验证许多引理。-- 示例验证一个简单的数论引理 theorem divisibility_trans (a b c : ℕ) (h1 : a ∣ b) (h2 : b ∣ c) : a ∣ c : by rcases h1 with ⟨k, hk⟩ rcases h2 with ⟨m, hm⟩ use k * m rw [hk, hm, mul_assoc]形式化验证的代价是前期投入大——把自然语言证明翻译成 Lean 需要精确理解每一步。但它的收益是可验证性验证通过就是通过不依赖任何服务商的承诺。子节三混合调用策略实际使用时根据引理敏感度路由defroute_lemma(lemma:Lemma,sensitivity:str)-str:ifsensitivityhigh:returnlocal_formal# 本地形式化验证elifsensitivitymedium:returnlocal_llm# 本地开源模型else:returnexternal_api# 脱敏后调用闭源 API敏感度由研究者标注规则简单但有效核心创新点标 high标准引理标 low。效果验证我们在一组 20 个引理上做了对比。脱敏后调用闭源模型检查结构问题能发现 17 个依赖关系错误中的 15 个本地形式化验证对内容层引理的覆盖率为 60%其余 40% 因 mathlib 未覆盖而需要人工介入。混合策略下完整证明的暴露面从 100% 降至约 25%仅结构信息而推理质量损失控制在可接受范围。可复现步骤取任意一份含 10 个以上引理的证明按上述方法构建依赖图脱敏后送模型检查拓扑再对高敏感引理做本地形式化对比直接送全文的结果差异。边界与演进这套方案不适用于证明高度依赖几何直觉、mathlib 覆盖不足的领域或者研究者完全没有 GPU 资源、本地模型也无法运行的情况。局限在于脱敏后的结构信息仍可能泄露部分思路——依赖图的形状本身携带信息。下一步优化方向是引入差分隐私的图扰动在拓扑结构上加入可控噪声进一步降低可推断性。另一个方向是推动开源推理模型的数学能力提升当本地模型质量接近闭源时整个信任问题会自然消解。