A Pilot Benchmark for NL-to-FOL Translation in Planetary Exploration

TL;DR

This paper introduces a novel benchmark dataset for translating natural language mission descriptions into formal First-Order Logic representations, based on real NASA mission documents, to advance language understanding in planetary exploration.

Contribution

It creates and annotates a dataset from NASA mission documents for NL-to-FOL translation, enabling research in formal reasoning for space missions.

Findings

Dataset includes real mission documents from NASA PDS.

Manual annotations link natural language to FOL representations.

Provides structured vocabularies for controlled experiments.

Abstract

Future planetary exploration envisions autonomous robotic agents operating under severe communication constraints, without global positioning, and with minimal human intervention. In such environments, agents must not only perceive and act, but also reason over mission objectives, operational constraints, and evolving environmental conditions. While prior work has largely focused on perception and control, the translation of high-level mission knowledge into structured, machine-interpretable representations remains underexplored. We introduce a pilot benchmark for translating natural language (NL) into First-Order Logic (FOL) within the domain of planetary exploration. The dataset is constructed from real mission documentation sourced from NASA's Planetary Data System (PDS), spanning missions from 2003 to 2013. These documents describe mission phases such as launch, boost, coast, cruise, and orbital operations in rich natural language. We manually annotate these documents with corresponding FOL representations that capture temporal structure, agent roles, and operational dependencies. In addition, we provide structured predicate vocabularies and typed constants to enable controlled experimentation with varying levels of prior knowledge. This pilot benchmark provides a foundation for research at the intersection of language understanding and formal reasoning, grounded in real-world, safety-critical mission data. The dataset is provided at: https://github.com/HaydenMM/planetary-logic-benchmark/blob/main/pilot_benchmark.json