math-olympiad

数学オリンピック問題ソルバー

結果を左右する5つのこと

1. 検証の前に思考を切り離す — 推論を見た検証者は、同意する方向に偏ります。新しいコンテキストに、整えた証明だけを渡します。
2. 「これはRHを証明するか？」 — 定理をζに特殊化した結果が有名な未解決問題になるなら、証明に穴があります。最も確実な危険信号です。
3. 短い証明 → 一般補題を取り出す — 2×2の反例を試します。一般形が成り立たないなら、今回の事例に特有の性質を見つけます。
4. 同じ穴が2回見つかったら、一歩引く — 場合分けによって、統一的な議論が見えにくくなっているかもしれません。12ページかけてもできなかったことが、3行でできることもあります。
5. 「確信の持てる解答はありません」と言う — 間違っているのに自信満々なのは、正直に回答を控えるよりも悪いことです。

---

ツールのポリシー：予算の限られたワークフローでは、ソルバーと検証者はTHINKING ONLYを使用します。競技数学は推論で解きます。計算を使うのはディープモード（§6c）のみで、その場合も範囲を制限します。倍指数時間の漸化式はn~30を超えると計算できないため、代わりにmod 2^mで計算します。

---

アプローチの使い分け

問題	アプローチ	検証
AIMEの数値解答	ベスト・オブ・N → 多数決	解答のみを確認
オリンピックの証明（IMO/Putnam/USAMO）	以下の完全なワークフロー	5パスの敵対的検証
「この証明は正しいですか？」	検証（ステップ4）に進む	敵対的検証 + 仕様の悪用
問題セット全体（例：大会の全6問）	順次処理：問題ごとに完全なワークフローを実行し、結果を集めて単一のPDFにまとめる	問題ごとの敵対的検証

1つのWorkflowでまとめて処理する場合：すべてのagent()呼び出しでopts.labelを設定し、問題IDを含めます（例：label: "P3:solver:2"）。ラベルがないと、36件の結果がどの問題に対応するのかわからなくなります。問題は並列で実行します。重要なのは順序ではなくラベルです。

問題セット全体の場合

問題ごとにソルバーのワークフローを1つ起動します（VERBATIMプロンプトは同じで、問題文だけを変えます）。並列で実行します。すべての結果が返ってきたら、問題ごとに敵対的検証を行います。合格した問題は証明をPDFに掲載し、回答を控えた問題は部分的なメモとともに「確信の持てる解答はありません」と記載します。

N問すべてを1つのエージェントのコンテキスト内で解こうとしてはいけません。各問題にそれぞれの思考予算と、新しいコンテキストでの検証者が必要です。まとめる作業は機械的です。問題ごとの出力を集め、LaTeXの各セクションに記入し、1回コンパイルするだけです。 | 「この証明を簡潔にしてください」 | プレゼンテーション（ステップ8）に進む | — |

---

ワークフロー

1. 解釈の確認（30秒で、ある種類の誤り63件中50件を検出）

解き始める前に、問題の解釈を特定します。

問題文を読み、解釈の候補を2～3通り挙げます。それぞれについて、 この読み方は自明に解けますか？ある読み方では簡単で、別の読み方では難しい場合、 難しいほうが意図されている可能性が非常に高いです。どの解釈で解くのか、 またそれが意図されたものだと考える理由を述べます。

Aletheiaのケーススタディでは、「技術的には正しい」解答63件のうち50件が、誤った解釈に基づくものだと判明しました。オリンピックの問題には、簡単に解ける読み方を誘う罠がよくあります。

2. 内部で改良を重ねながら候補を生成する（並列、思考のみ）

8〜12 個の試行エージェントを並列に起動します。各エージェントは内部で反復します — 解く → 自己改善する → 自己検証する → 修正する → 繰り返す。これが IMO で 85.7% を達成した Yang-Huang 構造です。一度きりの解答では不十分であり、試行ごとの改良が重要です。

Agent ツールではツールの使用制限を強制できません。 サブエージェントにはすべてのツールが与えられます。唯一の手段はプロンプトです。次のプロンプトを逐語的に使用してください — 要約したり、独自に作成したりしないでください。

NO COMPUTATION. Do not use Bash, Python, WebSearch, Read, Write, or any tool that runs code or fetches data. Numerical verification is not a proof step. "I computed n=1..10 and the pattern holds" is not a proof.

(If your agent harness requires a StructuredOutput or similar return-mechanism tool call, that is NOT a computation tool — call it to return your answer. The restriction is on tools that DO work, not tools that REPORT work.)

Your internal process (iterate until done):
- Solve: Complete rigorous solution.
- Self-improve: Reread. Fix gaps before a grader sees it.
- Self-verify: Strict grader mode. Every step justified?
- Correct: Fix and re-verify. Up to 5 rounds.
- Stop: Self-verify passes twice clean, OR 5 rounds, OR approach fundamentally wrong.

A correct answer from flawed reasoning is a failure. If incomplete, say so honestly. Never hide gaps.

PROBLEM: <insert the problem statement here>
ANGLE: <insert one starting angle here>

最初の 2 段落は重要です。独自のプロンプトを書いてこの部分を省略するセッションでは、サブエージェントが Python を 30 回実行し、間違った答えを自信満々に出すことになります。n≤10 では当てはまるのに n=100 では失敗するパターンは、証明ではありません。

出発点となる観点（エージェントごとに変えてください — references/solver_heuristics.md を参照）：

• 小さなケースを解く（n=3 より先もテストする）
• 不変量または単調量を探す
• 極端なケースを考える
• 帰納法を試す
• どのような対称性があるか？
• 逆向きに考える
• 条件を 1 つ取り除く — どこで自明に偽になるか？
• 一般化する（発明者のパラドックス — 構造を増やすと、かえって簡単になる場合がある）

各エージェントは中間ラウンドではなく、最終状態を返します。

**Verdict**: complete solution | partial result | no progress
**Rounds**: [how many verify→correct cycles]
**Method**: [key idea, one paragraph]
**Detailed Solution**: [full step-by-step, every step justified]
**Answer**: [if applicable]
**Self-verification notes**: [what you caught and fixed; remaining concerns]

再試行ポリシー：エージェントが失敗するかタイムアウトした場合は、1 回だけ再試行します。一時的な障害は発生します。

3. 解答を整理する（コンテキストの分離 — 最大の効果）

思考のトレースは検証者に同意するようバイアスを与えます。たとえ結論が間違っていても、長い推論の連鎖は裏付けとなる証拠のように読めてしまいます。検証の前に、次を取り除きます。

• 思考ブロックの内容すべて
• 「試してみましょう……」「いや、待って……」「うーん」といった文章すべて
• すべての誤った試みや後戻り

残すのは、問題文と整理された最終的な論証だけです。

各解答者の出力から、Method + Proof + Answer のセクションだけを抽出します。検証者には、解答者がそこに至った過程を一切見せません。

4. 敵対的に検証する（新しいコンテキスト、パターンを意識）

整理した各解答について、新しい検証エージェントを起動します。新しいコンテキスト：検証者が見るのは（問題文 + 整理した解答）だけです。ツールは使用しません。

検証者の役割は採点ではなく、攻撃することです。プロンプトは references/adversarial_prompts.md を読み込んでください。実行する主要なパターンは次のとおりです。

パターン	チェック内容
#4	この定理を有名な対象（ζ、平方剰余の相互法則など）に適用すると、その対象について未解決のことを証明してしまうか？→ 論理の飛躍
#18	証明の中間恒等式を「残されたギャップ」に代入する。元の主張が得られるか？→ 循環論法
#40	いずれかのステップは「一行の補題」か？その一般形を取り出す。2×2 の反例を見つける。一般形が偽なら、今回のケースで成立する特別な構造を見つける
#5	適用した定理ごとに、仮定を一から再確認する。「[0,1] 上で連続」は「ℝ 上で連続」とは異なる
#6	ある無限和を正則化した値で「有界」としていないか？境界を確認する — そこに極があれば、その和は発散する

パターンの全リスト：references/verifier_patterns.md

検証者は次を返します。

**Verdict**: HOLDS | HOLE FOUND | UNCLEAR

**If HOLE FOUND**:
- Location: [quote the problematic step]
- Pattern: [which check fired, or "other"]
- Why it breaks: [specific]
- Fixable?: [yes with X / no, fundamental]

5. 順位付けと投票による検証（非対称しきい値＋早期終了）

（判定、検証者の確信度）の順に解を順位付けし、最上位の解を選びます。新しい検証エージェントを最大5つ起動します。

非対称しきい値：確認には「成立」が4票、反証には「穴あり」が2票必要です。非対称にする理由：不安定な検証者が1人いるだけで正しい証明が却下されるのは避けたい一方、独立した異論が2つあれば実質的なシグナルだからです。

鳩の巣原理による早期終了：結論が決まったら、検証者の起動を停止します。

• 「穴あり」が2票 → 反証済みとして停止（残り3回の呼び出しを節約）
• 「成立」が4票 → 確認済みとして停止（5回目の呼び出しを節約）
• 検証者が3人の場合：「成立」2票＋「穴あり」1票なら、結論は未確定なので、さらに2人を起動します。「成立」3票＋「穴あり」0票なら、まだ4対1になる可能性があるため、さらに1人を起動します。

二重のコンテキスト隔離：各検証者は、（a）ソルバーの思考トレース（ステップ3ですでに除去済み）と、（b）他の検証者の判定の両方を知りません。各検証者は自分が最初の検証者だと思って作業します。「すでに3人のエージェントが確認しています」という社会的証明はありません。

ソルバーは自分自身の解を検証できません。 別のエージェントを使い、新しいコンテキストで検証します。

5b. あるケースがどうしても片付かないとき — 手を動かし続ける前に一歩引く

証明をケース分けした際、一方のケースは簡単に証明できるのに、もう一方で行き詰まる場合： 難しいケースに取り組み続ける前に、ケース分けそのものをなくせる別の道筋がないか考えます。

役に立つパターン：難しいケースの仮定そのものが、まだ調べていない 中間の対象 について、しばしば強い性質を含意しています。元の連鎖をたどる代わりに、その含意を直接使います。

具体例：制約付き関数 f について f(n) ≤ cn を証明するため、素数 p が f(n) を割るかどうかで場合分けします。一方の分岐は、(ℤ/p^e)* における添字の議論で片付きます。もう一方は、群の構造は同じでも、算術的な矛盾が見つからず行き詰まります。解決策は、仮定「p | f(n)」を支配方程式に代入すると、f(p) = p そのもの が導かれることに気づくことです。これが分かれば、フェルマー＋ディリクレの議論によって、両方の分岐を3行で片付けられます。ケース分けは遠回りでした。仮定のもとで既知の値を取る変数で場合分けしていたのです。

ケースBで行き詰まったら、次を確認してください。

• ケースBの仮定から、別の入力における f について何が導かれますか？
• 支配方程式に代入する別の組 (a,b) はありませんか？
• 証明しようとしていることが多すぎませんか？（よりすっきりした矛盾には、より少ない仕掛けで済むことがあります。）

これは、提示内容を整える段階でも効果があります。ケース分けを使わない証明は、より短く、より一般的です。

6. 必要に応じて修正する

検証で穴が見つかった場合は、修正エージェントを起動します。修正エージェントには（整理済みの解＋検証者による穴の報告）が渡されます。元の思考には引き続きアクセスできません。修正エージェントは、そこに至るまでの過程を読み直すのではなく、穴をもとに作業します。

A verifier found this issue in the proof:
[hole report]

Fix the proof. If the hole is fundamental (the approach doesn't work), say so and return **Verdict: no confident solution** with what partial progress remains.

For any step you cannot fully close, mark it inline: [GAP: specific description of what remains]. Gaps in the proof text, not in a separate list — they're greppable and the next reviser knows exactly where to look.

修正サイクルは最大3回です。その後、修正した証明について投票を再実行します。

パターン #40（1行の証明がきれいすぎる）が発動した場合、修正エージェントには、より強化された指示を渡します。references/adversarial_prompts.md の§7にある敵対的指示テンプレートです。このテンプレートによって、二者択一を迫ります。「一般補題は明らかに偽です（2×2の反例はこちら）。そのため、今回のケースに特別な点を見つけるか、証明のどこが破綻するかを見つけてください」。単に「問題なさそうです」と返すことはできません。

6c. ディープモード（タイトバジェットで棄権した場合）

標準のワークフローはタイトバジェットです。8 人のソルバー、約 15 分、純粋な推論で取り組みます。棄権した場合、問題に必要なのは能力ではなく、もっと時間かもしれません。

ディープモードでは、1 人のエージェントが問題に集中して取り組みます。

• 時間は無制限 — 制限時間を気にする必要はありません
• 的を絞った計算は許可 — 合同算術の確認、小規模な場合の列挙、恒等式の記号的な検証などです。探索的な総当たりや、上限のない再帰は許可されません。
• 棄権理由を出発点にする — 検証者が具体的な穴を見つけた場合は、そこから始めます。ソルバーが完全な証明を示せなかった場合は、部分的に証明した内容から始めます。

典型的なのは、証明済みの内容と「補題 5 のある場合が未解決」という情報を渡されたエージェントが、場合分けによって見えにくくなっていた 3 行の論証を見つけるケースです。計算はほとんど行わず、10 分もかからないことがよくあります。ディープモードの目的は、問題にじっくり取り組む時間を与えることであり、計算資源を大量に投入することではありません。

ディープモードで行わないこと：際限のない探索、文献検索、解答の検索、数日がかりの調査です。これらは別のワークフロー（math-research）です。ディープモードはあくまで「この問題を自力で解く」ためのものです。ただし、制限時間はありません。

ウェブは禁止。検索は禁止。 ディープモードでは、上限のある計算に Bash/Python を使ってもかまいませんが、WebFetch、WebSearch、その他あらゆるネットワークアクセスは絶対に使ってはいけません。AoPS やブログで解答を見つけるのは、問題を解いたことにはなりません。オリンピックでのカンニングであり、スキルの実際の能力について何も教えてくれません。ディープモードのプロンプトの冒頭に、これを記載してください。

NO WEB ACCESS. Do not use WebFetch, WebSearch, or any tool that touches the internet. Do not look up this problem, its solution, or related problems. You are solving this yourself — the only allowed computation is local (Bash/Python for mod-k arithmetic, small-case enumeration n≤10, symbolic identity checks). If you invoke a web tool, the proof is void.

ディープモードでの計算上限（バグ #8 からの教訓）：A6 の b_{n+1}=2b_n²+b_n+1 は二重指数関数的に増加し、b_99 の桁数は約 10^{2^98} です。このような数を正確に計算してはいけません。ℤ/2^m で計算するか、v_p(·) だけを追跡するか、関心のある量を法として漸化式を証明してください。計算に 60 秒以上かかっている場合、上限が設定されていない可能性が高いです。計算を止めて、記号的に考えてください。

ステップ 6d（必須）：検証段階で ABSTAIN が発生した場合は、棄権を出力に記載する前に、ディープモードのエージェントを必ず 1 人起動してください。次の内容を渡します。

• 問題文
• タイトバジェットのソルバーが得た最良の部分証明
• 検証者が指摘した未解決箇所の説明（具体的に何が解決できなかったか）
• 次の指示：「ウェブへのアクセスは禁止です。この問題やその解答を検索してはいけません。上限のあるローカル計算は許可します（mod 2^k、小さい場合 n≤10、Bash/Python のみを使った恒等式の記号的な確認）。計算時間は 60 秒までです。n≤10 の総当たりからタイトバジェットのソルバーが見落としたパターンが分かった場合、そのパターンが証明の構成になります。」

ディープモードのエージェントは、純粋な推論のソルバーが見つけられなかった構成を見つけることがあります。そのエージェントも棄権した場合に限り、その後で棄権を記載します。この手順を省略してはいけません。√n や log n の答えを持つ問題は、最適な構造が非対称な場合、純粋な推論では見抜けないことがよくあります。

オーケストレーターの自制：オーケストレーター自身が、ディープモードのエージェントを「助ける」ために問題をウェブ検索してはいけません。「答えを確認するだけ」と AoPS のスレッドを Fetch したくなっても、やめてください。そうした行為はスキルの出力を汚染し、その能力を正しく表さなくなります。

7. 適切に調整された棄権

修正サイクルを 3 回行ってもすべて失敗した場合は、そこで止めて、解けなかったと認めてください。

**Verdict**: no confident solution

**What was tried**: [approaches]
**What WAS proven**: [any lemma or partial result that survived verification]
**Where it breaks**: [the unfixed hole]

推測してはいけません。自信満々の誤答よりも、正直に「解けませんでした」と伝える方がましです。重要な指標は条件付き正解率です。「解けた」と言ったとき、本当に正解しているでしょうか？

8. 発表用の仕上げ（正しさを確認した後）

正しいことが検証済みの証明が、必ずしも美しい証明とは限りません。証明を発見した順序が、そのまま発表に最適な順序であることはほとんどありません。検証済みの証明を渡して、新しい発表用エージェントを起動してください。

references/presentation_prompts.md を読み込みます。エージェントは次の点を確認します。

• これを最も簡潔に述べるにはどうすればよいでしょうか？
• どの補題は本文に組み込むべきでしょうか？ どの補題は独立して扱う価値があるでしょうか？
• やりすぎている部分はありませんか？（線形で十分なのに二重指数を構成するなど）
• 答えが分かった今、振り返れば3行で済む証明はありますか？

出力：LaTeX 形式の証明。pdflatex が利用可能な場合（scripts/check_latex.sh が 0 を返す場合）は、scripts/compile_pdf.sh を使って PDF にもコンパイルします。

---

モデルのティア別デフォルト設定

詳細は references/model_tier_defaults.md をお読みください。概要：

モデル	ソルバー	検証パス	棄却まで	発表用
Haiku	8	3	修正失敗 2 回	スキップ
Sonnet	4	5	修正失敗 3 回	あり
Opus	3	5 + 全パターンの総点検	修正失敗 4 回	2 種類の草案を作成し、より明快な方を選択

弱いモデルでは、並列試行を増やし、より早く棄却します。強いモデルでは、検証を深め、発表用の仕上げにより力を入れます。

---

数値解を求める問題の場合（AIME 形式）

証明の手順は省略します。異なるアプローチを使って 5～7 個のソルバーを実行し、数値解について多数決を取ります。多数派がない場合は、上位 2 つの候補を代入して検証します。

---

主な参照資料

• references/verifier_patterns.md — 12 種類の敵対的チェック
• references/adversarial_prompts.md — すぐに使える検証プロンプト
• references/presentation_prompts.md — 推敲用プロンプト + LaTeX テンプレート
• references/model_tier_defaults.md — モデルごとの設定

---

汎用的な「検証して改善する」手法との違い

1. 二重のコンテキスト分離：検証者には、（a）ソルバーの思考過程（同意に偏らせる要因）と、（b）他の検証者の判定（社会的証明も偏りを生む）の両方を見せません。各検証者は自分が最初だと思って作業します。
2. パターン固有の攻撃：「これは正しいか？」ではなく、「#40 の間違いを犯していないか？ #4 の間違いはどうか？」と尋ねます。一般的な確認より、具体的な確認の方が効果的です。7 カテゴリーの反証分類により、検証者はチェックリストを使えます。
3. 非対称な投票と鳩の巣原理による終了条件：確認には 4 票、反証には 2 票です。信頼性の低い検証者が 1 人いても正しい証明が否定されることはありませんが、異論が 2 つあれば否定されます。結果が決まった時点で検証者の起動を止めます。明確なケースでは検証コストを約 30％削減できます。
4. 仕様の意図を先に確認：解き始める前に、「これは意図された解釈か？」と明示的に尋ねます。先行研究における最大の失敗要因はこれでした（「正解」とされた回答 63 件中 50 件は、誤った解釈に対する解答でした）。
5. 調整された棄却：部分的な結果を添えて「確信を持って解けません」と回答します。網羅性ではなく、条件付き正確性を最適化します。
6. 発表用の仕上げ：正しさと美しさは別々の工程です。発表用エージェントには検証済みの証明を渡し、それを最も明快に述べる方法を見つけてもらいます。