HILBERT:结合非形式化推理递归构建形式化证明
HILBERT: RECURSIVELY BUILDING FORMAL PROOFS WITHINFORMAL REASONING
https://arxiv.org/pdf/2509.22819?
摘要
大语言模型（LLMs）展现出令人印象深刻的数学推理能力，但其解决方案经常包含无法自动验证的错误。形式化定理证明系统（如 Lean 4）提供了完全准确的自动化验证，这促使近期研究致力于构建专门的证明器 LLM，以生成形式化语言中可验证的证明。然而，一个显著的差距仍然存在：当前的证明器 LLM 所解决的问题数量远少于使用自然语言进行推理的通用 LLM。我们提出 HILBERT——一种智能体框架，通过结合非形式化推理与形式化验证的互补优势来弥合这一差距。我们的系统协调四个组件：一个擅长数学推理的非形式化 LLM、一个针对 Lean 4 战术优化的专用证明器 LLM、一个形式化验证器，以及一个语义定理检索器。当证明器无法解决某个问题时，HILBERT 采用递归分解策略，将问题拆分为若干子目标，并利用证明器或推理型 LLM 分别求解。必要时，它利用验证器的反馈对错误的证明进行修正。实验结果表明，HILBERT 在关键基准上显著优于现有方法，在 miniF2F 上达到 99.2% 的准确率，比当前最佳公开方法高出 6.6 个百分点；在 PutnamBench 上取得已知最佳结果，解决了 462/660 道题目（70.0%），优于 SeedProver 等闭源方法（50.4%），相比最佳公开基线提升了 422%。因此，HILBERT 有效缩小了非形式化推理与形式化证明生成之间的差距。
1 引言
通用大语言模型（LLMs）在数学理解方面取得了显著进步。诸如 GPT-5 和 Gemini 2.5 Pro 等推理型 LLM 在高中奥林匹克竞赛（如 AIME）上接近完美表现，并能解决相当比例的普特南（Putnam）竞赛级别的本科难题（Dekoninck 等，2025）。这些系统在 FrontierMath 等研究级基准上也展现出潜力（Glazer 等，2024；OpenAI，2025）。
然而，几个根本性限制严重制约了它们的实际效用。这些系统经常产生幻觉，输出听起来自信但最终错误的解答。即使最终答案正确，其底层推理也常常包含严重缺陷：例如“举例证明”、逻辑谬误、未经证实的假设以及计算错误（Petrov 等，2025；Guo 等，2025；Mahdavi 等，2025；Balunović 等，2025）。人工验证生成的证明既耗时又困难，且容易出错。尽管近期进展表明基于 LLM 的验证器可接近人类水平（Guo 等，2025；Dekoninck 等，2025），但由于幻觉和静默失败（silent failures），它们仍不可靠（Mahdavi 等，2025；Petrov 等，2025）。
形式化定理证明系统（如 Lean 4；Moura 和 Ullrich，2021）通过实现完全准确的自动化证明验证，提供了一种有前景的解决方案，能够保证在形式化语言中证明或证伪证明的正确性。这一能力推动了专用证明器 LLM 的发展（Polu 和 Sutskever，2020），大量研究聚焦于开发用于生成 Lean 4 形式化证明的专用模型（Yang 等，2023；Xin 等，2024a,b, 2025；Ren 等，2025；Dong 和 Ma，2025；Wang 等，2025）。目前最佳的开源证明器模型在 miniF2F 上的通过率超过 90%（Zheng 等，2021），并在具有挑战性的 PutnamBench（Tsoukalas 等，2024）657 道题中解决了 86 道。AlphaProof（AlphaProof 和 AlphaGeometry，2024）和 SeedProver（Chen 等，2025）等闭源系统展示了该范式的潜力，在国际数学奥林匹克（IMO）问题上取得了银牌水平的表现。
尽管取得上述进展，专用证明器 LLM 与通用推理 LLM 之间仍存在显著性能差距。例如，Dekoninck 等（2025）通过人工验证发现，推理型 LLM 可非形式化地解决约 83% 的 PutnamBench 问题，而当前最佳公开的证明器 LLM 仅能用形式化证明解决其中的 13%。通用 LLM 擅长非形式化数学推理，并且对形式化语言语法的理解足以写出有效的证明草稿和简短证明（Ren 等，2025；Liang 等，2025）。然而，它们在完整的形式化程序合成方面表现不佳，在 miniF2F 上即使尝试 16384 次也仅达到 49.1% 的通过率（Zhou 等，2025b）。相反，专用证明器 LLM 擅长为独立定理生成语法正确的形式化证明，但在依赖语言能力的任务（如利用已有定理或错误修正）上表现脆弱（Liang 等，2025）。
为弥合这一差距，一些研究探索了利用通用 LLM 的非形式化推理能力来增强形式化定理证明。早期方法如 DSP（Jiang 等，2022）和 LEGO-Prover（Wang 等，2023）使用通用 LLM 提出证明草稿，再由自动定理证明器（ATP）填充形式化部分，但受限于基于启发式的 ATP 能力。DSP+（Cao 等，2025）在此基础上使用现代证明器 LLM 处理中间步骤。然而，这些方法因采用浅层、单层分解策略，在处理复杂子目标时表现不佳——它们虽能分解原始问题，却无法进一步分解那些仍难以直接求解的子目标。近期的智能体框架（如 COPRA（Thakur 等，2024）、Prover-Agent（Baba 等，2025）和 ProofCompass（Wischermann 等，2025））利用非形式化推理并结合形式化验证器的反馈迭代构造证明。尽管这些方法展现出潜力，其性能仍显著落后于通用推理 LLM。
我们提出 HILBERT——一种将非形式化推理与形式化验证相结合的智能体框架（见图 1）。它协调四个核心组件：一个通用推理 LLM、一个证明器 LLM、一个验证器和一个语义定理检索器。给定一个数学问题，HILBERT 首先从 Mathlib（mathlib Community，2020）中检索相关定理，并使用推理器生成详细的非形式化证明。随后，它创建一个 Lean 4 证明草稿，将问题分解为可管理的子目标。对于每个子目标，HILBERT 采用两阶段策略：首先尝试用证明器生成形式化证明，若失败则回退到结合检索定理增强的推理器。当两个阶段均失败时，系统会递归地将有问题的子目标进一步分解为更小的问题。在整个过程中，HILBERT 利用推理器在推理时解释编译错误、建议修正方案并指导证明精炼。我们总结主要贡献如下：
- 我们设计了 HILBERT——一个多轮次智能体框架，系统性地结合非形式化数学推理与形式化证明验证，弥合了这两种范式之间的性能差距。
- 我们在 MiniF2F 和 PutnamBench 上进行了全面实验，在两个基准上均取得当前最优性能：HILBERT 在 miniF2F 上达到 99.2% 的通过率（比最佳公开方法高 6.6 个百分点），并在 PutnamBench 上解决了 462/660 道题（70.0%），优于 SeedProver 等闭源系统（50.4%），相比最佳开源基线提升超过 4 倍。
- 通过广泛的消融实验，我们验证了关键技术的有效性：用于分解复杂证明的递归分解流程，以及用于增强推理能力的检索增强生成机制。
2 相关工作
自动定理证明器（ATPs） 是旨在自动发现数学定理证明的计算系统。传统方法主要依赖符号推理方法（Robinson, 1965；McCune, 2003；Schulz, 2002）以及像 Sledgehammer 这样的集成工具，后者将 ATPs 与交互式证明助手连接起来（Blanchette 等，2013；Czajka 和 Kaliszyk，2018）。近期，大语言模型（LLMs）作为一种有前景的新工具被引入自动定理证明领域（Polu 和 Sutskever，2020；Yang 等，2024）。
证明器 LLMs。其基本原理是在大规模形式化证明数据集上训练专用的证明器 LLM，其中最突出的是面向 Lean 定理证明器（Moura 和 Ullrich，2021）的模型。一些代表性模型包括 GPT-f（Polu 和 Sutskever，2020）、ReProver（Yang 等，2023）、DeepSeek Prover 系列模型（Xin 等，2024a,b；Ren 等，2025）、ABEL（Gloeckle 等，2024）、Goedel Prover V1 和 V2（Lin 等，2025a,b）、BFS Prover（Xin 等，2025）、STP-Prover（Dong 和 Ma，2025）以及 Kimina Prover（Wang 等，2025）。这些模型通过整理大量形式化证明语料库，并结合监督微调和强化学习进行训练。若干方法通过在训练过程中引入子目标分解来增强这些模型（Zhao 等，2023, 2024；Ren 等，2025），而 POETRY（Wang 等，2024）和 ProD-RL（Dong 等，2024）则采用递归问题分解策略。闭源的证明器 LLM 如 AlphaProof（AlphaProof 和 AlphaGeometry，2024）和 SeedProver（Chen 等，2025）进一步推动了该领域的前沿，在国际数学奥林匹克（IMO）问题上取得了银牌水平的表现。尽管如此，专用证明器模型与通用 LLM 在数学推理能力方面仍存在显著性能差距（Dekoninck 等，2025）。
使用非形式化 LLM 进行形式化定理证明。若干先前工作尝试利用通用 LLM 的非形式化推理能力来提升形式化推理能力。DSP（Jiang 等，2022）使用 Codex LLM 在 Isabelle 中提出证明草稿，中间步骤由 Sledgehammer 填充。LEGO-Prover（Wang 等，2023）将该框架扩展至处理一个不断增长的中间定理技能库，用于检索增强的证明。Liang 等（2025）指出，通用推理型 LLM 在将问题分解为更简单子目标方面比证明器 LLM 更有效。我们的工作在此观察基础上进一步推进，利用非形式化推理器递归地构建证明草稿，将问题分解为可由证明器或推理型 LLM 处理的更简单子问题。
若干研究还提出在智能体框架中使用非形式化 LLM 进行自动定理证明。COPRA（Thakur 等，2024）通过查询非形式化 LLM 逐个生成证明策略（tactic），并将执行反馈、搜索历史和检索到的引理整合到后续提示中。Prover-Agent（Baba 等，2025）使用一个小型非形式化推理模型生成证明步骤和引理，这些内容被自动形式化后由证明器 LLM 求解。Lean 的反馈被用于迭代修正错误的证明。ProofCompass（Wischermann 等，2025）通过在输入中添加非形式化证明步骤作为注释来增强证明器 LLM。当证明尝试失败时，它分析这些失败以提取中间引理，从而实现有效的问题分解。DeltaProver（Zhou 等，2025b）引入了一种自定义的领域特定语言（DSL）来进行子目标分解，并利用验证器反馈迭代修复生成的证明。值得注意的是，它仅使用非形式化 LLM，不依赖证明器 LLM。相比之下，我们的工作表明，当在适当设计的多智能体框架中协调调度时，证明器 LLM 会成为极为有效的工具。
3 HILBERT 系统
在本节中，我们详细介绍 HILBERT——一种多智能体系统，通过协调通用推理型大语言模型（LLM）与专用证明器 LLM，弥合非形式化数学推理与形式化验证之间的鸿沟。我们的方法采用递归子目标分解策略，将复杂定理拆解为更简单的子目标，这些子目标可被分别证明并组合起来，从而实现超越任一方法单独使用时的性能。
3.1 组件
在描述推理算法之前，我们首先介绍 HILBERT 所协调的各个组件。
推理器（Reasoner）：一个通用推理型 LLM，用于撰写非形式化证明、Lean 中的证明草稿，在某些情况下也可生成形式化证明。在我们的工作中，我们使用 Google Gemini 2.5 Flash 和 Pro（Comanici 等，2025），因其具备卓越的数学推理能力（Zhou 等，2025b；Dekoninck 等，2025）。
证明器（Prover）：一个专用的证明器 LLM，用于在给定形式化定理陈述的情况下生成形式化证明。在我们的工作中，我们使用 DeepSeek-V2-7B（Ren 等，2025）和 Goedel-Prover-V2 32B（Lin 等，2025b）。
验证器（Verifier）：一个形式化语言验证器，用于检查定理陈述和证明的正确性。我们使用 Kimina Lean 服务器（Santos 等，2025），其基于 Lean v4.15.0 和 Mathlib v4.15.0。
检索器（Retriever）：一个语义搜索引擎，用于从 Mathlib（mathlib Community，2020）中检索相关定理。该系统基于 sentence transformers（all-mpnet-base-v2；Song 等，2020）和 FAISS（Douze 等，2024）索引构建。系统计算查询嵌入与 mathlib_informal 数据集（Gao 等，2024）中非形式化定理描述的预计算嵌入之间的余弦相似度，从而提供一种简单而有效的替代方案，避免了使用定制的检索模型（Gao 等，2024；Lu 等，2025）。
3.2 算法
给定一个 Lean 4 中的形式化陈述，我们首先尝试使用 证明器（Prover） 直接证明。它生成 K initial proof = 4 个候选证明，我们使用 验证器（Verifier） 对其进行验证。如果其中任意一个证明有效，我们立即返回该证明。当直接证明尝试失败时，我们使用 推理器（Reasoner） 将问题分解为更简单的子问题，并将它们组合成一个有效的证明策略。图 2 概述了这一阶段。
3.2.1 子目标分解
步骤 1（定理检索）给定形式化陈述，我们提示推理器生成 s = 5 个搜索查询，以查找可能有助于简化证明策略的定理。对于每个搜索查询，我们使用 检索器（Retriever） 从 Mathlib 中检索前 m = 5
个语义最相似的定理和策略（tactics）。随后，我们再次提示推理器从检索到的结果中仅选择相关的定理。
步骤 2（形式化证明草稿生成）我们提示推理器利用检索到的定理生成一份详细的非形式化证明。在此证明作为上下文提供的基础上，我们要求推理器生成一个 Lean 4 证明草稿，将问题分解为以 have 语句表示的更简单子问题。所有子目标最初都用 sorry 填充——这是 Lean 中的一个占位符关键字，可被临时视为子目标的证明。我们使用验证器验证该证明草稿是否有效，并利用其反馈修正任何错误。对于每个输入定理，我们最多生成 K sketch attempts = 4 次草稿尝试。
步骤 3（子目标提取）推理器从证明草稿中提取子目标，将其转换为独立的定理陈述，并附加上原始问题及先前子目标的相关上下文。如前所述，证明部分仍使用 sorry。我们通过统计证明草稿中的 have 语句数量并确保全部被提取，来验证提取的完整性。若发现缺失，我们提示推理器提取遗漏的子目标。每个提取出的定理均通过验证器进行语法验证。当出现错误时，我们将错误信息作为上下文提供给推理器以进行修正。该方法比直接解析源代码或从 Lean 4 的证明状态数据结构（InfoTree）中提取子目标更为可靠（Liang 等，2025）。
步骤 4（基于子目标的证明组装）我们将提取出的子目标定理陈述（包含 sorry 占位符）和已验证的证明草稿提供给推理器。推理器通过将证明草稿中的每个 sorry 占位符替换为对应子目标定理的调用，生成目标定理的完整组装证明。随后，我们使用验证器同时验证子目标定理陈述和组装后的证明，以确保整体结构正确。我们通过验证器检查错误，并通过与推理器的迭代反馈进行修正。这保证了：一旦所有子目标被证明，我们就得到了给定定理的完整证明。
3.2.2 子目标验证
至此，我们已获得一个有效的定理证明结构，以及一组子目标——只要这些子目标被证明，即可完成原始证明。然而，这些子目标的数学正确性与可证性尚未验证。针对每个子目标，我们执行以下验证与证明流程：
步骤 1（证明器尝试）我们首先尝试使用 证明器 直接证明每个子目标，生成 K formal proof = 4
个候选证明，并用验证器进行验证。若任一生成的证明有效，则接受该证明并继续处理下一个子目标。
步骤 2（正确性验证）对于无法直接证明的子目标，我们提示推理器评估该子目标在数学上是否正确，以及其形式化陈述是否表述恰当且可证。如果推理器判定该子目标在数学上不正确、不可证或表述不当，我们将其标记为需修正，并返回以优化原始证明草稿，从第 3.2.1 节开始重复所有步骤，并将识别出的问题作为反馈纳入。除数学错误外，推理器在此阶段检测到的一些常见失败模式包括：子目标定理陈述中缺少假设或条件，以及由 Lean 类型系统引起的异常行为（例如自然数截断）³。
我们优先采用证明器尝试而非推理器验证，因为证明器模型计算成本更低，且一个有效的证明可自动确认数学正确性。经验表明，大量生成的子目标可被证明器成功证明。步骤 1 确保我们在成功证明的子目标上节省了昂贵的推理器模型用于验证的计算开销。
步骤 3（浅层求解）在步骤 1 失败且步骤 2 确认子目标正确的前提下，我们采用推理器模型进行“浅层求解”（shallow solve）：为证明器无法直接解决的子目标编写简短证明。我们从 Mathlib 库中检索相关定理，并要求推理器为该子目标编写形式化证明。推理器根据验证器反馈最多进行 K proof correction = 6
轮迭代修正。当编译错误表明缺少或引用了错误的定理时，我们会检索额外的相关定理。为节省计算资源，若某错误证明超过长度阈值 K max shallow solve length = 30 行，我们即终止此步骤——因为过长的证明表明需要进一步分解。整个浅层求解过程最多重复 K informal passes = 6
次，直至获得成功证明或耗尽所有尝试次数。
步骤 4（递归分解与证明组装）若经过步骤 1–3 后仍有子目标未被证明，我们递归地应用子目标分解流程（第 3.2.1 节）对其进行进一步拆分。每个子目标被持续细分，直至被成功证明，或达到最大递归深度 D 。一旦所有子目标均被证明，我们通过拼接所有子目标的证明与第 3.2.1 节步骤 4 中生成的组装证明大纲，构建给定定理的完整证明。具体做法是将子目标的证明与第 3.2.1 节步骤 4 产生的组装证明进行拼接。若此时仍有未解决的子目标，则触发证明失败，促使我们重新启动该定理的子目标分解流程。
完整算法见算法 1。关于实现细节，特别是并行化策略，请参见附录 A.3。
4 实验结果
4.1 主要结果
MiniF2F。MiniF2F 数据集（Zheng 等，2021）包含 488 道高中数学竞赛题目，其中部分题目特别具有挑战性，源自 AMC、AIME 和 IMO 竞赛。我们在 MiniF2F 测试集划分中的 244 道题目上进行基准测试。所有实验均采用递归深度 D = 5
。对于证明器（Prover），我们在 HILBERT 中实例化了两个 LLM：DeepSeek-Prover-V2-7B（Ren 等，2025），代表能力相对较弱的模型；以及 Goedel-Prover-V2-32B（Lin 等，2025b），代表能力更强的模型。这种配对使我们能够比较不同能力水平下的性能表现。对于推理器（Reasoner），我们相应地采用了 Google 的 Gemini 2.5 Flash 和 Gemini 2.5 Pro（Comanici 等，2025）。结果见表 1。
HILBERT 在所有模型配置下均展现出强劲性能。我们表现最佳的配置组合为 Gemini 2.5 Pro 与 Goedel-Prover-V2-32B，达到了 99.2% 的通过率，仅在两道题目上失败（AMC 12A 2020 第 25 题和 IMO Shortlist 2007 A6 题）。即使使用较弱的形式化证明器，HILBERT 仍保持出色结果：将 DeepSeek-Prover-V2-7B 与 Gemini 2.5 Pro 配对可达到 98.4%，而使用 Gemini 2.5 Flash 则达到 96.7%。值得注意的是，非形式化推理器的选择似乎比证明器强度更为关键。Gemini 2.5 Pro 在各类配置中始终比 Flash 版本高出 3–4%，这一差距大于不同证明器模型之间观察到的性能差异。
与独立的基础证明器在 pass@4 指标下的表现相比，我们的方法带来了显著提升，改进幅度介于 20.1% 至 37.1% 之间。
PutnamBench。PutnamBench 是一个具有挑战性的定理证明基准，包含 1962 年至 2024 年间威廉·洛厄尔·普特南数学竞赛（William Lowell Putnam Mathematical Competition）的 660 道题目。该数据集涵盖代数、分析、数论、几何、线性代数、组合数学、抽象代数、概率论和集合论等本科水平的数学问题。鉴于在此数据集上评估的高昂计算成本，我们仅使用 HILBERT 的最强配置进行实验（即 HILBERT 搭配 Gemini 2.5 Pro 和 Goedel-Prover-V2-32B）。如前所述，我们设定递归深度 D = 5
。结果见表 2。
HILBERT 在 PutnamBench 上取得了当前最优性能，成功解决了 660 道题中的 462 道（通过率为 70.0%）。这一结果比此前最佳方法——闭源的 SeedProver（50.4%）——高出近 20 个百分点。HILBERT 解决的问题数量超过最接近的公开基线模型 Goedel-Prover-V2-32B 达五倍以上。我们将这一成功归因于 HILBERT 能够组合长篇证明（见图 9），而不会受到传统 LLM 所面临的长上下文推理问题的困扰（Zhou 等，2025a）。
4.2 推理时计算资源的扩展行为
与传统证明器 LLM 将计算资源分配到大量从零开始的独立证明尝试不同，HILBERT 将推理时的计算资源分配到多个相互关联的阶段，从子目标分解到子目标证明生成。由于这种计算资源分配是自适应的，无法通过简单的独立尝试次数来衡量。
为说明计算开销与性能之间的权衡关系，我们绘制了 HILBERT 的通过率（pass rate）随每样本调用次数的变化曲线：(1) 仅调用推理器（Reasoner）的次数，以及 (2) 推理器与证明器（Reasoner + Prover）联合调用的总次数（见图 3）。结果显示出清晰的扩展关系：每样本的调用次数越多，通过率越高。我们表现最佳的配置（Gemini 2.5 Pro 搭配 Goedel Prover）最多需要约 4.5K 次推理器调用和 11.3K 次总调用，显著少于 DeltaProver 在使用 Gemini 2.5 Pro 时所需的 16,384 次调用。
有趣的是，较弱的推理器（Gemini 2.5 Flash）为了在两种证明器配置下达到相近的性能，需要明显更高的推理计算预算。虽然 HILBERT + DeepSeek Prover 初始通过率较低，但在低计算预算场景下展现出更快的提升速度，最终能够匹配 HILBERT + Goedel-Prover 的性能。
关于通过率与证明器/验证器调用次数及总 token 使用量的更多分析，请参见附录 A.6。
4.3 消融研究
性能（vs）递归深度。为评估子目标分解的有效性，我们在 MiniF2F 数据集上分析了使用 Gemini 2.5 Pro + Goedel-Prover-V2-32B 的 HILBERT 在不同递归深度 D D 下的通过率。基线（ D = 0
）对应无分解情形，此时我们报告独立证明器（pass@4）的性能。我们比较两种配置：完整的 HILBERT 系统，以及一个禁用浅层求解（shallow solving）的变体（即设 K informal passes = 0）。该变体仅依赖证明器来解决子目标。
图 4 展示了不同 D D 值下的性能表现，清楚表明子目标分解带来了显著增益。两种配置的性能均随深度单调递增，但呈现出不同的收敛模式。完整的 HILBERT 系统在较浅深度即获得快速性能提升：在 D = 2
时达到 98.36%，到 D = 3 时已达 98.7%。相比之下，无浅层求解的变体需要更大的深度才能达到相近性能，凸显了浅层求解机制的重要性。相较于 D = 0 基线（通过率 75%），性能持续提升，验证了分层子目标分解的有效性；完整系统在相对较小的深度下即可实现接近最优的性能。
检索消融实验。为评估检索器（Retriever）对性能和计算效率的影响，我们将 HILBERT 与一个省略检索步骤的变体进行比较。我们在 MiniF2F 上针对两种证明器配置进行实验：DeepSeek-Prover-V2-7B 和 Goedel-Prover-V2-32B。结果见表 3。
启用检索时，HILBERT 在两种配置下均取得更高的通过率：对于 DeepSeek Prover，98.4% 对比 97.1%；对于 Goedel Prover，99.2% 对比 97.9%。更重要的是，检索显著降低了推理时的计算资源消耗。对于 DeepSeek 模型，检索将推理器调用次数从 426 降至 420，平均证明器调用次数从 290 降至 205，平均推理器 token 使用量从 210 万降至 190 万。在 Goedel Prover 上，效率提升更为显著：检索将平均推理器调用次数从 862 降至 548，平均推理器 token 使用量从 400 万降至 230 万。
这些结果表明，检索通过提供有助于简化证明的有用定理，并避免因引用错误定理名称而导致的失败，同时提升了性能与效率。
5 结论
我们提出了 HILBERT——一种分层的智能体框架，它将 Lean 中的形式化定理证明与通用大语言模型（LLM）的非形式化数学推理能力相结合。我们的方法通过递归地将复杂问题分解为可管理的子目标，并协调非形式化推理器（Gemini 2.5 Pro/Flash）与形式化证明器（DeepSeek-Prover-V2-7B 和 Goedel-Prover-V2-32B），共同解决任一组件单独无法处理的定理。HILBERT 在 miniF2F 上取得了当前最优性能，通过率介于 94.7% 至 99.2%。在具有挑战性的 PutnamBench 数据集上，HILBERT 达到 70.0% 的通过率，比此前最佳方法高出近 20 个百分点，并接近 Dekoninck 等人（2025）报告的 82% 的非形式化证明率。
未来，我们计划利用该框架训练能力日益增强的模型。HILBERT 生成的证明和推理轨迹可用于训练更强大的证明器（Prover）和推理器（Reasoner）模型。这些改进后的模型将能够解决比以往更复杂的问题，从而形成一个良性循环，有望持续推动形式化推理能力的进步。
原文链接： https://arxiv.org/pdf/2509.22819?
热门跟贴