Research map / Large language models / Agents, code and math
Learning Structure-Aware Representations of Dependent Types
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Releases a first-of-its-kind Agda program-proof dataset extracted at sub-type resolution via the agda2train backend, and proposes Quill, a small structure-aware (tree-positional, variable-resolving linear attention) encoder for premise selection that beats ablations and a Transformer baseline.
Problem
Premise selection for dependently-typed proof assistants like Agda lacks ML resources, and sequential/string-based encoders poorly capture the binding, reference, and structural nature of dependent types.
Approach
Extract Agda's internal type ASTs at every hole and resolve de Bruijn variable references to pointers to binder nodes, then encode with a linear-attention Transformer using binary-tree orthogonal positional encodings and topologically ordered lemma representations, making the representation invariant to renaming.
Key results
- Quill reaches 50.2 AveP and 40.3 R-Prec on the stdlib in-distribution set, versus 10.9 AveP for the plain Transformer.
- Removing variable resolution drops in-distribution AveP to 35.8, while removing tree positional encoding drops it to 44.5.
- Quill keeps 38.7 AveP on the out-of-distribution stdlib split and 27.0 AveP on UniMath, showing partial zero-shot transfer.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| add Taylor expansion to the attention feature map (ablation) | Quill · stdlib:id | AveP: 47.0 -> 50.2 | Helped |
| add tree positional encoding to attention (ablation) | Quill · stdlib:id | AveP: 44.5 -> 50.2 | Helped |
| resolve de Bruijn variable references structurally (ablation) | Quill · stdlib:id | AveP: 35.8 -> 50.2 | Helped |
| use Quill's structure-aware architecture instead of a Transformer | premise selection · stdlib:id | AveP: 10.9 -> 50.2 | Helped |
| use Quill's structure-aware architecture instead of a Transformer | premise selection · stdlib:ood | AveP: 8.5 -> 38.7 | Helped |
| use Quill's structure-aware architecture instead of a Transformer | premise selection · Unimath | AveP: 9.4 -> 27.0 | Helped |
| use Quill's structure-aware architecture instead of a Transformer | premise selection · TypeTopology | AveP: 5.8 -> 22.5 | Helped |
Surprising findings
- Replacing all variables with a single meta-embedding (no de Bruijn resolution) still retains about 75% of the original AveP.
- A vanilla Transformer essentially collapses on the premise selection task (AveP 10.9), while the structured variant is far stronger.
Limitations
- Mutually inductive definitions are unsupported and 36 size-anomalous files were excluded or held out.
- Only proof-level terms within functions are extracted; terms in type-level indices, literals, sorts and levels are dropped.
- Extraction is computationally expensive and the system is not yet integrated into an interactive or end-to-end proof completion loop.
Experimental setup
Datasets: Agda standard library v1.7.2 extracted dataset UniMath (evaluation extract) TypeTopology (evaluation extract)
Benchmarks: stdlib:ID stdlib:OOD UniMath TypeTopology
Metrics: AveP R-Prec
Baselines: Transformer Quill without Taylor expansion Quill without tree positional encoding Quill without variable resolution
Builds on: linear attention (Katharopoulos et al.) InfoNCE RMSNorm SwiGLU de Bruijn indexing
Closest papers by meaning
- Premise Selection for a Lean Hammer (ICLR 2026 · similarity 0.87)
- BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving (AAAI 2024 · similarity 0.85)
- miniCTX: Neural Theorem Proving with (Long-)Contexts (ICLR 2025 · similarity 0.85)
- Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models (NeurIPS 2025 · similarity 0.85)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.84)
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.