論文の概要: AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics
- arxiv url: http://arxiv.org/abs/2609.05157v1
- Date: Fri, 04 Sep 2026 13:58:19 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-07 18:15:24.063605
- Title: AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics
- Title（参考訳）: AxQM:有限次元量子力学ライブラリにおける形式的証明合成のためのテキストスケールベンチマーク
- Abstract要約: AxQMは物理学における最大の証明合成ベンチマークである。
タスク数によっては、物理における証明合成のベンチマークとしては最大で4倍である。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Formalizing mathematics in a proof assistant, where a machine checks every definition, statement and proof, has set a new standard of rigor. Large language models are now capable of formalizing autonomously, even at the scale of whole textbooks. We bring this standard of rigor to physics, where theoretical arguments carry idealizations that are rarely stated fully, and any logical gaps could have a cascading effect on interdependent results. Recognizing the need to evaluate autoformalization systems for physics, we release AxQM, 1,019 kernel-checkable proof-synthesis tasks over 479 items drawn from the textbook Quantum Computation and Quantum Information by Nielsen and Chuang. The tasks are stated in a custom Lean library of finite-dimensional quantum mechanics. By task count, it is the largest proof-synthesis benchmark in physics by a factor of four. AxQM is derived from a near-complete formalization of the formal portions of the textbook, so every task is guaranteed a solution, which we keep private. Grading of the benchmark is done deterministically by the Lean kernel, which checks that the proof compiles, that no sorry appears in it or in any declaration it depends on, and that it introduces no new axioms.
- Abstract（参考訳）: 機械がすべての定義、ステートメント、証明をチェックする証明アシスタントでの数学の形式化は、新しい厳密な基準を設定した。
大規模な言語モデルは、教科書全体の規模であっても、自律的に形式化することが可能になった。
我々は、この厳密な標準を物理学に持ち込み、理論的議論は、完全に記述されることのほとんどない理想化を持ち、任意の論理的ギャップは、相互依存的な結果にカスケード効果を持つ。
AxQM, 1,019のカーネルチェック可能な証明合成タスクを, Nielsen と Chuang による教科書Quantum Computation and Quantum Information から479個の項目から抽出した。
これらのタスクは、有限次元量子力学のカスタムLeanライブラリに記述されている。
タスク数によっては、物理における証明合成のベンチマークとしては最大で4倍である。
AxQM は教科書の形式部分のほぼ完全な形式化から派生しているので、全てのタスクは、私たちがプライベートに維持するソリューションとして保証される。
ベンチマークのグラデーションは、Leanカーネルによって決定的に行われる。これは、証明がコンパイルされ、それや、それが依存する宣言に現れず、新しい公理を導入しないことをチェックします。
関連論文リスト
- QBism Logic [0.0]
QBismは、量子論をエージェントの確率割り当ての規範的分野として解釈する。
本稿ではその図式を論理的に定式化する。
論文 参考訳（メタデータ） (2026-07-19T10:20:53Z) - Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information [4.962621441807053]
理論解析のための再利用可能な形式的基盤として設計された,量子情報のためのLean 4ライブラリを提示する。
有限次元量子系上の正半定値作用素に対するサンドイッチ付きレニイ相対エントロピーのDPIを定式化する。
このライブラリは有限次元量子力学の基底非依存作用素理論フレームワークを提供する。
論文 参考訳（メタデータ） (2026-07-06T18:00:00Z) - Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
大きな言語モデル(LLM)は、人間の検出を避ける微妙なエラーを生成する。
最近の傾向は、汎用LLMがリーンのために明確に調整されたより小さなモデルを上回っていることを示している。
汎用LLMを用いたエージェントオートフォーマル化フレームワークを提案する。
論文 参考訳（メタデータ） (2026-06-30T05:05:03Z) - LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization [1.711666249985278]
本稿では,人間科学者とAIが共同で公式な証明を行う,ループ型アプローチを提案する。
Lean Atlasはリーン4プロジェクトの依存性グラフをインタラクティブなWebビューアとして視覚化するツールです。
コア機能であるLean Compassは、選択された定理セットが与えられたら、自動的にプロジェクト固有のノードを抽出するアルゴリズムである。
論文 参考訳（メタデータ） (2026-03-16T14:19:33Z) - A Formalization of the Generalized Quantum Stein's Lemma in Lean [0.0]
我々は、リーン対話的定理証明器において、ハヤシとヤマサキ(2024年)で提示された証明を定式化する。
これは、これまでコンピュータで検証された証明を持つ物理学で最も技術的に要求される定理である。
論文 参考訳（メタデータ） (2025-10-09T17:41:13Z) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - Autoformalizing Euclidean Geometry [74.72212706513318]
ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。
1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。
自己形式化定理文の自動意味評価を行う。
論文 参考訳（メタデータ） (2024-05-27T14:35:10Z) - Unifying (Quantum) Statistical and Parametrized (Quantum) Algorithms [65.268245109828]
我々はカーンズのSQオラクルとヴァリアントの弱い評価オラクルからインスピレーションを得ます。
評価クエリから学習するための非条件の下限を出力する,広範かつ直感的なフレームワークを提案する。
論文 参考訳（メタデータ） (2023-10-26T18:23:21Z) - Simple Tests of Quantumness Also Certify Qubits [69.96668065491183]
量子性の検定は、古典的検証者が証明者が古典的でないことを(のみ)証明できるプロトコルである。
我々は、あるテンプレートに従う量子性のテストを行い、(Kalai et al., 2022)のような最近の提案を捉えた。
すなわち、同じプロトコルは、証明可能なランダム性や古典的な量子計算のデリゲートといったアプリケーションの中心にあるビルディングブロックであるqubitの認定に使用できる。
論文 参考訳（メタデータ） (2023-03-02T14:18:17Z) - Noisy Quantum Kernel Machines [58.09028887465797]
量子学習マシンの新たなクラスは、量子カーネルのパラダイムに基づくものである。
消散と脱コヒーレンスがパフォーマンスに与える影響について検討する。
量子カーネルマシンでは,デコヒーレンスや散逸を暗黙の正規化とみなすことができる。
論文 参考訳（メタデータ） (2022-04-26T09:52:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。