AI 中文总结
本研究提出满足五项必要条件的Pistis智能体式证明搜索方法，通过OrderDecompose分治搜索生成欧几里得《几何原本》前三卷的忠实形式化Lean证明，其性能优于基线方法，可作为证明检查工具。
AI 中文摘要
在形式验证领域，语句的自动形式化与自动证明搜索均已得到广泛研究。自动证明搜索虽能生成可编译的形式化证明，但所生成的证明未必能反映自然语言论证得出结论的过程——我们将这一特性称为忠实性。借助忠实形式化的证明，人们可检验人类或AI所写论证背后的推理过程，并协助数学家形式化其证明草图。然而，由于形式化证明策略与自然语言推理存在错位，该任务极具挑战性。本研究严格定义了忠实形式化证明必须满足的五项必要条件，并引入Pistis——一种智能体式、神谕引导的证明搜索方法，可生成满足上述条件的Lean形式化证明。其核心是一种名为OrderDecompose的新型保忠实分治搜索，该方法会追踪引用依赖关系并阻止不忠实的捷径，同时搭配反驳搜索以揭示自然语言证明源中的漏洞与错误。OrderDecompose可完成基线方法在12小时预算内无法闭合的证明，且其生成的产物编译速度是过往工作的33倍以上。我们将Pistis应用于欧几里得《几何原本》的前三卷，生成包含忠实形式化证明的高质量产物。在盲法人类研究与基于严格 rubric 的LLM评审协议下，Pistis生成的证明相较于过往工作更受青睐——人类评审员与LLM评审员的偏好比例分别为2.89倍与5.2倍。此外，该方法还揭示了欧几里得证明及其翻译中的漏洞，且可对人类或AI撰写的自然语言证明进行接受或弃权（不执行）操作，表明忠实形式化可作为一种有用的证明检查工具。
英文摘要
In formal verification, both the autoformalization of statements and automated proof search have been studied extensively. While automated proof search can produce a formal proof that compiles, the generated proof does not necessarily reflect how the natural-language argument arrives at its conclusion--a property we refer to as faithfulness. With faithfully formalized proofs, one can check the reasoning behind a human- or AI-written argument, and assist mathematicians in formalizing their proof sketches. However, it is particularly challenging due to misalignment of formal proof tactics and natural language reasoning. In this work, we rigorously describe a set of five necessary conditions a faithful formal proof must satisfy, and introduce Pistis, an agentic, oracle-guided proof search that produces formal Lean proofs that satisfy them. At its core is a novel faithfulness-preserving divide-and-conquer search, which we name OrderDecompose, that tracks citation dependencies and blocks unfaithful shortcuts, paired with a refutation search, that surfaces gaps and errors in the natural language proof source. OrderDecompose completes proofs that baselines cannot close even within a 12-hour budget, and its artifacts compile over 33$\times$ as fast as prior work's. We apply Pistis on the first three books of Euclid's Elements, producing high-quality artifacts containing faithful formal proofs. Under a blinded human study and an LLM-as-a-judge protocol on rigorous rubrics, Pistis-generated proofs are favored over prior works--2.89$\times$ and 5.2$\times$ as often by human reviewers and the LLM judge, respectively. It further uncovers gaps in Euclid's proofs and their translation, and can accept or refute natural language proofs written by humans or AI, demonstrating that faithful formalization is useful as a proof-checking tool.
CommentsPreprint. 18 pages, 14 figures, 7 tables
