[ICLR 2026] ASSESS

📝 Official implementation for the paper:

ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity

Project Structure

The repository is organized as follows.

ASSESS/
├── benchmark/                         # Input benchmark files used by the evaluation scripts
│   ├── EPLA-miniF2F.json              # miniF2F split with label/prediction theorem pairs
│   └── EPLA-ProofNet.json             # ProofNet split with label/prediction theorem pairs
├── experiment/                        # Stored experiment artifacts and metric outputs
│   ├── EPLA-miniF2F/
│   │   ├── identity_match/
│   │   ├── typecheck/                 
│   │   ├── bleu/
│   │   ├── definitional_equality/
│   │   ├── beq/
│   │   ├── majority_voting/
│   │   ├── ted_similarity/            # Includes label/predict extract|processed|opt|figures
│   │   └── transted_similarity/
│   └── EPLA-ProofNet/                 
├── src/                               # Core implementation of the ASSESS pipeline
│   ├── hover.py                       # Lean hover extraction (LSP) and processing pool
│   ├── opter.py                       # Operator-tree construction, visualization, TED similarity
│   ├── verifier.py                    # Lean REPL verification scheduler / worker pool
│   ├── evaluator.py                   # Baseline evaluators and metric summarization
│   └── utilser.py                     # Shared JSON and LLM helper utilities
├── main.py                            # CLI entry for baseline metrics and TED similarity
├── transted.py                        # CLI entry for search-based TransTED similarity
├── utils.py                           # Shared utilities: tree build / TED / Lean interaction
└── README.md

Quick Start

1. Install Lean4. Follow the official Lean4 installation guide.
2. Clone the repository. Clone this repository and enter the project directory.
3. Build the project environment. Follow the Lean REPL setup, then update Lean/Mathlib paths:
   • main.py: LEAN_PATH, LEAN_WORKSPACE
   • transted.py: LEAN_PATH, LEAN_WORKSPACE
   • src/verifier.py: LAKE_PATH, LEAN_WORKSPACE
4. Evaluation. There are two script entries (main.py and transted.py) and two direct utility functions (tree_lean_codes, ted_lean_codes) for evaluation.

   • main.py: Run baseline metrics and TED similarity on EPLA-miniF2F or EPLA-ProofNet.

     # Baseline metrics
     python main.py --benchmark EPLA-miniF2F --identity_match
     python main.py --benchmark EPLA-miniF2F --typecheck
     python main.py --benchmark EPLA-miniF2F --bleu
     python main.py --benchmark EPLA-miniF2F --definitional_equality
     python main.py --benchmark EPLA-miniF2F --beq
     python main.py --benchmark EPLA-miniF2F --majority_voting
     
     # TED similarity
     python main.py --benchmark EPLA-miniF2F --ted_similarity
     python main.py --benchmark EPLA-ProofNet --ted_similarity

   • transted.py: Run search-based TransTED similarity.

     # TransTED similarity
     python transted.py --benchmark EPLA-miniF2F --search_tree_size 32
     python transted.py --benchmark EPLA-ProofNet --search_tree_size 32

   • tree_lean_codes: Input header and formal statement to build the corresponding operator tree.

     # Function1: tree_lean_codes
     import os
     import utils
     from src.hover import ExtractorPool
     
     HOME_DIR = os.path.expanduser("~")
     LEAN_PATH = f"{HOME_DIR}/.elan/bin/lean"
     LEAN_WORKSPACE = f"{HOME_DIR}/dv_mathlib/4_9_0_rc1"
     
     header_list = ["import Mathlib\n"] * 3
     formal_statement_list = ["theorem th_name (p : Prop) : let q := ¬¬p; p = q := by sorry"] * 3
     
     with ExtractorPool(num_workers=10, lean_bin=LEAN_PATH, mathlib_path=LEAN_WORKSPACE) as pool:
         print(utils.tree_lean_codes(pool, header_list, formal_statement_list, tag="demo_tree"))

   • ted_lean_codes: Input a pair of header and formal statements, build the corresponding operator tree and calculate TED similarity.

     # Function2: ted_lean_codes
     import os
     import utils
     from src.hover import ExtractorPool
     
     HOME_DIR = os.path.expanduser("~")
     LEAN_PATH = f"{HOME_DIR}/.elan/bin/lean"
     LEAN_WORKSPACE = f"{HOME_DIR}/dv_mathlib/4_9_0_rc1"
     
     label_header_list = ["import Mathlib\n"] * 3
     label_formal_statement_list = ["theorem th_name (p : Prop) : let q := ¬¬p; p = q := by sorry"] * 3
     predict_header_list = ["import Mathlib\n"] * 3
     predict_formal_statement_list = ["theorem th_name (p : Prop) : let q := ¬¬p; p = q := by sorry"] * 3
     
     with ExtractorPool(num_workers=10, lean_bin=LEAN_PATH, mathlib_path=LEAN_WORKSPACE) as pool:
         print(utils.ted_lean_codes(
             pool,
             label_header_list,
             label_formal_statement_list,
             predict_header_list,
             predict_formal_statement_list
         ))

Citation

@inproceedings{liu2026assess,
title={{ASSESS}: A Semantic and Structural Evaluation Framework for Statement Similarity},
author={Xiaoyang Liu and Tao Zhu and Zineng Dong and Yuntian Liu and Guo qingfeng and Liu ZhaoXuan and Yu Chen and Tao Luo},
booktitle={The Fourteenth International Conference on Learning Representations},
year={2026},
url={https://openreview.net/forum?id=avwNGWtiHF}
}

Contact

Feel free to discuss the paper/data/code with us through issues/emails!

• Xiaoyang Liu: xiaoyang.liu@sjtu.edu.cn