Aria

Aria consists of two main components: Aria Autoformalizer Agent, which converts natural language math into formal Lean code, and AriaScorer, which evaluates the semantic consistency of the formalization.

Open-Source Compliance

• Dependency manifests:
  • Aria-autoformalizer/requirements.txt
  • AriaScorer/requirements.txt
• Project license: Apache-2.0 (see LICENSE)

Before running, set your own service endpoints in config files (or override verifier URL via ARIA_VERIFY_URL).

Aria Autoformalizer Agent

Prerequisites

Before running the agent, you must configure your API credentials in configs/config.yaml.

All commands should be executed from the root directory of the Aria project.

Running on a Single Data Entry

To process a single statement, run the following command in your terminal:

python -m src.Agents.Flow.run_single

Running on a Batch of Data

To process multiple statements from a .jsonl file, use the following command:

python -m src.Agents.Flow.run_batch -i data.jsonl -o results/data.jsonl

Input File Format

The input .jsonl file must contain entries where each line is a JSON object. Each object must include the following two fields:

"id": A unique identifier for the entry, used for labeling purposes.

"nl_statement": The natural language statement to be formalized.

AriaScorer

Prerequisites

Before running the agent, you must configure your API credentials in config.py.

All commands should be executed from the root directory of the AriaScorer project.

Simple Inference

Our test environment use Gemini-2.5-Pro, and set THRESHOLD_PASS at 0.9.You can use the following script to run AriaScorer on your own dataset by changing the input and output paths. You can also change THRESHOLD_PASS according to your own preference. The script supports parallel processing to significantly speed up scoring. Use the --workers argument to specify the number of parallel threads. If you omit the --workers argument, it will use a default value of 10.

python run_lean_scorer.py --workers 20 example/test.json example/test_result

This will generate two files:

• example/test_result.json: A concise result file containing the original input data along with the final scores.
• example/test_result_full_output.txt: A detailed file containing all intermediate outputs from the scoring process.

Input File Format

The input file must be a standard JSON file containing a list of JSON objects. Each object in the list represents an entry to be scored. Each object must include the following two key fields:

"informal_statement": The natural language statement, which is the informal description of the mathematical theorem to be formalized.

"agent_output": The Lean code generated by the autoformalizer, which is the formal statement to be evaluated.

Additionally, it is recommended to include an "id" field for tracking purposes.s