Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving

Motivation

• Known: 기존 formal theorem proving(FTP)은 Lean 4와 같은 형식 언어를 통해 이미 알려진 명제(known proposition)의 증명 과정을 process-level로 검증할 수 있음이 잘 알려져 있으며, MiniF2F, PutnamBench 등 다양한 FTP 벤치마크가 존재한다. 반면 비형식적(informal) 수학 문제 해결 벤치마크(MATH500 등)는 최종 답의 outcome-level 정확성만 exact match, SymPy, relaxed match 등으로 검증한다.
• Gap: FTP는 명제가 고정된 상태에서의 검증(verification)에 국한되어 있어, 조건을 만족하는 미지항을 구성적으로 찾아내는 constructive problem-solving을 다루지 못하며, 기존 neuro-symbolic 접근은 informal 추론으로 답을 구한 뒤 사전 형식화된 명제에 답을 끼워넣고 사후적으로만 증명을 검증하므로 답 도출 과정 자체는 형식적으로 검증되지 않는다는 근본적 간극이 존재한다. 또한 informal 답 검사 방법들은 exact match, SymPy 등 취약한 문자열/기호 매칭에 의존해 복잡한 수학적 객체에 대해 false negative를 유발하고, 논리적으로는 타당하지만 사람의 직관과 어긋나는 답(예: lim 1/n 대신 0)을 걸러내지 못하는 false positive 문제도 있다.
• Why: 수학적 추론에서 hallucination과 잘못된 논리를 근본적으로 방지하려면 최종 답뿐 아니라 답을 도출하는 과정 자체가 형식적으로 검증 가능해야 하는데, 이는 자동 정리 증명 연구를 검증을 넘어 구성적 문제 해결로 확장하고, 신뢰할 수 있는 형식 데이터로 LLM을 훈련/평가하는 데 필수적인 인프라를 제공하기 때문에 중요하다.
• Approach: 답을 unknown metavariable과 이에 결부된 proof obligation의 dependent pair로 형식화하는 FPS를 정의하고, 이를 forward derivation과 backward verification 두 단계로 분리한 D-FPS를 제안하며, 답의 의미적 동치를 형식 커널로 판정하는 RPE 지표와 세 개의 파라렐(informal-formal) 벤치마크를 구축해 최신 prover들을 평가한다.

Achievement

Figure 2. Workflow comparison between FPS and D-FPS. (Left) FPS treats solving as term construction. The proof state inc

1. FPS 프레임워크: 미지의 답(metavariable)과 증명 의무(proof obligation)를 하나의 dependent pair로 묶어, 답의 도출과 정당성 증명을 형식 환경(Lean 4) 내에서 end-to-end로 통합하는 원칙적 형식화를 제시했다.
2. D-FPS: find-all 문제를 forward derivation(조건으로부터 답을 명시적으로 도출)과 backward verification(도출된 답의 정당성 검증)으로 구조화하여 사람의 연역적 추론 방식에 더 가깝게 정렬시켰으며, FPS의 soundness와 D-FPS의 expressiveness, soundness, completeness에 대한 이론적 보장을 제공했다.
3. RPE 지표: 형식 커널을 활용해 임의의 수학적 구조 간 의미적 동치를 판정하는 기호적 지표를 제안하여, 문자열/SymPy 매칭 대비 사람 판단과의 정합성이 Cohen's kappa 0.9732로 매우 높음을 실험적으로 검증했다.
4. 세 가지 벤치마크 구축: FormalMath500(MATH500 기반), MiniF2F-Solving, PutnamBench-Solving 등 1,000개 이상의 informal-formal parallel 문제·답 쌍으로 구성된 벤치마크를 원칙적 데이터 주석 파이프라인을 통해 구축했다.
5. "Alignment Tax" 발견: 최신 FTP 방법 및 prompting 기반 방법들에 대한 대규모 실험을 통해, 느슨한 유효성 검사(loose validity checking)에서 사람 정렬적 구성적 추론(constructive, human-aligned reasoning)으로 전환할 때 성능이 유의하게 저하되는 현상을 규명하여, problem-solving이 theorem proving보다 본질적으로 더 어렵다는 것을 실증했다.

How

Figure 2. Workflow comparison between FPS and D-FPS. (Left) FPS treats solving as term construction. The proof state inc

• 문제를 정의역과 답 후보 공간을 포함하는 형식 명제로 formalize하고, 답을 나타내는 unknown metavariable을 도입하여 이를 만족하는 proof term을 함께 구성하도록 요구하는 FPS 형식 체계를 Lean 4의 dependent type theory 위에 구축한다.
• D-FPS에서는 문제를 forward derivation(조건들로부터 답을 유도하는 계산/추론 단계)과 backward verification(유도된 답이 명제를 만족함을 별도로 증명하는 단계)으로 분리하는 워크플로우를 설계한다(Figure 2).
• RPE는 두 답 항(term)에 대해 형식 커널 상에서 제한된 propositional equivalence를 판정하는 metaprogram(예: A_pred = A_gt를 rpe tactic으로 증명)을 통해 검사하며, insufficient simplification 등 기존 방법의 실패 사례를 극복하도록 설계된다.
• MATH500, MiniF2F, PutnamBench의 문제들을 factored formalization 대신 find-construct 형태로 재구성(refactor)하는 원칙적 데이터 주석 파이프라인을 수립해 FormalMath500, MiniF2F-Solving, PutnamBench-Solving 세 벤치마크(총 1,000여 문제)를 제작한다.
• 최신 FTP prover 및 prompting 기반 LLM들을 FPS/D-FPS 벤치마크 상에서 평가하고, 기존 FTP 성능과 비교하여 solving과 proving 간 난이도 차이 및 "alignment tax"를 정량적으로 분석한다.

Originality

• 기존 FTP가 검증에 국한된다는 근본적 한계를 지적하고, 답 도출(discovery)과 검증(verification)을 dependent pair로 통합하는 새로운 형식적 문제 정의(FPS)를 제시한 점이 독창적이다.
• 사람의 연역적 추론 과정(forward derivation → backward verification)을 형식 체계에 명시적으로 반영한 D-FPS 구조는 기존 neuro-symbolic 파이프라인(사후 검증 방식)과 질적으로 다른 접근이다.
• 문자열/기호 매칭의 한계를 형식 커널 기반 동치 판정(RPE)으로 극복하려는 시도는 informal 평가와 formal 평가 사이의 간극을 메우는 새로운 방법론이다.
• 기존 FTP 벤치마크를 problem-solving 관점에서 재구성하여 informal-formal parallel 벤치마크 3종을 구축한 것은 이 새로운 연구 분야를 위한 실질적 인프라 기여이다.

Limitation & Further Study

• 발췌된 본문에서 FPS/D-FPS의 이론적 보장(soundness, completeness 등)에 대한 구체적 증명 및 조건이 상세히 제시되지 않아, 이론적 엄밀성의 범위와 한계를 정확히 판단하기 어렵다.
• RPE가 "restricted" propositional equivalence라는 이름에서 보이듯 임의의 동치 관계를 모두 포착하지 못할 가능성이 있으며, 어떤 종류의 수학적 구조에서 실패하는지에 대한 체계적 분석이 필요해 보인다.
• 벤치마크가 Lean 4 및 특정 수학 영역(MATH500, MiniF2F, PutnamBench 기반)에 국한되어 있어, 다른 형식 시스템(Coq, Isabelle 등)이나 더 광범위한 문제 유형에 대한 일반화 가능성은 추가 검증이 필요하다.
• "alignment tax" 현상의 원인(모델의 형식화 부족, 탐색 공간 폭발, 검증 전략의 한계 등)에 대한 심층적 원인 분석과 이를 완화하기 위한 구체적 방법론은 후속 연구로 남아있는 것으로 보인다.

Evaluation

총평: FTP를 검증에서 구성적 문제 해결로 확장하는 명확한 문제 설정과 이를 뒷받침하는 이론·지표·벤치마크를 종합적으로 제시한 견고한 연구로, formal reasoning 커뮤니티에 새로운 연구 방향과 실질적 평가 인프라를 제공하는 의미 있는 기여다.