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
Hacker News 의견