FormalAlign: Automated Alignment Evaluation for Autoformalization

• URL: http://arxiv.org/abs/2410.10135v1
• Date: Mon, 14 Oct 2024 03:58:35 GMT
• Title: FormalAlign: Automated Alignment Evaluation for Autoformalization
• Authors: Jianqiao Lu, Yingjia Wan, Yinya Huang, Jing Xiong, Zhengying Liu, Zhijiang Guo,
• Abstract summary: textscFormalAlign trains on both the autoformalization sequence generation task and the representational alignment between input and output. evaluated across four benchmarks, textscFormalAlign demonstrates superior performance. This effective alignment evaluation significantly reduces the need for manual verification.
• Score: 12.674957231226871
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Autoformalization aims to convert informal mathematical proofs into machine-verifiable formats, bridging the gap between natural and formal languages. However, ensuring semantic alignment between the informal and formalized statements remains challenging. Existing approaches heavily rely on manual verification, hindering scalability. To address this, we introduce \textsc{FormalAlign}, the first automated framework designed for evaluating the alignment between natural and formal languages in autoformalization. \textsc{FormalAlign} trains on both the autoformalization sequence generation task and the representational alignment between input and output, employing a dual loss that combines a pair of mutually enhancing autoformalization and alignment tasks. Evaluated across four benchmarks augmented by our proposed misalignment strategies, \textsc{FormalAlign} demonstrates superior performance. In our experiments, \textsc{FormalAlign} outperforms GPT-4, achieving an Alignment-Selection Score 11.58\% higher on \forml-Basic (99.21\% vs. 88.91\%) and 3.19\% higher on MiniF2F-Valid (66.39\% vs. 64.34\%). This effective alignment evaluation significantly reduces the need for manual verification. Both the dataset and code can be accessed via~\url{https://github.com/rookie-joe/FormalAlign}.

Related papers

• Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
  We introduce a novel framework that scores and selects the best result from k autoformalization candidates based on symbolic equivalence and semantic consistency. Our experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy.
  arXiv  Detail & Related papers  (2024-10-28T11:37:39Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [91.981439746404]
  We introduce QASemConsistency, a new formalism for localizing factual inconsistencies in attributable text generation. We first demonstrate the effectiveness of the QASemConsistency methodology for human annotation. We then implement several methods for automatically detecting localized factual inconsistencies.
  arXiv  Detail & Related papers  (2024-10-09T22:53:48Z)
• LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
  We propose Math-Minos, a natural language feedback-enhanced verifier. Our experiments reveal that a small set of natural language feedback can significantly boost the performance of the verifier.
  arXiv  Detail & Related papers  (2024-06-20T06:42:27Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  We propose a metric for evaluating the quality of specifications for verification-aware languages. We show that our metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark. We also outline formal verification challenges that need to be addressed to apply the technique more widely.
  arXiv  Detail & Related papers  (2024-06-14T06:52:08Z)
• Improving Autoformalization using Type Checking [15.58948808529849]
  Large language models show promise for autoformalization, the task of automatically translating natural language into formal languages. The last reported state-of-the-art performance on the ProofNet formalization benchmark for the Lean proof assistant, achieved using Codex for Lean 3, only showed successful formalization of 16.1% of informal statements. Our analysis shows that the performance of these models is largely limited by their inability to generate formal statements that successfully type-check.
  arXiv  Detail & Related papers  (2024-06-11T13:01:50Z)
• Process-Driven Autoformalization in Lean 4 [30.056591518828554]
  We develop a benchmark to evaluate the autoformalization capabilities of large language models. We also introduce a model that leverages the precise feedback from Lean 4 compilers to enhance autoformalization. Our experiments demonstrate that the PSV method improves autoformalization, enabling higher accuracy using less filtered training data.
  arXiv  Detail & Related papers  (2024-06-04T03:48:08Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  We introduce a neuro-symbolic framework for autoformalizing Euclidean geometry. One challenge is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. We provide automatic semantic evaluation for autoformalized theorem statements.
  arXiv  Detail & Related papers  (2024-05-27T14:35:10Z)
• Autoformalization with Large Language Models [22.86710743804944]
  A successful autoformalization system could advance the fields of formal verification, program synthesis, and artificial intelligence. We show large language models provide new prospects towards this goal. Our methodology results in a new state-of-the-art result on the MiniF2F theorem proving benchmark, improving the proof rate from $29.6%$ to $35.2%$.
  arXiv  Detail & Related papers  (2022-05-25T09:53:30Z)
• Bi-level Alignment for Cross-Domain Crowd Counting [113.78303285148041]
  Current methods rely on external data for training an auxiliary task or apply an expensive coarse-to-fine estimation. We develop a new adversarial learning based method, which is simple and efficient to apply. We evaluate our approach on five real-world crowd counting benchmarks, where we outperform existing approaches by a large margin.
  arXiv  Detail & Related papers  (2022-05-12T02:23:25Z)
• Text Revision by On-the-Fly Representation Optimization [76.11035270753757]
  Current state-of-the-art methods formulate these tasks as sequence-to-sequence learning problems. We present an iterative in-place editing approach for text revision, which requires no parallel data. It achieves competitive and even better performance than state-of-the-art supervised methods on text simplification.
  arXiv  Detail & Related papers  (2022-04-15T07:38:08Z)
• Automatic Extraction of Rules Governing Morphological Agreement [103.78033184221373]
  We develop an automated framework for extracting a first-pass grammatical specification from raw text. We focus on extracting rules describing agreement, a morphosyntactic phenomenon at the core of the grammars of many of the world's languages. We apply our framework to all languages included in the Universal Dependencies project, with promising results.
  arXiv  Detail & Related papers  (2020-10-02T18:31:45Z)

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.