Making Written Theorems Explorable by Grounding Them in Formal Representations

📄 arXiv: 2604.02598 📥 PDF

作者: Hita Kambhamettu, Will Crichton, Sean Welleck, Harrison Goldstein, Andrew Head

分类: cs.HC, cs.AI, cs.PL

发布日期: 2026-04-06

💡 一句话要点

提出Explorable Theorems，通过形式化表示增强数学定理的可探索性。

🎯 匹配领域: 支柱三：空间感知与语义 (Perception & Semantics)

关键词: 数学证明 形式化验证 大型语言模型 交互式学习 定理探索

📋 核心要点

  1. 现有LLM生成的解释虽然提升了技术内容的可访问性，但静态文本的本质限制了交互性和动态调试能力。
  2. Explorable Theorems通过将定理及其证明转化为形式化的Lean代码，实现了交互式的探索和验证，增强了理解深度。
  3. 用户研究表明，使用Explorable Theorems的参与者在证明理解任务中表现更佳，证明了该方法在提升理解方面的有效性。

📝 摘要（中文）

大型语言模型（LLM）生成的解释可以提高技术内容的可访问性，但其交互能力存在上限，因为LLM的输出是静态文本，无法执行或逐步调试。本文提出将解释建立在形式化表示之上，从而实现超越静态文本的交互功能。具体而言，本文针对数学证明理解问题，提出了Explorable Theorems系统，该系统利用LLM将定理及其书面证明翻译成Lean（一种用于机器验证证明的编程语言），并将书面证明与Lean代码链接起来。读者可以逐步完成证明，测试自定义示例或反例，并追踪连接每个步骤的逻辑依赖关系。每个步骤的结果都通过在示例上执行Lean证明并提取其中间状态来生成。用户研究（n = 16）表明了该方法的潜在优势：在校对任务中，可以使用所提供的可探索性功能的参与者对理解问题的回答更好、更正确、更详细，表明他们对基础数学有更强的整体理解。

🔬 方法详解

问题定义：现有方法依赖于LLM生成的静态文本解释，无法提供交互式的证明探索和验证功能。这使得读者难以深入理解证明的逻辑和细节，尤其是在面对复杂的数学定理时。现有方法缺乏动态调试和测试反例的能力，限制了学习和理解的深度。

核心思路：本文的核心思路是将数学定理及其证明转化为形式化的、可执行的表示形式，即Lean代码。通过将书面证明与Lean代码链接，读者可以交互式地探索证明的每个步骤，并验证其逻辑正确性。这种方法利用Lean的机器验证能力，确保证明的正确性，并提供动态调试和测试反例的功能，从而增强理解。

技术框架：Explorable Theorems系统包含以下主要模块：1) LLM翻译模块：将定理及其书面证明翻译成Lean代码。2) Lean执行模块：在给定示例上执行Lean证明，并提取中间状态。3) 链接模块：将书面证明与Lean代码链接起来，方便读者在两者之间切换。4) 用户界面：提供交互式界面，允许读者逐步完成证明，测试示例和反例，并追踪逻辑依赖关系。

关键创新：最重要的技术创新点在于将LLM生成的解释与形式化的证明系统相结合，实现了交互式的证明探索和验证。与现有方法相比，Explorable Theorems不仅提供了静态的文本解释，还提供了动态的、可执行的证明过程，从而增强了理解的深度和广度。

关键设计：LLM翻译模块使用了预训练的LLM模型，并针对数学证明的特点进行了微调。Lean执行模块利用Lean的机器验证能力，确保证明的正确性。链接模块使用了基于文本相似度的算法，将书面证明与Lean代码中的对应部分链接起来。用户界面采用了直观的设计，方便读者进行交互式探索。

📊 实验亮点

用户研究表明，使用Explorable Theorems的参与者在证明理解任务中表现更佳，能够给出更好、更正确、更详细的答案。这表明Explorable Theorems能够显著提升用户对数学定理的理解程度。具体性能数据未知，但研究结果表明该方法具有潜在优势。

🎯 应用场景

该研究成果可应用于在线教育、数学研究和软件验证等领域。通过提供交互式的定理探索工具，可以帮助学生更深入地理解数学概念和证明方法。研究人员可以使用该工具来验证和调试复杂的数学证明。软件工程师可以使用该工具来验证软件的正确性。

📄 摘要（原文）

LLM-generated explanations can make technical content more accessible, but there is a ceiling on what they can support interactively. Because LLM outputs are static text, they cannot be executed or stepped through. We argue that grounding explanations in a formalized representation enables interactive affordances beyond what static text supports. We instantiate this idea for mathematical proof comprehension with explorable theorems, a system that uses LLMs to translate a theorem and its written proof into Lean, a programming language for machine-checked proofs, and links the written proof with the Lean code. Readers can work through the proof at a step-level granularity, test custom examples or counterexamples, and trace the logical dependencies bridging each step. Each worked-out step is produced by executing the Lean proof on that example and extracting its intermediate state. A user study ($n = 16$) shows potential advantages of this approach: in a proof-reading task, participants who had access to the provided explorability features gave better, more correct, and more detailed answers to comprehension questions, demonstrating a stronger overall understanding of the underlying mathematics.