Proofs
[Paper Note] Aletheia tackles FirstProof autonomously, Tony Feng+, arXiv'26, 2026.02
Paper/Blog Link My Issue
#NLP #LanguageModel #AIAgents #Mathematics #ScientificDiscovery Issue Date: 2026-02-28 GPT Summary- 数理研究エージェントAletheiaは、Gemini 3 Deep Thinkを活用し、FirstProofチャレンジにおいて10問中6問を自動解決。問題8は専門家の合意が得られなかった。実験の詳細と評価、解釈についても明示し、生データは指定のリンクで入手可能。 Comment
元ポスト:
First Proof:
- [Paper Note] First Proof, Mohammed Abouzaid+, arXiv'26, 2026.02
[Paper Note] First Proof, Mohammed Abouzaid+, arXiv'26, 2026.02
Paper/Blog Link My Issue
#NLP #Dataset #LanguageModel #AIAgents #Evaluation #Mathematics #ScientificDiscovery #Selected Papers/Blogs Issue Date: 2026-02-16 GPT Summary- AIシステムの数学問題回答能力を評価するため、著者が作成した10の未公開の数学問題を共有。答案は著者に知られているが、短期間は非公開とする。 Comment
pj page: https://1stproof.org/
元ポスト:
ポイント解説:
自分たちの研究過程で生じた自分たちは答えを発見しているが世間には未発表な問題と暗号化された解答が公開されている。2月13日時点で鍵が公開されているようだ。果たしてどの程度AIは解答ができたのだろうか？
Google DeepmindのAlethiaは10個中6つの問題を解くことができたようである:
Alethia:
- [Paper Note] Accelerating Mathematical and Scientific Discovery with Gemini Deep Think, Google DeepMin, 2026.02
[Paper Note] Premise Selection for a Lean Hammer, Thomas Zhu+, ICLR'26, 2025.06
Paper/Blog Link My Issue
#MachineLearning #Mathematics Issue Date: 2026-02-05 GPT Summary- Lean向けの初のエンドツーエンドのドメイン一般ハンマー「LeanHammer」を提案。ユーザー固有のコンテキストに適応し、効率的な前提選択システムを導入。評価結果では、LeanHammerが既存の手法より21％多くの目標を解決し、さまざまなドメインでも良好な一般化を示す。形式的検証におけるニューラル検索とシンボリック推論の統合を図る。 Comment
pj page: https://cmu-l3.github.io/lean-hammer/
元ポスト:
Stress-Testing the Reasoning Competence of Language Models With Formal Proofs, Arkoudas+, EMNLP'25 Findings
Paper/Blog Link My Issue
#NLP #Dataset #LanguageModel #Evaluation #Reasoning #Mathematics Issue Date: 2025-11-12 GPT Summary- ProofGridという新しい論理推論タスクを用いて、LLMsとLRMsの性能を広範に評価。タスクは命題論理と方程式論理の証明作成・検証を含み、証明のインペインティングとギャップ埋めも新たに導入。実験ではトップモデルの優れたパフォーマンスが示される一方、体系的な失敗も確認。1万件以上の形式的推論問題と証明からなる新データリソースも公開。 Comment
元ポスト:
[Paper Note] Reliable Fine-Grained Evaluation of Natural Language Math Proofs, Wenjie Ma+, arXiv'25, 2025.10
Paper/Blog Link My Issue
#NLP #Dataset #LanguageModel #Evaluation #Mathematics #read-later #Selected Papers/Blogs Issue Date: 2025-10-18 GPT Summary- 大規模言語モデル（LLMs）による数学的証明の生成と検証における信頼性の高い評価者が不足している問題に対処するため、0から7のスケールで評価する新たな評価者ProofGraderを開発。ProofBenchという専門家注釈付きデータセットを用いて、評価者の設計空間を探求し、低い平均絶対誤差（MAE）0.926を達成。ProofGraderは、最良の選択タスクにおいても高いスコアを示し、下流の証明生成の進展に寄与する可能性を示唆している。 Comment
元ポスト:
これは非常に重要な研究に見える
QED-Nano: Teaching a Tiny Model to Prove Hard Theorems, LM Provers Team, 2026.02
Paper/Blog Link My Issue
#Article #NLP #LanguageModel #Supervised-FineTuning (SFT) #ReinforcementLearning #Blog #Mathematics #SmallModel #PostTraining #Rubric-based #Initial Impression Notes Issue Date: 2026-02-16 Comment
元ポスト:
ポイント解説:
早くもReasoning Cacheが利用されている:
- [Paper Note] Reasoning Cache: Continual Improvement Over Long Horizons via Short-Horizon RL, Ian Wu+, arXiv'26, 2026.02
4B級のモデルで特定タスクに特化したモデルを作りたい場合に非常に役立ちそうなレシピ
ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations, Gu+, 2025.10
Paper/Blog Link My Issue
#Article #NLP #LanguageModel #Mathematics #PostTraining #Simplification Issue Date: 2025-10-22 Comment
pj page: https://proof-optimizer.github.io
LLMの通常利用時の応答も（おそらくベンチマークに最適化されているせいで）長すぎると思っているけど、数学の証明も長いんだなあ、と感じた