frenzymath/Danus

何を解決するか

Danusは、単一のLLMコンテキストウィンドウでは処理できないほど大きな数学的推論問題、または単一の試行では困難な問題を解決するように設計されています。数学的に検証された事実のみがシステムの永続的メモリに格納されることで、『幻覚』の蓄積を防ぎ、複数のエージェントが長大な証明に協力しても真実を失わないようにします。

動作方法

Danusは、3つの専門的なエージェント役割に厳密な分権化を採用しています。

1. メインエージェント（オーガナイザー）：グローバルな計画を実行し、問題を小さなターゲットに分解し、ワーカーの群れを指揮します。直接メモリに事実を提出することはできません。
2. ワーカー：個々の主張（補題や反例）の証明に集中します。証明を検証者に提出し、フィードバックに基づいて修正します。
3. 検証者：状態を持たない権威として、唯一のゲートキーパーとして機能します。検証済みの結果を事実グラフに受け入れるか、修正ヒントとともに拒否します。

検証済みの結果は、コンテンツアドレス可能な事実グラフに格納され、各事実はその依存する事実とリンクされています。目標に到達すると、システムは最終結果を人間が読めるレポートやLaTeX論文に変換できます。

対象ユーザー

研究者や数学者で、研究レベルの数学的証明の発見と検証を自動化したい方々に向けられています。

特徴

• 事実グラフメモリ：構造的で依存関係を意識したメモリシステム。唯一の真実のソースとして機能します。
• 役割制限付きツール：ツールの権限（例：オーガナイザーは検証者をバイパスできない）によってセキュリティと正しさが保証されます。
• 提出・検証・修正のサイクル：ワーカーが証明を反復的に改善し、状態を持たない検証者に受け入れられるまで続けます。
• 自動論文生成：検証済みの事実グラフをコンパイル可能なLaTeX論文に変換し、全体として再検証します。