Fugu-MT 論文翻訳(概要): MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study

論文の概要: MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study

arxiv url: http://arxiv.org/abs/2503.04763v1
Date: Tue, 11 Feb 2025 09:32:55 GMT
ステータス: 翻訳完了
システム内更新日: 2025-03-16 10:18:16.332114
Title: MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
Title（参考訳）: RocqのMiniF2F: 証明アシスタント間の自動翻訳 - ケーススタディ
Authors: Jules Viennot, Guillaume Baudart, Emilio Jesùs Gallego Arias, Marc Lelarge,
Abstract要約: 我々は、MiniF2FをRocqに変換するために、最先端のLLMを用いて実験を行う。我々は488の定理のうち478をうまく翻訳した。
参考スコア（独自算出の注目度）: 4.0373504895791985
License:
Abstract: In this work, we conduct an experiment using state-of-the-art LLMs to translate MiniF2F into Rocq. The translation task focuses on generating a Rocq theorem based on three sources: a natural language description, the Lean formalization, and the Isabelle formalization. We conducted our experiment in 3 stages of increasing complexity, from basic one-shot prompting to multi-turn conversations that incorporate feedback from unsuccessful attempts. At each stage, we perform multiple rounds of translation using increasingly advanced models: GPT-4o mini, Claude 3.5 Sonnet, o1 mini, and o1. We successfully translated 478 out of 488 theorems. The dataset is opensource: https://github.com/LLM4Rocq/miniF2F-rocq.
Abstract（参考訳）: 本研究では,MiniF2F を Rocq に変換するために,最先端の LLM を用いて実験を行う。翻訳作業は、自然言語の記述、リーンの形式化、イザベルの形式化という3つの情報源に基づくロクックの定理の生成に焦点を当てている。難解な試みからフィードバックを取り入れた,基本的なワンショットプロンプトからマルチターン会話まで,複雑性を増大させる3段階の実験を行った。各段階で、GPT-4o mini、Claude 3.5 Sonnet、o1 mini、o1といった高度なモデルを用いて複数の翻訳を行う。我々は488の定理のうち478をうまく翻訳した。データセットはオープンソースである。 https://github.com/LLM4Rocq/miniF2F-rocq。

関連論文リスト

Herald: A Natural Language Annotated Lean 4 Dataset [15.42247133378869]
本稿では,Mathlib4コーパス(形式言語Lean 4における数学の統一ライブラリ)を自然言語に翻訳するための新しいフレームワークを提案する。私たちはこのパイプラインの結果をHeraldとしてMathlib4で発表します(階層とレトリバルベースのトランスレーショナルリーン)。また,Heraldを微調整したHerald Translatorを提案する。
論文参考訳（メタデータ） (2024-10-09T10:11:24Z)
Investigating the translation capabilities of Large Language Models trained on parallel data only [1.5974665548135587]
大規模言語モデル(LLM)は、自然言語処理(NLP)タスクの幅広い範囲で例外的な習熟性を示している。 PLUMEは,カタルーニャ語中心の並列例に特化して訓練された語彙サイズ(32k,128k,256k)の異なる3つの2B LLMのコレクションである。これらのモデルは、16の教師付き翻訳方向と56のゼロショット上で、以前のエンコーダ・デコーダアーキテクチャと互換性がある。
論文参考訳（メタデータ） (2024-06-13T14:08:56Z)
Can Small Language Models Help Large Language Models Reason Better?: LM-Guided Chain-of-Thought [51.240387516059535]
タスク推論において,ブラックボックスの大きな (>10B) LMを導くために,軽量 (すなわち 1B) 言語モデル (LM) を利用する新しいフレームワーク LM-Guided CoT を導入する。 1)知識蒸留と2)合理性指向とタスク指向の報酬信号からの強化学習を通してモデルを最適化する。
論文参考訳（メタデータ） (2024-04-04T12:46:37Z)
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文参考訳（メタデータ） (2024-02-14T05:57:58Z)
LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
論文参考訳（メタデータ） (2023-10-23T17:58:40Z)
MLAgentBench: Evaluating Language Agents on Machine Learning Experimentation [96.71370747681078]
我々は,CIFAR-10におけるモデル性能の改善から,BabyLMのような最近の研究課題まで,13のタスクからなるMLAgentBenchを紹介した。各タスクに対して、エージェントはファイルの読み書き、コードの実行、出力の検査などのアクションを実行することができる。我々は、Claude v1.0、Claude v2.1、Claude v3 Opus、GPT-4、GPT-4-turbo、Gemini-Pro、Mixtralに基づいてベンチマークエージェントをベンチマークし、Claude v3 Opusエージェントが成功率の点で最高であることを示す。
論文参考訳（メタデータ） (2023-10-05T04:06:12Z)
Multilingual Machine Translation with Large Language Models: Empirical Results and Analysis [103.89753784762445]
大規模言語モデル(LLM)は多言語機械翻訳(MMT)の処理において顕著な可能性を示した。本稿では, MMT における LLM の利点と課題を体系的に検討する。また,ChatGPTとGPT-4を含む8つのLLMを徹底的に評価した。
論文参考訳（メタデータ） (2023-04-10T15:51:30Z)
Document-Level Machine Translation with Large Language Models [91.03359121149595]
大規模言語モデル(LLM)は、様々な自然言語処理(NLP)タスクに対して、一貫性、凝集性、関連性、流動性のある回答を生成することができる。本稿では,LLMの談話モデルにおける能力について詳細に評価する。
論文参考訳（メタデータ） (2023-04-05T03:49:06Z)
Unsupervised Neural Machine Translation with Generative Language Models Only [19.74865387759671]
生成事前学習言語モデルから、最先端の教師なしニューラルネットワーク翻訳システムを導出する方法を示す。本手法は, 数発増幅, 蒸留, 逆翻訳の3段階からなる。
論文参考訳（メタデータ） (2021-10-11T17:35:34Z)
Using LSTM to Translate French to Senegalese Local Languages: Wolof as a Case Study [0.0]
我々は,低リソースのNiger-Congo言語であるWolofのニューラルマシン翻訳システムを提案する。私たちは7万行のフランス語-ウーロフ文の平行コーパスを集めました。われわれのモデルは、限られた量のフランス語とWolofのデータに基づいて訓練されている。
論文参考訳（メタデータ） (2020-03-27T17:09:52Z)

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