Deep Reasoning

🌐 English | 中文

Deep Reasoning (deep_explore)

deep_explore is Philont's protocol for changing what you know — a proof, a decision, a diagnosis. Where the plan protocol decomposes a task into action steps verified by completion, deep_explore decomposes a question into claims with a truth status (open / settled / refuted) and verifies each one before it counts.

It is a persistent reasoning tree. The loop — decompose → claim → verify → backtrack — runs in every domain, accumulating what's settled vs. still open across turns; you can resume a session days later. What changes between domains is only the verification substrate.

Enabled by default (PHILONT_DEEP_EXPLORE=on). State lives in agent-memory; orchestration in server/src/deep_explore.ts.

Two modes, one engine

mode="formal" — mathematical / formal proof

A claim is settled only when it is machine-checked and survives independent adversarial reviewers. Inside a round it deliberately does not browse the web (that would let the model retrieve instead of reason); it grounds every claim in deduction, computation, and exact order-of-growth algebra.

mode="deliberate" — evidence-based judgment

For open-ended questions: decisions ("should I take this offer?"), root-cause diagnosis ("why is retention dropping?"), due diligence. Here the substrate flips to cited evidence: the question is decomposed into sub-questions, evidence is gathered (the user's own memory & files first, then the web), and a finding is settled only when backed by a cited source — surviving an adversarial evidence reviewer that asks "is this actually supported, or motivated reasoning?". An honest "unresolved" beats a fabricated conclusion.

Before it grinds: grounding + feasibility

Across both modes, before spending rounds:

• a one-shot literature-grounding pass surfaces what's already known (cited);
• a feasibility gate flags goals blocked by a known no-go (the parity problem, relativization, undecidability, CAP/FLP, and ~20 others) — so it routes around the wall or records it, instead of burning rounds on it.

It counts only substantive progress, so trivial churn can't masquerade as advancement, and it tells you when a frontier is genuinely stuck.

The verification teeth (formal mode)

The hard part of a real proof is rarely the structure — it's the quantitative bookkeeping: tracking orders of growth like N^{3/2}·(log N)^{-A} across dozens of steps and choosing parameters so error terms balance. That's exactly where an LLM slips, so formal verification goes past a single solver. These live in agent-tools/src/runtime/:

Tooth	File	What it decides
z3	z3.ts	SMT solver — decidable checks, counterexample search.
PARI/GP	gp.ts	Number-theory CAS — exact computation.
magnitude	magnitude.ts	An asymptotic order-of-growth algebra. Decides o/O/Θ and whether a pile of bounds composes to beat a target — including whether a parameter choice even exists. Returns a witness when one does, or the honest "no choice closes this — it's a real gap" verdict when none can. Pure TypeScript, no external binary.
lemmaLookup	(lemma library)	A curated library of standard estimates with their precise hypotheses, magnitudes, and common misuses — so the model retrieves the right tool instead of mis-remembering a constant.
barrierCheck	barriers.ts	A curated library of meta-mathematical no-go results (parity, relativization / natural-proofs / algebrization, undecidability & Rice, ZFC independence, Abel–Ruffini, FLP/CAP, no-free-lunch, no-cloning, …), so a doomed approach is recognised before rounds are spent on it.

The honesty mechanism reaches here too: a node claimed proved on an order-bound that was never machine-checked is flagged (fabricated_reasoning_state / order-claim detection), so a hand-wave can't pass downstream as a verified lemma. None of this invents the missing idea — it makes the steps trustworthy, fast, and honest about where the real wall is.

…and one tooth that is not mode-scoped

PHILONT_DEEP_EXPLORE_VERIFY_OBJECTS · agent-memory/src/checkable_claim.ts

The teeth above are formal-mode furniture, and that was a hole: checkability is a property of the claim, not of the session it lands in. In July 2026 a deliberate session researching a famous counterexample held an explicit polynomial map, its determinant, and three points said to collide — all of it decidable in about four seconds — and settled every node on citations, with pariGp and z3Verify untouched for the whole round. Mode had been chosen once at entry, so no verification tooth was ever in the path.

Now a settle whose claim carries a machine-decidable object — a determinant value, a symbolic identity, an explicit point with its claimed image, a primality claim — is refused once, naming the tool that decides it, if the session has computed nothing yet. Three properties keep it safe enough to default on:

• Refuse-once. A second attempt on the same node goes through, annotated "unverified object". A false positive costs one iteration; it can never wedge a session — unlike a guard that refuses indefinitely.
• It stands down as soon as the session computes anything. The failure mode it exists for is never reaching for a tool, not reaching imperfectly.
• It does not tell the model what to conclude. The directive says compute it and settle with the tool's own output — "if the object turns out to be wrong, that is the finding." A tooth that demanded confirmation would be a worse liar than the one it replaces.

Guaranteeing the tree has something decidable on it

PHILONT_DEEP_EXPLORE_REFUTATION_NODE · agent-memory/src/refutable_goal.ts

The deeper failure behind a 14-round session that never converged is not slowness — it is that nothing on the tree could be checked, so no round produced a signal and "am I closer or further?" stayed unanswerable for hours. The engine's own reflection named this correctly and then filed it as advice for the owner to remember. A lesson you have to remember is not a mechanism.

There is an asymmetry that makes it mechanisable. For any universally quantified claim: confirming it needs an argument — no finite check settles it — but refuting it needs one witness, which is finite, cheap, and decidable. So a session attacking a ∀-goal can always be handed at least one node with a verifier attached, whatever happens on the proof side.

A universally quantified or conjecture-shaped goal is therefore seeded, before round one, with a sibling node under the root:

No counterexample to «goal» exists inside an explicitly stated bounded region. Settle this ONLY with the output of an actual computation — either the witness (which refutes the goal itself, the strongest possible outcome) or the region you enumerated and the tool's report that it is clear. "I looked and found nothing" is not a result.

Three deliberate choices:

• It is a claim, not a task. "Search for a counterexample" is something one can be busy with forever; it has no truth value, so nothing can ever check it — which is precisely how a decomposition full of tasks produces no signal. Both outcomes of the claim are worth having: a witness refutes the goal, and an exhausted region is a citable result.
• No list of problem names. The detector reads structure — an explicit quantifier, or the words that mark a statement as a conjecture — so it works on a problem invented tomorrow. A curated vocabulary of famous conjectures is the hard-coded-table trap this codebase has been bitten by elsewhere.
• Decision goals are never paired. "Which channel should we prioritise?" is not false in the presence of a witness; pairing it would be noise.

The node is otherwise ordinary: the model may work it, defer it, or close it as a dead end. What is guaranteed is that it exists — the tree cannot start with nothing on it that anything could check.

Every node states what would settle it

reasoning_nodes.check_criterion (schema v38)

The refutation node guarantees one checkable thing exists. The criterion field asks the same question of every node, at the moment it is created: what would confirm or refute this? — a tool call and its input, a citation that would answer it, a property a produced object must satisfy.

It is deliberately not a rejection. Some genuine subgoals are settled only by an argument, and refusing to create them would trade an unanswerable node for a wedged session. What changes is that the absence becomes countable and loud:

• at creation, reason_decompose names the children that stated none, with their ids, so they can be fixed in the same round;
• on every round's frontier, a node with no criterion renders as ⚠ no stated check next to the ones that have one;
• at round close the report carries the ratio — and when nothing open is checkable it says so plainly: narrowing one of them to something checkable is worth more than another round on all of them.

That last line is the whole point. A session can still choose to work an unanswerable frontier; what it can no longer do is spend fourteen rounds there and only discover afterwards that no round could ever have produced a signal.

How requests get here

A turn-entry intent router classifies every message (think / build / direct). Reasoning-shaped requests with router confidence ≥ 0.9 are guaranteed into the engine — if the model answers flat, the harness synthesizes the deep_explore(start) call itself. Mid-confidence (0.7–0.9) asks the owner one question first ("进" / "直接"); below that the request runs as a normal turn. Explicit depth phrases ("深入", "攻关") always force entry. Thresholds: PHILONT_DEEP_EXPLORE_FORCE_CONF / …_ASK_CONF.

vs. breadth-first research

A research agent (e.g. Google Deep Research) is one-shot and breadth-first: search, read, synthesise a cited summary of what's already known. deep_explore is depth-first and persistent — even in deliberate mode it builds a tree of sub-questions, gathers evidence per sub-question, adversarially checks each before settling, and accumulates across turns. Philont chains them: the grounding pass feeds known results in, then the tree reasons from there. (See the project's own deep-research harness for the breadth-first side.)

---

中文

English | 中文

深度推理(deep_explore)

deep_explore 是 Philont 用于改变你的认知的协议 —— 一个证明、一个决策、一个诊断。计划协议把任务分解为以完成验证的动作步骤,而 deep_explore 把问题分解为带真值状态的 claim(open / settled / refuted),每个在计入前都被验证。

它是一棵持久推理树。回路 —— 分解 → claim → 验证 → 回溯 —— 在每个领域都跑,跨 turn 累积「已定 vs 仍开放」;你可以几天后恢复一个会话。领域之间唯一变化的是验证基底。

默认开启(PHILONT_DEEP_EXPLORE=on)。状态在 agent-memory;编排在 server/src/deep_explore.ts。

两种模式,一个引擎

mode="formal" —— 数学/形式证明

一个 claim 只有在被机器校验且经受住独立对抗性审查者后才算定下。一轮之内它刻意不联网(否则模型会检索而非推理);它把每个 claim 扎根于演绎、计算和精确的增长阶代数。

mode="deliberate" —— 基于证据的判断

用于开放问题:决策(「该接受这个 offer 吗?」)、根因诊断(「留存为何下降?」)、尽调。此处基底翻转为带引用的证据:问题被分解为子问题,先采集证据(优先用户自己的记忆与文件,再到网络),一个结论只有在有引用来源支撑时才定下 —— 并要经受一个对抗性证据审查者:「这真的被支撑,还是动机性推理?」诚实的「未解决」胜过编造的结论。

开磨之前:扎根 + 可行性

两种模式下,在花费轮次之前:

• 一次性的文献扎根过程浮现已知结论(带引用);
• 一道可行性门标记被已知 no-go 挡住的目标(parity 问题、相对化、不可判定性、CAP/FLP 等约 20 张),从而绕开或记录,而非在墙上空耗。

它只计实质进展,因此琐碎打转无法冒充推进,并会在一个前沿真正卡住时告诉你。

验证之牙(formal 模式)

真实证明的难点很少在结构 —— 而在定量记账:跨几十步追踪 N^{3/2}·(log N)^{-A} 这样的增长阶,并选参数让误差项平衡。这正是 LLM 滑倒处,所以形式验证不止一个求解器。它们在 agent-tools/src/runtime/:

牙	文件	它判定什么
z3	z3.ts	SMT 求解器 —— 可判定检查、反例搜索。
PARI/GP	gp.ts	数论 CAS —— 精确计算。
magnitude	magnitude.ts	一套渐近增长阶代数。判定 o/O/Θ,以及一堆界能否复合击败目标 —— 包括是否存在这样的参数选择。能则返回见证,不能则给出诚实的**「无任何选择能闭合 —— 这是真缺口」**判决。纯 TypeScript,无外部二进制。
lemmaLookup	(引理库)	一个精选的标准估计库,带其精确前提、量级与常见误用 —— 让模型检索正确工具,而非记错某个常数。
barrierCheck	barriers.ts	一个精选的元数学 no-go 库(parity、相对化/自然证明/代数化、不可判定性与 Rice、ZFC 独立性、Abel–Ruffini、FLP/CAP、no-free-lunch、no-cloning…),从而在花费轮次之前识别注定失败的思路。

诚实机制也延伸到此:一个基于「从未被机器校验的阶界」而被标 proved 的节点会被标记(fabricated_reasoning_state / 阶声明检测),使挥手论证无法作为已验证引理流向下游。这一切都不发明缺失的想法 —— 它让步骤可信、快速,并对真正的墙在哪保持诚实。

……以及一颗不按模式划界的牙

PHILONT_DEEP_EXPLORE_VERIFY_OBJECTS · agent-memory/src/checkable_claim.ts

上面那些牙是 formal 模式的家具,而这本身就是个洞:「可判定」是 claim 的属性,不是它恰好落在哪个会话里的属性。 2026 年 7 月,一个 deliberate 会话在调研一个著名反例时,手里握着显式多项式映射、它的行列式、以及三个据称会相撞的点 —— 全部约四秒内可判定 —— 却把每个节点都结算在引用上,整轮 pariGp 与 z3Verify 一次没碰。模式在入口只选一次,于是没有任何验证之牙出现在路径上。

现在,一个携带机器可判定对象的结算 —— 行列式取值、符号恒等式、显式点及其宣称的像、素性断言 —— 若本会话尚未计算过任何东西,会被拒绝一次,并点名那个能判定它的工具。三条性质让它足以默认开启:

• 只拒一次。 同一节点的第二次尝试放行,并标注*「未验证对象」*。误判的代价是一次迭代;它永远卡不死会话 —— 不像会无限期拒绝的守卫。
• 会话一旦真的算过东西,它就退场。 它针对的失败模式是从不伸手拿工具,不是拿得不够好。
• 它不告诉模型该得出什么结论。 指令说的是去算,并用工具自己的输出来结算 —— 「如果这个对象是错的,那就是发现」。一颗要求确认的牙,会比它所替代的谎言更坏。

保证树上一定有可判定的东西

PHILONT_DEEP_EXPLORE_REFUTATION_NODE · agent-memory/src/refutable_goal.ts

一个跑了 14 轮仍不收敛的会话,更深的病根不是慢,而是树上没有任何东西可被检查:于是没有一轮产出信号,「我是更近了还是更远了」几个小时都无法回答。引擎自己的反思把这一点说对了,然后把它写成了一句给主人记住的忠告。需要你记住的教训不是机制。

有一个不对称使它可被机制化。对任何全称命题:确认它需要一个论证——没有任何有限检查能结算;而否证它只需要一个见证——有限、廉价、可判定。所以任何攻击 ∀ 型目标的会话,都总能被给到至少一个挂着验证器的节点,无论证明那一侧发生什么。

因此,一个全称量化或猜想形状的目标,会在第一轮之前就被在根节点下播下一个兄弟节点:

在一个明确写出的有界区域内,「目标」不存在反例。只能用一次真实计算的输出来结算它 —— 要么是那个见证(它直接否证了目标本身,这是最强的结果),要么是你枚举过的区域 + 工具报告它是干净的。「我找了,没找到」不算结果。

三个刻意的选择:

• 它是命题,不是任务。「搜索反例」是一件可以永远忙下去的事,它没有真值,所以永远无法被检查——而这恰恰就是「满树都是任务」产不出信号的原因。这个命题的两种结局都值钱:找到见证 = 否证目标;穷尽区域 = 一条可引用的真结果。
• 不写任何问题名单。 检测器读的是结构——显式量词,或标记「这是一个猜想」的那些词——所以它对明天才被提出的问题同样有效。一份精选的著名猜想词表,正是本仓库在别处已经吃过亏的硬编码表陷阱。
• 决策类目标永不配对。「我们下一步该优先做哪个渠道?」不会因为出现一个见证而变假,给它配对只是噪音。

这个节点其余方面完全普通:模型可以做它、押后它、或把它关成死胡同。被保证的只是它存在——树不可能在「没有任何东西能被检查」的状态下开局。

每个节点都要说出「什么能结算它」

reasoning_nodes.check_criterion(schema v38)

反例节点保证的是至少有一个可检查的东西存在。验收标准字段则把同一个问题问向每一个节点,并且在它被创建的当下就问:什么能确认或否证它? —— 一个工具调用及其输入、一条能回答它的引用、或一个产出对象必须满足的性质。

它刻意不是拒收。有些真实的子目标确实只能由论证结算,拒绝创建它们等于用「一个无法回答的节点」换来「一个被卡死的会话」。改变的是:缺席变得可计数且响亮:

• 创建时,reason_decompose 会点名哪些子节点没给标准、并带上 id,让它可以在同一轮里补上;
• 每一轮的 frontier 上,没有标准的节点会以 ⚠ no stated check 与有标准的并排显示;
• 轮末报告里带上比例——而当所有开放方向都不可检查时,它会直说:把其中一个收窄成可检查的,比再花一轮同时磨所有这些更值钱。

最后那句才是全部重点。会话仍然可以选择去啃一个无法回答的 frontier;它不能再做的是——在那儿花掉十四轮,事后才发现那里的任何一轮都不可能产出信号。

与广度优先研究的区别

研究型 agent(如 Google Deep Research)是一次性、广度优先:搜索、阅读、综合出一份关于已知的带引用摘要。deep_explore 是深度优先且持久 —— 即便在 deliberate 模式,它也构建子问题树、逐子问题采证、逐一对抗性检验后才定下,并跨 turn 累积。Philont 把两者串起来:扎根过程把已知结论喂进来,推理树再从那里往下推。