▲

ProofOfThought: Z3 정리 증명을 이용한 LLM 기반 추론

 (github.com/DebarghaG)
3P by GN⁺ 8일전 | ★ favorite | 댓글 1개
  • ProofOfThought는 대형 언어 모델(LLM) 과 Z3 정리 증명기를 결합해 강력하면서도 해석 가능한 추론을 지원함
  • 이 프로젝트는 자연어 질의에 대해 정확하고 신뢰성 높은 추론 결과를 제공함
  • 고수준 Python API를 통해 개발자들은 복잡한 추론 작업을 간편하게 구현 및 실험할 수 있음
  • Z3DSL을 통해 JSON 기반 저수준 DSL 접근성도 제공, 유연한 커스터마이징이 가능함
  • Sys2Reasoning Workshop NeurIPS 2024 게재를 통해 최신 연구 성과의 실용화 이점을 보여줌

ProofOfThought 오픈소스 프로젝트 소개

ProofOfThought는 대형 언어 모델(LLM)과 Z3 정리 증명기를 결합하는 뉴로심볼릭(신경-기호) 프로그램 합성 방식을 채택한 오픈소스 추론 라이브러리임. 실세계의 복잡한 문제에 대해 강건하고 해석 가능한 추론 결과를 제공하는 점이 실제 활용과 연구 양쪽에서 중요한 의의를 가짐.

오픈소스 특성상 누구나 연구, 서비스, 개발 등에 자유롭게 활용할 수 있으며, 기존의 단순 LLM 기반 추론 시스템보다 추론 과정 검증 및 오류 해석이 용이하다는 장점이 있음. 타 추론 시스템과 비교해 자연어 입력 → 논리 프로그램 자동 변환 → Z3 기반 추론이라는 구조적 투명성이 큰 특징임.

시스템 아키텍처 및 주요 구성

  • 고수준 API(z3dsl.reasoning) :

    • 자연어 기반의 추론 질의 수행
    • 초심자도 손쉽게 적용 가능한 Python 인터페이스 제공

  • 저수준 DSL(z3dsl) :

    • JSON 기반의 Z3 정리 증명기 접근 가능
    • 복잡한 커스터마이즈 및 자동화 파이프라인 구축에 유리함

주요 기능 예시

  • LLM이 입력된 질의를 논리식(심볼릭 프로그램)으로 변환

  • Z3 증명기를 통해 참·거짓(yes/no) 또는 조건 기반 해석 결과 생성

  • 예시:

    • 질의: "Nancy Pelosi가 낙태를 공개적으로 비난할 것인가?"
    • 결과: False(아님)

  • 평가 파이프라인(EvaluationPipeline) 제공:

    • 대량의 데이터셋에 대한 배치 평가 가능
    • 정확도 등 자동 리포팅

적용 및 활용 사례

  • 리서치 목적의 추론 벤치마크 자동화
  • LLM 기반 지식그래프나 고차 논리 문제 자동 증명 서비스
  • 복잡한 정책 질의, 자연어 토론 자동 판별 등 다양한 AI 서비스 적용 가능성 보유

연구적 의의와 특징

  • NeurIPS 2024의 Sys2Reasoning 워크숍에 발표
  • 기존 LLM 한계(추론 불확실성)를 보완하는 심볼릭 해석 기반 신뢰성
  • 추론 결과와 근거의 투명성 및 해석 가능성이 실제 서비스 개발에 큰 강점

결론

ProofOfThought는 LLM과 Z3 정리 증명기의 장점을 결합해, 강인하고 해석 가능한 AI 추론 인프라를 구축하고자 하는 개발자와 연구자들에게 실질적 가치 제공함. 프로젝트의 라이선스 및 구조는 오픈소스 생태계에 적합하게 설계되어 있어 학술 연구와 산업적 활용 양쪽 모두에 매력적임.

▲
GN⁺ 8일전  [-]
Hacker News 의견
  • Gemini 2.5 Pro와의 흥미로운 경험을 이야기함. 온라인 CAS 시스템에서 연립방정식 풀이를 시도 중 CAS가 기대처럼 동작하지 않아 Gemini에게 도움을 청하였는데, Gemini가 직접 해답을 제시함. Python의 sympy 패키지를 사용했다고 설명함. 모호한 LLM과 엄격한 도구의 결합이 강력한 효과를 낳을 수 있다는 인상 공유함
    • 인간과 비슷한 느낌임. 우리는 복잡한 계산에는 약하지만 대단한 컴퓨터를 만들어 이를 잘 해냄. 그리고 엄청난 노력 끝에 숫자 계산을 기반으로 그럭저럭 텍스트 예측은 하지만 어려운 계산에는 서툰 프로그램도 만듦. 결국 이 프로그램이 숫자 계산에 강한 프로그램을 만들어 사용하는 법을 예측할 수 있게 됨
    • 수학에 LLM과 sympy의 조합이 정말 마음에 듦. LLM에게 sympy 코드를 작성하게 하면, 기호 연산이 올바르게 이뤄졌는지 신뢰할 수 있음. 코드 자체가 산출물로 남아 사람이든 LLM이든 점진적으로 수정 및 개선할 수 있고, git 이력 등으로 관리 가능함. 테스트 및 검증 통과로 수학적 정확성에 대한 신뢰를 유지함. sympy 코드에서 쉽게 latex로 변환하는 헬퍼 함수도 사용함. 최근 quantum eraser 실험 관련 수학 작업도 이런 방식으로 진행함. github 링크
    • 도구로 문제 해결 과정을 LLM과 함께 따라가는 것은 괜찮은 방법임을 이해함. 실제로 기대 이상으로 잘 작동했음. 하지만 LLM으로 수학을 처리하게 유도하는 대신 CAS를 사용하지 않는 건, 아파트 이사를 화물 트럭 대신 버스로 여러 번 왕복하는 것과 같다는 비유를 듦. 이미 버스 패스가 있다고 해서 그렇다는 견해임
  • LLM은 결국 통계적 언어 모델임을 강조함. 논리 프로그램, 특히 Prolog 소스 코드를 생성하는 것은 기대 이상으로 잘 되는 것으로 경험함. 아마도 Prolog가 기호적 자연어처리에 도입되었고 트레이닝 데이터셋에도 번역 샘플이 풍부해서임. Z3의 Datalog 문법을 SMTLib 문법 대신 써보는 것도 고려할 만함. 관련 데모 및 Z3 Datalog 문법 참고를 권장함
    • Z3에서 Datalog 문법은 꽤 훌륭함. 우리는 grammars 논문에서 SMT를 사용했는데, 그 이유는 여러 솔버와의 호환성이 가장 높았기 때문임. 하지만 해당 방식은 PROLOG로도 잘 동작함을 NeurIPS 심사 과정에서 테스트함. Datalog로도 동작할 것으로 예상함. 논문 링크, datalog 예제
  • 흥미로운 접근이라는 생각임. 우리 팀도 비슷하게 LEAN으로 비즈니스 운영 정책을 인코딩하는 프로토타입을 만들었음. 내부 위키나 구글독스의 지식기반을 LLM이 먼저 LEAN 코드로 변환함. 그리고 일관성 검증을 위해 솔버를 실행함. 위키가 수정되면 전체 프로세스가 다시 실행되어, 일종의 프로세스 Linter 역할을 함. 다만 LEAN 변환 자체에서 엔지니어의 검토가 필요해서 프로토타입 단계에 머물렀음. 하지만 법적·재무적 컴플라이언스를 요구하는 도메인에는 유망한 방식임
    • 자동 형식화의 벽이 정말 높음을 언급함. 우리의 NeurIPS 2025 논문에서 잘 정의된 문법을 대상으로 자동 형식화의 불확실성을 정량화해서 분석한 경험을 공유함. 논문 링크 자세한 토론을 원하면 언제든 연락 바람
    • LEAN이 무엇인지 궁금한 분들을 위해 소개함. Microsoft에서 만든 Lean Theorem Prover임. 프로젝트 링크
    • 실제 예시가 궁금함. 현실에서 LEAN으로 정의할 만큼 정확하게 기술된 정책이 어떤 것인지 예시를 듣고 싶음
    • 이런 방식이 모순되는 가이드라인을 체계적으로 식별할 수 있게 해주는 점이 매우 유용할 듯함
  • 매우 흥미로운 연구 분야임. 몇 년 전에 논리 및 확률 기반 추론 엔진을 이용해 전제가 결론으로 잘 이어지는지 검증한 적이 있음. 또 agent들을 이용해 도메인 지식을 합성, 형식화, 비판하도록 했음. 은총알은 아니지만 어느 정도의 정확성은 담보할 수 있었음. 어느 정도의 상징성과 agent-as-a-judge 개념이 미래에 유망할 것으로 생각함. 참고 논문
    • 해당 연구를 읽어봤음. 꽤 멋짐. 나도 최근 AWS ARChecks에서 autoformalization 에이전트를 만든 경험 있음. 아직 비공개이지만 일반적으로 사용 가능한 제품도 있으니 참고하면 좋겠음 AWS 블로그
    • Agent/LLM을 판사로 쓰는 건 편향이 존재하며, 오직 부트스트래핑용으로 적합하다고 봄. 성능이 충분히 올라가면 LLM 판사가 인위적으로 한계가 되어버리므로, 결국 전문가 인간판사나 결정론적 오라클로 넘어가야 한다는 입장임
  • RHEL의 knife-edge rolling kernel이 proof of concept에 사용됨을 언급함
  • 리포지터리에 자세한 설명이 부족하다고 느꼈으며, 논문 보조 산출물 역할이라 그럴 수 있음. 본질적으로 LLM에 Z3 프로그램 생성을 시도하게 하는 API로 보임. 실세계 쿼리를 논리적으로 표현하도록 유도해, 사실, 추론 규칙, 목표를 모두 담아냄. 감독 기능은 논리 기술문을 직접 읽고, 솔버를 실행해 참/거짓 여부를 확인할 수 있게 하는 데 있음. 의구심이 드는 점은: SMT 규칙을 누가 일일이 읽고 실제 관점과 대조할 수 있을지, 상수값은 누가 검증하는지, LLM이 실수로 혹은 목표 달성을 위해 논리적/현실적으로 어긋난 규칙을 추가하지는 않을지임. 논문에서 논리 벤치마크 기준 *51%*의 false positive를 기록했는데, 이는 놀랍게 높은 수치로 LLM이 논리 모델링에 약하거나 불완전한 규칙을 생성한다는 신호로 풀이함. 평가가 빈약해 왜 그것이 발생하는지 명확히 설명하지 못함
    • 이 논문은 작년에 GPT-4o로 작성된 것으로, 최신 모델에서는 상황이 많이 좋아졌다고 주장함. 예를 들어 최근 논문 Tab 1에서, 텍스트 기반과 SMT 기반 성능을 비교함. o3-mini가 text reasoning과 SMT 상의 결과를 잘 일치시킴. 상업 제품인 AWS Automated Reasoning Checks에서는, 도메인 모델을 만들고, 검증하며, 답변 생성 단계에서는 LLM의 Q/A 쌍이 정책을 준수하는지 엄격한 솔버 검증을 거침. 이를 통해 Q/A 쌍의 정책 관련 타당성을 99% 이상 보장할 수 있음을 강조함 AWS 블로그
  • 내 해석이 맞는지 묻는 질문임. LLM이 내놓은 확률적 출력이 논리모델로 넘어가는 구조라면, “쓰레기가 들어오면 쓰레기가 나올 뿐” 아닌가 하는 의심을 표함
    • 형식 논리가 필터 역할을 해줌. 즉 “쓰레기가 들어오면, 필터링된 쓰레기가 나옴”임. 진화도 무작위적인 “쓰레기” 돌연변이들이 자연환경에서 걸러지는 것과 같다는 비유를 듦
    • “쓰레기”가 항상 나오진 않는다는 주장임. 꽤 자주 유용한 출력을 내니까 의미 있음
    • 주관적인 평가사항임. 지난 수천 년간 인류가 만든 것들도 다 쓰레기로 볼 수 있기 때문임. 굳이 따지면 동굴에서 산 삶이 더 단순했을 수도 있음
  • AI가 생각만 할 뿐 아니라 검증 가능한 다이어리를 남긴다는 점이 아주 흥미로움. 마치 암호학적 공증인을 두고 철학자가 살아가는 모습 같음. 정말 놀라운 작업임
  • 핵심 아이디어는 LLM이 추론 과정을 구조적이고 JSON DSL로 기초 설계하면, 이를 결정적으로 1차 논리로 변환해 Z3 정리 증명을 시도한다는 점임. 그래서 최종 출력은 증명이 가능한 결론(혹은 반례)이 나오므로, 설득력만 있는 텍스트 체인과 다름을 강조함
  • 흥미로운 연구임. DSL 예제가 궁금해서 레포를 확인했으나 명확한 예시 찾기가 어려웠음. README에 예제 코드 스니펫이 있으면 좋겠음
    • 관심에 감사하며, 곧 추가할 예정임. 그동안엔 논문 11페이지부터 여러 상황 설명이 있음 논문 PDF
답변달기