論文の概要: Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free
- arxiv url: http://arxiv.org/abs/2608.28997v1
- Date: Sat, 29 Aug 2026 02:09:18 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-01 18:31:30.812681
- Title: Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free
- Title（参考訳）: 証明の量, 偏見の不足: 検証が自由になったとき, 数学的知識に何が起こるか
- Abstract要約: 2026年5月、OpenAIモデルはアーズ単位距離予想に対する反例を生み出した。
同じ日に5人の数学者が人間による検証版を出版し、その結果は数週間以内に文献に載った。
2026年8月、同研究所は10の数学的および理論的コンピュータ科学結果を発表し、それぞれにマシンチェック可能なLean 4証明書を添付した。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: In May 2026 an OpenAI model produced a counterexample to the Erdős unit distance conjecture. Five mathematicians published a human-verified version the same day, and the result entered the literature within weeks. In August 2026 the same laboratory published ten mathematical and theoretical computer science results, each accompanied by a machine-checkable Lean 4 certificate with no unproved steps. Four weeks later, one remained the subject of an unresolved dispute over whether its formalization meant what it claimed. We argue that this difference is structural. We distinguish three layers of verification: derivational validity, which a kernel checks; representational fidelity, whether the formal statement means the intended question; and epistemic significance. Only the first is mechanizable. Making it effectively free therefore does not eliminate verification work but shifts the burden to layers dependent on scarce expert attention. Measurements of the August corpus illustrate the shift. The kernel-checked proofs total 20.6 MB, while the statements requiring human audit total 55.6 KB, a ratio of 379 to 1. Yet those statements contain 218 bespoke definitions rather than relying on community-vetted ones. The audit surface is therefore small in volume but irreducibly expert. We argue that machine checking produces verification abundance while leaving adjudication scarce. We propose a six-category taxonomy of representational mismatch, a disclosure schema for machine-generated mathematical claims, and implications for software, cryptography, and regulated decision systems.
- Abstract（参考訳）: 2026年5月、OpenAIモデルはエルデシュ単位距離予想に対する反例を生み出した。
同じ日に5人の数学者が人間による検証版を出版し、その結果は数週間以内に文献に載った。
2026年8月、同研究所は10の数学的および理論的コンピュータ科学結果を発表した。
4週間後、その形式化が主張するものを意味するかどうかに関して、未解決の論争の対象となった。
この違いは構造的だと主張する。
我々は、カーネルがチェックする導出的妥当性、表現的忠実性、形式的ステートメントが意図する質問を意味するかどうか、および認識的意義の3つの検証層を区別する。
1つ目だけが機械化可能である。
したがって、効果的に自由にすることは、検証作業を排除するのではなく、専門家の注意不足に依存するレイヤに負担をシフトさせる。
8月コーパスの測定では、この変化が示されている。
カーネルチェックされた証明は、合計20.6MB、人間の監査を必要とするステートメントは、合計55.6KB、比率379対1である。
しかし、これらのステートメントには、コミュニティが検証した定義に頼るのではなく、218のbespoke定義が含まれている。
したがって、監査面はボリュームが小さいが、不可解に熟練している。
我々は, マシンチェックは, 偏見が乏しいまま, 検証量の増大を招きかねないと主張している。
本稿では,表現ミスマッチの6カテゴリ分類,機械による数学的クレームの開示スキーマ,およびソフトウェア,暗号,規制決定システムへの影響について述べる。
関連論文リスト
- Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification [13.942115092285697]
リーンシグナルを推論プロセスに統合することで、非公式な推論と公式な推論のギャップを埋めます。
トレーニング不要のエージェントパイプラインであるMagentaを紹介します。これは、自然言語の問題のみを与えられた上で、回答を生成し、Lean 4ステートメントとして表現し、マシンチェックされた証明を構築します。
論文 参考訳（メタデータ） (2026-09-10T09:48:07Z) - VeriPhy: Agentic Physical Reasoning for World Model Evaluation and Refinement [57.86962208273888]
テキストのみのプランナが入力された物理義務にプロンプトをコンパイルする監査可能な物理検証システムを提案する。
それぞれのアクションは、ペイロードがタイプされた測定か、明示的にタグ付けされた学習状態である証明付きエビデンスレコードを返す。
我々は, 実発生障害を即時参照, 空間, 時間でローカライズする, 1500クリックの欠陥記録のコーパスにおいて, 評価をアンロックする。
論文 参考訳（メタデータ） (2026-09-02T20:36:45Z) - A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver [3.8048003898069975]
SAIR Mathematics Distillation Challenge on Equational Theories では、あるマグマが別のマグマの同一性を意味するかどうかを解き明かす。
我々は,最も安価な第1カスケードとして構成された単一ファイル解決器を提案する。
その偽分岐は、構造化代数族上の係数テスト、有界有限モデル探索、明示的な中心群群証人、およびいくつかの無限キャリア証人を組み合わせたものである。
論文 参考訳（メタデータ） (2026-09-01T04:34:00Z) - Surprisal Theory is Tautological (without Rational Grounding) [60.917028769172795]
予備理論は、文脈における言語単位の人間の処理困難は、ある言語モデルの下でのそのサブプライムのアフィン関数であると主張している。
この主張は、これ以上の制約を伴わないタウトロジーであると私は主張する。
私は、タウトロジーを破るには合理主義的な介入が必要だと結論付けます。
論文 参考訳（メタデータ） (2026-07-23T17:54:37Z) - A Machine-Verified Proof of a Quantum-Optimization Conjecture [0.0]
量子最適化における10年以上の課題を,マシンで検証した解決法について報告する。
大規模な言語モデルであるClaude Fable 5を用いて証明し,その正しさをエンドツーエンドで検証した。
この研究は、量子情報科学などにおけるオープンな予想を解決するための道を開いた。
論文 参考訳（メタデータ） (2026-06-29T01:25:40Z) - Can Humans Tell? A Dual-Axis Study of Human Perception of LLM-Generated News [47.03825808787752]
人間は、ニュース記事が人によって書かれたか、あるいは大きな言語モデル(LLM)によって書かれたかを知ることができますか?
本稿では,人間対機械(人間対機械)と正当性判定(正当性対偽判定)を連続的なスケールで測定する研究プラットフォームであるJiceGPTを用いて,この問題を考察する。
筆者らは,(1) 被験者が人文テキストから機械生成物を確実に識別できないこと,(2) 認知疲労による約30回の連続的な評価の後,その精度が低下すること,の5つを報告した。
論文 参考訳（メタデータ） (2026-04-04T15:03:42Z) - Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium [0.564046562677526]
本稿では、VML(Vlasov-Maxwell-Landau)システムにおける平衡特性の完全式化について述べる。
プロジェクトはAIによる数学的研究の完全なループを実証する。
論文 参考訳（メタデータ） (2026-03-16T21:21:53Z) - Mathematics with large language models as provers and verifiers [1.1029146548022293]
ChatGPT は6つの IMO 問題のうち5つを解き、[Cohen, Journal of Sequences, 2025] の 6 個の数理論の予想の約3分の1を閉じる。
論文 参考訳（メタデータ） (2025-10-11T20:35:25Z) - Solving Inequality Proofs with Large Language Models [42.667163027148916]
不等式証明は様々な科学・数学分野において不可欠である。
これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。
我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
論文 参考訳（メタデータ） (2025-06-09T16:43:38Z) - Natural Language Deduction with Incomplete Information [43.93269297653265]
当初,すべての前提が明記されていないような不特定設定を処理できる新しいシステムを提案する。
自然言語生成モデルを用いて、他の前提と結論が与えられた前提を誘導的に推論することにより、結論が真であるために必要な証拠の欠落を示唆することができる。
論文 参考訳（メタデータ） (2022-11-01T17:27:55Z) - Nested Counterfactual Identification from Arbitrary Surrogate
Experiments [95.48089725859298]
観測と実験の任意の組み合わせからネスト反事実の同定について検討した。
具体的には、任意のネストされた反事実を非ネストされたものへ写像できる反ファクト的非ネスト定理(英語版)(CUT)を証明する。
論文 参考訳（メタデータ） (2021-07-07T12:51:04Z) - Causal Expectation-Maximisation [70.45873402967297]
ポリツリーグラフを特徴とするモデルにおいても因果推論はNPハードであることを示す。
我々は因果EMアルゴリズムを導入し、分類的表現変数のデータから潜伏変数の不確かさを再構築する。
我々は、反事実境界が構造方程式の知識なしにしばしば計算できるというトレンドのアイデアには、目立たずの制限があるように思える。
論文 参考訳（メタデータ） (2020-11-04T10:25:13Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。