論文の概要: (Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofs
- arxiv url: http://arxiv.org/abs/2606.09674v1
- Date: Mon, 08 Jun 2026 15:57:14 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-09 14:42:07.489547
- Title: (Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofs
- Title（参考訳）: 自動形式化は簡単と思われる:厳密な証明を綴り出すトレリスプロセス意味論
- Abstract要約: 本稿では,LLMエージェントを決定論的に制約されたワークフローで活用して,リーンの自己形式化タスクの漸進的な進歩を実現する自動形式化システムを提案する。
我々のアプローチは、まず第一に厳密な証明を持つことの意味についての一般数学者の考えに動機づけられている。
プロセスによって生み出された最近のRamsey理論のブレークスルーを、エンドツーエンドのリーン形式化にリンクします。
- 参考スコア（独自算出の注目度）: 0.20305676256390937
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present Trellis: an autoformalization system that leverages LLM agents in a deterministically constrained workflow to enforce incremental progress in Lean autoformalization tasks through iterative refinement of natural language proofs. Our approach is motivated by the common mathematician's notion of what it means to have a rigorous proof in the first place: namely, that it would be routine to elaborate any part of the proof in further detail. The result is a system which aims to achieve reliable autoformalization on a modest budget and with generalist agents, with specialization to autoformalization coming not from any task-specific agent training but instead from a meaning-of-rigor inspired workflow enforced by process semantics. We link to an end-to-end Lean formalization of a recent Ramsey theory breakthrough produced by the process.
- Abstract（参考訳）: Trellis: LLMエージェントを決定論的に制約されたワークフローで活用し、自然言語証明の反復的洗練を通じて、リーンの自己形式化タスクの漸進的な進歩を強制する自動形式化システム。
私たちのアプローチは、まず第一に厳密な証明を持つことの意味についての一般数学者の考えによって動機付けられている。
その結果、質素な予算とジェネリストエージェントによる信頼性の高いオートフォーマル化を実現することを目的としており、タスク固有のエージェントトレーニングからではなく、プロセスセマンティクスによって強制されるリガーにインスパイアされたワークフローから自動フォーマル化を専門化することを目的としている。
プロセスによって生み出された最近のRamsey理論のブレークスルーを、エンドツーエンドのリーン形式化にリンクします。
関連論文リスト
- Faithful Autoformalization of Natural Language Assertions [2.8921494813790094]
Monty: アサーションのための自動形式化フレームワークを紹介します。
本手法は,新しい適合度測定値を用いたフィルタリング形式化に基づく。
提案手法は,LLMを用いてアサーションの翻訳を行う場合よりも,基礎的真理を確実に生成することを示す。
論文 参考訳（メタデータ） (2026-07-14T22:12:14Z) - Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries [18.744562922743405]
PRoSFI(Process Reward over Structured Formal Intermediates)は、精度を損なうことなく推論信頼性を高める新しい報奨法である。
完全に検証された推論チェーンのみが高い報酬を受け取る。
形式的検証の統合は、ステップバイステップのマシンチェック可能な証明を生成するためのモデルを導く。
論文 参考訳（メタデータ） (2026-03-31T09:42:13Z) - Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents [2.8292841621378844]
この設定は、協調的で分散化された証明探索と理論構築を探索する。
エージェントは、インタラクティブな証明システムと直接対話する。
承認されたすべての証明は、基礎となる証明アシスタントによってチェックされ、検証される。
論文 参考訳（メタデータ） (2026-03-06T07:34:07Z) - Refinement Provenance Inference: Detecting LLM-Refined Training Prompts from Model Behavior [58.751981587234916]
本稿では,Refinement Provenance Inference (RPI)監査タスクをRefinement Provenance Inference (RPI)として定式化する。
本稿では,ロジットレベルの信号で教師が強制する可能性機能を融合させるロジットベースのフレームワークであるReProを提案する。
トレーニング中、ReProはシャドウファインチューニングを通じて転送可能な表現を学び、訓練データアクセスなしで、見えない犠牲者の証明を推測するために軽量のリニアヘッドを使用する。
論文 参考訳（メタデータ） (2026-01-05T10:16:41Z) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - Conjecturing: An Overlooked Step in Formal Mathematical Reasoning [10.398167568549924]
結論を導かない限り、多くの数学的問題は直接形式化できない。
本研究では,大規模言語モデルの導出能力を測定するためにConjectureBenchを開発した。
提案手法は,GPT-4.1と7とDeepSeek-V3.1の13のPutnamBench問題において,最初のエンドツーエンドの自動形式化を実現する。
論文 参考訳（メタデータ） (2025-10-13T22:29:49Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
大規模言語モデル(LLM)は、幅広いタスクにまたがる強力な一般化を実証している。
最近の研究は、暗黙の推論に拍車をかけた、明示的な思考の連鎖から注意を向けている。
本調査では,表現形式から計算戦略へ焦点を移し,実行パラダイムを中心とした分類を紹介した。
論文 参考訳（メタデータ） (2025-09-02T14:16:02Z) - Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。
有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。
生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
論文 参考訳（メタデータ） (2025-07-22T08:13:01Z) - Reliable Evaluation and Benchmarks for Statement Autoformalization [18.218951526592914]
改良されたメトリクス、堅牢なベンチマーク、体系的な評価を組み合わせた総合的なアプローチを提案する。
まず、評価指標の質を評価するための新しいデータセットであるProofNetVerifとともに、人間の判断と強く相関する自動メトリクスBEq+を紹介する。
ProofNet#はProofNetの修正版であり、RLM25は6つの形式化プロジェクトから619の新しい研究レベルの数学のペアである。
論文 参考訳（メタデータ） (2024-06-11T13:01:50Z) - Rationale-Augmented Ensembles in Language Models [53.45015291520658]
我々は、数発のテキスト内学習のための合理化促進策を再考する。
我々は、出力空間における合理的サンプリングを、性能を確実に向上させるキーコンポーネントとして特定する。
有理拡張アンサンブルは既存のプロンプト手法よりも正確で解釈可能な結果が得られることを示す。
論文 参考訳（メタデータ） (2022-07-02T06:20:57Z) - Autoformalization with Large Language Models [22.86710743804944]
自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。
大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。
我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
論文 参考訳（メタデータ） (2022-05-25T09:53:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。