Rethlas 进阶指南：如何手动运行 Rethlas

这是一份为数学家撰写的 Rethlas 进阶指南，只需要微乎其微的计算机科学前置知识。我会深入介绍 Rethlas 的更多细节，并谈谈自己会如何使用它。

准备工作

1. 掌握使用终端的基础知识。参见我的终端指南。
2. 完成 Rethlas 的基本配置。参见我之前的文章——Rethlas 使用指南：如何借助 AI 运行 Rethlas（无需计算机科学背景）。

Rethlas 仓库概览

├── agents
│   ├── generation
│   │   ├── AGENTS.md
│   │   ├── data
│   │   ├── downloads
│   │   ├── logs
│   │   ├── mcp
│   │   ├── memory
│   │   ├── results
│   │   ├── scripts
│   │   ├── site
│   │   └── tests
│   └── verification
│       ├── AGENTS.md
│       ├── api
│       ├── mcp
│       ├── memory
│       ├── requirements.txt
│       ├── results
│       ├── schemas
│       └── scripts

Rethlas 有两个智能体：生成智能体和验证智能体。其基本思想非常简单：如果验证智能体能够可靠地拒绝错误证明，而生成智能体又足够强大，能够在解空间中搜索候选证明，那么，通过不断迭代生成—验证循环，生成智能体最终会通过修补小缺口并避免重复犯错而找到一个证明。

你可以用以下两种方式查看代码：

1. 喜欢图形界面的人：打开文件夹，点击你感兴趣的文件或子文件夹。
2. 喜欢终端的人：用 cd 进入目录，用 ls 查看可见文件，用 ls -alh 查看包括隐藏文件在内的所有文件，再用 less <filename> 在分页器中查看文件内容。

如果你只关心如何使用 Rethlas，那么只需要了解以下几点：

1. agents/generation/data 是放置问题与参考资料的地方。
2. agents/generation/results 是查看输出的解答（Markdown 文件）的地方。
3. agents/generation/logs 是查看 Rethlas 日志并研究其探索轨迹的地方。一般来说，这些日志可能太长，难以通读。
4. agents/generation/memory 也能帮助你理解推理轨迹中的要点，包括重大决策、分支状态、反例、事件、失败路径、即时结论、证明步骤、子目标、玩具示例以及验证报告。

下面我会更详细地逐一介绍这些目录。我将以拟阵的 Kazhdan–Lusztig 多项式的实根性猜想为例。

问题与参考资料

写下问题并提供参考资料

由于通常在终端中完成所有操作最为方便，我会先介绍这种标准做法。对于实在不喜欢终端的人，我也会说明如何用 GUI（图形用户界面）完成这些操作。

首先，用 cd 进入 rethlas 文件夹。

cd ~/Desktop
git clone https://github.com/frenzymath/Rethlas.git rethlas
cd rethlas

然后，为你的问题新建一个项目文件夹：

cd agents/generation/data
mkdir real_root_kl
cd real_root_kl

现在的要点是：

• touch real_root_kl.md。这会创建一个 Markdown 文件，你可以在其中写下问题。
• mkdir real_root_kl.refs。这会创建一个文件夹，你可以把参考资料放在其中。

问题叫什么名字并不重要。不过，x.md 和 x.refs 中的 x 必须相同，这一点很重要。

现在，用你喜欢的编辑器编辑这个 Markdown 文件，清晰、严谨地陈述问题（否则，智能体可能会给出平凡的例子！）。正如终端指南中所讲，在 macOS 上，你可以使用 open -e <filename.md> 在 TextEdit 中打开文件。如果你已经通过 Homebrew 或从网站下载安装了 Visual Studio Code，并使 code 命令可在终端中使用，就可以使用 code <filename> 在 VS Code 中编辑文件。你也可以使用 vim <filename>。

关于问题陈述与参考资料的建议

正如你所知道的，生成式 AI 本质上是在预测下一个 token，因此提示词和上下文非常重要。下面是我想强调的一些建议：

1. 确保问题陈述足够严谨，并包含所有必要条件；否则，智能体可能会给出平凡的例子。避免歧义和滥用记号。要把一切说得一清二楚。
2. 要提供参考资料，只需把文件放入 real_root_kl.refs。我强烈建议使用 Markdown、LaTeX 或纯文本格式。对于 arXiv 论文，你可以下载其 LaTeX 源代码。对于 PDF，你可以使用光学字符识别（OCR）或其他 AI 工具——例如 ChatGPT 网页界面——将其转换为 Markdown。
3. 你不需要提供 arXiv 上所有可用的参考资料，因为智能体可以自行使用搜索工具找到它们。不过，如果你提供一些自己认为有用、但受版权保护的书籍，可能会有很大帮助。
4. 如果参考资料没有用，反而会分散智能体的注意力。因此，只提供你认为与问题密切相关的必要参考资料，或者难以从互联网上免费下载的受版权保护的材料。
5. 你可以在问题陈述中提供解决问题所需的定义。当某个术语在其他领域中还有别的含义时，这一点尤其有用。

下面是一些更进阶的技巧：

在终端指南中，我说明了如何配合 Overleaf 使用 Git。因此，你可以把自己的 Overleaf 论文项目克隆到这个参考资料文件夹中。如果你把论文的各节清楚地拆分到不同的 .tex 文件里，并在 main.tex 中使用 \input，那么就可以向智能体提供你正在撰写的内容或个人笔记作为上下文。

如果问题需要用到你论文中的定义，我建议在问题陈述中重复这些定义，并加上一句类似 as defined in 1introduction.tex in refs. 的话。下面是一个提示词模板：

A monodromic crystalline D-module is defined to be ..., as in
3monodromic.tex. Prove ..., i.e., the unproved lemma lem:unproved in
3monodromic.tex.

之后，在修改输出并确信它正确之后，你可以根据自己的理解把证明写进论文，也可以让 Codex 或 Claude 把它合并到论文中。务必核验它的正确性，并认真重写这份证明。你可以使用 git add、git commit 和 git push 更新 Overleaf。也可以使用 git restore . 丢弃对已跟踪文件尚未暂存的更改。

运行 Rethlas

现在，你已经陈述了问题并提供了参考资料，让我们启动 Rethlas。当然，你仍然可以像 Rethlas 指南中所讲的那样，使用 AI 帮你启动和运行它。这里我想介绍如何手动控制实验。

再次用 cd 进入 rethlas 目录，并从那里开始：根据你放置 Rethlas 文件夹的位置，运行 cd ~/rethlas 或 cd ~/Desktop/rethlas。

然后使用 tmux 在一个会话中管理多个终端窗口。关于 tmux 及其优点，参见终端指南。

tmux

现在，我们用一个窗口运行生成智能体，另一个窗口运行验证服务。

配置验证服务

按下 ctrl+b，松开这两个键，然后按 ,，重命名当前窗口。输入 verify，再按 enter。

然后运行：

cd agents/verification

如果你已经按照 Rethlas 指南配置好了虚拟环境，只需运行：

source .venv/bin/activate

否则，请运行：

uv venv
source .venv/bin/activate
uv pip install -r requirements.txt

然后运行：

uvicorn api.server:app --host 0.0.0.0 --port 8091

你应该会看到：

现在，我们继续启动生成智能体。

配置生成智能体

首先，按下 ctrl+b，松开这两个键，然后按 c，创建一个新窗口。再次使用 ctrl+b，再按 ,，把这个窗口重命名为 gen1。

确保你位于 Rethlas 目录中，然后运行：

cd agents/generation

如果新的 tmux 窗口继承的是 agents/verification 目录，请运行 cd ../generation。

如果你已经配置好了生成智能体的虚拟环境，请运行：

source .venv/bin/activate

否则，请运行：

uv venv
source .venv/bin/activate
uv pip install -r mcp/requirements.txt

现在运行：

MODEL=gpt-5.6-sol REASONING_EFFORT=max PROBLEM_FILE=data/real_root_kl/real_root_kl.md ./tests/run_example.sh

现在你会看到：

计时器会显示它已经运行了多长时间。

接下来，你要等待它运行数小时，并希望最终能收获结果。按下 ctrl+c 可以停止运行。

在浏览器中查看输出

实验结束后，你可以运行以下命令查看结果：

./site/serve.sh

请在 agents/generation 目录中运行这条命令。

然后，在浏览器中打开 http://localhost:3264 查看结果。如果有些公式格式不正确，当然可以请 Codex 修复。

并行运行

只要你有足够的 GPT 用量，就可以同时运行多个生成智能体，并行攻克多个问题。

1. 使用 ctrl+b，再按 c，打开一个新窗口。使用 ctrl+b，再按 ,，把它重命名为 gen2。
2. 使用 cd 进入 agents/generation。
3. 运行 MODEL=gpt-5.6-sol REASONING_EFFORT=max PROBLEM_FILE=data/real_root_z/real_root_z.md ./tests/run_example.sh。

你可以使用 ctrl+b，再按 w，选择想要访问的窗口。也可以偶尔检查验证服务是否正常运行。

分析探索轨迹

如果你想了解 Rethlas 为什么能解决或未能解决某个问题，就必须查看日志文件和记忆文件。记忆文件通常较短且信息丰富，而日志文件往往极其冗长繁复，但包含更多可用于调试和理解失败原因的信息。

通过查看日志文件，我发现了以下几点：

1. 由于版权问题，Rethlas 在 Brian Conrad 的代数群问题 [1, Section 5.1.1] 中犯了一个引文替换错误：CGP 一书 [3] 对 Codex 不可访问，而且模型不会复述这本受版权保护的书中的内容。
2. 我还重建了 Rethlas 在 Kazhdan–Lusztig 多项式论文 [2] 中的推理轨迹。

当然，你可以使用 Codex 或 Claude 帮助理解日志，但不能过度依赖它们，因为日志非常长，智能体可能会忽略一些内容。

参考文献

[1] Haocheng Ju, Guoxiong Gao, Jiedong Jiang, Bin Wu, Zeming Sun, Shurui Liu, Leheng Chen, Yutong Wang, Yuefeng Wang, Zichen Wang, Wanyi He, Peihao Wu, Liang Xiao, Ruochuan Liu, Bryan Dai, and Bin Dong. Automated Conjecture Resolution with Formal Verification. arXiv:2604.03789.

[2] Ronnie Cheng and Shurui Liu. Kazhdan–Lusztig Polynomials of Matroids Need Not Be Unimodal. arXiv:2607.24186.

[3] Brian Conrad, Ofer Gabber, and Gopal Prasad. Pseudo-reductive Groups. 2nd ed., New Mathematical Monographs 26, Cambridge University Press, 2015. DOI: 10.1017/CBO9781316092439.