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

• URL: http://arxiv.org/abs/2607.22552v1
• Date: Fri, 15 May 2026 13:01:27 GMT
• Title: MioFFAn: an Annotation Software for Formula Formalization with LLM Automation Capabilities
• Abstract summary: MioFFAn is an open-source, document-centric, and customizable framework designed to facilitate rapid annotation.<n>We introduce specific functionalities for Formula Formalization, such as selection of equations of interest and aided symbolic specification.<n>MioFFAn is designed to incorporate partial automation via Large Language Models.
• Score: 1.4732668880321595
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The automatic translation of mathematical expressions in scientific literature into executable symbolic code (a process we refer to as Formula Formalization) is hindered by a severe scarcity of high-quality, ground-truth datasets specialized for technical scientific domains. In this paper, we present MioFFAn, an open-source, document-centric, and customizable framework designed to facilitate rapid annotation for this task. Building upon the MioGatto architecture, we extend existing features to overcome structural limitations and pivot its scope by introducing specific functionalities for Formula Formalization, such as selection of equations of interest and aided symbolic code specification. By allowing users to configure custom taxonomies and properties for identified symbols, and compatible symbolic operators, we ensure the framework is adaptable to diverse specialized scientific fields. Furthermore, MioFFAn is designed to incorporate partial automation via Large Language Models. By defining a modular set of automated sub-tasks with strict output formats, we enable researchers to iteratively refine automation capabilities and evaluate competing strategies using standard NLP metrics. We specify the current automation methodology and perform a preliminary evaluation that demonstrates to efficacy of this human-in-the-loop approach.

Related papers

• Automatic Translation of Unstructured Requirements into Linear Temporal Logic through Large Language Models [46.28810845443601]
  This paper evaluates whether contemporary off-the-shelf Large Language Models (LLMs) can help bridge this gap by generating Linear Temporal Logic (LTL) formulas directly from unstructured requirements.<n>The study examines six modern LLMs using a few-shot prompting strategy on a heterogeneous benchmark of 15 structurally varied requirements.<n>The results indicate that current general-purpose LLMs can achieve practically significant performance on the unstructured NLto-LTL task without task-specific fine-tuning.
  arXiv  Detail & Related papers  (2026-08-06T17:13:07Z)
• Agentic Design of Compositional Descriptors via Autoresearch for Materials Science Applications [0.0]
  We use composition-based materials-property prediction to test whether autoresearch agents can perform a task beyond model selection.<n>We introduce Automat, an autoresearch framework where a coding agent based on a large language model generates composition-only descriptors for chemical compounds.
  arXiv  Detail & Related papers  (2026-05-14T10:30:17Z)
• TCMIIES: A Browser-Based LLM-Powered Intelligent Information Extraction System for Academic Literature [5.417385211236298]
  This paper presents TCMIIES, a browser-based, zero-installation platform to perform structured information extraction from academic literature.<n>The system employs a novel schema-guided prompting framework with automatic system prompt generation, enabling researchers to define custom extraction schemas.<n>We demonstrate the system's effectiveness through comprehensive evaluation across multiple extraction scenarios in Traditional Chinese Medicine research.
  arXiv  Detail & Related papers  (2026-05-08T09:40:13Z)
• Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions [61.479946958462754]
  We study multi-task reinforcement learning (RL), a setting in which an agent learns a single, universal policy.<n>We present a novel task embedding technique leveraging a new generation of semantic translations-to-automata.
  arXiv  Detail & Related papers  (2026-02-06T14:46:27Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  Autoformalization addresses the scarcity of data for Automated Theorem Proving (ATP) by translating mathematical problems from natural language into formal statements.<n>Existing formalizer still struggles to consistently generate valid statements that meet syntactic validity and semantic consistency.<n>We propose the Autoformalizer with Tool Feedback (ATF), a novel approach that incorporates syntactic and consistency information as tools into the formalization process.
  arXiv  Detail & Related papers  (2025-10-08T10:25:12Z)
• The Return of Structural Handwritten Mathematical Expression Recognition [45.88028371034407]
  Handwritten Mathematical Expression Recognition is foundational for educational technologies.<n>Modern encoder-decoder architectures with large language models excel at generation, but lack explicit symbol-to-trace alignment.<n>This paper introduces a structural recognition approach with two innovations.
  arXiv  Detail & Related papers  (2025-08-27T10:58:59Z)
• Data Dependency-Aware Code Generation from Enhanced UML Sequence Diagrams [54.528185120850274]
  We propose a novel step-by-step code generation framework named API2Dep.<n>First, we introduce an enhanced Unified Modeling Language (UML) API diagram tailored for service-oriented architectures.<n>Second, recognizing the critical role of data flow, we introduce a dedicated data dependency inference task.
  arXiv  Detail & Related papers  (2025-08-05T12:28:23Z)
• Graft: Integrating the Domain Knowledge via Efficient Parameter Synergy for MLLMs [56.76586846269894]
  Multimodal Large Language Models (MLLMs) have achieved success across various domains.<n>Despite its importance, the study of knowledge sharing among domain-specific MLLMs remains largely underexplored.<n>We propose a unified parameter integration framework that enables modular composition of expert capabilities.
  arXiv  Detail & Related papers  (2025-06-30T15:07:41Z)
• Logic Mining from Process Logs: Towards Automated Specification and Verification [0.0]
  This article presents an approach for generating logical specifications from process models discovered via workflow.<n>The study examines the impact of quality data, particularly noise, on the structure and testability of generated specifications.
  arXiv  Detail & Related papers  (2025-06-10T09:44:19Z)
• VeriMind: Agentic LLM for Automated Verilog Generation with a Novel Evaluation Metric [4.590930025882158]
  We propose VeriMind, an agentic LLM framework for Verilog code generation.<n>We introduce a novel evaluation metric-pass@ARC-which combines the conventional pass@k measure with Average Refinement Cycles (ARC) to capture both success rate and the efficiency of iterative refinement.<n> Experimental results on diverse hardware design tasks demonstrated that our approach achieved up to $8.3%$ improvement on pass@k metric and $8.1%$ on pass@ARC metric.
  arXiv  Detail & Related papers  (2025-03-15T23:43:06Z)
• $\forall$uto$\exists$val: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks [21.12437562185667]
  This paper presents a new approach for scaling LLM assessment in translating formal syntax to natural language. We use context-free grammars (CFGs) to generate out-of-distribution datasets on the fly. We also conduct an assessment of several SOTA closed and open-source LLMs to showcase the feasibility and scalability of this paradigm.
  arXiv  Detail & Related papers  (2024-03-27T08:08:00Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.