汎用LLM・AI開発⭐ リポ 2品質スコア 59/100

seed-prover-automated-theorem-proving

形式検証フィードバックと長鎖の思考プロセスを組み合わせたフレームワークです。自動定理証明のための深く幅広い数学推論を実現します。補題ベースの改善とテスト時推論戦略により、形式化されたIMO問題で78.1%の成果を達成します。

description の原文を見る

Framework combining formal verification feedback with long chain-of-thought reasoning to enable deep and broad mathematical reasoning for automated theorem proving. Achieves 78.1% on formalized IMO problems through lemma-based refinement and test-time inference strategies.

SKILL.md 本文

注意: このスキルのライセンスは ライセンス未確認 です。本サイトでは本文プレビューのみを表示しています。利用前に GitHub の原本でライセンス条件をご確認ください。

Seed-Prover: 自動定理証明による形式的検証

Seed-Prover は、強化学習と Lean 証明支援系からの形式的検証フィードバックを組み合わせることで、自動定理証明における大きな進歩を実現しています。このシステムにより、言語モデルが複数の推論戦略を通じて数学的証明を反復的に改良でき、形式的数学の最先端パフォーマンスを達成しています。

コアコンセプト

重要な洞察は、形式的検証が明確で曖昧性のない教師信号を提供することです。証明は Lean で受け入れられるか（正しい）、または具体的なエラーを示して改良を導きます。Seed-Prover は言語モデルの出力だけに頼るのではなく、この構造化されたフィードバックを使用して以下を実現します:

Lean エラーメッセージに基づいて証明を反復的に改良
以前に証明された補題を活用して段階的により複雑な証明を構築
自己要約を適用して本質的な証明構造を抽出
3つのテスト時推論戦略を採用して深さ（単一証明の探索）と広さ（複数証明の試行）の両方の推論を実現

アーキテクチャ概要

システムは以下のコンポーネントで構成されています:

証明生成モジュール: 言語モデルが Lean 形式構文で証明を生成
形式的検証ループ: Lean 型チェッカ

...

全文を GitHub の原本で見る →リポジトリ

詳細情報

作者: ADu2021
リポジトリ: ADu2021/skillXiv
ライセンス: 不明
最終更新: 2026/3/26

GitHubで原本を見る →フィードバックを送る

Source: https://github.com/ADu2021/skillXiv / ライセンス: 未指定