A systematic inspection of extsf{FOLIO} and extsf{MALLS} validation splits revealed high rates of incorrect FOL formalizations and ambiguous NL sentences, distorting AI model evaluation. The authors developed and released corrected ground truths for these datasets, demonstrating how annotation errors impact the evaluation of state-of-the-art LLMs.
ImProver 2 is a new neurosymbolic framework for automated proof optimization in Lean 4, designed to address challenges in refactoring formal mathematics proofs. It uses a data-efficient expert-iteration pipeline and a neurosymbolic scaffold, enabling a 7B-parameter model to achieve competitive performance against much larger models.
NeuroNL2LTL is a neurosymbolic architecture that unifies learned translation with formal verification to translate natural language into Linear Temporal Logic. It employs verifier-in-the-loop training, where verification outcomes serve as reward signals for reinforcement learning, optimizing for formal correctness.