論文の概要: Mathesis: Towards Formal Theorem Proving from Natural Languages

• arxiv url: http://arxiv.org/abs/2506.07047v1
• Date: Sun, 08 Jun 2025 09:04:14 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-10 21:10:47.074926
• Title: Mathesis: Towards Formal Theorem Proving from Natural Languages
• Title（参考訳）: Mathesis: 自然言語から証明する形式理論を目指して
• Authors: Yu Xuejun, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haoxiong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, Claudia Beth Ong, Austen Jeremy Sugiarto, Yaoxi Zhang, Wai Ming Tai, Huan Cao, Dongcai Lu, Jiacheng Sun, Qiang Xu, Shen Xin, Zhenguo Li,
• Abstract要約: パイプライン処理の非公式な問題文を証明する最初のエンドツーエンド定理であるMathesisを開発した。 これは、自然言語問題の形式化能力を高めるために強化学習を用いた最初のオートフォーマライザであるMathesis-Autoformalizerに貢献する。 また、形式化された文から形式的な証明を生成するMathesis-Proverを提案する。
• 参考スコア（独自算出の注目度）: 40.397691467863886
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent advances in large language models show strong promise for formal reasoning. However, most LLM-based theorem provers have long been constrained by the need for expert-written formal statements as inputs, limiting their applicability to real-world problems expressed in natural language. We tackle this gap with Mathesis, the first end-to-end theorem proving pipeline processing informal problem statements. It contributes Mathesis-Autoformalizer, the first autoformalizer using reinforcement learning to enhance the formalization ability of natural language problems, aided by our novel LeanScorer framework for nuanced formalization quality assessment. It also proposes a Mathesis-Prover, which generates formal proofs from the formalized statements. To evaluate the real-world applicability of end-to-end formal theorem proving, we introduce Gaokao-Formal, a benchmark of 488 complex problems from China's national college entrance exam. Our approach is carefully designed, with a thorough study of each component. Experiments demonstrate Mathesis's effectiveness, with the autoformalizer outperforming the best baseline by 22% in pass-rate on Gaokao-Formal. The full system surpasses other model combinations, achieving 64% accuracy on MiniF2F with pass@32 and a state-of-the-art 18% on Gaokao-Formal.
• Abstract（参考訳）: 近年の大規模言語モデルの進歩は、形式的推論への強い期待を示している。 しかしながら、ほとんどの LLM ベースの定理証明者は、専門家による形式文を入力として必要とすることで、自然言語で表される実世界の問題への適用性を制限してきた。 このギャップを、パイプライン処理の非公式な問題文を証明する最初のエンドツーエンド定理であるMathesisで解決する。 自然言語問題の形式化能力を高めるために強化学習を用いた最初のオートフォーマライザであるMathesis-Autoformalizerに貢献する。 また、形式化された文から形式的な証明を生成するMathesis-Proverを提案する。 エンドツーエンドの形式的定理証明の現実的適用性を評価するため,中国の大学入試による488の複雑な問題のベンチマークであるGaokao-Formalを紹介した。 私たちのアプローチは慎重に設計されており、各コンポーネントについて綿密に研究しています。 実験はマテシスの有効性を示し、オートフォーマル化剤はガオカオホルムのパスレートを22%上回った。 システム全体の精度は、MiniF2Fでは64%、pass@32では64%、Gaokao-Formalでは18%だ。

関連論文リスト

• Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [37.10426226729792]
  本稿では,パターン駆動型推論と形式的定理証明を統合するモジュール型ニューロシンボリック手法であるLLMe-Conjecture-Prove(ECP)フレームワークを紹介する。 本稿では,様々な数学コンペティションにおける3,431の解題問題のデータセットであるConstructiveBenchを紹介する。
  論文  参考訳（メタデータ） (2025-05-24T03:52:25Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• Autoformalization with Large Language Models [22.86710743804944]
  自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。 大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。 我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
  論文  参考訳（メタデータ） (2022-05-25T09:53:30Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。