論文の概要: Can LLMs Reliably Grade Olympiad Proofs? A Study of Mathematical Verification with LLMs
- arxiv url: http://arxiv.org/abs/2610.36767v1
- Date: Tue, 27 Oct 2026 07:28:08 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-28 21:04:31.536479
- Title: Can LLMs Reliably Grade Olympiad Proofs? A Study of Mathematical Verification with LLMs
- Title（参考訳）: LLMは信頼性の高いオリンピアス証明が可能か? : LLMを用いた数学的検証
- Abstract要約: 本稿では,Large Language Models (LLM) に基づく検証の体系化について述べる。
具体的には,USAMO 2025候補解の人間計算データセットとエキスパートグレーディングを導入し,既存のLCM検証を広範囲に評価する。
また,TROJANを提案する。TROJANは大規模に高忠実度逆証明を生成するための反復的自己批判パイプラインである。
- 参考スコア（独自算出の注目度）: 43.088487248612985
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large Language Models (LLMs) have made remarkable progress on solving competition-level mathematics, yet their ability to verify natural-language mathematical proofs remains relatively underexplored. This gap is especially pronounced for Olympiad-level proofs, which require meticulous assessment of each claim in a long reasoning chain. Current proof verification thus primarily relies on expert inspection, which is costly to scale. In this paper, we present a systematic study of LLM-based verification in this setting. Specifically, we introduce a human-curated dataset of USAMO 2025 candidate solutions with expert grading, and conduct a broad evaluation of existing LLM verifiers across frontier models. We also propose TROJAN, an iterative self-critique pipeline for generating high-fidelity adversarial proofs at scale. Our comprehensive evaluation covers 20 models spanning seven metrics, two prompt styles, three inference methods, and three prompt templates, showing that state-of-the-art models still leave considerable room for improvement. To narrow this gap, we propose MABGrader, a Multi-Armed Bandit framework that reframes grading as arm selection over the discrete score space. MABGrader outperforms the SOTA ProofGrader by 26.4% in Quadratic Weighted Kappa and reduces grading error by 14%. Code and dataset are available at https://github.com/aziksh-ospanov/TROJAN.
- Abstract（参考訳）: 大規模言語モデル (LLM) は競争レベルの数学の解法において顕著な進歩を遂げているが、自然言語の数学的証明の検証能力はいまだに未熟である。
このギャップは特にオリンピアドレベルの証明で顕著であり、長い推論連鎖においてそれぞれの主張を慎重に評価する必要がある。
したがって、現在の検証は、主に専門家による検査に依存しており、スケールするのにコストがかかる。
本稿では, LLMによる検証の体系化について述べる。
具体的には,USAMO 2025候補解の人間計算データセットとエキスパートグレーディングを導入し,フロンティアモデル全体で既存のLLM検証を広範囲に評価する。
また,TROJANを提案する。TROJANは大規模に高忠実度逆証明を生成するための反復的自己批判パイプラインである。
総合評価では,7つの指標,2つのプロンプトスタイル,3つの推論方法,および3つのプロンプトテンプレートにまたがる20のモデルについて検討した。
このギャップを狭めるために、離散スコア空間上でのグルーピングをアーム選択として再配置するマルチアーマッド・バンディットフレームワークMABGraderを提案する。
MABGraderはSOTA ProofGraderを26.4%上回り、グレーディングエラーを14%減らす。
コードとデータセットはhttps://github.com/aziksh-ospanov/TROJAN.comで公開されている。
関連論文リスト
- LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - Human-in-the-Loop Benchmarking of Heterogeneous LLMs for Automated Competency Assessment in Secondary Level Mathematics [0.0]
本稿では,中等レベルの数学評価において,複数の LLM の有効性を評価するための "Human-in-the-Loop" ベンチマークフレームワークを提案する。
ネパールのグレード10オプショナル数学のカリキュラムに基づいて,4つのトピックと4つの横断的能力のための多次元ルーブリックを作成した。
GeminiベースのMixture-of-Experts(Sparse MoE)モデルはFair Agreement(Kappa_w 0.38)を達成したが、より大きなOrion(70B)モデルはNo Agreement(Kappa_w = -0.0261)を示した。
論文 参考訳（メタデータ） (2026-04-29T12:36:19Z) - Solving Inequality Proofs with Large Language Models [42.667163027148916]
不等式証明は様々な科学・数学分野において不可欠である。
これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。
我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
論文 参考訳（メタデータ） (2025-06-09T16:43:38Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。