💬 NLP

MioFFAn: an Annotation Software for Formula Formalization with LLM Automation Capabilities

本論文は、MioGattoアーキテクチャを拡張し、人間によるアノテーションとモジュール化された大規模言語モデルによる自動化を組み合わせることで、数式の定式化のための高品質なデータセット作成を促進する、オープンソースでカスタマイズ可能なアノテーションフレームワークであるMioFFAnを紹介するものである。

原著者： Nicolas Sibuet, Horacio Saggion, Riccardo Rossi

公開日 2026-07-28

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Nicolas Sibuet, Horacio Saggion, Riccardo Rossi

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

あなたは、コンピューターにしか読めない秘密のコードで書かれた手がかりを追う探偵だと想像してください。一方で、物語は人間だけに理解できる言語で書かれています。これは、複雑な数式で埋め尽くされた論文を書く科学者たちが日々直面している苦闘です。彼らは、世界の仕組みを記述するために美しくエレガントな数式を使用しますが、これらの数式はしばしば数学の「絵」に過ぎません。それはまるで、橋の「図面」のようなものです。しかし、実際にその橋を建設するためには、コンピュータには設計図が必要です。つまり、機械に対して、鋼鉄にかかる応力を正確に計算させるための具体的な指示、変数、そしてロジックです。この「数学の絵」を「コンピュータ用の設計図」へと変換するプロセスを、**数式の形式化（Formula Formalization）**と呼びます。

問題は、たとえ人工知能（AI）によって動かされている超スマートなコンピュータであっても、これらの設計図を自力で読み取ることは極めて苦手であるという点です。コンピュータが翻訳方法を学習するためには、膨大な事例のライブラリ、つまり何千組もの「数学の絵」と「コンピュータの設計図」のペアを必要とします。しかし、ここには落とし穴があります。このライブラリを構築した人はまだ誰もいません。なぜなら、それを構築することは非常に困難で退屈な作業だからです。人間は、論文の中にある一つ一つの数学記号を、コードへと手作業で書き直さなければなりません。これは、世界中のあらゆる料理について、材料を一つずつ手書きでレシピに書き写すような、非常に退屈で科学の進歩を遅らせる作業なのです。

ここで、MioFFAnと呼ばれる新しいツールが登場します。これは、数学をコードへと翻訳するという退屈な仕事を、より速く、より苦痛の少ないものにするために設計された、ハイテクでインタラクティブなノートブックのようなものです。研究者たちは単なる静的なツールを作ったのではありません。「ヒューマン・イン・ザ・ループ（人間が介在する）」システムを構築したのです。これは、ソフトウェアがAIを用いて翻訳を推測するアシスタントとして機能し、その後、人間の専門家に間違いをダブルチェックさせ、修正を求める仕組みを意味します。それは、ロボットが手紙の下書きをしてくれるものの、送信する前に人間が内容を確認し、事実が正しいことを確認して署名しなければならないようなものです。このチームアップのアプローチを用いることで、著者たちは、以前よりもずっと速いペースで、この極めて重要な「数学からコードへの例」のライブラリを構築できることを示しています。これにより、コンピュータがついに現代科学を駆動する複雑な数学を理解し、実行できる道が開かれます。

論文のストーリー：数学とコードの架け橋を築く

本論文では、研究者が科学文書のアノテーション（注釈付け）を行うのを支援するために設計されたオープンソースソフトウェア、MioFFAnを紹介しています。その主な目的は、論文内の数式を、コンピュータが実際に実行可能な記号コード（コンピュータ代数システムに記述するようなコード）へと変換する作業である数式の形式化を促進することです。著者らは、文書をスキャンしてテキストを読み取るツール（OCR）は優れているものの、スキャンされた数式をコンピュータが実行可能なコードへと変換するための「意味的な深み（semantic depth）」が不足していると主張しています。

これを解決するために、著者らはMioGattoという古いツールをベースにMioFFAnを構築しました。彼らは、旧ツールが単一の数学記号（例えば文字 $x$ ）を特定することには長けているものの、複雑な記号のグループ（例えば関数 $f(x)$ やテンソル $\delta u_i$ ）を扱うのは不得意であり、現実世界の科学に必要な柔軟な階層的アノテーションを可能にしていなかったことに気づきました。MioFFAnは、以下の主要なアップグレードを導入することで、この問題を解決しました。

グルーピングと階層構造： 単一の文字にタグを付けるだけでなく、MioFFAnでは数式の一塊を一つのユニットとして選択できます。これは、必要に応じて分解可能な「グループ」として複雑な式を扱います。
カスタマイズ可能なルール： このソフトウェアはカメレオンのようです。ユーザーは、異なる科学分野に応じた独自の「タクソノミー（分類体系）」を定義できます。例えば、物理学者は変数を「ベクトル」としてタグ付けする必要があるかもしれませんが、生物学者はそれを「濃度」としてタグ付けする必要があるかもしれません。ツールはこれらのニーズに適応します。
文脈による接地（Contextual Grounding）： 数学記号を、文書内でそれらが説明されているテキストへと結びつける手助けをします。論文に「 $v$ を速度とする」と書かれている場合、ツールはその文章をハイライトし、数式内の記号 $v$ と結びつけることができます。
「ヒューマン・イン・ザ・ループ」による自動化： これが最もエキサイティングな部分です。ソフトウェアには、AI（具体的には大規模言語モデル、LLM）が最初にアノテーションを試みる機能が含まれています。AIは、数式のどの部分が何であるか、変数が何を意味するか、そしてそれらがテキストのどこで定義されているかを提案します。しかし、人間のユーザーが置き換えられるわけではありません。ユーザーは監督者として機能します。彼らはAIの提案をレビューし、エラーを修正し、最終的な結果を確認します。

著者らは、自動車の衝突実験や橋のたわみのシミュレーションなどに使用される**有限要素法（FEM）**という特定の科学分野を用いて、このシステムをテストしました。彼らは、FEMの特定の数学規則を理解するようにソフトウェアを設定し、「概念実証」の実験を行いました。ソフトウェアに科学論文を入力し、AIにそれらをアノテーションさせ、その後、AIの成果を人間の専門家によって作成された「ゴールドスタンダード（正解）」と比較しました。

結果は、期待と現実が混ざり合ったものでした。AIはある程度のことは驚くほど上手くこなしましたが、他の点では苦戦しました。例えば、AIが元の数学記号（ギリシャ文字の $\lambda$ など）を見ることができた場合、記号を長いテキスト名に置き換えた場合（識別率が低下）と比較して、数式の構成要素を特定する能力が大幅に向上しました（約**57.7%**のカバー率）。しかし、AIは完璧ではなく、文書内のテキスト定義の正確な場所を特定することに苦労することが多く、特定の文章ではなく段落全体をハイライトしてしまうこともありました。

論文では、現在のAIが単独でこの仕事を完璧にこなせるという考えを明確に否定しています。著者らは、自動化された結果は「理想とは程遠い」ものであり、人間の専門家が迅速に洗練させるための「ベースライン」としてのみ使用されるべきであると述べています。彼らは、人間のチェックなしに完全自動のエンドツーエンドの翻訳をAIで行おうとすると、発見が困難なエラーを招く可能性が高いと主張しています。

評価において、著者らは「オリジナル文字（Original Characters）」アプローチ（数学記号をそのまま保持する手法）が、AIが数学の構造を理解する上で最も効果的であることを発見しました。また、3つの異なるAIモデル（NVIDIAのNemotron、GoogleのGemma、AlibabaのQwen）を比較したところ、Qwen3-4B-Instruct-2507モデルが他のモデルよりも著しく優れており、記号識別のカバー率において、次に優れたモデルの約**33.9%**に対し、**57.7%**を達成したことが分かりました。

最終的に、本論文はMioFFAnがより優れた自動化戦略を開発するための強力な「プレイグラウンド（実験場）」であることを示唆しています。これは、数学をコードに翻訳する問題を永遠に解決したと主張しているわけではありません。むしろ、研究者が異なるAI戦略をテストし、何が機能するかを確認し、システムを段階的に改善できる柔軟なフレームワークを提供しています。著者らは、現在の自動化はあくまで「暫定的な」ステップに過ぎないものの、この人間とAIのチームアップこそが、将来のよりスマートなシステムを訓練するために必要な高品質なデータセットを構築するための最も効果的な方法であると結論付けています。彼らは、このツールが数学からコードへの翻訳の巨大な共有ライブラリの構築を支援し、コンピュータが科学者と共に世界の最も複雑な問題を解決することを容易にする未来を描いています。

技術要約: MioFFAn

問題提起

科学文献に見られる数式を、実行可能な記号コード（本研究では**数式の定式化（Formula Formalization）**と定義）へと自動的に変換するプロセスは、現在、技術的な科学ドメインに特化した高品質なグラウンドトゥルース（正解）データセットの深刻な不足によって阻害されている。光学文字認識（OCR）システムは、LaTeXやMathMLのような提示形式を抽出することはできるが、これらの数式をコードとして実装するために必要な意味論的および計算的な深みは欠いている。大規模言語モデル（LLM）は、この変換をオーケストレートするための有望なメカニズムを提供しているが、変数定義、演算子の特性、ドメイン固有の制約といった特定のコンテキスト情報を捉えるベンチマークコーパスの欠如により、その発展が停滞している。既存のアノテーションツールは、個々の記号の特定や照応解析に焦点を当てることが多く、これらの要素を統合して制御する記号コードの生成には至っていない。

手法

著者らは、数式の定式化のための迅速なアノテーションを促進するために設計された、オープンソースでドキュメント中心、かつカスタマイズ可能なフレームワークであるMioFFAn（Math identifier-oriented Formula Formalization Annotator）を提案する。本システムはMioGattoアーキテクチャに基づいて構築されているが、元のツールの限界に対処するために、大幅な構造的・機能的な拡張を導入している。

フレームワークのアーキテクチャと拡張

MioFFAnは、動的なウェブベースのインタラクションを可能にするために、HTMLとMathMLを使用し、TypeScript/Pythonを用いたクライアント・サーバーアプリケーションとして動作する。MioGattoに対する主なアーキテクチャ上の拡張は以下の通りである：

階層的および複合的な識別子管理： システムは、単一の <mi> タグを超えて、複合構造（例：添え字、上付き文字）やユーザー定義の**グループ（Groups）**をサポートするように数式識別子（MI）の定義を拡張している。これにより、複雑な表記（例： $\delta u_i$ や $f(x)$ ）を、構成記号をアノテーションする能力を維持しつつ、単一のエンティティとして扱うことが可能になる。
分離されたプロパティ・スキーマ： 本フレームワークは、コンセプト（例：「速度ベクトル」）に割り当てられる不変の意味的特性（Invariant Semantic Properties）と、出現（Occurrence）に割り当てられる可変特性（Variant Properties）（例：「転置された」）を分離している。これにより、概念を異なる表記や実装形態間で再利用することが可能となる。
柔軟なグラウンディング（根拠付け）： グラウンディングのソース（SoG）は、複数のHTMLノードにわたるインター・スパンのハイライトをサポートしており、個々の出現（Occurrence）ではなくコンセプトに関連付けられている。これにより、表示された数式全体や、ノードをまたぐテキストセグメントの選択が可能となる。
ドキュメント中心のワークフロー： ユーザーはサーバーの再起動なしに単一のセッション内で複数のドキュメントサンプル間を移動でき、システムはJSON設定によるアノテーション・スキーマの動的な生成をサポートしている。

数式の定式化機能

数式の定式化を明確にターゲットとするため、MioFFAnは以下の3つのコア機能を紹介する：

関心対象の数式（Equations of Interest: EoI）： ユーザーは定式化のための特定の式を指定でき、これによりアノテーション・スキーマに専用のエントリが初期化される。
標準的な変数名（Canonical Variable Names）： 生成される記号コードにおいて曖昧な表現を避けるため、すべてのコンセプトは一意の変数名にマッピングされる。
統合された記号コード構築： インタラクティブな環境が、定義された変数名やドメイン固有の演算子（例：grad(), div()）のパレットを提供し、ユーザーが最終的な記号コードを合成する際の支援を行い、手動による構文エラーを最小限に抑える。

自動化パイプライン

MioFFAnは、LLMを用いたモジュール式のヒューマン・イン・ザ・ループ（人間が介在する）自動化パイプラインを組み込んでいる。この自動化はコアアプリケーションから切り離されており、研究者が戦略を入れ替えられるようになっている。パイプラインは以下の3つのサブタスクで構成される：

記号セグメンテーション（Symbol Segmentation）： LLMが、一意の出現（Occurrence）としてグループ化されるべきMathML要素または複合構造を特定する。
コンセプト割り当て（Concept Assignment）： LLMがコンセプト（変数名と説明を含む）を提案し、それらをセグメント化された記号にマッピングする。
SoG特定（SoG Identification）： LLMが、コンセプトのエビデンスとなるテキストスパンまたは数式を特定する。

システムは厳格な出力形式（グループ、コンセプトなどのリスト）を強制し、標準的なNLPメトリクスを用いた手法に依存しない評価を可能にしている。

ユースケースと評価

本フレームワークは、高次元テンソルや変分形式の精密な特性化を必要とする**有限要素法（FEM）**向けに構成された。カスタムのタクソノミーと、KratosMultiphysics向けのSympyベースのコンパイラをターゲットとした演算子ライブラリが定義された。

予備的な概念実証評価は、ローカルの Qwen3-4B-Instruct モデルを用い、厳選された6つのFEMサンプルに対して行われた。評価では、2つの自動化バリアントを比較した：

元の文字（Original Characters）： LLMが非標準のUnicode文字を含む生のHTMLを処理。
明示的な名称（Explicit Names）： LLMがUnicode文字が明示的な名称（例：「GREEK SMALL LETTER LAMBDA」）に置き換えられたHTMLを処理。

結果：

元の文字バリアントは、記号セグメンテーションにおいて、明示的な名称バリアントを大幅に上回った（カバレッジ 57.7% 対 36.2%、CoNLL 36.8% 対 26.9%）。
明示的な名称バリアントは、コンセプト割り当ておよびSoG特定において、わずかな改善を示した。
定性的分析では、モデルは正しい意味的コンテキストを特定することは多いものの、SoG特定タスクにおけるタグIDの正確な指定には苦慮しており、頻繁に特定の文章ではなく段落全体をハイライトしてしまうことが明らかになった。

主な貢献

MioFFAnフレームワーク： 数学的表記と実行可能な記号コードの間の溝を埋める、専門化されたオープンソースのアノテーションツールであり、数式の定式化のためのグラウンドトゥルース・データの不足に対処する。
アーキテクチャの拡張： 複合識別子、分離されたプロパティ・スキーマ、および柔軟なグラウンディング・メカニズムを含む、MioGattoのベースラインに対する重要な改善。
モジュール化された自動化： 特定のサブタスク（セグメンテーション、割り当て、グラウンディング）に分離し、標準的なメトリクスで評価することで、LLM戦略の反復的な洗練を可能にするパイプライン設計。
ドメイン適応性： カスタムのタクソノミーと演算子セットを含む、有限要素法への具体的な適用を通じた、本フレームワークの構成可能性のデモンストレーション。

意義と主張

本論文は、MioFFAnを完全な自動化ソリューションとしてではなく、ヒューマン・イン・ザ・ループの開発用プレイグラウンドとして位置づけている。著者らは、本フレームワークの主要な価値は以下の能力にあると主張している：

数式の定式化のためのLLMを訓練およびベンチマークするために必要な、高品質でドメイン固有のデータセットの作成を容易にすること。
特定のサブタスク（セグメンテーション、割り当て、グラウンディング）を分離し、それらを個別のメトリクスで評価することで、研究者が自動化機能を反復的に洗練できるようにすること。
現在のLLMの能力は、複雑な科学ドメインにおける完全な自律的定式化には不十分であることを認めつつ、人間の専門家によって迅速に洗練可能な自動化のベースラインを提供すること。

著者らは、現在の自動化は理想的ではないものの、MioFFAnのモジュール設計は、将来的に、より高度な自動化ワークフローの開発を効果的にサポートし、最終的には科学的コード生成におけるデータ不足というボトルネックを解消するものであると結論付けている。