Proofs
#Pocket
#NLP
#Dataset
#LanguageModel
#Evaluation
#Reasoning
#Mathematics
Issue Date: 2025-11-12 Stress-Testing the Reasoning Competence of Language Models With Formal Proofs, Arkoudas+, EMNLP'25 Findings GPT Summary- ProofGridという新しい論理推論タスクを用いて、LLMsとLRMsの性能を広範に評価。タスクは命題論理と方程式論理の証明作成・検証を含み、証明のインペインティングとギャップ埋めも新たに導入。実験ではトップモデルの優れたパフォーマンスが示される一方、体系的な失敗も確認。1万件以上の形式的推論問題と証明からなる新データリソースも公開。 Comment
#Pocket #NLP #Dataset #LanguageModel #Evaluation #Mathematics #read-later #Selected Papers/Blogs
Issue Date: 2025-10-18 [Paper Note] Reliable Fine-Grained Evaluation of Natural Language Math Proofs, Wenjie Ma+, arXiv'25, 2025.10 GPT Summary- 大規模言語モデル（LLMs）による数学的証明の生成と検証における信頼性の高い評価者が不足している問題に対処するため、0から7のスケールで評価する新たな評価者ProofGraderを開発。ProofBenchという専門家注釈付きデータセットを用いて、評価者の設計空間を探求し、低い平均絶対誤差（MAE）0.926を達成。ProofGraderは、最良の選択タスクにおいても高いスコアを示し、下流の証明生成の進展に寄与する可能性を示唆している。 Comment
#Article #NLP #LanguageModel #Mathematics #PostTraining #Simplification
Issue Date: 2025-10-22 ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations, Gu+, 2025.10 Comment
Issue Date: 2025-11-12 Stress-Testing the Reasoning Competence of Language Models With Formal Proofs, Arkoudas+, EMNLP'25 Findings GPT Summary- ProofGridという新しい論理推論タスクを用いて、LLMsとLRMsの性能を広範に評価。タスクは命題論理と方程式論理の証明作成・検証を含み、証明のインペインティングとギャップ埋めも新たに導入。実験ではトップモデルの優れたパフォーマンスが示される一方、体系的な失敗も確認。1万件以上の形式的推論問題と証明からなる新データリソースも公開。 Comment
元ポスト:
#Pocket #NLP #Dataset #LanguageModel #Evaluation #Mathematics #read-later #Selected Papers/Blogs
Issue Date: 2025-10-18 [Paper Note] Reliable Fine-Grained Evaluation of Natural Language Math Proofs, Wenjie Ma+, arXiv'25, 2025.10 GPT Summary- 大規模言語モデル（LLMs）による数学的証明の生成と検証における信頼性の高い評価者が不足している問題に対処するため、0から7のスケールで評価する新たな評価者ProofGraderを開発。ProofBenchという専門家注釈付きデータセットを用いて、評価者の設計空間を探求し、低い平均絶対誤差（MAE）0.926を達成。ProofGraderは、最良の選択タスクにおいても高いスコアを示し、下流の証明生成の進展に寄与する可能性を示唆している。 Comment
元ポスト:
これは非常に重要な研究に見える
#Article #NLP #LanguageModel #Mathematics #PostTraining #Simplification
Issue Date: 2025-10-22 ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations, Gu+, 2025.10 Comment
pj page: https://proof-optimizer.github.io
LLMの通常利用時の応答も（おそらくベンチマークに最適化されているせいで）長すぎると思っているけど、数学の証明も長いんだなあ、と感じた